Logics for Real Time: Decidability and Complexity

• Autorzy: Hirshfeld Y. , Rabinovich A.
• Języki publikacji: EN

Abstrakty

EN

Over the last fifteen years formalisms for reasoning about metric properties of computations were suggested and discussed. First as extensions of temporal logic, ignoring the framework of classical predicate logic, and then, with the authors' work, within the framework of monadic logic of order. Here we survey our work on metric logic comparing it to the previous work in the field. We define a quantitative temporal logic that is based on a simple modality within the framework of monadic predicate Logic. Its canonical model is the real line (and not an w-sequence of some type). It can be interpreted either by behaviors with finite variability or by unrestricted behaviors. For finite variability models it is as expressive as any logic suggested in the literature. For unrestricted behaviors our treatment is new. In both cases we prove decidability and complexity bounds using general theorems from logic (and not from automata theory).

Słowa kluczowe

EN

Monadic Logic of Order; temporal logic; Quantitative Monadic Logic of Order; QMLO; strong normalisation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 62, nr 1
• Strony: 1--28
• Opis fizyczny: Bibliogr. 27 poz.

Twórcy

autor

Hirshfeld Y.

• School of Computer Science, Sackler Faculty of Exact Sciences, Tel Aviv University, Tel Aviv, Israel 69978

autor

Rabinovich A.

• School of Computer Science, Sackler Faculty of Exact Sciences, Tel Aviv University, Tel Aviv, Israel 69978

Bibliografia

• [AD94] R. Alur, D. Dill A theory of timed Automata. Theoretical Computer Science 126 (1994), 183-235.
• [AFH96] R. Alur, T. Feder, T. A. Henzinger. The Benefits of Relaxing Punctuality. Journal of the ACM 43 (1996) 116-146.
• [AH92] R. Alur, T. A. Henzinger. Logics and Models of Real Time: a survey. In Real Time: Theory and Practice. Editors de Bakker et al. LNCS 600 (1992) 74-106.
• [AH92a] R. Alur, T. A. Henzinger. Back to the future: toward theory of timed regular languages. In 33th FOCS, pp l77-186,1992.
• [AH93] R. Alur, T.A. Henzinger. Real Time Logic: Complexity and Expressiveness. Information and Computation 104(1993) 35-77.
• [BKP85] H. Barringer, R. Kuiper, A. Pnueli. A really abstract concurrent model and its temporal logic. Proceedings of the 13th annual symposium on principles of programing languages (1986), 173-183.
• [Bu60] J. Blichi. On a decision method in restricted second order arithmetic In Proc. International Congress on Logic, Methodology and Philosophy of Science, E. Nagel et al. eds, Stanford University Press, pp 1-11,1960.
• [BL95] A. Bouajjani and Y. Lakhnech. Temporal Logic +Timed Automata: Expressiveness and Decidability. CONCUR95, LNCS 962, pp. 531-547,1995.
• [BG85] J.R Burges, Y. Gurevich. The Decision Problem for Temporal Logic. Notre Dame J. Formal Logic, 26 (1985)115-128.
• [Ehr61] A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129-141,1961.
• [GHR94] D.M. Gabbay, I. Hodkinson, M. Reynolds. Temporal Logics volume 1. Clarendon Press, Oxford (1994).
• [GPSS80] D.M. Gabbay, A. Pnueli, S. Shelah, J. Stavi. On the Temporal Analysis of Fairness. 7th ACM Symposium on Principles of Programming Languages. Las Vegas (1980) 163-173.
• [Hen98] T.A. Henzinger It's about time: real-time logics reviewed, in Concur 98, Lecture Notes in Computer Science 1466,1998.
• [HRS98] T.A. Henzinger, J.F. Raskin, P.Y. Schobbens. The Regular Real Time Languages. 25th ICALP Colloquium (1998).
• [HR99] Y. Hirshfeld and A. Rabinovich, A Framework for Decidable Metrical Logics. In Proc. 26th ICALP Colloquium, LNCS vol.1644, pp. 422-432, Springer Verlag, 1999.
• [HR99a] Y. Hirshfeld and A. Rabinovich. Quantitative Temporal Logic. In Computer Science Logic 1999, LNCS vol. 1683, pp 172-187, Springer Verlag 1999.
• [HR03] Y. Hirshfeld and A. Rabinovich, Timer formulas and decidable metric temporal logic. Technical report, Tel Aviv University (2003).
• [Kamp68] H. Kamp. Tense Logic and the Theory of Linear Order. Ph.D. thesis. University of California L.A. (1968).
• [MP93] Z. Manna, A. Pnueli. Models for reactivity. Acta informatica 30 (1993) 609-678.
• [Ra69] M. O. Rabin, Decidability of second order theories and automata on infinite trees. In Trans. Amer. Math. 5oc.,141, pp 1-35,1969.
• [Rab98] A. Rabinovich. On the Decidability of Continuous Time Specification Formalisms. In Journal of Logic and Computation, pp 669-678,1998.
• [Rab98a] A. Rabinovich. On the complexity of TL over the reals. Manuscript 1998.
• [RSH98] J.F. Raskin, P.Y. Schobbens, T.A. Henzinger. Axioms for real-time logics. In CONCUR 98, Lecture Notes in Computer Science 1466, pp. 439-454,1998.
• [Re99] M. Reynolds. The complexity of the temporal logic with until over general linear time, manuscript 1999.
• [She75] S. Shelah. The monadic theory of order. Ann. of Math., 102, pp 349-419,1975.
• [Trak99] B.A. Trakhtenbrot. Dynamic Systems and their interaction: Definitional Suggestions. Technical Report, Tel Aviv University, 1999.
• [Wilke94] T. Wilke. Specifying Time State Sequences in Powerful Decidable Logics and Time Automata. In Formal Techniques in Real Time and Fault Tolerance Systems. LNCS 863 (1994), 694-715.