Probabilistic Model Checking of Randomized Java Code

Java 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.