Ass.-Prof. Dr. Paolo Zuliani

Abstract:

I will give an overview of my recent work on verified probabilistic reachability for hybrid systems with uncertain parameters. Hybrid systems are mathematical models that combine discrete and continuous behaviour. They have been traditionally used for modelling and analysing cyber-physical systems, which feature digital computing modules interacting with a physical environment (e.g., insulin infusion pumps, car cruise control, etc.). Recently, hybrid systems have found application in modelling complex biological systems involving discrete modes and continuous-time behaviour. The probabilistic reachability problem essentially reduces to computing validated enclosures for reachability probabilities. I will present two approaches: one has high computational cost and provides absolute guarantees on the correctness of the answers, i.e., the computed enclosures are formally guaranteed to contain the reachability probabilities. The other approach combines rigorous and statistical reasoning, thereby yielding better scalability by trading absolute (formal) guarantees with statistical guarantees. I will exemplify both approaches with case studies from systems biology and cyber-physical systems.

This is joint work with my PhD student Fedor Shmarov.