Group colloquium: Parameter Synthesis Algorithms for Parametric Interval Markov Chains

When: Sept. 27, 2018, 15:45-16:45

Where: Cubicus B209

Who: Jaco van de Pol

Markov Chains are used to quantify the uncertainties in system modelling by probabilities.
However, one seldom knows the precise value of probabilistic parameters. To this end,
Parametric Markov Chains allow symbolic parameters, while Interval Markov Chains
specify intervals for the parameters. Both mechanisms are combined in so-called PIMCs.

This talk will consider the consistency problem for Parametric Interval Markov Chains. 
In particular, we introduce a co-inductive definition of consistency, which improves and 
simplifies the previous inductive definition considerably. The equivalence of the inductive 
and co-inductive definitions has been formally proved in the interactive theorem prover 
PVS.

These definitions lead to forward and backward algorithms, respectively, for synthesizing
an expression for all parameters for which a given PIMC is consistent. We also improve
the algorithms for consistency checking for IMCs. The algorithms are evaluated on a 
prototype implementation based on Constraint Logic Program and the PARMA library 
for convex polyhedra.