Database of Research Tools Developed Using CADP

SCOOP Tool for Symbolic Optimizations of Probabilistic Processes

Organisation: University of Twente (THE NETHERLANDS)
RWTH Aachen (GERMANY)

Functionality: State space generation and reduction for probabilistic processes.

Tools used: PRISM
CADP (Construction and Analysis of Distributed Processes)

Period: 2011

Description: Several algorithms and tools exist for model checking qualitative and quantitative properties for a wide range of probabilistic models, modelling for instance randomised protocols or biological processes. Although these techniques are promising, their applicability is limited by the well-known state-space explosion and the restricted treatment of data.

SCOOP (SymboliC Optimisations Of Probabilistic processes) is a tool that symbolically optimises process-algebraic specifications of probabilistic processes. It takes specifications written in the prCRL language (combining data and probabilities), which are linearised first to an intermediate format: the LPPE. On this format, optimisations such as dead-variable reduction and confluence reduction are applied automatically by SCOOP. That way, drastic state space reductions are achieved while never having to generate the complete state space, as data variables are unfolded only locally. The optimised state spaces are ready to be analysed by CADP or PRISM.

Conclusions: The introduction of an intermediate linear process algebraic format (LPPE) for systems incorporating both nondeterministic and probabilistic choice opens the way towards the symbolic minimisation of probabilistic state spaces, as well as the analysis of parameterised probabilistic protocols.

Publications: [Timmer-11] Mark Timmer. "Scoop: A tool for Symbolic Optimisations of Probabilistic Processes". Proceedings of the 8th International Conference on Quantitative Evaluation of SysTems QEST'2011 (Aachen, Germany), pages 149-150. IEEE Computer Society, September 2011.
Available on-line at: http://doc.utwente.nl/77422/1/paper.pdf
or from our FTP site in PDF or PostScript

[Katoen-vandePol-Stoelinga-Timmer-11] Joost-Pieter Katoen, Jaco van de Pol, Mariëlle Stoelinga, and Mark Timmer. "A Linear Process-Algebraic Format with Data for Probabilistic Automata". Theoretical Computer Science 413(1):36-57, 2011.
Available on-line at: http://eprints.eemcs.utwente.nl/20452/01/paper.pdf
or from our FTP site in PDF or PostScript

[Timmer-13] Mark Timmer. "Efficient Modelling, Generation and Analysis of Markov Automata". PhD thesis, Universtiy of Twente, September 2013.
Available on-line at: http://dx.doi.org/10.3990/1.9789036505925
or from our FTP site in PDF or PostScript

Contact:
Mark Timmer
Formal Methods and Tools Group
University of Twente
P.O. Box 217
7500 AE Enschede
The Netherlands
Tel: +31 53 489 3722
Fax: +31 53 489 3247
Email: timmer@cs.utwente.nl



Further remarks: This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software


Last modified: Fri Feb 19 09:13:01 2016.


Back to the CADP research tools page