Branching time logics BTL, U,S , N,N −1(Z)α with operations until and since based on bundles of integer numbers, logical consecutions, deciding algorithms

Rybakov, Vladimir V. (2008) Branching time logics BTL, U,S , N,N −1(Z)α with operations until and since based on bundles of integer numbers, logical consecutions, deciding algorithms. Theory of computing systems, 43 (2). pp. 254-271. ISSN 1433-0490

File not available for download.

Abstract

This paper is intended as an attempt to describe logical consequence in branching time logics. We study temporal branching time logics which use the standard operations Until and Next and dual operations Since and Previous (LTL, as standard, uses only Until and Next). Temporal logics are generated by semantics based on Kripke/Hinttikka structures with linear frames of integer numbers with a single node (glued zeros). For , the permissible branching of the node is limited by α (where 1≤α≤ω). We prove that any logic is decidable w.r.t. admissible consecutions (inference rules), i.e. we find an algorithm recognizing consecutions admissible in . As a consequence, it implies that itself is decidable and solves the satisfiability problem.