{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:31:23Z","timestamp":1774837883310,"version":"3.50.1"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,11,30]],"date-time":"2014-11-30T00:00:00Z","timestamp":1417305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s00236-014-0210-1","type":"journal-article","created":{"date-parts":[[2014,12,1]],"date-time":"2014-12-01T14:10:16Z","timestamp":1417443016000},"page":"61-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes"],"prefix":"10.1007","volume":"52","author":[{"given":"Marco","family":"Bernardo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rocco","family":"De Nicola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,11,30]]},"reference":[{"key":"210_CR1","doi-asserted-by":"crossref","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: the temporal logic of stochastic systems. In: Proceedings of the 7th International Conference on Computer Aided Verification (CAV 1995), vol. 939 of LNCS, pp. 155\u2013165. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60045-0_48"},{"key":"210_CR2","doi-asserted-by":"crossref","first-page":"665","DOI":"10.1017\/S0960129599002984","volume":"10","author":"C Baier","year":"2000","unstructured":"Baier, C., Kwiatkowska, M.: Domain equations for probabilistic processes. Math. Struct. Comput. Sci. 10, 665\u2013717 (2000)","journal-title":"Math. Struct. Comput. Sci."},{"key":"210_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.tcs.2004.07.019","volume":"327","author":"F Bartels","year":"2004","unstructured":"Bartels, F., Sokolova, A., de Vink, E.P.: A hierarchy of probabilistic system types. Theor. Comput. Sci. 327, 3\u201322 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"210_CR4","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.ic.2013.02.004","volume":"225","author":"M Bernardo","year":"2013","unstructured":"Bernardo, M., De Nicola, R., Loreti, M.: A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences. Inf. Comput. 225, 29\u201382 (2013)","journal-title":"Inf. Comput."},{"key":"210_CR5","doi-asserted-by":"crossref","unstructured":"Bernardo, M., De Nicola, R., Loreti. M.: Group-by-group probabilistic bisimilarities and their logical characterizations. In: Proceedings of the 8th International Symposium on Trustworthy Global Computing (TGC 2013), vol. 8358 of LNCS, pp. 315\u2013330. Springer, Berlin (2013)","DOI":"10.1007\/978-3-319-05119-2_18"},{"key":"210_CR6","doi-asserted-by":"crossref","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Proceedings of the 15th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1995), vol. 1026 of LNCS, pp. 499\u2013513. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60692-0_70"},{"key":"210_CR7","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Gr\u00fcmberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115\u2013131 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"210_CR8","doi-asserted-by":"crossref","unstructured":"Cattani, S., Segala, R., Kwiatkowska, M., Norman, G.: Stochastic transition systems for continuous state spaces and non-determinism. In: Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2005), vol. 3441 of LNCS, pp. 125\u2013139. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31982-5_8"},{"key":"210_CR9","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1093\/comjnl\/bxp004","volume":"54","author":"C C\u00eerstea","year":"2011","unstructured":"C\u00eerstea, C., Kurz, A., Pattinson, D., Schr\u00f6der, L., Venema, Y.: Modal logics are coalgebraic. Comput. J. 54, 31\u201341 (2011)","journal-title":"Comput. J."},{"key":"210_CR10","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Progr. Lang. Syst. 8, 244\u2013263 (1986)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"key":"210_CR11","doi-asserted-by":"crossref","unstructured":"Crafa, S., Ranzato, F.: A spectrum of behavioral relations over LTSs on probability distributions. In: Proceedings of the 22nd International Conference on Concurrency Theory (CONCUR 2011), vol. 6901 of LNCS, pp. 124\u2013139. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-23217-6_9"},{"key":"210_CR12","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P.R., Wolovick, N., Sanchez Terraf, P., Celayes, P.: Nondeterministic labeled Markov processes: bisimulations and logical characterizations. In: Proceedings of the 6th International Conference on the Quantitative Evaluation of Systems (QEST 2009), pp. 11\u201320. IEEE-CS Press (2009)","DOI":"10.1109\/QEST.2009.17"},{"issue":"3:7","key":"210_CR13","first-page":"1","volume":"4","author":"L Alfaro de","year":"2008","unstructured":"de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Log. Methods Comput. Sci. 4(3:7), 1\u201328 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"210_CR14","doi-asserted-by":"crossref","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.: Three logics for branching bisimulation. J. ACM 42, 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"210_CR15","volume-title":"Finite State Markovian Decision Processes","author":"C Derman","year":"1970","unstructured":"Derman, C.: Finite State Markovian Decision Processes. Academic Press, London (1970)"},{"key":"210_CR16","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1006\/inco.2001.2962","volume":"179","author":"J Desharnais","year":"2002","unstructured":"Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179, 163\u2013193 (2002)","journal-title":"Inf. Comput."},{"key":"210_CR17","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1016\/S0890-5401(03)00051-8","volume":"184","author":"J Desharnais","year":"2003","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating labelled Markov processes. Inf. Comput. 184, 160\u2013200 (2003)","journal-title":"Inf. Comput."},{"key":"210_CR18","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/j.ic.2009.11.002","volume":"208","author":"J Desharnais","year":"2010","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Weak bisimulation is sound and complete for pCTL*. Inf. Comput. 208, 203\u2013219 (2010)","journal-title":"Inf. Comput."},{"key":"210_CR19","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/S0304-3975(99)00035-3","volume":"221","author":"EP Vink de","year":"1999","unstructured":"de Vink, E.P., Rutten, J.J.M.M.: Bisimulation for probabilistic transition systems: a coalgebraic approach. Theor. Comput. Sci. 221, 271\u2013293 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"210_CR20","doi-asserted-by":"crossref","unstructured":"Giry, M.: A categorical approach to probability theory. In: Proceedings of the International Conference on Categorical Aspects of Topology and Analysis, vol. 915 of LNM, pp. 68\u201385. Springer, Berlin (1981)","DOI":"10.1007\/BFb0092872"},{"key":"210_CR21","doi-asserted-by":"crossref","first-page":"1069","DOI":"10.1093\/logcom\/exn092","volume":"20","author":"R Goldblatt","year":"2010","unstructured":"Goldblatt, R.: Deduction systems for coalgebras over measurable spaces. J. Log. Comput. 20, 1069\u20131100 (2010)","journal-title":"J. Log. Comput."},{"key":"210_CR22","doi-asserted-by":"crossref","unstructured":"Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proceedings of the 11th IEEE Real-Time Systems Symposium (RTSS 1990), pp. 278\u2013287. IEEE-CS Press (1990)","DOI":"10.1109\/REAL.1990.128759"},{"key":"210_CR23","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6, 512\u2013535 (1994)","journal-title":"Formal Asp. Comput."},{"key":"210_CR24","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1007\/s00165-012-0242-7","volume":"24","author":"M Hennessy","year":"2012","unstructured":"Hennessy, M.: Exploring probabilistic bisimulations, part I. Formal Asp. Comput. 24, 749\u2013768 (2012)","journal-title":"Formal Asp. Comput."},{"key":"210_CR25","doi-asserted-by":"crossref","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. J. ACM 32, 137\u2013162 (1985)","journal-title":"J. ACM"},{"key":"210_CR26","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1016\/j.ic.2010.11.024","volume":"209","author":"H Hermanns","year":"2011","unstructured":"Hermanns, H., Parma, A., Segala, R., Wachter, B., Zhang, L.: Probabilistic logical characterization. Inf. Comput. 209, 154\u2013172 (2011)","journal-title":"Inf. Comput."},{"key":"210_CR27","volume-title":"An Introduction to Modal Logic","author":"GE Hughes","year":"1977","unstructured":"Hughes, G.E., Creswell, M.J.: An Introduction to Modal Logic. Methuen, London (1977)"},{"key":"210_CR28","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"H Jifeng","year":"1997","unstructured":"Jifeng, H., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Sci. Comput. Progr. 28, 171\u2013192 (1997)","journal-title":"Sci. Comput. Progr."},{"key":"210_CR29","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19, 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"210_CR30","doi-asserted-by":"crossref","unstructured":"Klin, B.: Coalgebraic modal logic beyond sets. In: Proceedings of the 23rd International Conference on the Mathematical Foundations of Programming Semantics (MFPS 2007), vol. 173 of ENTCS, pp. 177\u2013201. Elsevier, Amsterdam (2007)","DOI":"10.1016\/j.entcs.2007.02.034"},{"key":"210_CR31","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1093\/logcom\/exn094","volume":"20","author":"A Kurz","year":"2010","unstructured":"Kurz, A., Palmigiano, A., Venema, Y.: Coalgebra and logic: a brief overview. J. Log. Comput. 20, 985\u2013990 (2010)","journal-title":"J. Log. Comput."},{"key":"210_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"210_CR33","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Compositional verification of probabilistic processes. In: Proceedings of the 3rd International Conference on Concurrency Theory (CONCUR 1992), vol. 630 of LNCS, pp. 456\u2013471. Springer, Berlin (1992)","DOI":"10.1007\/BFb0084809"},{"key":"210_CR34","doi-asserted-by":"crossref","unstructured":"Parma, A., Segala, R.: Logical characterizations of bisimulations for discrete probabilistic systems. In: Proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2007), vol. 4423 of LNCS, pp. 287\u2013301. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-71389-0_21"},{"key":"210_CR35","doi-asserted-by":"crossref","unstructured":"Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR 2000), vol. 1877 of LNCS, pp. 334\u2013349. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44618-4_25"},{"key":"210_CR36","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1016\/S0019-9958(63)90290-0","volume":"6","author":"MO Rabin","year":"1963","unstructured":"Rabin, M.O.: Probabilistic automata. Inf. Control 6, 230\u2013245 (1963)","journal-title":"Inf. Control"},{"key":"210_CR37","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD Thesis (1995)"},{"key":"210_CR38","doi-asserted-by":"crossref","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. In: Proceedings of the 5th International Conference on Concurrency Theory (CONCUR 1994), vol. 836 of LNCS, pp. 481\u2013496. Springer, Berlin (1994)","DOI":"10.1007\/978-3-540-48654-1_35"},{"key":"210_CR39","doi-asserted-by":"crossref","unstructured":"Segala, R., Turrini, A.: Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In: Proceedings of the 2nd International Conference on the Quantitative Evaluation of Systems (QEST 2005), pp. 44\u201353. IEEE-CS Press (2005)","DOI":"10.1109\/QEST.2005.9"},{"key":"210_CR40","doi-asserted-by":"crossref","unstructured":"Sokolova, A., de Vink, E.P.: Probabilistic automata: System types, parallel composition and comparison. In: Validation of Stochastic Systems, vol. 2925 of LNCS, pp. 1\u201343. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24611-4_1"},{"issue":"2:7","key":"210_CR41","first-page":"1","volume":"9","author":"L Song","year":"2013","unstructured":"Song, L., Zhang, L., Godskesen, J.C., Nielson, F.: Bisimulations meet PCTL equivalences for probabilistic automata. Log. Methods Comput. Sci. 9(2:7), 1\u201334 (2013)","journal-title":"Log. Methods Comput. Sci."},{"key":"210_CR42","doi-asserted-by":"crossref","unstructured":"Tracol, M., Desharnais, J., Zhioua, A.: Computing distances between probabilistic automata. In: Proceedings of the 9th International Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), vol. 57 of EPTCS, pp. 148\u2013162 (2011)","DOI":"10.4204\/EPTCS.57.11"},{"key":"210_CR43","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the 26th IEEE Symposium on Foundations of Computer Science (FOCS 1985), pp. 327\u2013338. IEEE-CS Press (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"210_CR44","unstructured":"van Benthem, J.: Modal Correspondence Theory. PhD Thesis (1976)"},{"key":"210_CR45","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"RJ Glabbeek van","year":"1995","unstructured":"van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121, 59\u201380 (1995)","journal-title":"Inf. Comput."},{"key":"210_CR46","doi-asserted-by":"crossref","unstructured":"Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. In: Proceedings of the 12th International Symposium on Protocol Specification, Testing and Verification (PSTV 1992), pp. 47\u201361. North-Holland (1992)","DOI":"10.1016\/B978-0-444-89874-6.50010-6"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-014-0210-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-014-0210-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-014-0210-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T00:28:07Z","timestamp":1566088087000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-014-0210-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,30]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["210"],"URL":"https:\/\/doi.org\/10.1007\/s00236-014-0210-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,11,30]]}}}