Joost-Pieter Katoen

 

Interactive Markov Chains: Theory and Practice

 

Abstract:

We consider a continuous-time stochastic model (called interactive
Markov chains (IMCs)) which allows interaction and concurrency in a
process-algebraic fashion.  We discuss notions of strong and weak
(bi)simulation and their congruence properties.  We show how
simulation pre-congruences provide the basis for compositional
abstraction where abstract models are a mixture of interval IMCs and
modal transition systems.

A key problem in model checking IMCs, in fact stochastic real-time
games, is computing maximal time-bounded reachability probabilities.
We show a discretisation approach to determine optimal timed
(measurable) policies, and report on some practical results.

Finally, we show that IMCs are the semantical backbone for
higher-level formalisms from various domains such as generalized
stochastic Petri nets (GSPNs) used in performance evaluation, dynamic
fault trees (DFTs) used in reliability and safety engineering, and
AADL, a standardised language in hardware/software co-design.