Laura Bozzelli ; Alberto Molinari ; Angelo Montanari ; Adriano Peron ; Pietro Sala - Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption

lmcs:6542 - Logical Methods in Computer Science, February 1, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:24)2022
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

The expressive power of interval temporal logics (ITLs) makes them one of the most natural choices in a number of application domains, ranging from the specification and verification of complex reactive systems to automated planning. However, for a long time, because of their high computational complexity, they were considered not suitable for practical purposes. The recent discovery of several computationally well-behaved ITLs has finally changed the scenario. In this paper, we investigate the finite satisfiability and model checking problems for the ITL D, that has a single modality for 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). We first prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete, and then we show that the same holds for its model checking problem, over finite Kripke structures. In such a way, we enrich the set of tractable interval temporal logics with a new meaningful representative.


Volume: Volume 18, Issue 1
Published on: February 1, 2022
Accepted on: January 17, 2022
Submitted on: June 9, 2020
Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory


Share

Consultation statistics

This page has been seen 324 times.
This article's PDF has been downloaded 393 times.