{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:36:22Z","timestamp":1767137782620,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319051185","type":"print"},{"value":"9783319051192","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05119-2_18","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T04:36:28Z","timestamp":1394166988000},"page":"315-330","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bernardo","sequence":"first","affiliation":[]},{"given":"Rocco","family":"De Nicola","sequence":"additional","affiliation":[]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"18_CR1","series-title":"LNCS","first-page":"155","volume-title":"CAV 1995","author":"A Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: the temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"key":"18_CR2","doi-asserted-by":"publisher","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":"18_CR3","unstructured":"Bernardo, M., De Nicola, R., Loreti, M.: Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes. Technical report 06\/2013, IMT Institute for Advanced Studies Lucca (2013). http:\/\/eprints.imtlucca.it\/1553\/"},{"key":"18_CR4","series-title":"LNCS","first-page":"499","volume-title":"FSTTCS 1995","author":"A Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M Browne","year":"1988","unstructured":"Browne, M., Clarke, E., Gr\u00fcmberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115\u2013131 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E Clarke","year":"1986","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-23217-6_9","volume-title":"CONCUR 2011","author":"S Crafa","year":"2011","unstructured":"Crafa, S., Ranzato, F.: A spectrum of behavioral relations over LTSs on probability distributions. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 124\u2013139. Springer, Heidelberg (2011)"},{"issue":"3\u20137","key":"18_CR8","first-page":"1","volume":"4","author":"L de Alfaro","year":"2008","unstructured":"de Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Logical Meth. Comput. Sci. 4(3\u20137), 1\u201328 (2008)","journal-title":"Logical Meth. Comput. Sci."},{"key":"18_CR9","volume-title":"Finite State Markovian Decision Processes","author":"C Derman","year":"1970","unstructured":"Derman, C.: Finite State Markovian Decision Processes. Academic Press, New York (1970)"},{"key":"18_CR10","doi-asserted-by":"publisher","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":"18_CR11","doi-asserted-by":"crossref","unstructured":"Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proceedings of RTSS 1990, pp. 278\u2013287. IEEE-CS Press (1990)","DOI":"10.1109\/REAL.1990.128759"},{"key":"18_CR12","doi-asserted-by":"publisher","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 Aspects Comput. 24, 749\u2013768 (2012)","journal-title":"Formal Aspects Comput."},{"key":"18_CR13","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. J. ACM 32, 137\u2013162 (1985)","journal-title":"J. ACM"},{"key":"18_CR14","doi-asserted-by":"publisher","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":"18_CR15","doi-asserted-by":"publisher","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. Program. 28, 171\u2013192 (1997)","journal-title":"Sci. Comput. Program."},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"R Keller","year":"1976","unstructured":"Keller, R.: Formal verification of parallel programs. Commun. ACM 19, 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K Larsen","year":"1991","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"18_CR18","series-title":"LNCS","first-page":"456","volume-title":"CONCUR 1992","author":"K Larsen","year":"1992","unstructured":"Larsen, K., Skou, A.: Compositional verification of probabilistic processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 456\u2013471. Springer, Heidelberg (1992)"},{"key":"18_CR19","series-title":"LNCS","first-page":"287","volume-title":"FOSSACS 2007","author":"A Parma","year":"2007","unstructured":"Parma, A., Segala, R.: Logical characterizations of bisimulations for discrete probabilistic systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 287\u2013301. Springer, Heidelberg (2007)"},{"key":"18_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-44618-4_25","volume-title":"CONCUR 2000","author":"A Philippou","year":"2000","unstructured":"Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334\u2013349. Springer, Heidelberg (2000)"},{"key":"18_CR21","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/S0019-9958(63)90290-0","volume":"6","author":"M Rabin","year":"1963","unstructured":"Rabin, M.: Probabilistic automata. Inf. Control 6, 230\u2013245 (1963)","journal-title":"Inf. Control"},{"key":"18_CR22","unstructured":"Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis (1995)"},{"key":"18_CR23","series-title":"LNCS","first-page":"481","volume-title":"CONCUR 1994","author":"R Segala","year":"1994","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481\u2013496. Springer, Heidelberg (1994)"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Segala, R., Turrini, A.: Comparative analysis of bisimulation relations on alternating and non-alternating probabilistic models. In: Proceedings of QEST 2005, pp. 44\u201353. IEEE-CS Press (2005)","DOI":"10.1109\/QEST.2005.9"},{"key":"18_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24611-4_1","volume-title":"Validation of Stochastic Systems","author":"A Sokolova","year":"2004","unstructured":"Sokolova, A., de Vink, E.: Probabilistic automata: system types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1\u201343. Springer, Heidelberg (2004)"},{"key":"18_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-23217-6_8","volume-title":"CONCUR 2011","author":"L Song","year":"2011","unstructured":"Song, L., Zhang, L., Godskesen, J.C.: Bisimulations meet PCTL equivalences for probabilistic automata. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 108\u2013123. Springer, Heidelberg (2011)"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Tracol, M., Desharnais, J., Zhioua, A.: Computing distances between probabilistic automata. In: Proceedings of QAPL 2011. EPTCS, vol. 57, pp. 148\u2013162 (2011)","DOI":"10.4204\/EPTCS.57.11"},{"key":"18_CR28","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"R van Glabbeek","year":"1995","unstructured":"van Glabbeek, R., Smolka, S., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Inf. Comput. 121, 59\u201380 (1995)","journal-title":"Inf. Comput."},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of FOCS 1985, pp. 327\u2013338. IEEE-CS Press (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Yi, W., Larsen, K.: Testing probabilistic and nondeterministic processes. In: Proceedings of PSTV 1992, pp. 47\u201361. North-Holland (1992)","DOI":"10.1016\/B978-0-444-89874-6.50010-6"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05119-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,22]],"date-time":"2023-12-22T00:11:57Z","timestamp":1703203917000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05119-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319051185","9783319051192"],"references-count":30,"aliases":["10.1007\/978-3-319-14128-2_18"],"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05119-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}