论文标题
无限单词的参数间隔时间逻辑
Parametric Interval Temporal Logic over Infinite Words
论文作者
论文摘要
最近对Halpern和Shoham的间隔时间逻辑HS进行了模型检查，最近以系统的方式进行了研究，并且已知在三种不同的语义下是可决定的。 在这里，我们关注基于痕量的语义，其中给定（有限）Kripke结构的无限执行路径（痕迹）是主要的语义实体。在这种情况下，迹线的每个有限插条都被解释为一个间隔，并且仅当其在每个组件状态（同质性假设）上时，命题才能在一个间隔上保持一定间隔。在本文中，我们引入了HS在痕迹上的定量扩展，称为参数HS（PHS）。新颖的逻辑允许在间隔的持续时间（长度）上表达参数时序约束。我们表明，检查Kripke结构满足PHS公式（模型检查）的参数估值的存在，或者PHS公式可以在同质性假设（满意度）下作为模型作为模型。 此外，我们确定了pHS的片段，这些pHs属于参数LTL，并显示出模型检查和可满足性是expspace-complete。
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.
