Model checking 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. Here, we focus on the trace-based semantics, where the infinite execution paths (traces) of the given (finite) Kripke structure are the main semantic entities. In this setting, each finite infix of a trace is interpreted as an interval, and a proposition holds over an interval if and only if it holds over each component state (homogeneity assumption). In this paper, we introduce a quantitative extension of HS over traces, called parametric HS (PHS). The novel logic allows to express parametric timing constraints on the duration (length) of the intervals. We show that checking the existence of a parameter valuation for which a Kripke structure satisfies a PHS formula (model checking), or a PHS formula admits a trace as a model under the homogeneity assumption (satisfiability) is decidable. Moreover, we identify a fragment of PHS which subsumes parametric LTL and for which model checking and satisfiability are shown to be EXPSPACE-complete.

Parametric Interval Temporal Logic over Infinite Words

Peron A.
2022-01-01

Abstract

Model checking 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. Here, we focus on the trace-based semantics, where the infinite execution paths (traces) of the given (finite) Kripke structure are the main semantic entities. In this setting, each finite infix of a trace is interpreted as an interval, and a proposition holds over an interval if and only if it holds over each component state (homogeneity assumption). In this paper, we introduce a quantitative extension of HS over traces, called parametric HS (PHS). The novel logic allows to express parametric timing constraints on the duration (length) of the intervals. We show that checking the existence of a parameter valuation for which a Kripke structure satisfies a PHS formula (model checking), or a PHS formula admits a trace as a model under the homogeneity assumption (satisfiability) is decidable. Moreover, we identify a fragment of PHS which subsumes parametric LTL and for which model checking and satisfiability are shown to be EXPSPACE-complete.
File in questo prodotto:
File Dimensione Formato  
2209.10316v1.pdf

accesso aperto

Tipologia: Documento in Versione Editoriale
Licenza: Creative commons
Dimensione 240.41 kB
Formato Adobe PDF
240.41 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

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