Abstract
Cyber-physical systems (CPS), such as airplanes, operate based on sensor and communication data, i.e. on potentially noisy or erroneous beliefs about the world. Realistic CPS models must therefore incorporate the notion of beliefs if they are to provide safety guarantees in practice as well as in theory. To fundamentally address this challenge, this paper introduces a first-principles framework for reasoning about CPS models where control decisions are explicitly driven by controller beliefs arrived at through observation and reasoning. We extend the differential dynamic logic Open image in new window for CPS dynamics with belief modalities, and a learning operator for belief change. This new dynamic doxastic differential dynamic logic Open image in new window does due justice to the challenges of CPS verification by having (1) real arithmetic for describing the world and beliefs about the world; (2) continuous and discrete world change; (3) discrete belief change by means of the learning operator. We develop a sound sequent calculus for Open image in new window , which enables us to illustrate the applicability of Open image in new window by proving the safety of a simplified belief-triggered controller for an airplane.
Original language | English |
---|---|
Title of host publication | Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2019 |
Editors | S. Cerrito, A. Popescu |
Place of Publication | Cham |
Publisher | Springer |
Pages | 428-445 |
Number of pages | 18 |
ISBN (Electronic) | 978-3-030-29026-9 |
ISBN (Print) | 978-3-030-29025-2 |
DOIs | |
Publication status | Published - 2019 |
Event | International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - Duration: 3 Sep 2019 → 5 Nov 2019 Conference number: 28 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Publisher | Springer |
Volume | 11714 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | International Conference on Automated Reasoning with Analytic Tableaux and Related Methods |
---|---|
Abbreviated title | TABLEAUX 2019 |
Period | 3/09/19 → 5/11/19 |
Keywords
- Differential dynamic logic
- Dynamic epistemic logic
- Sequent calculus
- Hybrid systems
- Cyber-physical systems