# zbMATH — the first resource for mathematics

Branching time logics $$\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }$$ with operations Until and Since based on bundles of integer numbers, logical consecutions, deciding algorithms. (English) Zbl 1148.03011
Summary: This paper is intended as an attempt to describe logical consequence in branching time logics. We study temporal branching time logics $$\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}$$ which use the standard operations Until and Next and dual operations Since and Previous (LTL, as standard, uses only Until and Next). Temporal logics $$\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}$$ are generated by semantics based on Kripke/Hintikka structures with linear frames of integer numbers $$\mathcal {Z}$$ with a single node (glued zeros). For $$\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}$$, the permissible branching of the node is limited by $$\alpha$$ (where $$1\leq \alpha \leq \omega)$$. We prove that any logic $$\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}$$ is decidable w.r.t. admissible consecutions (inference rules), i.e. we find an algorithm recognizing consecutions admissible in $$\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}$$. As a consequence, it implies that $$\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}$$ itself is decidable and solves the satisfiability problem.

##### MSC:
 03B44 Temporal logic 03B25 Decidability of theories and sets of sentences 03B70 Logic in computer science
Full Text: