LIPIcs.ICALP.2017.120.pdf
- Filesize: 0.61 MB
- 14 pages
Document
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
Authors
-
Part of:
Volume:
44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Colloquium on Automata, Languages, and Programming (ICALP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2017-07-07
Cite AsGet 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
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.
Keywords
- Interval Temporal Logic
- Satisfiability
- Model Checking
- Decidability
- Computational Complexity
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- 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.
- 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/.
- 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.
- 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.
- 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.
- 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.
- 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.
-
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.