Top

Published in:

2017 | OriginalPaper | Chapter

Timed Temporal Logics

Authors : Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine, James Worrell

Published in: Models, Algorithms, Logics and Tools

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Since the early 1990’s, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.

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 "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

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

previous chapter Negative Results on Decidability and Small Model Property of Process Equations

next chapter Synchronous Interfaces and Assume/Guarantee Contracts

Zero-delay transitions are not allowed here, but could be included without affecting the presented results.

Rational bounds could be considered at the expense of scaling all constants by an appropriate factor.

That is, for every \(a \in \varSigma \), \(f_{\text {inter}}(a,\bullet ) = a_1\) and \(f_{\text {inter}}(\bullet ,a)=a_2\).

As shown in [30] this property fails without the assumption of finite variability.

Aceto, L., Bouyer, P., Burgueño, A., Larsen, K.G.: The power of reachability testing for timed automata. Theoret. Comput. Sci. 300(1–3), 411–475 (2003). http://dx.doi.org/10.1016/S0304-3975(02)00334-1 MathSciNetCrossRefMATH

Aceto, L., Ingólfsdóttir, A., Pedersen, M.L., Poulsen, J.: Characteristic formulae for timed automata. RAIRO - Theoret. Inf. Appl. 34(6), 565–584 (2000). http://dx.doi.org/10.1051/ita:2000131 MathSciNetCrossRefMATH

Aceto, L., Laroussinie, F.: Is your model checker on time? J. Log. Algebr. Program. 52(53), 3–51 (2002). http://dx.doi.org/10.1016/S1567-8326(02)00022-X MATH

Alur, R.: Techniques for automatic verification of real-time systems. Ph.D. thesis, Stanford University, Palo Alto, California, USA (1991)

Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comp. 104(1), 2–34 (1993). http://dx.doi.org/10.1006/inco.1993.1024 MathSciNetCrossRefMATH

Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994). http://dx.doi.org/10.1016/0304-3975(94)90010-8 MathSciNetCrossRefMATH

Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996). http://dx.doi.org/10.1145/227595.227602 MathSciNetCrossRefMATH

Alur, R., Henzinger, T.A.: A really temporal logic. In: FOCS 1989, pp. 164–169. IEEE Computer Society Press (1989). http://dx.doi.org/10.1109/SFCS.1989.63473

Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Bakker, J.W., Huizing, C., Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992). doi:10.1007/BFb0031988 CrossRef

10.

Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comp. 104(1), 35–77 (1993). http://dx.doi.org/10.1006/inco.1993.1025 MathSciNetCrossRefMATH

11.

Andersen, H.R.: Partial model-checking (extended abstract). In: LICS 1995, pp. 398–407. IEEE Computer Society Press (1995). http://dx.doi.org/10.1109/LICS.1995.523274

12.

Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST 2006, pp. 125–126. IEEE Computer Society Press (2006). http://dx.doi.org/10.1109/QEST.2006.59

13.

Bersani, M.M., Rossi, M., Pietro, P.S.: Deciding the satisfiability of MITL specifications. In: GandALF 2013, EPTCS, vol. 119, pp. 64–78 (2013). http://dx.doi.org/10.4204/EPTCS.119.8

14.

Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 432–443. Springer, Heidelberg (2005). doi:10.1007/11590156_35 CrossRef

15.

Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: LICS 2007, pp. 109–118. IEEE Computer Society Press (2007). http://dx.doi.org/10.1109/LICS.2007.49

16.

Brihaye, T., Estiévenart, M., Geeraerts, G., Ho, H.-M., Monmege, B., Sznajder, N.: Real-time synthesis is hard!. In: Fränzle, M., Markey, N. (eds.) FORMATS 2016. LNCS, vol. 9884, pp. 105–120. Springer, Cham (2016). doi:10.1007/978-3-319-44878-7_7 CrossRef

17.

Brihaye, T., Laroussinie, F., Markey, N., Oreiby, G.: Timed concurrent game structures. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 445–459. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74407-8_30 CrossRef

18.

Čerāns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification — theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253–267. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_21 CrossRef

19.

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.1007/BFb0025774 CrossRef

20.

Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986). http://dx.doi.org/10.1145/5397.5399 CrossRefMATH

21.

Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996). doi:10.1007/BFb0020947 CrossRef

22.

D’Souza, D., Prabhakar, P.: On the expressiveness of MTL in the pointwise and continuous semantics. Int. J. Softw. Tools Technol. Transf. 9(1), 1–4 (2007). http://dx.doi.org/10.1007/s10009-005-0214-9 CrossRef

23.

Furia, C.A., Rossi, M.: On the expressiveness of MTL variants over dense time. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 163–178. Springer, Heidelberg (2007). doi:10.1007/978-3-540-75454-1_13 CrossRef

24.

Gabbay, D.M.: Expressive functional completeness in tense logic (preliminary report). In: Mönnich, U. (ed.) SYLI, vol. 147, pp. 91–117. Springer, Heidelberg (1981). doi:10.1007/978-94-009-8384-7_4

25.

Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980, pp. 163–173. ACM Press (1980). http://dx.doi.org/10.1145/567446.567462

26.

Godskesen, J.C., Larsen, K.G., Skou, A.: Automatic verification of real-time systems using epsilon. In: IFIP Conference Proceedings on PSTV 1994, vol. 1, pp. 323–330. Chapman & Hall (1995)

