Abstract
Stochastic process algebras have been introduced in order to enable compositional performance analysis. The size of the state space is a limiting factor, especially if the system consists of many cooperating components. To fight state space explosion, various proposals for compositional aggregation have been made. They rely on minimisation with respect to a congruence relation. This paper addresses the computational complexity of minimisation algorithms and explains how efficient, BDD-based data structures can be employed for this purpose.
A preliminary version of this paper has been presented at the PAPM’98 workshop [20].
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
C. Baier and H. Hermanns. Weak Bisimulation for Fully Probabilistic Processes. In Proc. CAV’ 97, Springer LNCS 1254:119–130, 1997.
M. Bernardo and R. Gorrieri. A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theoretical Computer Science 202:1–54, 1998.
T. Bolognesi and E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14:25–59, 1987.
A. Bouali. Weak and branching bisimulation in FCTOOL. Rapports de Recherche 1575, INRIA Sophia Antipolis, Valbonne Cedex, France, 1992.
H. Bruchner. Symbolische Manipulation von stochastischen Transitionssystemen. Internal study, Universität Erlangen-Nürnberg, IMMD VII, 1998. in German.
R.E. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transaction on Computers, C-35(8):677–691, August 1986.
R.E. Bryant and Y. Chen. Verification of Arithmetic Functions with Binary Moment Diagrams. In Proc. 32nd Design Automation Conference, 535–541, ACM/IEEE, 1995.
E.M. Clarke, M. Fujita, P. McGeer, K. McMillan, J. Yang, and X. Zhao. Multi-terminal Binary Decision Diagrams: An efficient data structure for matrix representation. In Proc. International Workshop on Logic Synthesis, Tahoe City, May 1993.
D. Coppersmith and S. Winograd. Matrix Multiplication via Arithmetic Progressions. In Proc. 19th ACM Symposium on Theory of Computing, 1987.
R. Enders, T. Filkorn, and D. Taubner. Generating BDDs for symbolic model checking in CCS. Distributed Computing, 6:155–164, 1993.
J.C. Fernandez. An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming, 13:219–236, 1989.
R. J. van Glabbeek and W. Weijland:. Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM, 43(3):555–600, 1996.
J. F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proc. ICALP’90, Springer LNCS 443:626–638, 1990.
G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. Markovian Analysis of Large Finite State Machines. IEEE Transactions on CAD, 15(12):1479–1493, 1996.
H. Hermanns. Interactive Markov Chains. PhD thesis, Universität Erlangen-Nürnberg, 1998.
H. Hermanns, U. Herzog, and V. Mertsiotakis. Stochastic Process Algebras-Between LOTOS and Markov Chains. Computer Networks and ISDN Systems, 30(9–10):901–924, 1998.
H. Hermanns and M. Rettelbach. Syntax, Semantics, Equivalences, and Axioms for MTIPP. In Proc. 2nd PAPM Workshop. University of Erlangen-Nürnberg, IMMD 27(4):71–87, 1994.
H. Hermanns and J.P. Katoen. Automated Compositional Markov Chain Generation for a Plain Old Telephony System. to appear in Science of Computer Programming, 1998.
H. Hermanns and M. Lohrey. Priority and maximal progress are completely axiomatisable. In Proc. CONCUR’98, Springer LNCS 1466:237–252, 1998.
H. Hermanns and M. Siegle. Computing Bisimulations for Stochastic Process Algebras using Symbolic Techniques. In Proc. 6th Int. PAPM Workshop, 103–118, Nice, 1998.
H. Hermanns, J. Meyer-Kayser and M. Siegle. Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains. submitted for publication, 1999.
J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
T. Huynh and L. Tian. On some Equivalence Relations for Probabilistic Processes. Fundamenta Informaticae, 17:211–234, 1992.
P. Kanellakis and S. Smolka. CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation, 86:43–68, 1990.
J. G. Kemeny and J.L. Snell. Finite Markov Chains. Springer, 1976.
Y.-T. Lai and S. Sastry. Edge-Valued Binary Decision Diagrams for Multi-Level Hierarchical Verification. In 29th Design Automation Conference,608–613, ACM/IEEE, 1992.
K. Larsen and A. Skou. Bisimulation through Probabilistic Testing. Information and Computation, 94(1):1–28, 1991.
R. Milner. Communication and Concurrency. Prentice Hall, London, 1989.
R. Paige and R. Tarjan. Three Partition Refinement Algorithms. SIAM Journal of Computing, 16(6):973–989, 1987.
M. Siegle. Technique and tool for symbolic representation and manipulation of stochastic transition systems. TR IMMD 7 2/98, Universität Erlangen-Nürnberg, March 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hermanns, H., Siegle, M. (1999). Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementation. In: Katoen, JP. (eds) Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48778-6_15
Download citation
DOI: https://doi.org/10.1007/3-540-48778-6_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66010-1
Online ISBN: 978-3-540-48778-4
eBook Packages: Springer Book Archive