Logic of `initially' and `next': Complete axiomatization and complexity

P.-Y. Schobbens, J.-F. Raskin

Research output: Contribution to journalArticlepeer-review


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.
Original languageEnglish
Pages (from-to)221-225
Number of pages5
JournalInformation processing letters
Issue number5
Publication statusPublished - 12 Mar 1999


Dive into the research topics of 'Logic of `initially' and `next': Complete axiomatization and complexity'. Together they form a unique fingerprint.

Cite this