eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2017-07-07
120:1
120:14
10.4230/LIPIcs.ICALP.2017.120
article
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
Bozzelli, Laura
Molinari, Alberto
Montanari, Angelo
Peron, Adriano
Sala, Pietro
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol080-icalp2017/LIPIcs.ICALP.2017.120/LIPIcs.ICALP.2017.120.pdf
Interval Temporal Logic
Satisfiability
Model Checking
Decidability
Computational Complexity