An In-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions

  • Laura Bozzelli
  • Alberto Molinari
  • Angelo MontanariEmail author
  • Adriano Peron
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10469)


In the last years, the model checking (MC) problem for interval temporal logic (ITL) has received an increasing attention as a viable alternative to the traditional (point-based) temporal logic MC, which can be recovered as a special case. Most results have been obtained by imposing suitable restrictions on interval labeling. In this paper, we overcome such limitations by using regular expressions to define the behavior of proposition letters over intervals in terms of the component states. We first prove that MC for Halpern and Shoham’s ITL (HS), extended with regular expressions, is decidable. Then, we show that formulas of a large class of HS fragments, namely, all fragments featuring (a subset of) HS modalities for Allen’s relations meets, met-by, starts, and started-by, can be model checked in polynomial working space (MC for all these fragments turns out to be PSPACE-complete).


  1. 1.
    Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (1983)CrossRefGoogle Scholar
  2. 2.
    Bozzelli, L., Molinari, A., Montanari, A., Peron, A.: An in-depth investigation of ITL MC with regular expressions. Technical report 2, University of Udine, Italy (2017).
  3. 3.
    Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: Interval temporal logic model checking: the border between good and bad HS fragments. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 389–405. Springer, Cham (2016). doi: 10.1007/978-3-319-40229-1_27CrossRefGoogle Scholar
  4. 4.
    Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: Interval vs. point temporal logic model checking: an expressiveness comparison. In: FSTTCS (2016)Google Scholar
  5. 5.
    Bozzelli, L., Molinari, A., Montanari, A., Peron, A., Sala, P.: MC the logic of Allen’s relations meets and started-by is P\(^{\rm NP}\)-C. In: GandALF, pp. 76–90 (2016)Google Scholar
  6. 6.
    Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: The dark side of interval temporal logic: marking the undecidability border. Ann. Math. Artif. Intell. 71(1–3), 41–83 (2014)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000). doi: 10.1007/10722167_20CrossRefGoogle Scholar
  8. 8.
    Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38(4), 935–962 (1991)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods Syst. Des. 34(2), 83–103 (2009)CrossRefGoogle Scholar
  10. 10.
    Lomuscio, A., Michaliszyn, J.: An epistemic HS logic. In: IJCAI, pp. 1010–1016 (2013)Google Scholar
  11. 11.
    Lomuscio, A., Michaliszyn, J.: Decidability of model checking multi-agent systems against a class of EHS specifications. In: ECAI, pp. 543–548 (2014)Google Scholar
  12. 12.
    Lomuscio, A., Michaliszyn, J.: Model checking multi-agent systems against epistemic HS specifications with regular expressions. In: KR, pp. 298–308 (2016)Google Scholar
  13. 13.
    Marcinkowski, J., Michaliszyn, J.: The undecidability of the logic of subintervals. Fundamenta Informaticae 131(2), 217–240 (2014)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Molinari, A., Montanari, A., Murano, A., Perelli, G., Peron, A.: Checking interval properties of computations. Acta Informatica 53, 587–619 (2016)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Molinari, A., Montanari, A., Peron, A.: Complexity of ITL model checking: some well-behaved fragments of the interval logic HS. In: TIME, pp. 90–100 (2015)Google Scholar
  16. 16.
    Molinari, A., Montanari, A., Peron, A.: A model checking procedure for interval temporal logics based on track representatives. In: CSL, pp. 193–210 (2015)Google Scholar
  17. 17.
    Molinari, A., Montanari, A., Peron, A., Sala, P.: Model checking well-behaved fragments of HS: the (Almost) final picture. In: KR, pp. 473–483 (2016)Google Scholar
  18. 18.
    Montanari, A.: Interval temporal logics model checking. In: TIME, p. 2 (2016)Google Scholar
  19. 19.
    Moszkowski, B.: Reasoning about digital circuits. Ph.D. thesis, Stanford (1983)Google Scholar
  20. 20.
    Roeper, P.: Intervals and tenses. J. Philos. Log. 9, 451–469 (1980)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Venema, Y.: Expressiveness and completeness of an interval tense logic. Notre Dame J. Formal Log. 31(4), 529–547 (1990)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Laura Bozzelli
    • 1
  • Alberto Molinari
    • 2
  • Angelo Montanari
    • 2
    Email author
  • Adriano Peron
    • 1
  1. 1.University of Napoli “Federico II”NapoliItaly
  2. 2.University of UdineUdineItaly

Personalised recommendations