e-space
Manchester Metropolitan University's Research Repository

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

Full text not available from this repository.

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.

Impact and Reach

Statistics

Downloads
Activity Overview
0Downloads
226Hits

Additional statistics for this dataset are available via IRStats2.

Altmetric

Actions (login required)

View Item View Item