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 the CADP Web 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 the CADP Web 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 the CADP Web 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: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page