Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism

Abstract. 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 mean-ing of the atomic actions is specified axiomatically using hypotheses of a certain form. Our logical formalism is entirely compositional and it sub-sumes the non-compositional formalism of safety games on finite graphs. We present sound and complete Hoare-style (partial-correctness) calculi that are useful for establishing Hoare assertions, as well as for synthesiz-ing 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.