A quantitative extension of Interval Temporal Logic over infinite words

TL;DR

This paper introduces a quantitative extension of Interval Temporal Logic over infinite traces, identifying decidable fragments and analyzing their computational complexity, thereby advancing formal verification methods for timing constraints.

Contribution

It proposes Difference HS (DHS), a new quantitative logic for infinite traces, and characterizes its decidable fragments and complexity, extending the expressiveness of HS.

Findings

Identified the maximal decidable fragment DHSS of DHS.

Proved that model checking and satisfiability are at least 2EXPSPACE-hard for DHS.

Showed EXPSPACE-completeness for an expressive fragment of DHSS.

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 (state-based, trace-based and tree-based semantics). Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure, assuming in addition homogeneity in the propositional valuation. 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). The quantitative extension of some modalities leads immediately to undecidability, so, we investigate the decidability border for the model checking and satisfiability problems by considering strict syntactical fragments of DHS. In particular, we identify the maximal decidable fragment DHSS of DHS proving in addition that the considered problems for the 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 DHSS, 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.