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
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption / Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, P. i. e. t. r. o.. - 80:(2017), pp. 1-14. (Intervento presentato al convegno 44th International Colloquium on Automata, Languages, and Programming ICALP 2017 tenutosi a Warsaw nel July 10-14 2017) [10.4230/LIPIcs.ICALP.2017.120].
Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption
Bozzelli, Laura;PERON, ADRIANO;
2017
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 | Dimensione | Formato | |
|---|---|---|---|
|
LIPIcs-ICALP-2017-120.pdf
accesso aperto
Descrizione: Articolo ricerca
Tipologia:
Documento in Post-print
Licenza:
Dominio pubblico
Dimensione
630.92 kB
Formato
Adobe PDF
|
630.92 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
