Differential game logic

DOI10.1145/2817824zbMATH Open1367.68201arXiv1408.1980OpenAlexW3125808851WikidataQ130844047 ScholiaQ130844047MaRDI QIDQ5277902FDOQ5277902

Authors: André Platzer 

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: Differential game logic (dGL) is a logic for specifying and verifying properties of hybrid games, i.e. games that combine discrete, continuous, and adversarial dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players with different objectives. The logic dGL can be used to study the existence of winning strategies for such hybrid games, i.e. ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e. from each state, one player has a winning strategy, yet computing their winning regions may take transfinitely many steps. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic. Separating axioms are identified that distinguish hybrid games from hybrid systems. Finally, dGL is proved to be strictly more expressive than the corresponding logic of hybrid systems by characterizing the expressiveness of both.

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

Recommendations

• Differential Hybrid Games
• Playing Hybrid Games with KeYmaera
• An introduction to game logic
• Logics of dynamical systems
• Game logic -- an overview

zbMATH Keywords

axiomatizationexpressivenessgame logichybrid games

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Games involving topology, set theory, or logic (91A44) Logic in computer science (03B70)

Cites Work

• Title not available (Why is that?)
• Differential dynamic logic for hybrid systems
• Alternating-time temporal logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
• Elementary induction on abstract structures
• Borel determinacy
• Backward induction and common knowledge of rationality
• Title not available (Why is that?)
• Title not available (Why is that?)
• A unified framework for hybrid control: model and optimal control theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Functional calculus of first order based on strict implication
• Title not available (Why is that?)
• Soundness and Completeness of an Axiom System for Program Verification
• Conflict resolution for air traffic management: a study in multiagent hybrid systems
• The algorithmic analysis of hybrid systems
• Results on the propositional \(\mu\)-calculus
• An application of games to the completeness problem for formalized theories
• Grammar Analysis and Parsing by Abstract Interpretation
• What makes \textsc{Atl}* decidable? A decidable fragment of strategy logic
• Noncooperative differential games
• The calculus of constructions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Strategy logic
• Title not available (Why is that?)
• O-minimal hybrid reachability games
• Timed Parity Games: Complexity and Robustness
• Topology and descriptive set theory
• Game logic -- an overview
• Higher set theory and mathematical practice
• Differential Games Through Viability Theory: Old and Recent Results
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• On the Reachability Problem for Uncertain Hybrid Systems
• Program invariants as fixedpoints
• A programming language for the inductive sets, and applications
• Complete axiomatization and decidability of alternating-time temporal logic
• Game logic is strong enough for parity games
• Specifications for decidable hybrid games
• On the Expressiveness and Complexity of ATL
• Logics of dynamical systems
• The Complete Proof Theory of Hybrid Systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• A uniform substitution calculus for differential dynamic logic
• The structure of differential invariants and differential cut elimination
• Title not available (Why is that?)
• The variable hierarchy of the \(\mu\)-calculus is strict
• Axiomatic Definitions of Programming Languages
• Title not available (Why is that?)
• The Game Quantifier
• McNaughton games and extracting strategies for concurrent programs
• Title not available (Why is that?)
• Zero-sum differential games involving hybrid controls
• Playing Hybrid Games with KeYmaera
• Stochastic differential dynamic logic for stochastic hybrid programs
• Diamond formulas: A fragment of dynamic logic with recursively enumerable validity problem
• Title not available (Why is that?)
• Game Quantification Patterns
• On the Completeness of Dynamic Logic

Cited In (11)

• Constructive game logic
• A uniform substitution calculus for differential dynamic logic
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• A complete uniform substitution calculus for differential dynamic logic
• Title not available (Why is that?)
• Uniform substitution for differential game logic
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Uniform substitution at one Fell swoop
• Sufficient Conditions for Optimality and Asymptotic Stability in Two-Player Zero-Sum Hybrid Games
• Constructive hybrid games

Uses Software

• KeYmaera
• Differential_Game_Logic

This page was built for publication: Differential game logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277902)