MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments

MPI-I-1999-3-004

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.

  • MPI-I-1999-3-004.ps
  • Attachement: MPI-I-1999-3-004.ps (235 KBytes)

URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1999-3-004

Hide details for BibTeXBibTeX
@TECHREPORT{RaskinSchobbens99,
  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},
}