Computer Science Thesis Proposal
- Gates Hillman Centers
- Traffic21 Classroom 6501
- JOAO G. MARTINS
- Ph.D. Student
- Computer Science Department
- Carnegie Mellon University
Changing Beliefs in a Changing World
\We find ourselves on the cusp of a revolution in the transportation industry, with an expectation for the impending widespread adoption of self-driving capabilities, promising faster and more efficient deliveries, more comfort and better bottom lines.
Critical to achieving this vision, however, is large scale deployment of vehicles with self-driving capabilities, or cyber-physical systems (CPSs), into roadways and airways already teeming with other human- and computer-controlled vehicles. This deployment cannot, and indeed should not be acceptable until the safety of the controllers in charge of new CPSs is credibly proven.Already several incidents, some fatal, cast a shadow of doubt onto the public's belief about whether heterogeneously controlled systems can safely function within the same environments.
While significant progress has been made in formally verifying the safety of CPS models, we argue that current models often do not accurately represent real systems because of an implicit assumption of perfect knowledge of the real-world. In reality, sensor noise and incomplete or even counterfactual beliefs create ample possibilities for controller decisions that lead to safety violations. We claim that the notion of belief can capture the real life phenomena of noisy observations and faulty human intuition, leading to appropriately informed decisions. A failure to take belief into account results in a critical gap between theoretical and practical safety of CPSs.
One such example, and inspiration for this thesis, is the crash of Air France Flight 447, in which the interaction between beliefs, control and physics led an aircraft with no actuator malfunctions from safety to tragedy in under four minutes.
We propose to address this safety-critical intersection by developing the technical underpinnings of a change towards belief-triggered controllers, where decisions are grounded in imperfect perceptions of the real world rather than the real world itself.
In this proposal, we develop a logic whose semantics are capable of adequately capturing the interleaved changes of both belief and world-state that characterize real-world CPSs: a logic for changing beliefs in a changing world.
We prove the soundness of a sequent calculus which captures the fundamental behaviors of doxastic change within the context of CPSs, and propose to generalize it to augment its applicability to more complex scenarios.
We further propose to conduct case studies of small scenarios exhibiting safety-violation symptoms similar to those of AF-447, or fragments of the AF-447 incident itself. The expected outcome of such case studies are formal safety proofs of revised belief-triggered controllers, built from state-triggered controllers whose flaws that led to safety violations on display in real scenarios. These revisions highlight safety-critical changes that can be adopted by legislative, regulation and training authorities to create better policies leading to a safer world.
Ultimately, this thesis proposal argues for the necessity of a paradigm shift in which belief becomes a first-class citizen of CPS design, verification and legislation processes, and provides the first technical steps on that long road.
André Platzer (Co-Chair)
João Leite (Co-Chair, UNL)
Wiebe van der Hoek (University of Liverpool)
Copy of Thesis Summary