Timed hyperproperties
Timed hyperproperties
复制标题
DOI：
10.1016/j.ic.2020.104639
复制
发表时间：
2020-11
期刊：
影响因子：
--
通讯作者：
Hsi-Ming Ho;Ruoyu Zhou;Timothy M. Jones
中科院分区：
文献类型：
--
作者：
Hsi-Ming Ho;Ruoyu Zhou;Timothy M. Jones
我们研究了用HyperLTL （HyperLTL的一个时间扩展）指定的时间超属性的可满足性和模型检验问题。虽然可满足性问题可以与HyperLTL类似地解决，但我们表明，HyperMITL的模型检查问题即使在允许非常有限的时间约束的情况下也是不可确定的，除非规范是无变更的。从积极的方面来看，我们证明了在某些语义限制下，使用量词交替进行HyperMITL模型检查是可能的。作为一种中间工具，我们给出了Wilke的相对距离（L d↔）一元逻辑的“异步”解释，并表明它表征了由具有无声过渡的时间自动机识别的时间语言。
We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMITL, a timed extension of HyperLTL. While the satisfiability problem can be solved similarly as for HyperLTL, we show that the model-checking problem for HyperMITL, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMITL with quantifier alternations is possible under certain semantic restrictions. As an intermediate tool, we give an ‘asynchronous’ interpretation of Wilke's monadic logic of relative distance (L d↔) and show that it characterises timed languages recognised by timed automata with silent transitions.