The paper “Parameter Synthesis for Markov Models: Covering the Parameter Space” by Sebastian Junges (Nijmegen), Erika Abraham, Christian Hensel (Amazon), Nils Jansen (Nijmegen), Joost-Pieter Katoen, Tim Quatmann and Matthias Volk (Twente) has been accepted for publication in the journal Formal Methods in Systems Design.

The paper (85 pages) presents various analysis algorithms for parametric discrete-time Marko chains and Markov decision processes. We focus on three problems: (a) do all parameter values within a given region satisfy φ?, (b) which regions satisfy φ and which ones do not?, and (c) an approximate version of (b) focusing on covering a large fraction of all possible parameter values.