Synthesis from hyperproperties
Synthesis from hyperproperties
复制标题
DOI：
10.1007/s00236-019-00358-2
复制
发表时间：
2020-04-01
期刊：
影响因子：
0.6
通讯作者：
Tentrup, Leander
中科院分区：
文献类型：
--
作者：
Finkbeiner, Bernd;Hahn, Christopher;Tentrup, Leander
我们研究了作为时间逻辑超ltl的公式的超代理的反应性合成问题。 HyperProperties将跟踪属性（即痕迹集）概括为一组痕迹。典型的示例是信息流策略，例如非干预，它们规定没有敏感数据必须泄漏到公共领域。此类属性不能用标准线性或分支时间时间逻辑（例如LTL，CTL或CTL*\ DocumentClass [12PT]）表示。此外，HyperLTL涵盖了LTL可靠性问题的许多经典扩展，包括在不完整的信息下可实现的性，分布式合成和耐断层耐受性的合成。我们表明，尽管对于完整的超级LTL而言，综合问题是不可决定的，但对于存在的*\ documentClass [12pt]，片段仍然是可决定的。除了这些碎片之外，合成问题立即变得不可确定。对于通用超级LTL，我们提出了一个半决定程序，该程序将实现和反例构建到给定的界限。我们报告了通过实施原型实施获得的令人鼓舞的实验结果，该示例规格具有对称响应，保密和信息流量等超代理。
We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to sets of sets of traces. Typical examples are information-flow policies like noninterference, which stipulate that no sensitive data must leak into the public domain. Such properties cannot be expressed in standard linear or branching-time temporal logics like LTL, CTL, or CTL*\documentclass[12pt]. Furthermore, HyperLTL subsumes many classical extensions of the LTL realizability problem, including realizability under incomplete information, distributed synthesis, and fault-tolerant synthesis. We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the there exists*\documentclass[12pt], fragments. Beyond these fragments, the synthesis problem immediately becomes undecidable. For universal HyperLTL, we present a semi-decision procedure that constructs implementations and counterexamples up to a given bound. We report encouraging experimental results obtained with a prototype implementation on example specifications with hyperproperties like symmetric responses, secrecy, and information flow.