Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism

DOI10.2168/LMCS-12(3:6)2016zbMath1445.03037arXiv1606.09110MaRDI QIDQ2974777

Konstantinos Mamouras

Publication date: 11 April 2017

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1606.09110

zbMATH Keywords

program synthesisHoare logicsafety gamesprogram schemesangelic and demonic nondeterminismdual nondeterminism

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items (4)

Constructive Game Logic ⋮ Semantic Foundations for Deterministic Dataflow and Stream Processing ⋮ Equational Theories of Abnormal Termination Based on Kleene Algebra ⋮ Constructive hybrid games

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Modelling angelic and demonic nondeterminism with multirelations
• Generic weakest precondition semantics from monads enriched with order
• Duality in specification languages: A lattice-theoretical approach
• Strategy logic
• Ten years of Hoare's logic: A survey. II: Nondeterminism
• Combining angels, demons and miracles in program specifications
• Propositional dynamic logic of regular programs
• A completeness theorem for Kleene algebras and the algebra of regular events
• Program schemes, recursion schemes, and formal languages
• Game logic -- an overview
• On the completeness of propositional Hoare logic
• On formalised computer programs
• Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism
• Alternating-time temporal logic
• Ten Years of Hoare's Logic: A Survey—Part I
• Alternation
• Guarded commands, nondeterminacy and formal derivation of programs
• Soundness and Completeness of an Axiom System for Program Verification
• A Modal Logic for Coalitional Power in Games
• Refinement Calculus
• On the synthesis of strategies in infinite games
• On the Hoare theory of monadic recursion schemes
• The algebra of multirelations
• Kleene Algebra with Equations
• A Relatively Complete Generic Hoare Logic for Order-Enriched Effects
• The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes
• Mathematics of Program Construction
• An axiomatic basis for computer programming
• On Ianov's Program Schemata
• On Hoare logic and Kleene algebra with tests
• A note on the complexity of propositional Hoare logic
• Theory and Applications of Relational Structures as Knowledge Instruments

This page was built for publication: Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism