Relational Differential Dynamic Logic

被引：2

作者：

Kolcak, Juraj ^{[1
,2
]}

Dubut, Jeremy ^{[3
,4
]}

Hasuo, Ichiro ^{[3
,5
]}

Katsumata, Shin-ya ^{[3
]}

Sprunger, David ^{[3
]}

Yamada, Akihisa ^{[3
]}

机构：

[1] Univ Paris Saclay, CNRS, LSV, Cachan, France

[2] Univ Paris Saclay, ENS Paris Saclay, Cachan, France

[3] Natl Inst Informat, Tokyo, Japan

[4] Japanese French Lab Informat, CNRS IRL 3527, Tokyo, Japan

[5] Grad Univ Adv Studies SOKENDAI, Tokyo, Japan

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2020 | 2020年 / 12078卷

关键词：

hybrid system; cyber-physical system; formal verification; theorem proving; dynamic logic;

D O I：

10.1007/978-3-030-45190-5_11

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In the field of quality assurance of hybrid systems, Platzer's differential dynamic logic (dL) is widely recognized as a deductive verification method with solid mathematical foundations and sophisticated tool support. Motivated by case studies provided by our industry partner, we study a relational extension of dL, aiming to formally prove statements such as "an earlier engagement of the emergency brake yields a smaller collision speed." A main technical challenge is to combine two dynamics, so that the powerful inference rules of dL (such as the differential invariant rules) can be applied to such relational reasoning, yet in such a way that we relate two different time points. Our contributions are a semantical theory of time stretching, and the resulting synchronization rule that expresses time stretching by the syntactic operation of Lie derivative. We implemented this rule as an extension of KeYmaera X, by which we successfully verified relational properties of a few models taken from the automotive domain.

引用

页码：191 / 208

页数：18

共 50 条

[31] Logic synthesis technique for high speed differential dynamic logic with asymmetric slope transition
Morimoto, M
Tanaka, Y
Nagata, M
Taki, K
IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2005, E88A (12) : 3324 - 3331
[32] DESIGN AND APPLICATION OF PIPELINED DYNAMIC CMOS TERNARY LOGIC AND SIMPLE TERNARY DIFFERENTIAL LOGIC
WU, CY
HUANG, HY
IEEE JOURNAL OF SOLID-STATE CIRCUITS, 1993, 28 (08) : 895 - 906
[33] The relational logic of moral inference
Crockett, Molly J.
Everett, Jim A. C.
Gill, Maureen
Siegel, Jenifer Z.
ADVANCES IN EXPERIMENTAL SOCIAL PSYCHOLOGY, VOL 64, 2021, 64 : 1 - 64
[34] Relational Concepts and the Logic of Reciprocity
Winter, Yoad
LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, WOLLIC 2011, 2011, 6642 : 5 - 5
[35] RELATIONAL PARAMETRICITY AND SEPARATION LOGIC
Birkedal, Lars
Yang, Hongseok
LOGICAL METHODS IN COMPUTER SCIENCE, 2008, 4 (02)
[36] The Description Logic for Relational Databases
Ma Yue
Shen Yuming
Sui Yuefei
Cao Cungen
INTELLIGENT INFORMATION PROCESSING V, 2010, 340 : 64 - 71
[37] Quantum Relational Hoare Logic
Unruh, Dominique
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2019, 3 (POPL):
[38] A RELATIONAL ALGEBRA FOR PROPOSITIONAL LOGIC
BLANNING, RW
DECISION SUPPORT SYSTEMS, 1994, 11 (02) : 211 - 218
[39] Relational pararnetricity and separation logic
Birkedal, Lars
Yang, Hongseok
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2007, 4423 : 93 - +
[40] Dependable Reinforcement Learning via Timed Differential Dynamic Logic
Wang, Runhao
Zhang, Yuhong
Sun, Haiying
Liu, Jing
26TH IEEE SYMPOSIUM ON COMPUTERS AND COMMUNICATIONS (IEEE ISCC 2021), 2021,

← 1 2 3 4 5 →