From (Non)deterministic to Probabilistic Verification

In our research on this project we propose a new approach to verification of the accurate functioning of ``safety critical systems''. The heart of the approach is to not verify that every run of the hybrid system satisfies certain safety or liveness parameters, rather to check that the properties are satisfied with a certain probability, given uncertainties of actuation and sensing. In this sense, this is a ``softening'' of the notion of verification and represents the rapproachment between stochastic control, Bayesian decision networks and soft computing that was mentioned above. Since the systems are safety critical, we will be interested in guarantees of performance which are high in the unfaulted mode and slightly lower in the faulted modes.

Design Mode Verification

Multi-agent systems like UCAV or aero engine test bed will need to have multiple modes of operation, including hover, take off, land, track, etc. It will be important to prove that control algorithms that switch between these modes based on high level commands and vision data do not cause the aircraft to enter unstable or unsafe states. Control algorithms need to be designed to not compromise safety, but allow for efficient functioning with multiple agents for wide area coverage.

Faulted Mode Verification

When there are faults or damage detected, multi-agent systems like the UCAV or aero engine will need to have fault detection and handling routines, which maintain integrity of the aircraft and safety with possible gradual degradation in the performance of the functioning of the system. Fault handing routines have to be proven to work, with high probability in both detecting the fault and then providing the sequence of mode changes as well as tactical and possibly strategic redeployment so as to make for reliable operation.

Probabilistic Verification

In the conceptual underpinings of the research, we will attempt a rapproachment between Markov decision networks, AI based Bayesian decision networks to come up with a ``soft'' version of verification for hybrid systems. Conceptually this method will be like the change in computational complexity theory between studying worst case behavior of an algorithm and the mean behavior of the algorithm.