Document Open Access Logo

A Model Checking Procedure for Interval Temporal Logics based on Track Representatives

Authors Alberto Molinari, Angelo Montanari, Adriano Peron

PDF
Thumbnail PDF

File

LIPIcs.CSL.2015.193.pdf
  • Filesize: 0.66 MB
  • 18 pages

Document Identifiers

Author Details

Alberto Molinari
Angelo Montanari
Adriano Peron

Cite As Get BibTex

Alberto Molinari, Angelo Montanari, and Adriano Peron. A Model Checking Procedure for Interval Temporal Logics based on Track Representatives. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 193-210, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.193

Abstract

Model checking is commonly recognized as one of the most effective tool in system verification. While it has been systematically investigated in the context of classical, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACE-hardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones.

Subject Classification

Keywords
  • Interval Temporal Logic
  • Model Checking
  • Complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. J. F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983. Google Scholar
  2. D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. The dark side of interval temporal logic: marking the undecidability border. Annals of Mathematics and Artificial Intelligence, 71(1-3):41-83, 2014. Google Scholar
  3. D. Bresolin, V. Goranko, A. Montanari, and P. Sala. Tableau-based decision procedures for the logics of subinterval structures over dense orderings. Journal of Logic and Computation, 20(1):133-166, 2010. Google Scholar
  4. D. Bresolin, V. Goranko, A. Montanari, and G. Sciavicco. Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions. Annals of Pure and Applied Logic, 161(3):289-304, 2009. Google Scholar
  5. D. Bresolin, A. Montanari, P. Sala, and G. Sciavicco. What’s decidable about Halpern and Shoham’s interval logic? The maximal fragment AB ̅BL. In LICS, pages 387-396, 2011. Google Scholar
  6. E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2002. Google Scholar
  7. M. Fränzle. Model-checking dense-time Duration Calculus. Formal Aspects of Computing, 16(2):121-139, 2004. Google Scholar
  8. M. Fränzle and M. R. Hansen. Efficient model checking for Duration Calculus? International Journal of Software and Informatics, 3(2-3):171-196, 2009. Google Scholar
  9. J. Y. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38(4):935-962, 1991. Google Scholar
  10. M. R. Hansen. Model-checking discrete Duration Calculus. Formal Aspects of Computing, 6(6A):826-845, 1994. Google Scholar
  11. M. R. Hansen, A. D. Phan, and A. W. Brekling. A practical approach to model checking Duration Calculus using Presburger Arithmetic. Annals of Mathematics and Artificial Intelligence, 71(1-3):251-278, 2014. Google Scholar
  12. K. Lodaya. A language-theoretic view of verification. In Modern Applications of Automata Theory, pages 149-170, 2012. Google Scholar
  13. A. R. Lomuscio and J. Michaliszyn. An epistemic Halpern-Shoham logic. In IJCAI, pages 1010-1016, 2013. Google Scholar
  14. A. R. Lomuscio and J. Michaliszyn. Decidability of model checking multi-agent systems against a class of EHS specifications. In ECAI, pages 543-548, 2014. Google Scholar
  15. R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking Duration Calculus: a practical approach. Formal Aspects of Computing, 20(4-5):481-505, 2008. Google Scholar
  16. A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking Interval Properties of Computations. Technical Report 2015/01, Dept. of Math. and CS, University of Udine, 2015. URL: https://www.dimi.uniud.it/assets/preprints/1-2015-montanari.pdf.
  17. A. Molinari, A. Montanari, and A. Peron. A Model Checking Procedure for Interval Temporal Logics based on Track Representatives. Technical Report 2015/02, Dept. of Math. and CS, University of Udine, 2015. URL: https://www.dimi.uniud.it/assets/preprints/2-2015-montanari.pdf.
  18. A. Montanari, A. Murano, G. Perelli, and A Peron. Checking interval properties of computations. In TIME, pages 59-68, 2014. Google Scholar
  19. A. Montanari, G. Puppis, and P. Sala. Maximal decidable fragments of Halpern and Shoham’s modal logic of intervals. In ICALP (2), LNCS 6199, pages 345-356, 2010. Google Scholar
  20. B. Moszkowski. Reasoning About Digital Circuits. PhD thesis, Dept. of Computer Science, Stanford University, Stanford, CA, 1983. Google Scholar
  21. P. K. Pandya. Model checking CTL*[DC]. In TACAS, LNCS 2031, pages 559-573, 2001. Google Scholar
  22. I. Pratt-Hartmann. Temporal prepositions and their logic. Artificial Intelligence, 166(1-2):1-36, 2005. Google Scholar
  23. P. Roeper. Intervals and tenses. Journal of Philosophical Logic, 9:451-469, 1980. Google Scholar
  24. Y. Venema. Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact