Constructive Hybrid Games

被引：4
作者：
Bohrer, Rose [1 ]
Platzer, Andre [1 ,2 ]
机构：
[1] Carnegie Mellon Univ, Comp Sci Dept, Pittsburgh, PA USA
[2] Tech Univ Munich, Fak Informat, Munich, Germany
来源：
AUTOMATED REASONING, PT I | 2020年 / 12166卷
关键词：
Game logic; Constructive logic; Hybrid games; Dependent types; DYNAMIC LOGIC; CALCULUS;
D O I：
10.1007/978-3-030-51074-9_26
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Hybrid games combine discrete, continuous, and adversarial dynamics. Differential game logic (dGL) enables proving (classical) existence of winning strategies. We introduce constructive differential game logic (CdGL) for hybrid games, where proofs that a player can win the game correspond to computable winning strategies. This constitutes the logical foundation for synthesis of correct control and monitoring code for safety-critical cyber-physical systems. Our contributions include novel semantics as well as soundness and consistency.
引用
收藏
页码：454 / 473
页数：20
相关论文
共 59 条
[1]  
Abramsky S, 2000, INFORM COMPUT, V163, P409, DOI [10.1006/inco.2000.2930, 10.1006/inco2000.2930]
[2]   Alternating-time temporal logic [J].
Alur, R ;
Henzinger, TA ;
Kupferman, O .
JOURNAL OF THE ACM, 2002, 49 (05) :672-713
[3]  
[Anonymous], 1976, FOCS, DOI DOI 10.1109/SFCS.1976.27
[4]  
[Anonymous], 2005, AAMAS
[5]  
[Anonymous], 2010, EMSOFT
[6]  
Bishop E., 1967, Foundations of Constructive Analysis
[7]  
Bohrer B, 2020, Arxiv, DOI arXiv:2002.02536
[8]   Constructive Game Logic [J].
Bohrer, Brandon ;
Platzer, Andre .
PROGRAMMING LANGUAGES AND SYSTEMS ( ESOP 2020): 29TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2020, 12075 :84-111
[9]   dLι: Definite Descriptions in Differential Dynamic Logic [J].
Bohrer, Brandon ;
Fernandez, Manuel ;
Platzer, Andre .
AUTOMATED DEDUCTION, CADE 27, 2019, 11716 :94-110
[10]  
Bohrer B, 2018, ACM SIGPLAN NOTICES, V53, P617, DOI [10.1145/3192366.3192406, 10.1145/3296979.3192406]
123456