Jul 12, 2016: Jaco van de Pol: Parametric Interval Markov Chains

July 12, 2016Parametric Interval Markov Chains
Room: HB 2BJaco van de Pol

Using Markov Chains is complicated, since the actual probabilistic values are often unknown. One way out is to specify intervals and allow any value in the interval. Another possibility is to allow parameters. We study the combination: intervals with parametric bounds.

We review the algorithm to check if a parametric Interval Markov Chain (pIMC) is consistent. The consistency problem resembles a two-player game. Our contributions are coinductive definitions and results for infinite pIMCs, shorter proofs (formalized in PVS), and slightly improved algorithms (in Prolog-CLP).