Synthesizing Reactive Systems from Hyperproperties
Synthesizing Reactive Systems from Hyperproperties
复制标题
从超性质合成反应系统
DOI：
10.1007/978-3-319-96145-3_16
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Leander Tentrup
中科院分区：
文献类型：
--
作者：
B. Finkbeiner;Christopher Hahn;Philip Lukert;Marvin Stenger;Leander Tentrup
我们研究作为时态逻辑HyperLTL公式给出的超属性的反应综合问题。超属性将踪迹属性(即踪迹集合)概括为踪迹集合的集合。典型的例子是不干涉等信息流政策，它规定任何敏感数据都不能泄露到公共领域。这样的属性不能用LTL、CTL或CTL(^*)这样的标准线性或分支时间时态逻辑来表示。我们证明了，虽然合成问题对于完全超LTL是不可判定的，但对于(全部^1)、(全部^1)和(线性全部^*)片段，合成问题仍然是可判定的。除了这些片断，合成问题立即变得无法决定。对于通用的超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\(^*\). We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the \(\exists ^*\), \(\exists ^*\forall ^1\), and the \( linear \;\forall ^*\) 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.
DOI：
10.1007/978-3-642-27940-9_12
发表时间：
2012-01
期刊：
--
影响因子：
--
作者：
Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl
通讯作者：
Rayna Dimitrova;B. Finkbeiner;Máté Kovács;M. Rabe;H. Seidl