TY - JOUR
T1 - Logic of `initially' and `next'
T2 - Complete axiomatization and complexity
AU - Schobbens, P.-Y.
AU - Raskin, J.-F.
N1 - Publication code : **RES. ACAD.
PY - 1999/3/12
Y1 - 1999/3/12
N2 - Andreka et al. (1995) obtained a large number of completeness results for discrete linear-time temporal logics. One of them is left open: the completeness of the logic of `initially' and `next', for which a deductive system is proposed. This simple logic is of practical importance, since the proof of program invariants only require these modalities. We show here that the conjectured medium completeness of this system indeed holds; further, we show that deciding this entailment is PSPACE-complete, while deciding validity is only coNP-complete.
AB - Andreka et al. (1995) obtained a large number of completeness results for discrete linear-time temporal logics. One of them is left open: the completeness of the logic of `initially' and `next', for which a deductive system is proposed. This simple logic is of practical importance, since the proof of program invariants only require these modalities. We show here that the conjectured medium completeness of this system indeed holds; further, we show that deciding this entailment is PSPACE-complete, while deciding validity is only coNP-complete.
UR - http://www.scopus.com/inward/record.url?scp=0033548337&partnerID=8YFLogxK
U2 - 10.1016/S0020-0190(99)00022-8
DO - 10.1016/S0020-0190(99)00022-8
M3 - Article
VL - 69
SP - 221
EP - 225
JO - Information processing letters
JF - Information processing letters
IS - 5
ER -