Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems

João G. Martins, André Platzer, João Leite

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

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 languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2019
EditorsS. Cerrito, A. Popescu
Place of PublicationCham
PublisherSpringer
Pages428-445
Number of pages18
ISBN (Electronic)978-3-030-29026-9
ISBN (Print)978-3-030-29025-2
DOIs
Publication statusPublished - 2019
EventInternational Conference on Automated Reasoning with Analytic Tableaux and Related Methods -
Duration: 3 Sep 20195 Nov 2019
Conference number: 28

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer
Volume11714
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Automated Reasoning with Analytic Tableaux and Related Methods
Abbreviated titleTABLEAUX 2019
Period3/09/195/11/19

Keywords

  • Differential dynamic logic
  • Dynamic epistemic logic
  • Sequent calculus
  • Hybrid systems
  • Cyber-physical systems

Fingerprint Dive into the research topics of 'Dynamic Doxastic Differential Dynamic Logic for Belief-Aware Cyber-Physical Systems'. Together they form a unique fingerprint.

Cite this