jpf-probabilistic: an extension of Java PathFinder to model check randomized Java code

jpf-probabilistic is a basic extension of Java PathFinder (JPF) to model check randomized algorithms implemented in Java. It allows us to express probabilistic choices (as can be found in, for example, randomized algorithms) in Java code so that JPF recognizes them. As we will discuss below, the probabilistic choices in the Java code need to be implemented in a specific way. Such code can be model checked by JPF in the usual way. As we will show below, the extension jpf-probabilistic also allows us to print the Markov chain underlying the randomized code. Furthermore, the extension provides a new search strategy that randomly choses the state to explore. The chance that a state is chosen is proportional to the probability of the path along which the state is discovered during the search.

In order to exploit jpf-probabilistic, the randomized choices in the Java code need to be expressed by means of the method make of the class Choice, which is part of the package probabilistic. For example, if

double[] p = { 0.4, 0.6 };

Choice.make(p); 

For convenience, the classes Coin, Die and UniformChoice, which are all part of the package probabilistic as well, can also be used to implement randomized algorithms in Java. For example, the class Coin has the method flip which returns either 0 or 1, each with probability 0.5.

Let us consider a simple example. Knuth and Yao [1] have shown how to implement a die by means of a coin. Their algorithm can be coded in Java as follows.

public int roll() {
  int state = 0;
  while (true) {
    switch(state) {
      case 0 :
        switch (Coin.flip()) {
          case 0 : 
            state = 1; break;
          case 1 :
            state = 2; break;
        }
        break;
      case 1 :
        switch (Coin.flip()) {
          case 0 :
            state = 3; break;
          case 1:
            state = 4; break;
        }
        break;
      case 2 :
        switch (Coin.flip()) {
          case 0 :
            state = 5; break;
          case 1:
            state = 6; break;
        }
        break;
      case 3 :
        switch (Coin.flip()) {
          case 0 :
            state = 1; break;
          case 1:
            return 1;
        }
        break;
      case 4 :
        switch (Coin.flip()) {
          case 0 :
            return 2;
          case 1:
            return 3;
        }
        break;
      case 5 :
        switch (Coin.flip()) {
          case 0 :
            return 4;
          case 1:
            return 5;
        }
        break;
      case 6 :
        switch (Coin.flip()) {
          case 0 :
            state = 2; break;
          case 1:
            return 6;
        }
        break;
    }
  }
}

0 ------> 1
1 ------> 2
2 -0.50-> 3
3 -0.50-> 4
4 -0.50-> 3
4 -0.50-> 5
3 -0.50-> 6
6 -0.50-> 5
6 -0.50-> 5
2 -0.50-> 7
7 -0.50-> 8
8 -0.50-> 5
8 -0.50-> 5
7 -0.50-> 9
9 -0.50-> 7
9 -0.50-> 5

1. Donald E. Knuth and Andrew C. Yao. The Complexity of Nonuniform Random Number Generation. In, J.F. Traub, editor, Proceedings of a Symposium on New Directions and Recent Results in Algorithms and Complexity, pages 375-428, Pittsburgh, PA, USA, April 1976. Academic Press.

By default, JPF uses a depth-first search strategy. In our extension, we provide a new search strategy that explores the state space in a random way. The likelyhood that a state is chosen to be explored is proportional to the probability of the path along which the state was discovered (the probability of a path is the product of the probabilities of its transitions).

Licensing of jpf-probabilistic

This extension is free software: it can be redistributed and/or modified under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or any later version.

This extension is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

A copy of the GNU General Public License at http://www.gnu.org/licenses.

Installing of jpf-probabilistic

To install jpf-probabilistic, follow the steps below.

1. Install JPF. See http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/start for details.
2. Save the file jpf-probabilistic-1.1.zip in the directory which contains the directory jpf-core.
3. Unzip the file jpf-probabilistic-1.1.zip.
4. Build jpf-probabilistic using ant. See http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/build for details. To create the APIs, use ant api. To clean up the build directory, use ant clean.
5. Add jpf-probabilistic to the file site.properties. See http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/site-properties for details.

Running JPF with jpf-probabilistic

To model check the class randomized.DieTest, which is one of the examples included in jpf-probabilistic and which is included in jpf-probabilistic-examples.jar in the build directory, and to print its underlying Markov chain, we create a file named, for example, Die.jpf with the following contents:

target=randomized.DieTest
classpath=${jpf-probabilistic}/build/jpf-probabilistic-examples.jar
listener=probabilistic.listener.StateSpacePrinter

To use the random search strategy, add the following to the above file.

search.class=probabilistic.search.RandomSearch

Questions/comments/suggestions

Please email them to franck@cs.yorku.ca.

Thanks