Hybrid UAM Model Checking

Principal Investigator: James Goppert

To analyze the complex concurrent interaction of aerial vehicles in the UAM system, we will employ model checking to verify logical properties in a finite state machine model. For example, if a no-fly zone is declared, all agents will leave the no-fly zone by a mandated deadline. Another example: Assuming random wind gusts of 20 knots, we will determine whether the planned UAM traffic can safely navigate without collision. We will verify the system using existing languages such as NuSMV50 and Spin51 by approximating the system as a Polyhedral-Invariant Hybrid Automaton (PIHA). Constructing a PIHA model allows verification of universal Computation Tree Logic (CTL) specifications. To construct a PIHA model, boundary certificates are not sufficient, since they do not compute a flow pipe. Flow pipes can be created through the creation of invariant sets around the reference trajectory and then sweeping the invariant set along it. Once flow pipes have been computed, the hybrid system can be converted to an approximate quotient transition system (AQTS) that can either over-approximate the reachable set of the system to prove safety or under-approximate it to prove reachability. The AQTS converts the hybrid model into a finite state machine that can be readily verified with existing model checkers.

Personnel

Students: Li-Yu Lin