论文标题
间隔时间逻辑超过无限单词的定量扩展
A quantitative extension of Interval Temporal Logic over infinite words
论文作者
论文摘要
最近对Halpern和Shoham的间隔时间逻辑HS进行了模型检查，最近以系统的方式进行了研究，并且已知在三种不同的语义（基于州基于痕迹的，基于树和树的语义）下是可决定的。在这里，我们专注于基于痕量的语义，其中主要语义实体是给定的Kripke结构的无限执行路径（痕迹），假设在命题估值中另外具有同质性。我们引入了HS在痕迹上的定量扩展，称为差异HS（DHS），允许一个人在间隔长度（持续时间）之间的差异上表达时间限制。某些模式的定量扩展会立即导致不可证明性，因此，我们通过考虑严格的DHS句法片段来研究模型检查和满足性问题的可定性边界。特别是，我们确定了DHS的最大可决定性片段DHSS，此外，该片段的考虑问题至少是2个expspace-Hard。此外，通过利用线性时间混合逻辑上的新结果，我们表明，对于DHSS的同样表达片段，问题是Expass-Complete。最后，我们通过新型混合逻辑的单变量片段在痕迹上提供了HS的特征。
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.
