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′.
Preview
Unable to display preview. Download preview PDF.
References
M. Abadi. The power of temporal proofs. Theoretical Computer Science, 65:35–83, 1989.
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.
R. Alur and T. A. Henzinger. A really temporal logic. Technical Report STAN-CS-89-1267, Stanford University, Dept. of Computer Science, 1989.
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.
J. Allen. Towards a general theory of action and time. Artificial Intelligence, 23(2):123–154, 1984.
M. Abadi and Z. Manna. Temporal logic programming. J. Symbolic Computation, 8:277–295, 1989.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Luis Farinas del Cerro. Molog: A system that extends PROLOG with modal logic. New Generation Computing, 4:35–50, 1986.
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.
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.
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.
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.
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.
R. Hale. Temporal logic programming. In A. Galton, editor, Temporal Logics and their Applications, chapter 3, pages 91–119. Academic Press, London, December 1987.
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.
T. Hrycej. Temporal prolog. In ECAI 88 Proceedings of the 8th European Conference on Artificial Intelligence, Munich, August 1988.
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.
J. Jaffar and J.-L. Lassez. Constraint logic programming. Technical report, Department of Computer Science, Monash University, Australia, June 1986.
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]
R. Koymans. Specifying Message Passing and Time-Critical Systems with Temporal Logic. PhD thesis, Technical University of Eindhoven, 1989.
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.
L. Lamport. Specifying concurrent programs modules. ACM Transactions on Programming Languages and Systems, 5:190–222, April 1983.
J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, 1984.
J.-L. Lassez and M. J. Maher. On fourier's algorithm for linear arithmetic constraints. Journal of Automated Reasoning, 9(3), December 1992.
S. Merz, October 1990. Private communication.
S. Merz. Temporal Logic as a Programming Language. Dissertation, Ludwig-Maximilians. Universitat, München, 1992.
B. Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, Cambridge, 1986.
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.
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.
H. J. Ohlbach. Context logic. SEKI Report SR-89-08, FB Informatik, University of Kaiserslautern, 1989.
M. A. Orgun and W. W. Wadge. Towards a unified theory of intensional logic programming. Journal of Logic Programming, 13(4):413 ff, 1992.
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.
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.
A. Schriver. Theory of Linear and Integer Programming. Wiley, 1986.
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.
A. Szalas. Concerning the semantic consequence relation in first-order temporal logic. Theoretical Computer Science, 47:329–334, 1986.
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.
Editor information
Rights 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