Branching time logics BT LN,N-1U,S(Z)α with operations Until and Since based on bundles of integer numbers, logical consecutions, deciding algorithms

被引:0
|
作者
Rybakov, V. [1 ]
机构
[1] Manchester Metropolitan Univ, Dept Comp & Math, Manchester M1 5GD, Lancs, England
基金
英国工程与自然科学研究理事会;
关键词
decidability; algorithms; logical consecutions; inference rules; temporal logic; linear temporal logic; branching time logic; admissible consecutions;
D O I
10.1007/s00224-007-9059-9
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:254 / 271
页数:18