An efficient symbolic elimination algorithm for the stochastic process algebra tool CASPA. CASPA is a stochastic process algebra tool for performance and dependability modelling, analysis and verification. It is based entirely on the symbolic data structure MTBDD (multi-terminal binary decision diagram) which enables the tool to handle models with very large state space. This paper focuses on an extension of CASPA’s modelling language by weighted immediate actions. We discuss the pertaining semantics and present an efficient symbolic algorithm for the elimination of vanishing states. A non-trivial case study illustrates the usage features of CASPA, from graphical model specification to numerical analysis.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Tati, Bharath Siva Kumar; Siegle, Markus: Parameter and controller synthesis for Markov chains with actions and state labels (2015)
- Lampka, Kai; Siegle, Markus; Ossowski, Joern; Baier, Christel: Partially-shared zero-suppressed multi-terminal BDDs: Concept, algorithms and applications (2010)
- Bachmann, Jens; Riedl, Martin; Schuster, Johann; Siegle, Markus: An efficient symbolic elimination algorithm for the stochastic process algebra tool CASPA (2009)
- Lampka, Kai: A new algorithm for partitioned symbolic reachability analysis (2008)