Temporal Logic as a Programming Language

Stephan Merz

Abstract

The central topic of this thesis is the characterization of a class of temporal logic formulas for which a model can be constructed automatically and efficiently. This study is motivated by the desire to close the gap between the ``declarative'' use of temporal logic as a specification formalism, especially for reactive systems, and the implementation of such systems in a different ``operational'' formalism.

The logical framework employed is a temporal logic based on fixpoint operators, allowing the results to be as general as practical by treating various temporal operators in a uniform way. A characterization of safety properties in this framework is given, which is then specialized to a similar characterization of deterministic safety properties. Starting from such formulas, the theory of ``executable'' temporal logic formulas is at first developed for propositional temporal logic, aiming at the characterization of formulas which allow for a model construction using a backtracking-free and future-directed algorithm whose time complexity is linear in the length of the input formulas.

For the first-order case, first some new incompleteness results are presented which further motivate the preference of a model-construction over a ``proofs-as-programs'' paradigm for the design of a programming language based on temporal logic. The framework developed for propositional temporal logic is extended to first-order temporal logic. Finally, the parallel composition of modules is studied using a conventional interleaving semantics and, in particular, the transition from properties of single modules to properties of composed systems is addressed. For programs expressed in the formalism developed before, a rule is given which allows the derivation of unconditional system properties in the presence of mutual dependencies between the modules.

Available as:  gzip'ed Postscript 

Reference

@PhdThesis{merz:diss,
  author = "Stephan Merz",
  title =  "Temporal Logic as a Programming Language",
  school = "Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen",
  year =   1992,
  address ="Munich, Germany",
  month =  jul
}