Propositional Temporal Logics: Decidability and Completeness
O. Lichtenstein and A. Pnueli
A sound and complete axiomatic system and a tableau-based decision
procedure are presented for propositional temporal logic over linear
and discrete time models. The axiomatic system and decision procedure
are presented for the full logic, including the past operators, but
contain a clear identification of the parts whose omission yields
axiomatization and a decision procedure for the future fragment. The
paper summarizes work of over 20 years and is intended to provide a
definitive reference to the version of propositional temporal logic
used for the specification and verification of reactive systems.
Logic Journal of the IGPL
Gzipped PostScript