Model checking (MC) for Halpern and Shoham’s interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics), all of them assuming homogeneity in the propositional valuation. Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure. We introduce a quantitative extension of HS over traces, called Difference HS (DHS), allowing one to express timing constraints on the difference among interval lengths (durations). We show that MC and satisfiability of full DHS are in general undecidable, so, we investigate the decidability border for these problems by considering natural syntactical fragments of DHS. In particular, we identify a maximal decidable fragment DHSsimple of DHS proving in addition that the considered problems for this fragment are at least 2Expspace-hard. Moreover, by exploiting new results on linear-time hybrid logics, we show that for an equally expressive fragment of DHSsimple, the problems are Expspace-complete. Finally, we provide a characterization of HS over traces by means of the one-variable fragment of a novel hybrid logic.

A Quantitative Extension of Interval Temporal Logic over Infinite Words / Bozzelli, L.; Peron, A.. - 247:(2022). (Intervento presentato al convegno 29th International Symposium on Temporal Representation and Reasoning (TIME 2022) tenutosi a Virtual Conference nel November 7-9, 2022) [10.4230/LIPIcs.TIME.2022.11].

A Quantitative Extension of Interval Temporal Logic over Infinite Words

Bozzelli L.
;
Peron A.
2022

Abstract

Model checking (MC) for Halpern and Shoham’s interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics), all of them assuming homogeneity in the propositional valuation. Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure. We introduce a quantitative extension of HS over traces, called Difference HS (DHS), allowing one to express timing constraints on the difference among interval lengths (durations). We show that MC and satisfiability of full DHS are in general undecidable, so, we investigate the decidability border for these problems by considering natural syntactical fragments of DHS. In particular, we identify a maximal decidable fragment DHSsimple of DHS proving in addition that the considered problems for this fragment are at least 2Expspace-hard. Moreover, by exploiting new results on linear-time hybrid logics, we show that for an equally expressive fragment of DHSsimple, the problems are Expspace-complete. Finally, we provide a characterization of HS over traces by means of the one-variable fragment of a novel hybrid logic.
2022
978-3-95977-262-4
A Quantitative Extension of Interval Temporal Logic over Infinite Words / Bozzelli, L.; Peron, A.. - 247:(2022). (Intervento presentato al convegno 29th International Symposium on Temporal Representation and Reasoning (TIME 2022) tenutosi a Virtual Conference nel November 7-9, 2022) [10.4230/LIPIcs.TIME.2022.11].
File in questo prodotto:
File Dimensione Formato  
TIME_2022.pdf

solo utenti autorizzati

Licenza: Copyright dell'editore
Dimensione 829.94 kB
Formato Adobe PDF
829.94 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11588/955824
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact