Jip Spel: Monotonicity in Parametric Markov Chains

 

Parametric Markov chains (pMCs) are an operational model to treat robustness against uncertainties. Jip Spel’s research focuses on two aspects: how to check whether the reachability probabilities in pMCs, or similar measures, are monotonic in (some of) the parameters?, and how can such monotonicity information be exploited to accelerate existing parameter synthesis approaches? As checking monotonicity is as hard as solving the parameter synthesis problem itself, Spel (in co-operation with UNRAVEL doctoral researcher Junges) developed a simple algorithm that efficiently checks a sufficient condition for monotonicity. This is done by constructing — only using the graph structure of the pMC and local transition probabilities — a pre-order on the states. This algorithm has been tightly integrated with parameter lifting, an existing synthesis algorithm so as to prove robustness, i.e., to find a parameter valuation that yields an ε-close upper bound on the maximal reachability probability of all pMC instantiations. Experiments show that monotonicity can be checked in various benchmarks and that almost-optimal synthesis is accelerated by up to two orders of magnitude. Spel is currently working on exploiting stochastic gradient descent algorithms for parameter synthesis (publication in progress), and is applying her techniques to the settings of parametric probabilistic graphical models and probabilistic timed automata.