A quantitative extension of interval temporal logic over infinite words

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 a given Kripke structure and intervals are fragments of traces. 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.