{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:31:22Z","timestamp":1774837882190,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":49,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540724827","type":"print"},{"value":"9783540725220","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-72522-0_5","type":"book-chapter","created":{"date-parts":[[2007,6,5]],"date-time":"2007-06-05T15:02:12Z","timestamp":1181055732000},"page":"180-219","source":"Crossref","is-referenced-by-count":7,"title":["A Survey of Markovian Behavioral Equivalences"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bernardo","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M. Ajmone Marsan","year":"1995","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, Chichester (1995)"},{"key":"5_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624193","volume-title":"Process Algebra","author":"J.C.M. Baeten","year":"1990","unstructured":"Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge University Press, Cambridge (1990)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"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.\u00a01664, pp. 146\u2013162. Springer, Heidelberg (1999)"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C. Baier","year":"2005","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative Branching-Time Semantics for Markov Chains. Information and Computation\u00a0200, 149\u2013214 (2005)","journal-title":"Information and Computation"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/978-3-540-39800-4_10","volume-title":"Formal Methods for Software Architectures","author":"S. Balsamo","year":"2003","unstructured":"Balsamo, S., Bernardo, M., Simeoni, M.: Performance Evaluation at the Software Architecture Level. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol.\u00a02804, pp. 207\u2013258. Springer, Heidelberg (2003)"},{"key":"5_CR6","volume-title":"Handbook of Process Algebra","year":"2001","unstructured":"Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)"},{"key":"5_CR7","unstructured":"Bernardo, M.: Non-Bisimulation-Based Markovian Behavioral Equivalences. To appear in Journal of Logic and Algebraic Programming."},{"key":"5_CR8","unstructured":"Bernardo, M., Aldini, A.: Weak Markovian Bisimilarity: Abstracting from Prioritized\/Weighted Internal Immediate Actions: Submitted for publication."},{"key":"5_CR9","unstructured":"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."},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0304-3975(01)00090-1","volume":"290","author":"M. Bernardo","year":"2003","unstructured":"Bernardo, M., Bravetti, M.: Performance Measure Sensitive Congruences for Markovian Process Algebras. Theoretical Computer Science\u00a0290, 117\u2013160 (2003)","journal-title":"Theoretical Computer Science"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/3-540-44618-4_23","volume-title":"CONCUR 2000 - Concurrency Theory","author":"M. Bernardo","year":"2000","unstructured":"Bernardo, M., Cleaveland, W.R.: A Theory of Testing for Markovian Processes. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 305\u2013319. Springer, Heidelberg (2000)"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"H. Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.-P.: Modest: A Compositional Modeling Formalism for Hard and Softly Timed Systems. IEEE Trans. on Software Engineering\u00a032, 812\u2013830 (2006)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Bravetti, M.: Revisiting Interactive Markov Chains. In: 3rd Int. Workshop on Models for Time-Critical Systems (MTCS\u00a02002), Brno, Czech Republic. ENTCS, vol.\u00a068(5), pp. 1\u201320 (2002)","DOI":"10.1016\/S1571-0661(04)80520-6"},{"key":"5_CR14","unstructured":"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\u00a01998), Nice France, pp. 153\u2013164 (1998)"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"59","DOI":"10.2307\/3215235","volume":"31","author":"P. Buchholz","year":"1994","unstructured":"Buchholz, P.: Exact and Ordinary Lumpability in Finite Markov Chains. Journal of Applied Probability\u00a031, 59\u201375 (1994)","journal-title":"Journal of Applied Probability"},{"key":"5_CR16","unstructured":"Buchholz, P.: Markovian Process Algebra: Composition and Equivalence. In: Proc. of the 2nd Int. Workshop on Process Algebra and Performance Modelling (PAPM\u00a01994), Erlangen, Germany, Technical Report\u00a027-4, pp.\u00a011-30 (1994)"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/BFb0039056","volume-title":"CONCUR \u201990","author":"I. Christoff","year":"1990","unstructured":"Christoff, I.: Testing Equivalences and Fully Abstract Models for Probabilistic Processes. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol.\u00a0458, pp. 126\u2013140. Springer, Heidelberg (1990)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/3-540-48778-6_13","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"G. Clark","year":"1999","unstructured":"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.\u00a01601, pp. 211\u2013227. Springer, Heidelberg (1999)"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1006\/inco.1999.2808","volume":"154","author":"R. Cleaveland","year":"1999","unstructured":"Cleaveland, R., Dayar, Z., Smolka, S.A., Yuen, S.: Testing Preorders for Probabilistic Processes. Information and Computation\u00a0154, 93\u2013148 (1999)","journal-title":"Information and Computation"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01211314","volume":"5","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing\u00a05, 1\u201320 (1993)","journal-title":"Formal Aspects of Computing"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R. Nicola De","year":"1983","unstructured":"De Nicola, R., Hennessy, M.: Testing Equivalences for Processes. Theoretical Computer Science\u00a034, 83\u2013133 (1983)","journal-title":"Theoretical Computer Science"},{"key":"5_CR22","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1145\/1066677.1066777","volume-title":"Proc. of the 20th ACM Symp. on Applied Computing (SAC\u00a02005)","author":"R. Nicola De","year":"2005","unstructured":"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\u00a02005), Santa Fe, NM, pp. 428\u2013435. ACM Press, New York (2005)"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/S0020-0190(03)00343-0","volume":"87","author":"S. Derisavi","year":"2003","unstructured":"Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal State-Space Lumping in Markov Chains. Information Processing Letters\u00a087, 309\u2013315 (2003)","journal-title":"Information Processing Letters"},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1109\/32.922715","volume":"27","author":"S. Gilmore","year":"2001","unstructured":"Gilmore, S., Hillston, J., Ribaudo, M.: An Efficient Algorithm for Aggregating PEPA Models. IEEE Trans. on Software Engineering\u00a027, 449\u2013464 (2001)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/B978-044482830-9\/50019-9","volume-title":"Handbook of Process Algebra","author":"R.J. Glabbeek van","year":"2001","unstructured":"van Glabbeek, R.J.: The Linear Time - Branching Time Spectrum\u00a0I. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3\u201399. Elsevier, Amsterdam (2001)"},{"key":"5_CR26","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"R.J. Glabbeek van","year":"1995","unstructured":"van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, Generative and Stratified Models of Probabilistic Processes. Information and Computation\u00a0121, 59\u201380 (1995)","journal-title":"Information and Computation"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BFb0013851","volume-title":"Performance Evaluation of Computer and Communication Systems","author":"N. G\u00f6tz","year":"1993","unstructured":"G\u00f6tz, 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.\u00a0729, pp. 121\u2013146. Springer, Heidelberg (1993)"},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"896","DOI":"10.1145\/4221.4249","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M.: Acceptance Trees. Journal of the ACM\u00a032, 896\u2013928 (1985)","journal-title":"Journal of the ACM"},{"key":"5_CR29","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM\u00a032, 137\u2013162 (1985)","journal-title":"Journal of the ACM"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains. LNCS, vol.\u00a02428. Springer, Heidelberg (2002)"},{"key":"5_CR31","unstructured":"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\u00a01994), Erlangen, Germany, Technical Report\u00a027-4, pp. 71\u201387 (1994)"},{"key":"5_CR32","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569951","volume-title":"A Compositional Approach to Performance Modelling","author":"J. Hillston","year":"1996","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press, Cambridge (1996)"},{"key":"5_CR33","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"key":"5_CR34","volume-title":"Dynamic Probabilistic Systems","author":"R.A. Howard","year":"1971","unstructured":"Howard, R.A.: Dynamic Probabilistic Systems. John Wiley & Sons, Chichester (1971)"},{"key":"5_CR35","doi-asserted-by":"crossref","first-page":"211","DOI":"10.3233\/FI-1992-17304","volume":"17","author":"D.T. Huynh","year":"1992","unstructured":"Huynh, D.T., Tian, L.: On Some Equivalence Relations for Probabilistic Processes. Fundamenta Informaticae\u00a017, 211\u2013234 (1992)","journal-title":"Fundamenta Informaticae"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/BFb0039071","volume-title":"CONCUR \u201990","author":"C.-C. Jou","year":"1990","unstructured":"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.\u00a0458, pp. 367\u2013383. Springer, Heidelberg (1990)"},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P.C. Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation\u00a086, 43\u201368 (1990)","journal-title":"Information and Computation"},{"key":"5_CR38","volume-title":"Queueing Systems","author":"L. Kleinrock","year":"1975","unstructured":"Kleinrock, L.: Queueing Systems. John Wiley & Sons, Chichester (1975)"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"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\u00a01998), Nice, France. ENTCS, vol.\u00a016(2), pp. 114\u2013132 (1998)","DOI":"10.1016\/S1571-0661(04)00121-5"},{"key":"5_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through Probabilistic Testing. Information and Computation\u00a094, 1\u201328 (1991)","journal-title":"Information and Computation"},{"key":"5_CR41","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"5_CR42","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three Partition Refinement Algorithms. SIAM Journal on Computing\u00a016, 973\u2013989 (1987)","journal-title":"SIAM Journal on Computing"},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"5_CR44","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1093\/comjnl\/38.7.578","volume":"38","author":"C. Priami","year":"1995","unstructured":"Priami, C.: Stochastic \u03c0-Calculus. Computer Journal\u00a038, 578\u2013589 (1995)","journal-title":"Computer Journal"},{"key":"5_CR45","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1109\/TSE.2006.74","volume":"32","author":"J. Sproston","year":"2006","unstructured":"Sproston, J., Donatelli, S.: Backward Bisimulation in Markov Chain Model Checking. IEEE Trans. on Software Engineering\u00a032, 531\u2013546 (2006)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"5_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/978-3-540-45187-7_13","volume-title":"CONCUR 2003 - Concurrency Theory","author":"E.W. Stark","year":"2003","unstructured":"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.\u00a02761, pp. 193\u2013207. Springer, Heidelberg (2003)"},{"key":"5_CR47","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1137\/0221017","volume":"21","author":"W.-G. Tzeng","year":"1992","unstructured":"Tzeng, W.-G.: A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata. SIAM Journal on Computing\u00a021, 216\u2013227 (1992)","journal-title":"SIAM Journal on Computing"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/978-3-540-72522-0_11","volume-title":"Formal Methods for Performance Evaluation","author":"C.M. Woodside","year":"2007","unstructured":"Woodside, C.M.: From Annotated Software Designs (UML SPT\/MARTE) to Model Formalisms. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 429\u2013467. Springer, Heidelberg (2007)"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"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\u00a02005), Edinburgh, UK. ENTCS, vol.\u00a0153(2), pp. 259\u2013277 (2005)","DOI":"10.1016\/j.entcs.2005.10.042"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Performance Evaluation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72522-0_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,14]],"date-time":"2021-08-14T12:46:53Z","timestamp":1628945213000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72522-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540724827","9783540725220"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72522-0_5","relation":{},"subject":[]}}