Multi-Objective Parameter Synthesis in Probabilistic Hybrid Systems

Technical systems interacting with the real world can be modelled elegantly using probabilistic hybrid automata (PHA). Parametric probabilistic hybrid automata are dynamical systems featuring hybrid discrete-continuous dynamics and parametric probabilistic branching, thereby generalizing PHA by capturing a family of PHA withina single model. Such system models have a broad range of applications, from control systems over network protocols to biological components. We present a novel method to synthesize parameter instances (if such exist)of PHA satisfying a multi-objective bounded horizon specification overexpected rewards.  Our approach combines three techniques: statistical model checking of model instantiations, a symbolic version of importance sampling to handle the parametric dependence, and SAT-modulo-theory solving for finding feasible parameter instances in a multi-objective setting.  The method provides statistical guarantees on the synthesized parameter instances. To illustrate the practical feasibility of the approach, we present experiments showing the potential benefit of the scheme compared to a naive parameter exploration approach.

Joint work with Alessandro Abate, Sebastian Gerwinn, Joost-Pieter Katoen, and Paul Kroeger.

Short biography

Martin Fränzle is professor at the Department of Computing Science  at Oldenburg University, Germany, where he teaches formal methods and hybrid discrete-continuous systems, as well as related subjects. His research interests are in modelling, verification, and synthesis of reactive, real-time, and hybrid systems, as well as applications in advanced driver assistance, autonomous driving, and power networks.