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.

Later, we extended SCOOP to work with a process algebra for Markov Automata, called MAPA. It is described in the paper

"Efficient Modelling and Generation of Markov Automata" (published at CONCUR 2012)

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

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

Another one is confluence reduction, as described in the papers

"Confluence Reduction for Probabilistic Systems" (published at TACAS 2011)
"A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time" (published in TCS)
"Confluence Reduction for Markov Automata" (published at FORMATS 2013)
"On-the-fly confluence detection for statistical model checking" (published at NFM 2013)

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)

An overview of the analysis techniques that can be applied on MAPA models using the IMCA tool, is given in the paper

"Modelling, Reduction and Analysis of Markov Automata" (published at QEST 2013)

A complete overview of everything is given in the thesis

"Efficient Modelling, Generation and Analysis of Markov Automata"

Models and test scripts accompanying papers

The version of the tool that was used for the paper "Confluence Reduction for Markov Automata", submitted to TCS-QAPL 2014, including models and test scripts, can be found here.
The version of the tool that was used for the paper "MaMa: A Tool-Chain for Modelling and Analysing Markov Automata", in the proceedings of QEST 2013, including models and test scripts, can be found here.
The version of the tool that was used for the paper "Confluence Reduction for Markov Automata", in the proceedings of FORMATS 2013, including models and test scripts, can be found here.
The version of the tool that was used for the paper "Efficient Modelling and Generation of Markov Automata" in the proceedings of 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, 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.

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