NoDI seminar

From Reasoning with Constraints to Mining Constraints: Multi-Objective Parameter Fitting in Parametric Probabilistic Hybrid Automata

Martin Fränzle 16:00, November 27, 2014 321 Main Building, Beihang University

Abstract: Technical systems interacting with (parts of) the real world can be modelled elegantly using probabilistic hybrid automata (PHA). Parametric probabilistic hybrid automata are dynamical systems featuring hybrid discrete-continuous state dynamics and parametric probabilistic branching, thereby extending PHA by capturing a family of PHA in a single model. Such systems have a broad range of application from controller synthesis to network protocols. In our talk, we presented a novel method to synthesize parameter instances (if such exist) of such models that satisfy a multi-objective bounded horizon specification over expected rewards. Our method combines three distinct techniques: (1.) statistical model checking of a model instance devoid of parameters, (2.) a symbolic version of importance sampling yielding an arithmetic constraint reflecting the parameter dependence of the expected rewards, and (3.) SAT-modulo-theory (SMT) solving applied to that constraint for finding a feasible parameter instance consistent with the multi-objective design goal modulo sampling effects. Using a check-and-refine approach enhancing the constraint based on counterexamples, we are able to provide strong statistical guarantees on feasibility of the synthesized parameter instance.

(Joint Work with Alessandro Abate, Sebastian Gerwinn, Joost-Pieter Katoen, Paul Kröger)

Poster Slides Photos