2026-07-23T03:27:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7470 2024-03-12T11:58:28Z ddc:004 open_access

Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption Bozzelli, Laura Molinari, Alberto Montanari, Angelo Peron, Adriano Sala, Pietro Interval Temporal Logic Satisfiability Model Checking Decidability Computational Complexity 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Laura Bozzelli and Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala 2017 Is Part Of LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2017.120 urn:nbn:de:0030-drops-74703 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.120 eng https://creativecommons.org/licenses/by/3.0/legalcode