Computer Science Speaking Skills Talk

Tuesday, December 11, 2018 - 12:00pm to 1:00pm


Traffic21 Classroom 6501 Gates Hillman Centers



Designing and Verifying Belief-Aware Cyber Physical Systems

Speaker: João Martins

Location: GHC 6501

Designing and Verifying Belief-Aware Cyber Physical Systems

In this talk, we will argue, by means of the crash of Air France Flight 447 in June 1st 2009, that cyber physical systems such as an airplane cannot in good conscience be considered safe until their design and verification processes fully integrate the notion of belief.

Indeed, counterfactual beliefs and the absence of belief (i.e. unawareness) were the primary cause of this tragedy.

We will present Dynamic Doxastic Differential Dynamic Logic (d4L) as a tool capable of addressing the challenges of changing beliefs in a changing world, and thus, the existing gap in practical CPS safety.

We will show how d4L can be used to reason simultaneously about 2) the continuous-time physical evolution of CPSs, and 2) their controller's beliefs about the world, incorporating such phenomena as incomplete information, sensor noise, and counterfactual beliefs into CPS design.

The applicability of d4L is assured by proving the safety of an airplane that keeps itself at a safe altitude based on a noisy altimeter, using a sound d4L sequent calculus. This illustrates how d4L's belief-triggered controllers are more aware and better capable of making the decisions that keep CPSs safe.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.

For More Information, Contact:


Speaking Skills