Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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)
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)
Frank, E.: Erweiterung eines MTBDD-basierten Werkzeugs für die Analyse stocchastischer Transitionssysteme. Int. Report, Univ. of Erlangen, Computer Science 7 (2000) (in German)
Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
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)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
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)
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)
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)
Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with generalized stochastic Petri nets. Wiley, Chichester (1995)
Parker, D.: Implementation of symbolic model checking for probabilistic systems. PhD thesis, School of Computer Science, Faculty of Science, University of Birmingham (2002)
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)
Siegle, M.: Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties. Shaker-Verlag (2002)
Tofts, C.: Processes with probabilities, priority and time. Formal Aspects of Computing 6(5), 536–564 (1994)
Werner, E.: Leistungsbewertung mit Multi-terminalen Binären Entscheidungsdiagrammen. Master’s thesis, Univ. Erlangen, Computer Science 7 (2003) (in German)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bachmann, J., Riedl, M., Schuster, J., Siegle, M. (2009). An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra Tool CASPA. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds) SOFSEM 2009: Theory and Practice of Computer Science. SOFSEM 2009. Lecture Notes in Computer Science, vol 5404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-95891-8_44
Download citation
DOI: https://doi.org/10.1007/978-3-540-95891-8_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-95890-1
Online ISBN: 978-3-540-95891-8
eBook Packages: Computer ScienceComputer Science (R0)