Differential game logic
From MaRDI portal
Publication:5277902
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
- 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?)
- 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 Games Through Viability Theory: Old and Recent Results
- Differential dynamic logic for hybrid systems
- Differential-algebraic Dynamic Logic for Differential-algebraic Programs
- Elementary induction on abstract structures
- Game Quantification Patterns
- Game logic -- an overview
- Game logic is strong enough for parity games
- Grammar Analysis and Parsing by Abstract Interpretation
- Higher set theory and mathematical practice
- 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 Complete Proof Theory of Hybrid Systems
- The Game Quantifier
- The algorithmic analysis of hybrid systems
- The calculus of constructions
- 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
(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
- scientific article; zbMATH DE number 7064064 (Why is no real title available?)
- 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
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)
