Prophesy

Table of Contents

 

Video Tutorial

This is a short video tutorial on how to use the PROPhESY GUI.

Using the PROPhESY GUI

Abstract

We present PROPhESY, a tool for analyzing parametric Markov chains. It can compute a rational function (i.e., a fraction of two polynomials in the model parameters) for reachability and expected reward objectives.  PROPhESY supports incremental automatic parameter synthesis (using SMT techniques) to determine “safe” and “unsafe” regions of the parameter space. All values in these regions give rise to instantiated MCs satisfying or violating the (conditional) probability or expected reward objective. PROPhESY features a web front-end supporting visualization and user-guided parameter synthesis. Experimental results  show that PROPhESY scales to Markov chains with millions of states and several parameters.

Benchmarks

We evaluated our tool on the following case studies.

Bounded Retransmission Protocol

Model

This model is taken from the PRISM website. It describes sending a file over a faulty network connection. Losing messages is compensated by a bounded number of retransmissions. The model is scalable in two parameters N and MAX, where N denotes the number of chunks that need to be transmitted and MAX is an upper bound on the number of retransmissions of each chunk. The model’s probability parameters are pL and pK, which represent the probability of message loss on the two involved lossy channels. In the full list of benchmarks, we list all instances (N, MAX), we considered.

Properties

Based on the target objective, we consider two different properties for this model.

  • What is the probability that the sender does not report a successful transmission?
  • What is the probability that the file is successfully?

Crowds Protocol

This protocol tries to establish anonymity for the sender of a message. It does so by randomly forwarding the message in a crowd, before it is finally delivered to the recipient. However, corrupted hosts in the crowd try to recognize the real sender by observing who sent the message to them. The model is taken from the PRISM website. The model size can be governed by the number of participating hosts N and the number of times R the protocol is run consecutively. The model contains the probability parameters PF and badC, where PF is the probability that a message is forwarded another time and badC is the probability that a crowd member is corrupted. We report on all instances (N, R) we considered. Since we consider two different properties for conditional probabilities for this model, we list the instances (N, R, i), referring to checking the i-th property on instance (N, R).

Properties

Based on the target objective, we consider three different properties for this model.

  • What is the probability that the real sender is observed more than once?
  • What is the probability that the real sender is observed more than once, given that any of the other hosts has also been observed more than once?
  • What is the probability that a crowd member other than the original sender is observed more than once, given that the real sender is observed more than once?

Zeroconf Protocol

This protocol (taken from the PARAM website) offers a way for a client to select an IP address without further configuration. The client first chooses an address at random and then informs the network about its choice. If a collision is detected, the host chooses a different address. If the client does not get an answer, however, it will retry the claim of the address. If the client did not receive an answer after a given number N of retries, the client considers its IP to be valid and will use it. The probability p of not receiving an answer after telling the network about the choice, as well as the probability q of choosing an address that is currently in use are parameters of the model. The full table of results lists all instances (N).

For this model, we computed the expected number of tests for a collision until a final decision has been made.

Probabilistic Contract Signing

This protocol, available on the PRISM website, aims at establishing the commitment of two parties to a contract, where either party does not fully trust the other one. It does so by revealing secrets bit by bit with the intention that either both parties are committed or none of them is. The model has scalable parameters N and L that govern how many secrets each party possesses (N) and how many different values each of them can take (L). The probability parameter p influences which secrets are revealed. The benchmark times for all instances (N, L) are given in the full table.

We computed the expected number of messages the first party needs to know once the second party knows any of the first parties’ secrets.

NAND Multiplexing

Taken from the PRISM website, this model constructs a fault-tolerant hardware circuit based on possibly faulty NAND gates. Letting the sub-units all perform the same job leads to fault-tolerance by redundancy. Scalable parameters of this model are the number N of inputs in each bundle and the number of restorative stages K. Furthermore, the model contains two probability parameters perr and prob1 that indicate the probability that a unit is functioning properly and that the initial inputs are stimulated, respectively.

Properties

Based on the target objective, we consider two different properties for this model.

  • What is the probability that less than 10% of the outputs were erroneous?
  • What is the expected number of  erroneous outputs after completion?

Benchmark Setup & Results

We provide a text file that explains which parameters were passed to the tools and the concrete models and properties used can be found in the Downloads section. The full list of benchmark results can be found here. Note that this table does not match the table from the paper exactly. This is because we noticed only after the submission that PARAM produces wrong results for the fastest setting on the zeroconf case study. We now list the times for the best correct setup of PARAM on these instances.

Downloads

Here, we provide useful downloads related to the tool.

  • A VirtualBox disk image with all tools preinstalled can be found here. We also provide a README that should get you started. To use the virtual machine, please import it using VirtualBox.
  • The Prophesy toolchain can be found here.
  • The benchmark models and properties can be found here.
  • The tools can be found here.
  • Instructional video can be found here