Mark Timmer (FMT/UT)

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

"A linear process algebraic format for probabilistic systems with data" (published at ACSD 2010)
"A linear process-algebraic format with data for probabilistic automata" (published in TCS)

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.

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

"State Space Reduction of Linear Processes Using Control Flow Reconstruction" (published at ATVA 2009)

Another one applies confluence reduction, as described in the papers

"Confluence Reduction for Probabilistic Systems" (published at TACAS 2011)
"Why Confluence is More Powerful than Ample Sets in Probabilistic and Non-Probabilistic Branching Time" (in submission)

A high-level overview of the tool, including its input langage and the reduction methods that it applies, is given in the paper

"SCOOP: A Tool for SymboliC Optimisations Of Probabilistic Processes" (published at QEST 2011)

Later, we extended SCOOP to work with a process algebra for Markov Automata, called MAPA. A paper on this is currently in submission.

Models and test scripts accompanying papers

The version of the tool that was used for the paper "Efficient Modelling and Generation of Markov Automata", currently in submission for CONCUR 2012, including models and test scripts, can be found here.
The version of the tool that was used for the paper "A linear process-algebraic format with data for probabilistic automata" in Theoretical Computer Science, including models and test scripts, can be found here.
The version of the tool that was used for the paper "SCOOP: A Tool for SymboliC Optimisations Of Probabilistic Processes" in the proceedings of QEST 2011, including models and test scripts, can be found here.
The version of the tool that was used for the paper "Confluence Reduction for Probabilistic Systems" in the proceedings of TACAS 2011, including models and test scripts, can be found here.

The SCOOP tool

We implemented a tool that can be used to experiment with everything that is discussed above. It takes a prCRL or MAPA specification as its input, linearises it to an LPPE or MLPPE, and can apply all the reduction techniques. It can apply dead variable reduction, transition merging, constant elimination, summation elimination and expression simplification for both prCRL and MAPA.
Additionally, for prCRL it can apply confluence reduction, and for MAPA it allows maximal progress reduction. Then, it can either present the output again as an (optimised) (M)LPPE 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.

The web-based version does not require compiling or installing of any software, and contains all functionality.
The stand-alone version needs to be downloaded and compiled, but can be applied easier for batches of multiple experiments.

Using the tool
To use either the web-based or the stand-alone version of the tool, a model in the prCRL language should be provided. An abstract overview of the syntax, including its precise semantics, can be found in the ACSD 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.