Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Acta Informatica
Published in: Acta Informatica 3/2016

01-04-2016 | Original Article

Metric temporal logic revisited

Author: Mark Reynolds

Published in: Acta Informatica | Issue 3/2016

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We introduce a new way of defining metric temporal logic over the continuous real model of time. The semantics refer to a single universal clock in order to impose metric constraints to any desired precision. Furthermore, the expression of any non-metric aspects can correctly utilise the full power of continuous time temporal logic. Syntactic constructs afford the convenient succinct expression of many useful and typical constraints including some interesting requirements for regular occurrences. A decision procedure is provided via a simple translation into an existing non-metric temporal logic and this gives a workable complexity and the possibility of automated reasoning. There are advantages in expressiveness, naturalness, generality and amenability to reasoning techniques over the existing metric temporal logics. Combining purely continuous with adequate metric aspects in one language makes the logic very suitable for dealing with hybrid systems.
previous article Extracting unsatisfiable cores for LTL via temporal resolution

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Literature
1.
2.
Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop. Lecture Notes in Computer Science, vol. 600, pp. 74–106. Springer, Berlin (1991)
3.
4.
5.
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T.: When are timed automata determinizable? In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 5556, pp. 43–54. Springer, Berlin (2009). doi:10.​1007/​978-3-642-02930-1_​4
6.
Bersani, M.M., Rossi, M., Pietro, P.S.: A tool for deciding the satisfiability of continuous-time metric temporal logic. In: Temporal Representation and Reasoning (TIME), 2013 20th International Symposium on, pp. 99–106. IEEE (2013)
7.
Bian, J., French, T., Reynolds, M.: An efficient tableau for linear time temporal logic. In: Cranefield, S., Nayak, A. (eds.) 26th Australasian Joint Conference on Artificial Intelligence, AI 2013, 1–6 December 2013, Dunedin, New Zealand, LNCS, vol. 8272, pp. 289–300. Springer, Berlin (2013)
8.
Bianculli, D., Spoletini, P., Morzenti, A., Pradella, M., Pietro, P.S.: Model checking temporal metric specifications with Trio2Promela. In: FSEN’07, Proceedings of the International Symposium on Fundamentals of Software Engineering (2007)
9.
Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Hyderabad, India, December 15–18, 2005, Proceedings, pp. 432–443. Springer, Berlin (2005)
10.
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: On expressiveness and complexity in real-time model checking. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP (2). Lecture Notes in Computer Science, vol. 5126, pp. 124–135. Springer, Berlin (2008)
11.
12.
Chaochen, Z.: Duration calculus, a logical approach to real-time systems. In: Haeberer, A.M. (ed.) AMAST. Lecture Notes in Computer Science, vol. 1548, pp. 1–7. Springer, Berlin (1998)
13.
Davoren, J., Nerode, A.: Logics for hybrid systems. Proc. IEEE 88(7), 985–1010 (2000)CrossRef
14.
D’Souza, D., Prabhakar, P.: On the expressiveness of MTL in the pointwise and continuous semantics. STTT 9(1), 1–4 (2007)CrossRef
15.
Falcon, E., Laroche, C., Fauve, S., Coste, C.: Behaviour of one inelastic ball bouncing repeatedly off the ground. Eur. Phys. J. B B(3), 45–57 (1998)
16.
Furia, C.A., Rossi, M.: On the expressiveness of MTL variants over dense time. In: Raskin, J.F., Thiagarajan, P.S. (eds.) FORMATS. Lecture Notes in Computer Science, vol. 4763, pp. 163–178. Springer, Berlin (2007)
17.
Furia, C.A., Rossi, M.: MTL with bounded variability: decidability and complexity. In: Cassez, F., Jard, C. (eds.) Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15–17, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5215, pp. 109–123. Springer, Berlin (2008)
18.
Gabbay, D.M., Hodkinson, I.M.: An axiomatisation of the temporal logic with until and since over the real numbers. J. Log. Comput. 1(2), 229–260 (1990)MathSciNetCrossRefMATH
19.
Gupta, V., Henzinger, T., Jagadeesan, R.: Robust timed automata. In: Proceedings of the International Workshop on Hybrid and Real-Time Systems (HART). LNCS, vol. 1201, pp. 331–345. Springer, Berlin (1997)
20.
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Proceedings of the 19th International Colloquium on Automata. Languages, and Programming (ICALP), LNCS, vol. 623, pp. 545–558. Springer, Berlin (1992)
21.
Hirshfeld, Y., Rabinovich, A.: An expressive temporal logic for real time. MFCS (2006)
22.
Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. Log. Methods Comput. Sci. 3(1) (2007)
23.
Hirshfeld, Y., Rabinovich, A.M.: A framework for decidable metrical logics. In: Wiedermann, J., van Emde Boas, P., Nielsen, M. (eds.) ICALP. Lecture Notes in Computer Science, vol. 1644, pp. 422–432. Springer, Berlin (1999)
24.
Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: decidability and complexity. Fundam. Inform. 62(1), 1–28 (2004)MathSciNetMATH
25.
Huang, J., Voeten, J., Geilen, M.: Real-time property preservation in approximation of timed systems. In: 1st ACM and IEEE International Conference on Formal Methods and Models for Co-Design (2003)
26.
Kamp, H.: Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California, Los Angeles (1968)
27.
28.
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, September 25–27, 2006, Proceedings, Lecture Notes in Computer Science, vol. 4202, pp. 274–289. Springer, Berlin (2006). doi:10.​1007/​11867340_​20
29.
Marx, M., Mikulas, S., Reynolds, M.: The mosaic method for temporal logics. In: Dyckhoff, R. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of International Conference, TABLEAUX 2000, Saint Andrews, Scotland, July 2000, LNAI 1847, pp. 324–340. Springer, Berlin (2000)
30.
Nickovic, D., Piterman, N.: From mtl to deterministic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) Formal Modeling and Analysis of Timed Systems—8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8–10, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6246, pp. 152–167. Springer, Berlin (2010). doi:10.​1007/​978-3-642-15297-9_​13
31.
Ostroff, J.S.: Temporal Logic for Real-Time Systems. Advanced Software Development Series. Wiley, New York (1989)
32.
Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proceedings of the 20th Annual Symposium on Logic in Computer Science (LICS’05), pp. 188–197. IEEE Comp. Soc. Press (2005)
33.
Ouaknine, J., Worrell, J.: Some recent results in metric temporal logic. In: FORMATS ’08: Proceedings of the 6th international conference on Formal Modeling and Analysis of Timed Systems, pp. 1–13. Springer, Berlin (2008). doi:10.​1007/​978-3-540-85778-5-1
34.
Rabinovich, A.: Complexity of metric temporal logics with counting and the Pnueli modalities. In: Cassez, F., Jard, C. (eds.) Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15–17, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5215, pp. 93–108. Springer, Berlin (2008)
35.
Raskin, J.: Logics, Automata and Classical Theories for Deciding Real Time. Ph.D. thesis. Université de Namur, Belgium (1999)
36.
37.
Reynolds, M.: Dense time reasoning via mosaics. In: TIME ’09: Proceedings of the 2009 16th International Symposium on Temporal Representation and Reasoning, pp. 3–10. IEEE Computer Society, Washington, DC (2009). doi:10.​1109/​TIME.​2009.​16
38.
39.
40.
Reynolds, M.: A new metric temporal logic for hybrid systems. In: Sanchez, C., Venables, B., Zimanyi, E. (eds.) Twentieth International Symposium on Temporal Representation and Reasoning, TIME 2013, 26–28 September 2013, Pensacola, FL (USA), pp. 73–80. IEEE CPS (2013)
41.
Reynolds, M.: A tableau for general linear temporal logic. J. Log. Comput. (2013)
42.
Reynolds, M.: A tableau for temporal logic over the reals. In: Goré, R., Kooi, B., Kurucz, A. (eds.) Advances in Modal Logic, vol. 10, pp. 439–458. College Publications (2014)
43.
Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata (extended abstract). In: LNCS 863, pp. 694–715. Springer, Berlin (1994)
Metadata
Title
Metric temporal logic revisited
Author
Mark Reynolds
Publication date
01-04-2016
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 3/2016
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-015-0243-0

Premium Partner

    Image Credits