salle A. Turing CE4
11 June 2013 - 14h30
Of Markov Decision Processes and Airborne Collisions
by Christian von Essen from Verimag
Abstract: Airspace collision avoidance systems have a long history. The several revisions
of TCAS (Traffic Collision Avoidance System) have been mandatory on medium
and large airplanes for decades.
For the next generation of TCAS (called ACAS-X), developed by MIT Licoln Labs,
quantitative synthesis techniques are employed.
In this talk, we will present this system from the perspective of Model
Checking. We will present several questions that have not been addressed so
far. We will show how we can tackle them with techniques based on
Probabilistic Model Checking, and how we can improve the synthesis.
