Temporal logic programming is complete and expressive

ABSTRACT

This paper addresses semantic and expressiveness issues for temporal logic programming and in particular for the TEMPLOG language proposed by Abadi and Manna. Two equivalent formulations of TEMPLOG's declarative semantics are given: in terms of a minimal Herbrand model and in terms of a least fixpoint. By relating these semantics to TEMPLOG's operational semantics, we prove the completeness of the resolution proof system underlying TEMPLOG's execution mechanism. To study TEMPLOG's expressiveness, we consider its propositional version. We show how propositional TEMPLOG programs can be translated into a temporal fixpoint calculus and prove that they can express essentially all regular properties of sequences.

REFERENCES

• Aba87: M. Abadi, Temporal-logic theorem proving, Stanford University, Stanford, CA, 1987
• AM87: Martin Abadi and Zohar Manna. TemporM logic programming. In International Symposium on Logic Programming, pages 4-16, San Francisco, CA, September 1987. IEEE. An extended version will appear in the Journal of Symbolic Computation.
• Apt87: Krzysztof R. Apt, Introduction to Logic Programming, University of Texas at Austin, Austin, TX, 1988
• AvE82: Krzysztof R. Apt , M. H. van Emden, Contributions to the Theory of Logic Programming, Journal of the ACM (JACM), v.29 n.3, p.841-862, July 1982 [doi>10.1145/322326.322339]
• Bau88a: Marianne Baudinet, On the Semantics of Temporal Logic Prograrnrning, Stanford University, Stanford, CA, 1988
• Bau88b: Marianne Baudinet. Proving termination properties of PROLOQ programs: A semantic approach. In Symposium on Logic in Computer Science, pages 336- 347, Edinburgh, Scotland, July i988. IEEE.
• BB86: Behnam Banieqbal and Howard Barringer. A study of an extended temporal logic and a temporal fixed point calculus. Technical Report UMCS86-10-2, Department of Computer Science, University of Manchester, 1986.
• BFH88: Ph. Balbiani, L. Farifias del Cerro, and A. Herzig. Declarative semantics for modal logic programs. In International Conference on Fifth Generation Computer Systems 1988, Tokyo, Japan, December 1988.
• CH85: Ashok K. Chandra and David Harel. Horn clause queries and generalizations. Journal of Logic Programming, 2(1):1- 15, 1985.
• Cla79: K.L. Clark. Predicate logic as a computational formalism. Technical Report 79/59 TOC, Department of Computing and Control, Imperial College, London, December 1979.
• CM84: W F. Clocksin , Christopher S. Mellish, Programming in Prolog (2nd ed.), Springer-Verlag New York, Inc., New York, NY, 1984
• DM88: Saumya K. Debray , Prateek Mishra, Denotational and operational semantics for Prolog, Journal of Logic Programming, v.5 n.1, p.61-91, March 1988 [doi>10.1016/0743-1066(88)90007-6]
• End72: tIerbert B. Enderton. A Maihemalical Introduction to Logic. Academic Press, 1972.
• Far86: L Fariñas del Cerro, MOLOG: A system that extends PROLOG with modal logic, New Generation Computing, v.4 n.1, p.35-50, 1986 [doi>10.1007/BF03037381]
• FKTMo86: M Fujita , S Kono , H Tanaka , T Moto-oka, Tokio: logic programming language based on temporal logic and its compilation to Prolog, Proceedings on Third international conference on logic programming, p.695-709, September 1986, London, United Kingdom
• Gab86: Dov Gabbay. Modal and temporal logic programming. Technical Report 86/15, Department of Computing, Imperial College, London, June 1986.
• Gab87: Dov Gabbay, Modal and temporal logic programming, Temporal logics and their applications, Academic Press Professional, Inc., San Diego, CA, 1987
• Hil74: Robert ttill. LUSH-resolution and its completeness. Technical Report 78, Department of Artificial Intelligence, University of Edinburgh, Edinburgh, Scotland, 1974.
• JM84: Neil D. Jones and Alan Mycroft. Stepwise development of operational and denotational semantics for Prolog. In International Symposium on Logic Programming, pages 281-288, Atlantic City, NJ, February 1984. IEEE.
• Kol88: Phokion Kolaitis. The expressive power of stratified logic programs. Manuscript, Submitted for Publication, 1988.
• Llo84: J. W. Lloyd, Foundations of logic programming, Springer-Verlag New York, Inc., New York, NY, 1984
• LMM88: J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• Lov78: Donald W Loveland, Automated theorem proving: A logical basis (Fundamental studies in computer science), sole distributor for the U.S.A. and Canada, Elsevier North-Holland, 1978
• Min88: J. Minker, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• Mos84: Ben Moszkowski. Executing temporal logic programs. Technical Report No. 55, Computer Laboratory, University of Cambridge, Cambridge, England, 1984.
• Mos86: Ben Moszkowski, Executing temporal logic programs, Cambridge University Press, New York, NY, 1986
• MW89: Zohar Manna , Richard Waldinger, The logical basis for computer programming: vol. 2, deductive systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• OW88a: Mehmet A. Orgun and William W. Wadge. Chronolog: A temporal logic programming language and its formal semantics. Unpublished Manuscript, 1988.
• OW88b: Mehmet A. Orgun and William W. Wadge. A theoretical basis for intensional logic programming. In Symposium on Lucid and lntensional Programming, pages 33-49, Sidney, B.C., Canada, April 1988.
• Par81: David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
• Rob65: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• Sak: Takashi Sakuragawa. Temporal Prolog. To appear in RIMS Conference on Software Science and Engineering. LNCS, Springer-Verlag.
• Tho81: Wolfgang Thomas. A combinatorial approach to the theory of w-automata. Information and Control, 48(3):261-283, March 1981.
• Var88: M. Y. Vardi, A temporal fixpoint calculus, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.250-259, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73582]
• vEK76: M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976 [doi>10.1145/321978.321991]
• VW88: Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computation paths. Manuscript, Submitted for Publieation, 1988.
• Wad85: William W. Wadge. Tease logic programming: a sane alternative. Unpublished Manuscript, 1985.
• Wad88: William W. Wadge. Tense logic programming: a respectable alternative. In Symposium on Lucid and Inlensional Programming, pages 26-32, Sidney, B.C., Canada, April 1988.
• Wol83: Pierre Wolper. Temporal logic can be more expressive, b~formation and Control, 56(1-2):72-99, 1983.
• WVS83: Pierre Wolper, Moshe Y. Vardi, and A. Prasad Sistla. Reasoning about infinite computation paths, in 24th Symposium on Foundations of Computer Science, pages 185-194, Tucson, Arizona, November 1983.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Logic and constraint programming

General Terms:
Languages, Theory, Verification