一句话：提出一种命题 Hoare 逻辑，统一刻画天使/恶魔非确定性，支持部分正确性验证与策略合成，并证明其判定复杂度为 EXPTIME。
论文研究如何对同时包含天使非确定性（由实现者选择）与恶魔非确定性（由环境选择）的程序进行推理与合成。作者在无解释设定下工作，用特定形式的假设公理化原子动作，提出一种组合式的命题 Hoare 逻辑，其表达能力涵盖有限图上的安全性博弈这一非组合式形式。文章给出可靠且完备的 Hoare 风格演算，既可用于建立部分正确性断言，也可从规约合成实现与策略。借助操作模型分析该双重非确定性 Hoare 理论的计算复杂度，证明其判定问题为指数时间完备（EXPTIME-complete）。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Mamouras16,
title = {Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism},
author = {Konstantinos Mamouras},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 3},
year = {2017},
doi = {10.2168/lmcs-12(3:6)2016}
}