Metric temporal logic revisited

详细信息    查看全文

• 作者：Mark Reynolds
• 刊名：Acta Informatica
• 出版年：2016
• 出版时间：April 2016
• 年：2016
• 卷：53
• 期：3
• 页码：301-324
• 全文大小：711 KB
• 参考文献：1.Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996). doi:10.​1145/​227595.​227602 MathSciNet CrossRef MATH
  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.Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)MathSciNet CrossRef MATH
  4.Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–203 (1994). doi:10.​1145/​174644.​174651 MathSciNet CrossRef MATH
  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.Burgess, J.P., Gurevich, Y.: The decision problem for linear temporal logic. Notre Dame J. Form. Log. 26(2), 115–128 (1985)MathSciNet CrossRef MATH
  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)MathSciNet CrossRef MATH
  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)MathSciNet MATH
  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.Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990). doi:10.​1007/​BF01995674 CrossRef
  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.Reynolds, M.: An axiomatization for Until and Since over the reals without the IRR rule. Stud. Log. 51, 165–193 (1992)MathSciNet CrossRef MATH
  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.Reynolds, M.: The complexity of the temporal logic over the reals. Ann. Pure Appl. Log. 161(8), 1063–1096 (2010). doi:10.​1016/​j.​apal.​2010.​01.​002 MathSciNet CrossRef MATH
  39.Reynolds, M.: Metric temporal reasoning with less than 2 clocks. J. Appl. Non-class. Log. 20, 437–455 (2010)MathSciNet CrossRef MATH
  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)
  
• 作者单位：Mark Reynolds (1)
  
  1. School of Computer Science and Software Engineering, The University of Western Australia, Perth, Australia
  
• 刊物类别：Computer Science
• 刊物主题：Logics and Meanings of Programs
  Computer Systems Organization and Communication Networks
  Software Engineering, Programming and Operating Systems
  Data Structures, Cryptology and Information Theory
  Theory of Computation
  Information Systems and Communication Service
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1432-0525

文摘

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.