van Breugel, FranckFatmi, Syyeda Aamina Zainab2021-07-062021-07-062020-092021-07-06http://hdl.handle.net/10315/38445Java PathFinder (JPF) and PRISM are the most popular model checkers for Java code and systems that exhibit random behaviour, respectively. JPF, in combination with its extension jpf-probabilistic, extracts the underlying Markov chain of randomized Java code. We developed a new extension of JPF, called jpf-label, which provides users with an easy way to label the states of this Markov chain. Furthermore, we implemented a converter that leads to the first model checking tool that can check probabilistic properties of randomized algorithms implemented in Java, by making it possible to use JPF in conjunction with PRISM. Probabilistic bisimilarity is a technique used to minimize the state space of a labelled Markov chain in order to combat the state space explosion. We implemented three known algorithms to compute probabilistic bisimilarity for labelled Markov chains. We boosted the performance of these algorithms by improving those areas of the code which are most frequently executed. Moreover, we compared the practical running time and memory consumption of these algorithms with PRISM's.Author owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.Computer scienceElectronic Thesis or Dissertation2021-07-06(probabilistic) model checkingJava PathFinderPRISMprobabilistic bisimilaritylabelled Markov chain