Pubblicazioni

Model Checking the Logic of Allen's Relations Meets and Started-by is P^NP-Complete  (2016)

Autori:
Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro
Titolo:
Model Checking the Logic of Allen's Relations Meets and Started-by is P^NP-Complete
Anno:
2016
Tipologia prodotto:
Contributo in atti di convegno
Tipologia ANVUR:
Contributo in Atti di convegno
Lingua:
Inglese
Nome rivista:
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
ISSN Rivista:
2075-2180
N° Volume:
226
Titolo del Convegno:
GandALF
Luogo:
Catania
Periodo:
14-16 September 2016
Intervallo pagine:
76-90
Parole chiave:
Interval Logic, Model Checking, Complexity
Breve descrizione dei contenuti:
In the plethora of fragments of Halpern and Shoham's modal logic of time intervals (HS), the logic AB of Allen's relations Meets and Started-by is at a central position. Statements that may be true at certain intervals, but at no sub-interval of them, such as accomplishments, as well as metric constraints about the length of intervals, that force, for instance, an interval to be at least (resp., at most, exactly) k points long, can be expressed in AB. Moreover, over the linear order of the natural numbers N, it subsumes the (point-based) logic LTL, as it can easily encode the next and until modalities. Finally, it is expressive enough to capture the {omega}-regular languages, that is, for each {omega}-regular expression R there exists an AB formula {phi} such that the language defined by R coincides with the set of models of {phi} over N. It has been shown that the satisfiability problem for AB over N is EXPSPACE-complete. Here we prove that, under the homogeneity assumption, its model checking problem is {Delta}^p_2 = P^NP-complete (for the sake of comparison, the model checking problem for full HS is EXPSPACE-hard, and the only known decision procedure is nonelementary). Moreover, we show that the modality for the Allen relation Met-by can be added to AB at no extra cost (AA'B is P^NP-complete as well).
Id prodotto:
93891
Handle IRIS:
11562/951255
ultima modifica:
13 novembre 2022
Citazione bibliografica:
Bozzelli, Laura; Molinari, Alberto; Montanari, Angelo; Peron, Adriano; Sala, Pietro, Model Checking the Logic of Allen's Relations Meets and Started-by is P^NP-Complete in «ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE» vol. 226  in Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016, Catania, Italy, 14-16 September 2016Atti di "GandALF" , Catania , 14-16 September 2016 , 2016pp. 76-90

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

<<indietro

Attività

Strutture

Condividi