Sep 15, 2015: Thomas Neele: Symbolic bisimulation minimisation in IscasMC

September 15, 2015Symbolic bisimulation minimisation in IscasMC
Room: HB 2AThomas Neele

The presentation is about the research I performed during my internship
in Beijing, China. We investigated the eff
ectiveness of symbolic bisimulation
minimisation (lumping) for probabilistic model checking. The aim is to reduce the
time required to perform model checking by reducing the size of the model.
The approach employs BDDs and signature-based partition refi
nement. We
present an implementation of lumping for discrete and continuous
time Markov chains and also for probabilistic automata. The algorithms are
integrated into IscasMC, a probabilistic model checker written in Java. The
benchmarks we performed show that symbolic lumping can be eff
ective, but
certainly not for all models.
We also integrated several BDD packages into IscasMC. The performance of
 these packages is analysed in a paper that was submitted to SETTA 2015