MOVES Seminar, 28 Jan 2010, 10:00

Stefan Herting

 

 

An Equivalence and Minimization Algorithm for CTMCs

 

 We present Markovian testing minimization equivalence (MTME) as an
alternative to bisimulation for state space minimization of CTMCs. MTME
contains bisimulation and thus always provides at least the state space
reduction of bisimulation. However it does not preserve as many
properties. We show that timed reachability is preserved by MTME.
MTME is based on Markovian testing equivalence (MTE) presented by Marco
Bernardo in 2007. MTE is originally defined on the sequential Markovian
process calculus and we also translate it to CTMCs.
Furthermore we construct an algorithm for the computation of MTME. It is
able to reduce the state space by up to another 40 percent compared to
bisimulation.