(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)

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)

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)

*"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)

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

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

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

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

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.

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.