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

Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala
Titolo Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
Numero 4/2017
Sottomesso da Alberto Molinari
Sottomesso il 24/4/2017
Stato Submitted
Autori Laura Bozzelli, Alberto Molinari, Angelo Montanari, Adriano Peron, Pietro Sala
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.
File 4-2017-Molinari.pdf