A Method for the Determinisation of Propositional Temporal Formulae

  • Philippe Noel
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


This paper is concerned with the generation of models for specifications expressed in a propositional temporal logic. These specifications represent dynamic and interacting systems and hence contain references to the environment in which the systems will execute.

In the current version of the executable temporal logic system, MetateM, a model may be generated directly from a given specification. However, in general, this model construction involves backtracking. We show how to transform an arbitrary specification, 5, into another specification, S’, from which a model can be generated without backtracking. S’ is such that any of its models is a model of 5, and it is satisfiable only if S is satisfiable.


Temporal Logic Inference Rule Conjunctive Normal Form State Formula Tree Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    H. Barringer, M. Fisher, D. Gabbay, G. Gough, and R. Owens. MetateM: A Framework for Programming in Temporal Logic. In REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Corredness (LNCS Volume 430), pages 94-129, Mook, Netherlands, June 1989. Springer Verlag.Google Scholar
  2. [2]
    H. Barringer, M. Fisher, D. Gabbay, and A. Hunter. Meta-Reasoning in Executable Temporal Logic. In James Allen, Richard Fikes, and Erik Sandewall, editors, Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, Cambridge, Massachusetts, April 1991. Morgan Kaufmann.Google Scholar
  3. [3]
    E.A. Emerson and A.P. Sistla. Deciding full Branching Time Logic. In formation and Control, 61: 175–201, 1984.MathSciNetMATHCrossRefGoogle Scholar
  4. [4]
    M. Fisher. A Resolution Method for Temporal Logic. In Proceedings of the International Joint Conference on Artificial Intelligence, Sydney, Australia, August 1991. Morgan Kaufman.Google Scholar
  5. [5]
    M. Fisher and H. Barringer. Concurrent MetateM Processes — A Language for Distributed AI. In Proceedings of the European Simulation Multiconference, Copenhagen, Denmark, June 1991.Google Scholar
  6. [6]
    M. Fisher and P. Noel. Transformation and Synthesis in MetateM — Part I: Propositional MetateM. MetateM project report, May 1991.Google Scholar
  7. [7]
    G.D. Gough. Decision Procedures for Temporal Logic. Master’s thesis, Department of Computer Science, University of Manchester, 1984.Google Scholar
  8. [8]
    A. Hossley and C. Rackoff. The Emptiness Problem for Automata on Infinite Trees. In 13th IEEE Symposium on Switching and Automata Theory, pages 121-124, 1972.Google Scholar
  9. [9]
    O. Lichtendtein, A. Pnueli, and L.Zuck. The Glory of the Past. In Proc. Workshop on Logic of Programs, pages 196-218. Springer-Verlag, 1985. LNCS 193.Google Scholar
  10. [10]
    A. Pnueli. The Temporal Logic of Programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science, Providence, November 1977.Google Scholar
  11. [11]
    A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In 16th ACM POPL, pages 179-190, January 1989.Google Scholar
  12. [12]
    A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The Complementation Problem for Buchi Automata with Application to Temporal Logic. Theoretical Computer Science, 49: 217–237, 1987.MathSciNetMATHCrossRefGoogle Scholar
  13. [13]
    P. Wolper. The Tableau Method for Temporal Logic: An overview. Logique et Analyse, 110-111: 119–136, June-Sept 1985.MathSciNetGoogle Scholar
  14. [14]
    P. Wolper. On the Relation of Programs and Computations to Models of Temporal Logic. In Temporal Logic in Specification, pages 75-123. Springer-Verlag, 1987. LNCS 398.Google Scholar

Copyright information

© Springer-Verlag London 1992

Authors and Affiliations

  • Philippe Noel
    • 1
  1. 1.Department of Computer ScienceUniversity of ManchesterUK

Personalised recommendations