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.
@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 }