From safety properties to temporal logic programming: A study in fixed point temporal logic

Stephan Merz

Abstract

Starting from a syntactic characterization of safety properties of reactive systems in the fixed point temporal logic νTL, we define a class of formulas for which a model can be effectively generated and which can thus be considered as the core of a programming language based on temporal logic.

Available as:  gzip'ed Postscript 

Reference

@InCollection{merz:fixedpoint,
  author =    {Stephan Merz},
  title =     {From safety properties to temporal logic programming:
               A study in fixed point temporal logic},
  booktitle = {Logica e filosofia della scienza},
  publisher = {Edizioni ETS},
  year =      1994,
  editor =    {G. Corsi},
  address =   {Pisa, Italy}
}