Branching Time Logics BT L_(N,N~(-1))~(U,S)(Z)_α with Operations Until and Since Based on Bundles of Integer Numbers, Logical Consecutions,Deciding Algorithms

摘要

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