Abstract
Markovian behavioral equivalences are a means to relate and manipulate the formal descriptions of systems with an underlying CTMC semantics. There are three fundamental approaches to their definition: bisimilarity, testing, and trace. In this paper we survey the major results appeared in the literature about Markovian bisimilarity, Markovian testing equivalence, and Markovian trace equivalence. The objective is to compare these equivalences with respect to a number of criteria such as their discriminating power, the exactness of the CTMC-level aggregations they induce, the achievement of the congruence property, the existence of sound and complete axiomatizations, the existence of logical characterizations, and the existence of efficient verification algorithms.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, Chichester (1995)
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge University Press, Cambridge (1990)
Baier, C., Katoen, J.-P., Hermanns, H.: Approximate Symbolic Model Checking of Continuous-Time Markov Chains (Extended Abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 146–162. Springer, Heidelberg (1999)
Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative Branching-Time Semantics for Markov Chains. Information and Computation 200, 149–214 (2005)
Balsamo, S., Bernardo, M., Simeoni, M.: Performance Evaluation at the Software Architecture Level. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 207–258. Springer, Heidelberg (2003)
Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)
Bernardo, M.: Non-Bisimulation-Based Markovian Behavioral Equivalences. To appear in Journal of Logic and Algebraic Programming.
Bernardo, M., Aldini, A.: Weak Markovian Bisimilarity: Abstracting from Prioritized/Weighted Internal Immediate Actions: Submitted for publication.
Bernardo, M., Botta, S.: A Survey of Modal Logics Characterizing Behavioral Equivalences for Nondeterministic and Stochastic Systems. To appear in Mathematical Structures in Computer Science.
Bernardo, M., Bravetti, M.: Performance Measure Sensitive Congruences for Markovian Process Algebras. Theoretical Computer Science 290, 117–160 (2003)
Bernardo, M., Cleaveland, W.R.: A Theory of Testing for Markovian Processes. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 305–319. Springer, Heidelberg (2000)
Bohnenkamp, H., D’Argenio, P.R., Hermanns, H., Katoen, J.-P.: Modest: A Compositional Modeling Formalism for Hard and Softly Timed Systems. IEEE Trans. on Software Engineering 32, 812–830 (2006)
Bravetti, M.: Revisiting Interactive Markov Chains. In: 3rd Int. Workshop on Models for Time-Critical Systems (MTCS 2002), Brno, Czech Republic. ENTCS, vol. 68(5), pp. 1–20 (2002)
Bravetti, M., Bernardo, M., Gorrieri, R.: A Note on the Congruence Proof for Recursion in Markovian Bisimulation Equivalence. In: Proc. of the 6th Int. Workshop on Process Algebra and Performance Modelling (PAPM 1998), Nice France, pp. 153–164 (1998)
Buchholz, P.: Exact and Ordinary Lumpability in Finite Markov Chains. Journal of Applied Probability 31, 59–75 (1994)
Buchholz, P.: Markovian Process Algebra: Composition and Equivalence. In: Proc. of the 2nd Int. Workshop on Process Algebra and Performance Modelling (PAPM 1994), Erlangen, Germany, Technical Report 27-4, pp. 11-30 (1994)
Christoff, I.: Testing Equivalences and Fully Abstract Models for Probabilistic Processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 126–140. Springer, Heidelberg (1990)
Clark, G., Gilmore, S., Hillston, J.: Specifying Performance Measures for PEPA. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 211–227. Springer, Heidelberg (1999)
Cleaveland, R., Dayar, Z., Smolka, S.A., Yuen, S.: Testing Preorders for Probabilistic Processes. Information and Computation 154, 93–148 (1999)
Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing 5, 1–20 (1993)
De Nicola, R., Hennessy, M.: Testing Equivalences for Processes. Theoretical Computer Science 34, 83–133 (1983)
De Nicola, R., Latella, D., Massink, M.: Formal Modeling and Quantitative Analysis of Klaim-Based Mobile Systems. In: Proc. of the 20th ACM Symp. on Applied Computing (SAC 2005), Santa Fe, NM, pp. 428–435. ACM Press, New York (2005)
Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal State-Space Lumping in Markov Chains. Information Processing Letters 87, 309–315 (2003)
Gilmore, S., Hillston, J., Ribaudo, M.: An Efficient Algorithm for Aggregating PEPA Models. IEEE Trans. on Software Engineering 27, 449–464 (2001)
van Glabbeek, R.J.: The Linear Time - Branching Time Spectrum I. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3–99. Elsevier, Amsterdam (2001)
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, Generative and Stratified Models of Probabilistic Processes. Information and Computation 121, 59–80 (1995)
Götz, N., Herzog, U., Rettelbach, M.: Multiprocessor and Distributed System Design: The Integration of Functional Specification and Performance Analysis Using Stochastic Process Algebras. In: Donatiello, L., Nelson, R. (eds.) SIGMETRICS 1993 and Performance 1993. LNCS, vol. 729, pp. 121–146. Springer, Heidelberg (1993)
Hennessy, M.: Acceptance Trees. Journal of the ACM 32, 896–928 (1985)
Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM 32, 137–162 (1985)
Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Hermanns, H., Rettelbach, M.: Syntax, Semantics, Equivalences, and Axioms for MTIPP. In: Proc. of the 2nd Int. Workshop on Process Algebra and Performance Modelling (PAPM 1994), Erlangen, Germany, Technical Report 27-4, pp. 71–87 (1994)
Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Howard, R.A.: Dynamic Probabilistic Systems. John Wiley & Sons, Chichester (1971)
Huynh, D.T., Tian, L.: On Some Equivalence Relations for Probabilistic Processes. Fundamenta Informaticae 17, 211–234 (1992)
Jou, C.-C., Smolka, S.A.: Equivalences, Congruences, and Complete Axiomatizations for Probabilistic Processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 367–383. Springer, Heidelberg (1990)
Kanellakis, P.C., Smolka, S.A.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation 86, 43–68 (1990)
Kleinrock, L.: Queueing Systems. John Wiley & Sons, Chichester (1975)
Kwiatkowska, M.Z., Norman, G.J.: A Testing Equivalence for Reactive Probabilistic Processes. In: Proc. of the 2nd Int. Workshop on Expressiveness in Concurrency (EXPRESS 1998), Nice, France. ENTCS, vol. 16(2), pp. 114–132 (1998)
Larsen, K.G., Skou, A.: Bisimulation through Probabilistic Testing. Information and Computation 94, 1–28 (1991)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Paige, R., Tarjan, R.E.: Three Partition Refinement Algorithms. SIAM Journal on Computing 16, 973–989 (1987)
Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Priami, C.: Stochastic π-Calculus. Computer Journal 38, 578–589 (1995)
Sproston, J., Donatelli, S.: Backward Bisimulation in Markov Chain Model Checking. IEEE Trans. on Software Engineering 32, 531–546 (2006)
Stark, E.W., Cleaveland, W.R., Smolka, S.A.: A Process-Algebraic Language for Probabilistic I/O Automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 193–207. Springer, Heidelberg (2003)
Tzeng, W.-G.: A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata. SIAM Journal on Computing 21, 216–227 (1992)
Woodside, C.M.: From Annotated Software Designs (UML SPT/MARTE) to Model Formalisms. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 429–467. Springer, Heidelberg (2007)
Wolf, V., Baier, C., Majster-Cederbaum, M.: Trace Machines for Observing Continuous-Time Markov Chains. In: Proc. of the 3rd Int. Workshop on Quantitative Aspects of Programming Languages (QAPL 2005), Edinburgh, UK. ENTCS, vol. 153(2), pp. 259–277 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this chapter
Cite this chapter
Bernardo, M. (2007). A Survey of Markovian Behavioral Equivalences. In: Bernardo, M., Hillston, J. (eds) Formal Methods for Performance Evaluation. SFM 2007. Lecture Notes in Computer Science, vol 4486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72522-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-72522-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72482-7
Online ISBN: 978-3-540-72522-0
eBook Packages: Computer ScienceComputer Science (R0)