SCOOP: A tool for symbolic optimisations of probabilistic processes. ... 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).
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Timmer, Mark; Katoen, Joost-Pieter; van de Pol, Jaco; Stoelinga, Mariëlle: Confluence reduction for Markov automata (2016)
- Guck, Dennis; Hatefi, Hassan; Hermanns, Holger; Katoen, Joost-Pieter; Timmer, Mark: Analysis of timed and long-run objectives for Markov automata (2014)
- Timmer, Mark; Katoen, Joost-Pieter; van de Pol, Jaco; Stoelinga, Mariëlle I.A.: Efficient modelling and generation of Markov automata (2012)