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

A. Montanari;P. Sala
2017-01-01

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.
2017
9783959770415
Interval Temporal Logic, Satisfiability, Model Checking, Decidability, Computational Complexity
File in questo prodotto:
File Dimensione Formato  
LIPIcs-ICALP-2017-120.pdf

accesso aperto

Tipologia: Versione dell'editore
Licenza: Creative commons
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/969964
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 13
  • ???jsp.display-item.citation.isi??? ND
social impact