An efficient symbolic elimination algorithm for the stochastic process algebra tool CASPA. (English) Zbl 1206.68208

Nielsen, Mogens (ed.) et al., SOFSEM 2009: Theory and practice of computer science. 35th conference on current trends in theory and practice of computer science, Špindlerův Mlýn, Czech Republic, January 24–30, 2009. Proceedings. Berlin: Springer (ISBN 978-3-540-95890-1/pbk). Lecture Notes in Computer Science 5404, 485-496 (2009).
Summary: 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.
For the entire collection see [Zbl 1154.68020].


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)


Full Text: DOI


[1] Au-Yeung, S.W.M., Harrison, P.G., Knottenbelt, W.J.: A Queueing Network Model of Patient Flow in an Accident and Emergency Department. In: Proc. 20th Ann. European Simulation and Modelling Conf., Toulouse, France, pp. 60–67 (2006)
[2] Bachmann, J.: Entwurf und Implementierung eines graphischen Modelleditors und einer Benutzerschnittstelle für das Werkzeug CASPA. Master’s thesis, Universität der Bundeswehr München, Dept. of Computer Science 4 (2007) (in German)
[3] Bernardo, M., Gorrieri, R.: A tutorial on EMPA: A theory of concurrent processes with nondeterminism, priorities, probabilities and time. Theoret. Comp. Science 202, 1–54 (1998) · Zbl 0902.68075
[4] Frank, E.: Erweiterung eines MTBDD-basierten Werkzeugs für die Analyse stocchastischer Transitionssysteme. Int. Report, Univ. of Erlangen, Computer Science 7 (2000) (in German)
[5] Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002) · Zbl 1012.68142
[6] Hermanns, H., Rettelbach, M.: Syntax, Semantics, Equivalences, and Axioms for MTIPP. In: Proc. of PAPM 1994, Arbeitsberichte des IMMD, vol. 27(4), pp. 71–88 (1994)
[7] Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996) · Zbl 1080.68003
[8] Kuntz, M., Siegle, M.: Deriving symbolic representations from stochastic process algebras. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 188–206. Springer, Heidelberg (2002) · Zbl 1065.68594
[9] Kuntz, M., Siegle, M.: Symbolic Model Checking of Stochastic Systems: Theory and Implementation. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 89–107. Springer, Heidelberg (2006) · Zbl 1178.68346
[10] Kuntz, M., Siegle, M., Werner, E.: Symbolic Performance and Dependability Evaluation with the Tool CASPA. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol. 3236, pp. 293–307. Springer, Heidelberg (2004)
[11] Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with generalized stochastic Petri nets. Wiley, Chichester (1995) · Zbl 0843.68080
[12] Parker, D.: Implementation of symbolic model checking for probabilistic systems. PhD thesis, School of Computer Science, Faculty of Science, University of Birmingham (2002)
[13] Schuster, J., Siegle, M.: A symbolic multilevel method with sparse submatrix representation for memory-speed tradeoff. In: 14. GI/ITG Conf. Measurement, Modelling and Evaluation of Comp. and Communic. Systems (MMB 2008), pp. 191–205. VDE Verlag (2008)
[14] Siegle, M.: Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties. Shaker-Verlag (2002)
[15] Tofts, C.: Processes with probabilities, priority and time. Formal Aspects of Computing 6(5), 536–564 (1994) · Zbl 0820.68072
[16] Werner, E.: Leistungsbewertung mit Multi-terminalen Binären Entscheidungsdiagrammen. Master’s thesis, Univ. Erlangen, Computer Science 7 (2003) (in German)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.