27.

Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modelling and analysis of an audio/video protocol: an industrial case study using Uppaal. In: RTSS 1997, pp. 2–13. IEEE Computer Society Press (1997). http://dx.doi.org/10.1109/REAL.1997.641264

28.

Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model-checker for hybrid systems. Int. J. Softw. Tools Technol. Transf. 1(1–2), 110–122 (1997). http://dx.doi.org/10.1007/s100090050008 CrossRefMATH

29.

Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. Log. Methods Comput. Sci. 3(1:3), 1–11 (2007). http://dx.doi.org/10.2168/LMCS-3(1:3)2007 MathSciNetMATH

30.

Hirshfeld, Y., Rabinovich, A.M.: Future temporal logic needs infinitely many modalities. Inf. Comp. 187(2), 196–208 (2003). http://dx.doi.org/10.1016/S0890-5401(03)00163-9 MathSciNetCrossRefMATH

31.

Hunter, P.: When is metric temporal logic expressively complete? In: CSL 2013, LIPIcs, vol. 23, pp. 380–394. Leibniz-Zentrum für Informatik (2013). http://dx.doi.org/10.4230/LIPIcs.CSL.2013.380

32.

Hunter, P., Ouaknine, J., Worrell, J.: Expressive completeness for metric temporal logic. In: LICS 2013, pp. 349–357. IEEE Computer Society Press (2013). http://dx.doi.org/10.1109/LICS.2013.41

33.

Jaziri, S., Larsen, K.G., Mardare, R., Xue, B.: Adequacy and complete axiomatization for timed modal logic. In: Proceedings of the 30th Conference on Mathematical Foundations of Programming Semantics (MFPS 2014), ENTCS, vol. 308, pp. 183–210. Elsevier Science Publishers (2014)

34.

Kamp, J.A.W.: Tense logic and the theory of linear order. Ph.D. thesis, Computer Science Department, University of California at Los Angeles, USA (1968)

35.

Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990). http://dx.doi.org/10.1007/BF01995674 CrossRef

36.

Krishna, S.N., Madnani, K., Pandya, P.K.: Metric temporal logic with counting. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 335–352. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49630-5_20 CrossRef

37.

Torre, S.L., Napoli, M.: A decidable dense branching-time temporal logic. In: Kapoor, S., Prasad, S. (eds.) FSTTCS 2000. LNCS, vol. 1974, pp. 139–150. Springer, Heidelberg (2000). doi:10.1007/3-540-44450-5_11 CrossRef

38.

Laroussinie, F., Larsen, K.G.: CMC: a tool for compositional model-checking of real-time systems. In: IFIP Conference Proceedings on FORTE/PSTV 1998, vol. 135, pp. 439–456. Kluwer Academic (1998)

39.

Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic — and back. In: Wiedermann, J., Hájek, P. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995). doi:10.1007/3-540-60246-1_158 CrossRef

40.

Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). doi:10.1007/3-540-52148-8_19 CrossRef

41.

Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997). http://dx.doi.org/10.1007/s100090050010 CrossRefMATH

42.

Maler, O.: Some thoughts on runtime verification. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 3–14. Springer, Cham (2016). doi:10.1007/978-3-319-46982-9_1 CrossRef

43.

Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12 CrossRef

44.

Milner, R.: Communication and Concurrency, Prentice Hall International Series in Computer Science. Prentice Hall Int., Upper Saddle River (1989)MATH

45.

Ouaknine, J., Rabinovich, A., Worrell, J.: Time-bounded verification. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 496–510. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04081-8_33 CrossRef

46.

Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: LICS 2005, pp. 188–197. IEEE Computer Society Press (2005). http://dx.doi.org/10.1109/LICS.2005.33

47.

Ouaknine, J., Worrell, J.: On metric temporal logic and faulty turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006). doi:10.1007/11690634_15 CrossRef

48.

Ouaknine, J., Worrell, J.: Safety metric temporal logic is fully decidable. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 411–425. Springer, Heidelberg (2006). doi:10.1007/11691372_27 CrossRef

49.

Pandya, P.K., Shah, S.S.: On expressive powers of timed logics: comparing boundedness, non-punctuality, and deterministic freezing. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 60–75. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23217-6_5 CrossRef

50.

Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE Computer Society Press (1977). http://dx.doi.org/10.1109/SFCS.1977.32

51.

Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982). doi:10.1007/3-540-11494-7_22 CrossRef

52.

Raskin, J.-F.: Logics, automata and classical theories for deciding real time. Thèse de doctorat, FUNDP, Namur, Belgium (1999)

53.

Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: FOCS 1983, pp. 185–194. IEEE Computer Society Press (1983). http://dx.doi.org/10.1109/SFCS.1983.51

54.

Yi, W.: CCS + time = an interleaving model for real time systems. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991). doi:10.1007/3-540-54233-7_136 CrossRef

Title: Timed Temporal Logics
Authors: Patricia Bouyer
François Laroussinie
Nicolas Markey
Joël Ouaknine
James Worrell
Publisher: Springer International Publishing
Book: Models, Algorithms, Logics and Tools
Print ISBN: 978-3-319-63120-2

Electronic ISBN: 978-3-319-63121-9

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-63121-9_11

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner