Branching time logics BT LN,N-1U,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)(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 BT L-N,N-1(U,S)(Z)(alpha) 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)(alpha), the permissible branching of the node is limited by alpha ( where 1 <= alpha <= omega.). We prove that any logic BT L-N,N-1(U,S)(Z)(alpha) 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())alpha. As a consequence, it implies that BT L-N,(U,S)(N-1)(Z)(alpha) itself is decidable and solves the satisfiability problem.