Advertisement

The Compound Interest in Relaxing Punctuality

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

Imprecision in timing can sometimes be beneficial: Metric interval temporal logic (MITL), disabling the expression of punctuality constraints, was shown to translate to timed automata, yielding an elementary decision procedure. We show how this principle extends to other forms of dense-time specification using regular expressions. By providing a clean, automaton-based formal framework for non-punctual languages, we are able to recover and extend several results in timed systems. Metric interval regular expressions (MIRE) are introduced, providing regular expressions with non-singular duration constraints. We obtain that MIRE are expressively complete relative to a class of one-clock timed automata, which can be determinized using additional clocks. Metric interval dynamic logic (MIDL) is then defined using MIRE as temporal modalities. We show that MIDL generalizes known extensions of MITL, while translating to timed automata at comparable cost.

Notes

Acknowledgments

I thank Eugene Asarin, Tom Henzinger, Oded Maler, Dejan Ničković, and anonymous reviewers of multiple conferences for their helpful feedback.

References

  1. 1.
    Abdulla, P.A., Deneux, J., Ouaknine, J., Quaas, K., Worrell, J.: Universality analysis for one-clock timed automata. Fundam. Inform. 89(4), 419–450 (2008)MathSciNetMATHGoogle Scholar
  2. 2.
    Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)MathSciNetCrossRefGoogle Scholar
  4. 4.
    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 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992).  https://doi.org/10.1007/BFb0031988CrossRefGoogle Scholar
  5. 5.
    Alur, R., La Torre, S., Madhusudan, P.: Perturbed timed automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 70–85. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31954-2_5CrossRefGoogle Scholar
  6. 6.
    Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Basin, D., Krstić, S., Traytel, D.: Almost event-rate independent monitoring of metric dynamic logic. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 85–102. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67531-2_6CrossRefGoogle Scholar
  8. 8.
    Bersani, M.M., Rossi, M., Pietro, P.S.: A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Informatica 53(2), 171–206 (2016)MathSciNetCrossRefGoogle Scholar
  9. 9.
    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).  https://doi.org/10.1007/11590156_35CrossRefMATHGoogle Scholar
  10. 10.
    Brihaye, T., Estiévenart, M., Geeraerts, G.: On MITL and alternating timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 47–61. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40229-6_4CrossRefMATHGoogle Scholar
  11. 11.
    Brihaye, T., Estiévenart, M., Geeraerts, G.: On MITL and alternating timed automata over infinite words. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 69–84. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-10512-3_6CrossRefMATHGoogle Scholar
  12. 12.
    Brihaye, T., Geeraerts, G., Ho, H.-M., Monmege, B.: MightyL: a compositional translation from MITL to timed automata. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 421–440. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63387-9_21CrossRefGoogle Scholar
  13. 13.
    De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. IJCAI 13, 854–860 (2013)Google Scholar
  14. 14.
    Eisner, C., Fisman, D.: A Practical Introduction to PSL. Integrated Circuits and Systems. Springer, Heidelberg (2006).  https://doi.org/10.1007/978-0-387-36123-9CrossRefGoogle Scholar
  15. 15.
    Fischer, M.J.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Furia, C.A., Rossi, M.: MTL with bounded variability: decidability and complexity. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 109–123. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-85778-5_9CrossRefMATHGoogle Scholar
  17. 17.
    Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–591. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055086CrossRefGoogle Scholar
  18. 18.
    Hirshfeld, Y., Rabinovich, A.: An expressive temporal logic for real time. In: Královič, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 492–504. Springer, Heidelberg (2006).  https://doi.org/10.1007/11821069_43CrossRefGoogle Scholar
  19. 19.
    Hirshfeld, Y., Rabinovich, A.: Expressiveness of metric modalities for continuous time. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 211–220. Springer, Heidelberg (2006).  https://doi.org/10.1007/11753728_23CrossRefGoogle Scholar
  20. 20.
    Kleene, S.C.: Representation of events in nerve nets and finite automata. Automata Stud., 3–42 (1956)Google Scholar
  21. 21.
    Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRefGoogle Scholar
  22. 22.
    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).  https://doi.org/10.1007/978-3-662-49630-5_20CrossRefGoogle Scholar
  23. 23.
    Krishna, S.N., Madnani, K., Pandya, P.K.: Making metric temporal logic rational. In: Mathematical Foundations of Computer Science, pp. 77:1–77:14 (2017)Google Scholar
  24. 24.
    Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 250–265. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31982-5_16CrossRefGoogle Scholar
  25. 25.
    Maler, O., Nickovic, D., Pnueli, A.: Real time temporal logic: past, present, future. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 2–16. Springer, Heidelberg (2005).  https://doi.org/10.1007/11603009_2CrossRefGoogle Scholar
  26. 26.
    Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006).  https://doi.org/10.1007/11867340_20CrossRefMATHGoogle Scholar
  27. 27.
    Michel, M.: Composition of temporal operators. Logique et Analyse 28(110/111), 137–152 (1985)MathSciNetMATHGoogle Scholar
  28. 28.
    Ničković, D., Piterman, N.: From Mtl to deterministic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 152–167. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15297-9_13CrossRefMATHGoogle Scholar
  29. 29.
    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).  https://doi.org/10.1007/978-3-642-04081-8_33CrossRefGoogle Scholar
  30. 30.
    Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Logic in Computer Science, pp. 188–197. IEEE (2005)Google Scholar
  31. 31.
    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).  https://doi.org/10.1007/11690634_15CrossRefMATHGoogle Scholar
  32. 32.
    Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science, pp. 46–57. IEEE (1977)Google Scholar
  33. 33.
    Pnueli, A., Zaks, A.: On the merits of temporal testers. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 172–195. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-69850-0_11CrossRefMATHGoogle Scholar
  34. 34.
    Roohi, N., Viswanathan, M.: Revisiting MITL to fix decision procedures. In: Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 474–494. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-73721-8_22CrossRefGoogle Scholar
  35. 35.
    Sipser, M.: Introduction to the Theory of Computation, vol. 2. Thomson Course Technology, Boston (2006)MATHGoogle Scholar
  36. 36.
    Vardi, M.Y.: From philosophical to industrial logics. In: Ramanujam, R., Sarukkai, Sundar (eds.) ICLA 2009. LNCS (LNAI), vol. 5378, pp. 89–115. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-92701-3_7CrossRefGoogle Scholar
  37. 37.
    Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58468-4_191CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.IST AustriaKlosterneuburgAustria

Personalised recommendations