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.
翻译:最近对Halpern和Shoham的间隙时间逻辑 HS 模型检查进行了系统化调查,已知该模型在三种不同的语义(基于国家、基于痕量和基于树的语义)下可分解。这里,我们侧重于基于痕量的语义学,主要语义学实体是给定的Kripke结构的无限执行路径(跟踪),假设在假设的估价中存在同质性。我们引入了HS相对于痕迹的定量延伸,称为差异 HS(DHS),允许一个人对间距(时间长度)的差异明确时间限制。一些模式的数量延伸立即导致不可分化,因此,我们通过考虑严格的同步断层断层,调查模型检查和可谱性问题的可分解边界边界。我们特别确定了DHSDS的最大可分解的碎片DIS,证明所考虑的问题至少是2EXPSPACE(DH)硬性。此外,我们通过对线-时间混合逻辑的新的结果进行新的探索,我们通过HPAS-PIS的一条分级逻辑的分解,向我们展示了HS-S-CE的一条分级的分级的分解,我们同样展示了HIS-C。