SCOOP: A Tool for SymboliC Optimisations of Probabilistic Processes

(Immediately move to the web-based implementation of this work)

To enable the symbolic reduction of probabilistic specifications that are enriched with data types, we developed the probabilistic process algebra prCRL, described in the papers The main idea was to define a normal form for the process algebra, called the Linear Probabilistic Process Equation (LPPE), which enables all kinds of analyses aimed at optimisalitions of the model. In the ACSD paper we introduced an algorithm to transform any specification in the prCRL language to such an LPPE.

Later, we extended SCOOP to work with a process algebra for Markov Automata, called MAPA. It is described in the paper It is also possible to translate GSPN models (specified in the PNML format) to MAPA specifications. Details can be found here.

We developed reduction methods that can be applied to models specified in prCRL (based on the translation to LPPE). One of them performs dead variable analysis, and is a trivial probabilistic generalisation of the method described for μCRL in the paper Another one is confluence reduction, as described in the papers A high-level overview of the tool, including its input langage and the reduction methods that it applies, is given in the paper An overview of the analysis techniques that can be applied on MAPA models using the IMCA tool, is given in the paper A complete overview of everything is given in the thesis

Models and test scripts accompanying papers

The SCOOP tool

We implemented a tool that can be used to experiment with everything that is discussed above. It takes a prCRL, MAPA or GSPN specification as its input, linearises it to an LPPE or MLPE, and can apply all the reduction techniques. It can apply confluence reduction, dead variable reduction, constant elimination, summation elimination and expression simplification for both prCRL, MAPA and GSPN. Additionally, for MAPA and GSPN it allows maximal progress reduction.

Most importantly, SCOOP can output state spaces in the input format for the IMCA tool. Also, it can either present the output again as an (optimised) (M)LPE or generate the state space, or just count the number of states and transitions when investigating the effects of reduction techniques. A prCRL specification can also be exported to a PRISM specification and to a variety of formats (to be analysed by for instance CADP or PRISM).

Obtaining the tool
To try out the linearisation techniques and reduction methods we developed, you can either download the tool or resort to the web-based version of it. Using the tool
To use either the web-based or the stand-alone version of the tool, a model in the prCRL, MAPA or PNML language should be provided. An abstract overview of the syntax of prCRL, including its precise semantics, can be found in the ACSD 2010 paper. An abstract overview of the syntax of MAPA can be found in the CONCUR 2012 paper. However, for the specific syntactical details of the input language of the tool, as well as the description of all features of the tool, please look at the following two pages.