A Method for the Determinisation of Propositional Temporal Formulae
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.
KeywordsTemporal Logic Inference Rule Conjunctive Normal Form State Formula Tree Automaton
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- 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
- M. Fisher and P. Noel. Transformation and Synthesis in MetateM — Part I: Propositional MetateM. MetateM project report, May 1991.Google Scholar
- G.D. Gough. Decision Procedures for Temporal Logic. Master’s thesis, Department of Computer Science, University of Manchester, 1984.Google Scholar
- 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
- 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
- A. Pnueli. The Temporal Logic of Programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science, Providence, November 1977.Google Scholar
- A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In 16th ACM POPL, pages 179-190, January 1989.Google Scholar
- 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