使用天使和恶魔非决定论的霍尔逻辑的策略综合
Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism
摘要：
我们研究了霍尔逻辑的一个命题变体，它可以用于推理表现出天使和恶魔非决定论的程序。我们在一个未解释的环境中工作，其中原子动作的意义是使用某种形式的假设公理化地指定的。我们的逻辑形式主义是完全合成的，它包含了有限图上的安全游戏的非合成形式主义。我们提出了声音和完整的霍尔式演算，是有用的建立部分正确性断言，以及合成实现。利用运算模型研究了Hoare对偶不确定性理论的计算复杂性，证明了该理论在指数时间上是完备的.
英文摘要：
We study a propositional variant of Hoare logic that can be used for reasoning about programs that exhibit both angelic and demonic nondeterminism. We work in an uninterpreted setting, where the meaning of the atomic actions is specified axiomatically using hypotheses of a certain form. Our logical formalism is entirely compositional and it subsumes the non-compositional formalism of safety games on finite graphs. We present sound and complete Hoare-style calculi that are useful for establishing partial-correctness assertions, as well as for synthesizing implementations. The computational complexity of the Hoare theory of dual nondeterminism is investigated using operational models, and it is shown that the theory is complete for exponential time.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
