Differential Game Logic for Hybrid Games

Author(s):  
Andre Platzer
2015 ◽  
Vol 17 (1) ◽  
pp. 1-51 ◽  
Author(s):  
André Platzer
Keyword(s):  

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Brandon Bohrer ◽  
André Platzer

Many cyber-physical systems (CPS) are safety-critical, so it is important to formally verify them, e.g. in formal logics that show a model’s correctness specification always holds. Constructive Differential Game Logic ( CdGL ) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proof-checking tool. We introduce Kaisar , the first language and tool for CdGL proofs, which until now could only be written by hand with a low-level proof calculus. Kaisar’s structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and high-level stateful reasoning. Kaisar exploits CdGL ’s constructivity and refinement relations to build proofs around models of game strategies. The evaluation reproduces and extends existing case studies on 1D and 2D driving. Proof metrics are compared and reported experiences are discussed for the original studies and their reproductions.


2019 ◽  
Vol 38 ◽  
pp. 43-54
Author(s):  
Gafurjan Ibragimov ◽  
Usman Waziri ◽  
Idham Arif Alias ◽  
Zarina Bibi Ibrahim

2020 ◽  
Vol 81 (11) ◽  
pp. 2108-2131
Author(s):  
V. I. Zhukovskiy ◽  
A. S. Gorbatov ◽  
K. N. Kudryavtsev

Sign in / Sign up

Export Citation Format

Share Document