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 dL for CPS dynamics with belief modalities, and a learning operator for belief change. This new dynamic doxastic differential dynamic logic d⁴$L$ 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 d⁴$L$, which enables us to illustrate the applicability of d⁴$L$ by proving the safety of a simplified belief-triggered controller for an airplane.

49 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu