Differential game logic
From MaRDI portal
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.
Recommendations
Cites work
- A Functional calculus of first order based on strict implication
- A programming language for the inductive sets, and applications
- A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games
- A unified framework for hybrid control: model and optimal control theory
- A uniform substitution calculus for differential dynamic logic
- Alternating-time temporal logic
- An application of games to the completeness problem for formalized theories
- Axiomatic Definitions of Programming Languages
- Backward induction and common knowledge of rationality
- Borel determinacy
- Complete axiomatization and decidability of alternating-time temporal logic
- Conflict resolution for air traffic management: a study in multiagent hybrid systems
- Diamond formulas: A fragment of dynamic logic with recursively enumerable validity problem
- Differential dynamic logic for hybrid systems
- Differential Games Through Viability Theory: Old and Recent Results
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Elementary induction on abstract structures
- Game logic -- an overview
- Game logic is strong enough for parity games
- Game Quantification Patterns
- Grammar Analysis and Parsing by Abstract Interpretation
- Higher set theory and mathematical practice
- scientific article; zbMATH DE number 1701362 (Why is no real title available?)
- scientific article; zbMATH DE number 3122413 (Why is no real title available?)
- scientific article; zbMATH DE number 3880483 (Why is no real title available?)
- scientific article; zbMATH DE number 1183917 (Why is no real title available?)
- scientific article; zbMATH DE number 3670430 (Why is no real title available?)
- scientific article; zbMATH DE number 1263213 (Why is no real title available?)
- scientific article; zbMATH DE number 1361131 (Why is no real title available?)
- scientific article; zbMATH DE number 617141 (Why is no real title available?)
- scientific article; zbMATH DE number 1157649 (Why is no real title available?)
- scientific article; zbMATH DE number 1556014 (Why is no real title available?)
- scientific article; zbMATH DE number 2163583 (Why is no real title available?)
- scientific article; zbMATH DE number 755666 (Why is no real title available?)
- scientific article; zbMATH DE number 6456199 (Why is no real title available?)
- scientific article; zbMATH DE number 3078993 (Why is no real title available?)
- scientific article; zbMATH DE number 3106184 (Why is no real title available?)
- Logical analysis of hybrid systems. Proving theorems for complex dynamics.
- Logics of dynamical systems
- McNaughton games and extracting strategies for concurrent programs
- Noncooperative differential games
- O-minimal hybrid reachability games
- On the Completeness of Dynamic Logic
- On the Expressiveness and Complexity of ATL
- On the Reachability Problem for Uncertain Hybrid Systems
- Playing Hybrid Games with KeYmaera
- Program invariants as fixedpoints
- Results on the propositional \(\mu\)-calculus
- Soundness and Completeness of an Axiom System for Program Verification
- Specifications for decidable hybrid games
- Stochastic differential dynamic logic for stochastic hybrid programs
- Strategy logic
- The algorithmic analysis of hybrid systems
- The calculus of constructions
- The Complete Proof Theory of Hybrid Systems
- The Game Quantifier
- The structure of differential invariants and differential cut elimination
- The variable hierarchy of the \(\mu\)-calculus is strict
- Timed Parity Games: Complexity and Robustness
- Topology and descriptive set theory
- What makes \textsc{Atl}* decidable? A decidable fragment of strategy logic
- Zero-sum differential games involving hybrid controls
Cited in
(16)- A complete uniform substitution calculus for differential dynamic logic
- Uniform substitution for differential game logic
- Constructive hybrid games
- Uniform substitution at one Fell swoop
- A uniform substitution calculus for differential dynamic logic
- KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
- Constructive game logic
- scientific article; zbMATH DE number 7064064 (Why is no real title available?)
- Sufficient Conditions for Optimality and Asymptotic Stability in Two-Player Zero-Sum Hybrid Games
- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- Refining constructive hybrid games
- Semi-competitive differential game logic
- Trigger-based discretization of hybrid games for autonomous cyber-physical systems
- Embedding differential dynamic logic in PVS
- Complete game logic with sabotage
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)
