Bisimulation minimisation and probabilistic model checking

Kemna, Tim (2006) Bisimulation minimisation and probabilistic model checking.

[img]
Preview
PDF
367kB
Abstract:Probabilistic model checking is a technique for the verication of probabilistic systems. The size of the state space is a limiting factor for model checking. We used bisimulation minimisation to combat this problem. Bisimulation minimisation is a technique where the model under consideration is first minimised prior to the actual model checking. We also considered a technique where the model is minimised for a specic property, called formuladependent lumping. The minimisation algorithm has been implemented into the model checker MRMC. Using case studies, we empirically studied the eectiveness of bisimulation minimisation for probabilistic model checking. The probabilistic models we consider are discrete-time Markov chains and continuous-time Markov chains. Properties are expressed in the temporal logic PCTL or CSL. Our experiments showed that bisimulation minimisation can result into large state space reductions. Formula-dependent lumping can lead to even larger state space reductions. For several cases, minimising the original model plus checking the minimised model is faster than model checking the original model. We conclude that bisimulation minimisation is a good state space reduction technique.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:http://purl.utwente.nl/essays/57281
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page