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

TL;DR

This paper studies the computational complexity of satisfiability and model checking for a specific interval temporal logic under the homogeneity assumption, showing they are PSPACE-complete, thus expanding the set of practical ITLs.

Contribution

It proves PSPACE-completeness of satisfiability and model checking for the logic D under the homogeneity assumption, demonstrating its tractability for finite structures.

Findings

Satisfiability for D over finite linear orders is PSPACE-complete.

Model checking for D over finite Kripke structures is PSPACE-complete.

Enriches the class of tractable interval temporal logics.

Abstract

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.