Hostname: page-component-586b7cd67f-gb8f7 Total loading time: 0 Render date: 2024-11-25T09:11:23.796Z Has data issue: false hasContentIssue false
  • English
  • Français

An introduction to executable temporal logics

Published online by Cambridge University Press:  07 July 2009

Michael Fisher
Michael Fisher
Affiliation:
Department of Computing, Manchester Metropolitan University, Manchester MI 5GD, UK (Email: M. [email protected])
Get access Rights & Permissions [Opens in a new window]

Extract

In recent years a number of programming languages based upon the direct execution of temporal logic formulae have been developed. The use of such logics provides a powerful basis for the representation and implementation of a range of dynamic behaviours. Though many of these languages are still experimental, they are beginning to be applied, not only in computer science and AI, but also in less obvious areas such as user interfaces, process control and social modelling. This article provides an introduction to some of the basic concepts of executable temporal logics, together with an overview of the main approaches being pursued.

Type
Research Article
Information
The Knowledge Engineering Review , Volume 11 , Issue 1 , March 1996 , pp. 43 - 56
Copyright
Copyright © Cambridge University Press 1996

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M, 1989. “The power of temporal proofs” Theoretical Computer Science 64 35–84.CrossRefGoogle Scholar
Abadi, M and Manna, Z, 1989. “Temporal logic programming” Journal of Symbolic Computation 8 277–295.CrossRefGoogle Scholar
Abadi, M and Manna, Z, 1990. “Nonclausal deduction in first-order temporal logic” ACM Journal 37 (2) 279–317.CrossRefGoogle Scholar
Aït-Kaci, H, 1991. Warren's Abstract Machine—A Tutorial Reconstruction, MIT Press.CrossRefGoogle Scholar
Allen, J, 1983. “Maintaining knowledge about temporal intervals” Comm. ACM 26 (11) 832–843.CrossRefGoogle Scholar
Allen, J, 1984. “Towards a general theory of action and time” Artificial Intelligence 23 (2) 123–154.CrossRefGoogle Scholar
Allen, J and Hayes, P, 1985. “A common sense theory of time”. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI) 528–531, Los Angeles CA.Google Scholar
Allen, J and Koomen, J, 1983. “Planning using a temporal world model”. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI) 741–747, Karlsruhe, Germany.Google Scholar
Balbiani, PHerzig, A and Lima-Marques, M, 1991. “TIM: The Toulouse Inference Machine for non- classical logic programming” Lecture Notes in Computer Science 567, Springer-Verlag.Google Scholar
Banieqbal, B and Barringer, H, 1986. “A study of an extended temporal language and a temporal fixed point calculus” Technical Report UMCS-86−10–2, Department of Computer Science, University of Manchester.Google Scholar
Barringer, H, Fisher, M, Gabbay, D, Gough, G and Owens, R, 1989. “METATEM: a framework for programming in temporal logic”. In: Proceedings of REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, Mook, Netherlands. (Published in Lecture Notes in Computer Science 430. Springer-Verlag.)Google Scholar
Barringer, H, Fisher, M, Gabbay, D and Hunter, A, 1991. “Meta-reasoning in executable temporal logic”. In: Allen, J, Fikes, R and Sandewall, E, editors, Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR) Cambridge, MA. Morgan Kaufmann.Google Scholar
Baudinet, M, 1989. “Temporal logic programming is complete and expressive”. In: Proceedings of the Sixteenth ACM Symposium on the Principles of Programming Languages (POPL) Austin, Texax. ACM Press.Google Scholar
Baudinet, M, 1992. “A simple proof of the completeness of temporal logic programming”. In: del, Cerro, LF, and Penttonen, M, editors, Intensional Logics for Programming. Oxford University Press.Google Scholar
Brzoska, C, 1991. “Temporal logic programming and its relation to constraint logic programming”. In:Proceedings of International Symposium on Logic Programming (ILPS) San Diego, CA. MIT Press.Google Scholar
Brzoska, C, 1995. “Temporal logic programming with metric and past operators”. In: Fisher, M and Owens, R, editors, Executable Modal and Temporal Logics: vol 897 of Lecture Notes in Artificial Intelligence. Springer-Verlag.Google Scholar
Brzoska, C and Schafer, K, 1993. “LIMETFE: Logic programming integrating metric temporal extensions— language definition and user manual”. Interner Bericht 9/93, Fak für Informatik, Universität Karlsruhe.Google Scholar
Bull, R and Segerberg, K, 1984. “Basic modal logic”. In: Gabbay, D and Guenthner, F, editors, Handbook of Philosophical Logic (II): Vol. 165 of Synthese Library, Chapter 11.1, pp. 1–88. Reidel.Google Scholar
Burgess, J, 1984. “Basic tense logic”. In: Gabbay, D and Guenthner, F, editors, Handbook of Philosophical Logic (II): Vol. 165 of Synthese Library, Chapter 11.2, pp. 89–134.CrossRefGoogle Scholar
Dean, T, 1987. “Large-scale temporal data bases for planning in complex domains”. In: Proceedings of International Joint Conference on Artificial Intelligence (IJCAI) 860–866, Milan, Italy.Google Scholar
Emerson, E, 1990. “Temporal and modal logic”. In: van Leeuwen, J, editor, Handbook of Theoretical Computer Science 996–1072. Elsevier.Google Scholar
Emerson, E and Halpern, J, 1986. “‘Sometimes’ and ‘Not Never’ revisited: on branching versus linear time temporal logic” Journal of the ACM 33 (1) 151–178.CrossRefGoogle Scholar
Finger, M, Fisher, M and Owens, R, 1993. “METATEM at work: modelling reactive systems using executable temporal logic”. In: Sixth International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA/AIE) Edinburgh, UK. Gordon and Breach.Google Scholar
Finger, M, McBrien, P and Owens, R, 1991. “Databases and executable temporal logic”. In: Proceedings of the ESPRIT Conference Brussels, Belgium.Google Scholar
Fisher, M, 1991. “A re/ution method for temporal logic”. In: Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI) Sydney, Australia. Morgan Kaufmann.Google Scholar
Fisher, M, 1992. “A normal form for first-order temporal formulae”. In: Proceedings of Eleventh International Conference on Automated Deduction (CADE) Saratoga Springs New York. (Published in Lecture Notes in Computer Science, 607, Springer-Verlag.)Google Scholar
Fisher, M, 1993. “Concurrent METATEM—A language for modeling reactive systems”. In: Parallel Architectures and Languages, Europe (PARLE) Munich, Germany. (Published as Lecture Notes in Computer Science, 694, Springer-Verlag.)Google Scholar
Fisher, M, 1994. “A survey of concurrent METATEM—The language and its applications”. In: First International Conference on Temporal Logic (ICTL) Bonn, Germany. (Published in Lecture Notes in Computer Science, 827, Springer-Verlag.)Google Scholar
Fisher, M and Noel, P, 1992. “Transformation and synthesis in METAM—Part I: Propositional METATEM. Technical Report UMCS−92−2−1 Department of Computer Science, University of Manchester, Oxford Road, Manchester M13 9PL, UK.Google Scholar
Fisher, M and Owens, R, 1992. “From the past to the future: executing temporal logic programs”. In: Proceedings of Logic Programming and Automated Reasoning (LPA R) St. Petersberg, Russia. (Published in Lecture Notes in Computer Science, 624, Springer-Verlag.)Google Scholar
Fisher, M and Owens, R, editors, 1995. Executable Modal and Temporal Logics. vol. 897 of Lecture Notes in Artificial Intelligence. Springer-Verlag.Google Scholar
Fisher, M and Wooldridge, M, 1993b. “Executable temporal logic for distributed A.I.” In: Twelfth International Workshop on Distributed A.I. Hidden Valley Resort, Pennsylvania.Google Scholar
Frühwirth, T, 1995. “Temporal logic and annotated constraint logic programming”. In: Fisher, M and Owens, R, editors, Executable Modal and Temporal Logics, vol. 897 of Lecture Notes in Artificial Intelligence. Springer: Verlag.Google Scholar
Fujita, M, Kono, S, Tanaka, T and Moto-oka, T, 1986. “Tokio: Logic programming language based on temporal logic and its compilation into Prolog”. In: 3rd International Conference on Logic Programming London, UK. (Published in Lecture Notes in Computer Science, 225, Springer-Verlag.)Google Scholar
Gabbay, D, 1987. “Declarative past and imperative future: executable temporal logic for interactive systems”. In: Banieqbal, B, Barringer, H and Pnueli, A, editors, Proceedings of Colloquium on Temporal Logic in Specification 402–450, Altrincham, UK. (Published in Lecture Notes in Computer Science, 398, Springer-Verlag.)Google Scholar
Gabbay, D, 1991. “Modal and temporal logic II (a temporal Prolog machine)”. In: Dodd, T, Owens, R, and Torrance, S, editors, Logic Programming—Expanding the Horizon. Intellect Books.Google Scholar
Gabbay, D, Pnueli, A, Shelah, S and Stavi, J, 1980. “The temporal analysis of fairness”. In: Proceedings of the Seventh ACM Symposium on the Principles of Programming Languages (POPL) 163–173, Las Vegas NV, ACM Press.Google Scholar
Hale, R and Moszkowski, B, 1987. “Parallel programming in temporal logic”. In: ParallelArchitectures and Languages Europe (PARLE) Eindhoven, The Netherlands. (Published as Lecture Notes in Computer Science, 259, Springer-Verlag.)Google Scholar
Hrycej, T, 1988. “Temporal Prolog”. In: Kodratoff, Y, editor, Proceedings of the European Conference on Artificial Intelligence 296–301. Pitman.Google Scholar
Hrycej, T, 1993. “A temporal extension of Prolog” Journal of Logic Programming 15(1&2) 113–145.CrossRefGoogle Scholar
Johnson, CW and Harrison, MD, 1992. “Using temporal logic to support the specification and prototyping of interactive control systems” International Journal of Man-Machine Studies 36.Google Scholar
Jones, CB, 1986. Systematic Software Development Using VDM Prentice Hall.Google Scholar
K&, JAW, 1968. Tense Logic and the Theory of Linear Order PhD thesis, University of California.Google Scholar
King, P, 1995. “Towards an ITL based formalism for expressing temporal constraints in multimedia documents”. In: Proceedings of IJCAI Workshop on Executable Temporal Logics Montreal, Canada.Google Scholar
Kono, S., 1995. “A combination of clausal and non-clausal temporal logic programs”. In: Fisher, M and Owens, R, editors, Executable Modal and Temporal Logics, vol 897 of Lecture Notes in Artificial Intelligence. Springer-Verlag.Google Scholar
Kröger, F, 1987. Temporal Logic of Programs Monographs on Theoretical Computer Science. Springer- Verlag.CrossRefGoogle Scholar
Manna, Z and Pnueli, A, 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification Springer-Verlag.CrossRefGoogle Scholar
Merz, S, 1995. “Efficiently executable temporal logic programs”. In: Fisher, M and Owens, R, editors, Executable Modal and Temporal Logics, vol 897 of Lecture Notes in Artificial Intelligence. Springer- Verlag.Google Scholar
Moszkowski, B, 1983. “Reasoning about digital circuits” Technical report, Stanford University.Google Scholar
Moszkowski, B, 1986. Executing Temporal Logic Programs Cambridge University Press.Google Scholar
Moszkowski, B and Manna, Z, 1984. “Reasoning in interval temporal logic”. In: AMC/NSF/ONR Workshop on Logics of Programs Berlin, Germany. (Published as Lecture Notes in Computer Science, 164, Springer- Verlag.)Google Scholar
Orgun, M and Ma, W, 1994. “An overview of temporal and modal logic programming”. In: First Internaional Conference on Temporal Logic (ICTL) Bonn, Germany. (Published in Lecture Notes in Computer Science, 827, Springer-Verlag.)Google Scholar
Orgun, M and Wadge, W, 1992a. “Theory and practice of temporal logic programming”. In: del, Cerro, LF, and Penttonen, M, editors, Intensional Logics for Programming Oxford University Press.Google Scholar
Orgun, MA and Wadge, W, 1992b. “Towards a unified theory of intensional logic programming”. Journal of Logic Programming 13 (1, 2, 3 and 4) 413–440.CrossRefGoogle Scholar
Schäfer, K, 1993. “Entwicklung einer temporal logischen Sprache zur Beschreibung von Ablaufen in Straβenverkehrsszenen” Diplomarbeit, Universität Karlsruhe, Inst. für Logik, Komplexität und Deduktionssysteme.Google Scholar
Schwartz, R, Melliar-Smith, P and Vogt, F, 1983. “An interval-based temporal logic” Lecture Notes in Computer Science 164 443–457.CrossRefGoogle Scholar
Sistla, A and Clarke, E, 1985. “Complexity of propositional linear temporal logics” ACM Journal 32 (3) 733–749.CrossRefGoogle Scholar
Sterling, L and Shapiro, E, 1987. The Art of Prolog MIT Press.CrossRefGoogle Scholar
Szalas, A and Holenderski, L, 1988. “Incompleteness of first-order temporal logic with until” Theoretical Computer Science 57 317–325.CrossRefGoogle Scholar
Tang, T, 1989. “Temporal Logic CTL + Prolog” Journal of Automated Reasoning 5 49–65.CrossRefGoogle Scholar
Van Bentham, J, 1988. “A logician's point of view concerning the use of temporal logic in computer science”. In: REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. (Published as Lecture Notes in Computer Science, 354, Springer-Verlag.)Google Scholar
Wolper, P, 1985. “The tableau method for temporal logic: an overview” Logique et Analyse 110–111, 119–136.Google Scholar