MPI-INF/SWS Research Reports 1991-2021

2. Number - only D3


Proving a conjecture of Andreka on temporal logic

Raskin, Jean-Francois and Schobbens, Pierre-Yves

August 1999, 13 pages.

Status: available - back from printing

In \cite{Andreka}, a large number of completeness results about variants of discrete linear-time temporal logic are obtained. One of them is left as an open problem: 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 {\em medium completeness} of this system indeed holds; further, we show that deciding this entailment is PSPACE-complete, while deciding validity is only coNP-complete.

  • Attachement: (235 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Raskin, Jean-Francois and Schobbens, Pierre-Yves},
  TITLE = {Proving a conjecture of Andreka on temporal logic},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-1999-3-004},
  MONTH = {August},
  YEAR = {1999},
  ISSN = {0946-011X},