Skip to main content
SpringerLink
Log in
Book cover

International Joint Conference on Artificial Intelligence

IJCAI 1993: Executable Modal and Temporal Logics pp 21–39Cite as

Temporal logic programming with metric and past operators

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 897))

Abstract

Temporal logic allows us to use logic programming to specify and to program dynamically changing situations and non-terminating computations in a natural and problem oriented way. Recently so called metric or real-time temporal logics have been proposed for the specification of real-time systems, for which not only qualitative but also quantitative temporal properties are very important. In this work we investigate a subset of metric temporal Horn logic called MTL-programs, for which we give a translation into CLP(A′)-programs and CLP(A′)-goals over a suitable algebra A′. We give a restriction of the CLP(A′)-derivation mechanism sufficient for the derivation of MTL-goals from MTL-programs, which admits efficient satisfiability checking of the constraints generated. Its worst case complexity is linear in the number of variables involved, contrary to general satisfiability checking of constraints over A′ which is NP-complete. Moreover, we show that an extension of the metric temporal logic considered by the inclusion of variables within the temporal operators leads already to a temporal Horn logic which is expressively equivalent to constraint logic programs over A′.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi. The power of temporal proofs. Theoretical Computer Science, 65:35–83, 1989.

    Google Scholar 

  2. Y. Auffray and P. Enjalbert. Modal theorem proving: An equational viewpoint. In Proc. of the 11th International joint Conference on Artificial Intelligence, volume 1, Detroit, 1989.

    Google Scholar 

  3. R. Alur and T. A. Henzinger. A really temporal logic. Technical Report STAN-CS-89-1267, Stanford University, Dept. of Computer Science, 1989.

    Google Scholar 

  4. R. Alur and T. A. Henzinger. Real-time logics: Complexity and expressiveness. In Proc. of the 5th IEEE Symposium on Logic in Computer Science, Philadelphia, 1990. IEEE Computer Society Press.

    Google Scholar 

  5. J. Allen. Towards a general theory of action and time. Artificial Intelligence, 23(2):123–154, 1984.

    Google Scholar 

  6. M. Abadi and Z. Manna. Temporal logic programming. J. Symbolic Computation, 8:277–295, 1989.

    Google Scholar 

  7. M. Baudinet. Temporal logic programming is complete and expressive. In Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989.

    Google Scholar 

  8. Ph. Balbiani, L. Farinas Del Cerro, and A. Herzig. Declarative semantics for modal logic programs. In Proceedings of the International Conference on Fifth Generation Computer Systems, 1988.

    Google Scholar 

  9. M. Baudinet, J. Chomicki, and P. Wolper. Temporal deductive databases. In A. Tansel, J. Clifford, S. Gadia, S. Jajodia, A. Segev, and R. Snodgrass, editors, Temporal Databases. Benjamin/Cummings, 1992.

    Google Scholar 

  10. H. Barringer, M. Fisher, D. Gabbay, G. Gought, and R. Owens. A framework for programming in temporal logic. In Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, Netherlands, 1989. LNCS 430, Springer Verlag.

    Google Scholar 

  11. P. Balbiani, Andreas Herzig, and Mamede Marques. TIM: The Toulouse inference machine. In H. Boley and M. M. Richter, editors, Processing Declarative Knowledge — International Workshop PDK'91. Springer Verlag, LNAI 567, 1991.

    Google Scholar 

  12. C. Brzoska. Temporal logic programming and its relation to constraint logic programming. In Proc. of the 1991 Logic Programming Symposium, San Diego, California, October 1991. MIT Press.

    Google Scholar 

  13. C. Brzoska. Temporal logic programming with bounded universal (modality) goals. In Proc. of the 10th International Conference on Logic Programming, Budapest, Hungary, 1993. MIT Press.

    Google Scholar 

  14. C. Brzoska. Temporal logic programming with metric and past operators based on constraint logic programming. Interner Bericht 2/93, Universität Karlsruhe, Fak. für Informatik, 1993.

    Google Scholar 

  15. C. Brzoska and K. Schafer, LIMETTE: Logic programming integrating metric temporal extensions, language definition and user manual. Interner Bericht 9/93, Fak. für Informatik, Universität Karlsruhe, 1993.

    Google Scholar 

  16. J. Chomicki and T. Imieliński. Temporal deductive databases and infinite objects. In Proc. of the 7th Symposium on Principles of Database Systems, Austin, Texas, 1988.

    Google Scholar 

  17. J. G. Cleary and V. Kaushik. Updates in a temporal logic programming language. Research Report 91/427/11, Univ. of Calgary, Dept. of Computer Science, 1991.

    Google Scholar 

  18. Luis Farinas del Cerro. Molog: A system that extends PROLOG with modal logic. New Generation Computing, 4:35–50, 1986.

    Google Scholar 

  19. L. Farinas del Cerro and A. Herzig. Automated quantified modal logic. In P. Brazdil and K. Konolige, editors, Machine Learning, Meta-Reasoning and Logics. Kluwer Academic Publishers, 1990.

    Google Scholar 

  20. M. Fujita, S. Kono, T. Tanaka, and T. Moto-oka. Tokio: Logic programming language based on temporal logic and its compilation to prolog. In Proc. of the 3rd International Conference on Logic Programming, pages 695–709. Springer-Verlag, LNCS 225, 1986.

    Google Scholar 

  21. D. M. Gabbay. Modal and temporal logic programming. In A. Galton, editor, Temporal Logics and Their Applications, chapter 6, pages 197–237. Academic Press, London, December 1987.

    Google Scholar 

  22. D. M. Gabbay. Declarative past and imperative future. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. of Colloquium on Temporal Logic and Specification, LNCS 398, pages 76–89, Altrincham, 1989. Springer Verlag.

    Google Scholar 

  23. D. M. Gabbay. A temporal logic programming machine. In T. Dodd, R. Owens, and S. Torrance, editors, Logic Programming: Expanding the Horizonts, chapter 3, pages 82–123. Intellect Books, 1991.

    Google Scholar 

  24. R. Hale. Temporal logic programming. In A. Galton, editor, Temporal Logics and their Applications, chapter 3, pages 91–119. Academic Press, London, December 1987.

    Google Scholar 

  25. E. Harel, O. Lichtenstein, and A. Pnueli. Explicit clock temporal logic. In Proc. of the 5th Annual IEEE Symposium on Logic in Computer Science, Philadelphia, 1990. IEEE Computer Society Press.

    Google Scholar 

  26. T. Hrycej. Temporal prolog. In ECAI 88 Proceedings of the 8th European Conference on Artificial Intelligence, Munich, August 1988.

    Google Scholar 

  27. J. Jaffar and J.-L. Lassez. Constraint logic programming. In Proc. of the 14th ACM Symposium on Principles of Programming Languages, pages 111–119, Munich, 1986.

    Google Scholar 

  28. J. Jaffar and J.-L. Lassez. Constraint logic programming. Technical report, Department of Computer Science, Monash University, Australia, June 1986.

    Google Scholar 

  29. T. Käufl. Simplification and decision of linear inequalities over the integers. Technical Report 9/88, University of Karlsruhe, Fak. für Informatik, 1988.[Koy89]

    Google Scholar 

  30. R. Koymans. Specifying Message Passing and Time-Critical Systems with Temporal Logic. PhD thesis, Technical University of Eindhoven, 1989.

    Google Scholar 

  31. R. Koymans, J. Vytopil, and W. P. de Roever. Real-time programming and asynchronous message passing. In Proc. of the 2nd ACM Symp. on Principles of Distributed Computing, pages 187–197, Montreal, Canada, 1983.

    Google Scholar 

  32. L. Lamport. Specifying concurrent programs modules. ACM Transactions on Programming Languages and Systems, 5:190–222, April 1983.

    Google Scholar 

  33. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1984.

    Google Scholar 

  34. J.-L. Lassez and M. J. Maher. On fourier's algorithm for linear arithmetic constraints. Journal of Automated Reasoning, 9(3), December 1992.

    Google Scholar 

  35. S. Merz, October 1990. Private communication.

    Google Scholar 

  36. S. Merz. Temporal Logic as a Programming Language. Dissertation, Ludwig-Maximilians. Universitat, München, 1992.

    Google Scholar 

  37. B. Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, Cambridge, 1986.

    Google Scholar 

  38. Z. Manna and A. Pnueli. Verification of concurrent programs: the temporal framework. In R. S. Boyer and J. S. Moore, editors, The Correctness Problem in Computer Science, pages 215–273. Academic Press, London, 1981.

    Google Scholar 

  39. H. J. Ohlbach. A resolution calculus for modal logics. In E. Lusk and R. Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction. Springer-Verlag, LNCS 310, 1988.

    Google Scholar 

  40. H. J. Ohlbach. Context logic. SEKI Report SR-89-08, FB Informatik, University of Kaiserslautern, 1989.

    Google Scholar 

  41. M. A. Orgun and W. W. Wadge. Towards a unified theory of intensional logic programming. Journal of Logic Programming, 13(4):413 ff, 1992.

    Google Scholar 

  42. A. Porto and C. Ribeiro. Temporal inference with a point-based interval algebra. In B. Neumann, editor, Proc. of the ECAJ'92 10th European Conference on Artificial Intelligence, Wien, 1992. John Wiley & Sons.

    Google Scholar 

  43. B. Richards, Y. Jiang, and H. Choi. On interval-based temporal planning: An IQ strategy. In Z. Ras, editor, Proc. of the 6th ISMIS'91, LNAI 542. Springer Verlag, 1991.

    Google Scholar 

  44. A. Schriver. Theory of Linear and Integer Programming. Wiley, 1986.

    Google Scholar 

  45. K. Schäfer. Entwicklung einer temporallogischen Sprache zur Beschreibung von Abläufen in Straßenverkehrsszenen. Diplomarbeit, Universität Karlsruhe, Inst. für Logik, Komplexität und Deduktionssysteme, 1993.

    Google Scholar 

  46. A. Szalas. Concerning the semantic consequence relation in first-order temporal logic. Theoretical Computer Science, 47:329–334, 1986.

    Google Scholar 

  47. Ch.-S. Tang. Toward a unified logic basis for programming languages. In R.E.A. Mason, editor, Proc. Information Processing 83. Elsevier Science Publisher B.V. (North Holland), 1993.

    Google Scholar 

Download references

Authors
  1. Christoph Brzoska
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael Fisher Richard Owens

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brzoska, C. (1995). Temporal logic programming with metric and past operators. In: Fisher, M., Owens, R. (eds) Executable Modal and Temporal Logics. IJCAI 1993. Lecture Notes in Computer Science, vol 897. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58976-7_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-58976-7_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58976-1

  • Online ISBN: 978-3-540-49168-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation