Document Open Access Logo

Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption

Authors Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2017.120.pdf
  • Filesize: 0.61 MB
  • 14 pages

Document Identifiers

Author Details

Laura Bozzelli
Alberto Molinari
Angelo Montanari
Adriano Peron
Pietro Sala

Cite As Get BibTex

Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, and Pietro Sala. Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 120:1-120:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ICALP.2017.120

Abstract

In this paper, we investigate the finite satisfiability and model checking problems for the logic D of the sub-interval relation under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over all its points. First, we prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete; then, we show that its model checking problem, over finite Kripke structures, is PSPACE-complete as well.

Subject Classification

Keywords
  • Interval Temporal Logic
  • Satisfiability
  • Model Checking
  • Decidability
  • Computational 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. URL: http://dx.doi.org/10.1145/182.358434.
  2. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Interval temporal logic model checking: The border between good and bad HS fragments. In Proceedings of the 8th International Joint Conference (IJCAR), pages 389-405, 2016. URL: http://dx.doi.org/10.1007/978-3-319-40229-1_27.
  3. L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Satisfiability and model checking for the logic of sub-intervals under the homogeneity assumption. Technical report, University of Udine, Italy, 2017. URL: https://www.dimi.uniud.it/la-ricerca/pubblicazioni/preprints/4.2017/.
  4. D. Bresolin, V. Goranko, A. Montanari, and P. Sala. Tableaux for logics of subinterval structures over dense orderings. Journal of Logic and Computation, 20(1):133-166, 2010. URL: http://dx.doi.org/10.1093/logcom/exn063.
  5. 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. URL: http://dx.doi.org/10.1016/j.apal.2009.07.003.
  6. D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Interval temporal logics: a journey. Bulletin of the EATCS, 105:73-99, 2011. URL: http://albcom.lsi.upc.edu/ojs/index.php/beatcs/article/view/98.
  7. J. Y. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38:279-292, 1991. URL: http://dx.doi.org/10.1145/115234.115351.
  8. M. Holzer and M. Kutrib. Descriptional and computational complexity of finite automata - a survey. Information and Computation, 209(3):456-470, 2011. URL: http://dx.doi.org/10.1016/j.ic.2010.11.013.
  9. H. Kamp and U. Reyle. From Discourse to Logic: Introduction to Model-theoretic Semantics of Natural Language, Formal Logic and Discourse Representation Theory, Volume 42 of Studies in Linguistics and Philosophy. Springer, 1993. Google Scholar
  10. K. Lodaya. Sharpening the undecidability of interval temporal logic. In Proceedings of the 6th Asian Computing Science Conference (ASIAN), pages 290-298, 2000. URL: http://dx.doi.org/10.1007/3-540-44464-5_21.
  11. J. Marcinkowski and J. Michaliszyn. The undecidability of the logic of subintervals. Fundamenta Informaticae, 131(2):217-240, 2014. URL: http://dx.doi.org/10.3233/FI-2014-1011.
  12. A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking interval properties of computations. Acta Informatica, 53(6-8):587-619, 2016. URL: http://dx.doi.org/10.1007/s00236-015-0250-1.
  13. A. Montanari. Interval temporal logics model checking. In Proceedings of the 23rd International Symposium on Temporal Representation and Reasoning, (TIME), page 2, 2016. URL: http://dx.doi.org/10.1109/TIME.2016.32.
  14. A. Montanari, I. Pratt-Hartmann, and P. Sala. Decidability of the logics of the reflexive sub-interval and super-interval relations over finite linear orders. In Proceedings of the 17th International Symposium on Temporal Representation and Reasoning (TIME), pages 27-34, 2010. URL: http://dx.doi.org/10.1109/TIME.2010.18.
  15. M. Otto. Two variable first-order logic over ordered domains. Journal of Symbolic Logic, 66(2):685-702, 2001. URL: http://dx.doi.org/10.2307/2695037.
  16. I. Shapirovsky. On PSPACE-decidability in transitive modal logic. In Proceedings of the 5th conference on Advances in Modal logic (AiML), pages 269-287, 2004. URL: http://www.aiml.net/volumes/volume5/Shapirovsky.ps.
  17. Y. Venema. Expressiveness and completeness of an interval tense logic. Notre Dame Journal of Formal Logic, 31(4):529-547, 1990. URL: http://dx.doi.org/10.1305/ndjfl/1093635589.
  18. Y. Venema. A modal logic for chopping intervals. Journal of Logic and Computation, 1(4):453-476, 1991. URL: http://dx.doi.org/10.1093/logcom/1.4.453.
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