{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T09:51:47Z","timestamp":1764841907234,"version":"3.40.3"},"publisher-location":"Cham","reference-count":46,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319476766"},{"type":"electronic","value":"9783319476773"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47677-3_5","type":"book-chapter","created":{"date-parts":[[2016,10,5]],"date-time":"2016-10-05T06:17:10Z","timestamp":1475648230000},"page":"67-84","source":"Crossref","is-referenced-by-count":7,"title":["Behavioural Pseudometrics for Nondeterministic Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Wenjie","family":"Du","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuxin","family":"Deng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Gebler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,6]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Castiglioni, V., Gebler, D., Tini, S.: Logical characterization of bisimulation metrics. In: Proceedings of QAPL 2016. EPTCS (2016)","DOI":"10.4204\/EPTCS.227.4"},{"issue":"3:13","key":"5_CR2","first-page":"1","volume":"6","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., De Alfaro, L., Majumdar, R., Raman, V.: Algorithms for game metrics. Log. Methods Comput. Sci. 6(3:13), 1\u201327 (2010)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2\u20133","key":"5_CR3","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1016\/j.tcs.2005.03.048","volume":"342","author":"R Cleaveland","year":"2005","unstructured":"Cleaveland, R., Iyer, S.P., Narasimha, M.: Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci. 342(2\u20133), 316\u2013350 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"5_CR4","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1017\/S0960129511000454","volume":"22","author":"PR D\u2019Argenio","year":"2012","unstructured":"D\u2019Argenio, P.R., S\u00e1nchez Terraf, P., Wolovick, N.: Bisimulations for non-deterministic labelled Markov processes. Math. Struct. Comput. Sci. 22(1), 43\u201368 (2012)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2","key":"5_CR5","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1109\/TSE.2008.106","volume":"35","author":"L Alfaro De","year":"2009","unstructured":"De Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Softw. Eng. 35(2), 258\u2013273 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"De Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game relations and metrics. In: Proceedings of LICS 2007, pp. 99\u2013108. IEEE (2007)","DOI":"10.1109\/LICS.2007.22"},{"issue":"3:7","key":"5_CR7","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."},{"issue":"1\/2","key":"5_CR8","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(1\/2), 271\u2013293 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR9","unstructured":"den Hartog, J.I.: Probabilistic Extensions of Semantical Models. Ph.D. thesis, Free University Amsterdam (2002)"},{"key":"5_CR10","volume-title":"Semantics of Probabilistic Processes: An Operational Approach","author":"Y Deng","year":"2015","unstructured":"Deng, Y.: Semantics of Probabilistic Processes: An Operational Approach. Springer, Heidelberg (2015)"},{"issue":"2","key":"5_CR11","first-page":"79","volume":"153","author":"Y Deng","year":"2006","unstructured":"Deng, Y., Chothia, T., Palamidessi, C., Pang, J.: Metrics for action-labelled quantitative transition systems. ENTCS 153(2), 79\u201396 (2006)","journal-title":"ENTCS"},{"key":"5_CR12","unstructured":"Deng, Y., Du, W.: Logical, metric, and algorithmic characterisations of probabilistic bisimulation. Technical report CMU-CS-11-110, Carnegie Mellon University, March 2011"},{"key":"5_CR13","unstructured":"Deng, Y., Feng, Y., Dal Lago, U.: On coinduction and quantum lambda calculi. In: Proceedings of CONCUR 2015, pp. 427\u2013440. LIPIcs (2015)"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/j.ic.2012.10.010","volume":"222","author":"Y Deng","year":"2013","unstructured":"Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222, 139\u2013168 (2013)","journal-title":"Inf. Comput."},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-04081-8_19","volume-title":"CONCUR 2009-Concurrency Theory","author":"Y Deng","year":"2009","unstructured":"Deng, Y., Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 274\u2013288. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04081-8_19"},{"issue":"3","key":"5_CR16","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/j.tcs.2003.09.013","volume":"318","author":"J Desharnais","year":"2004","unstructured":"Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323\u2013354 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proceedings of LICS 2002, pp. 413\u2013422. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029849"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-319-19249-9_16","volume-title":"FM 2015: Formal Methods","author":"C Eisentraut","year":"2015","unstructured":"Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Probabilistic bisimulation for realistic schedulers. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 248\u2013264. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-19249-9_16"},{"key":"5_CR19","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1016\/j.tcs.2013.07.030","volume":"538","author":"U Fahrenberg","year":"2014","unstructured":"Fahrenberg, U., Legay, A.: The quantitative linear-time branching-time spectrum. Theor. Comput. Sci. 538, 54\u201369 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR20","unstructured":"Feng, Y., Ying, M.: Toward automatic verification of quantum cryptographic protocols. In: Proceedings of CONCUR 2015. LIPIcs, vol. 42, pp. 441\u2013455 (2015)"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-06410-9_18","volume-title":"FM 2014: Formal Methods","author":"Y Feng","year":"2014","unstructured":"Feng, Y., Zhang, L.: When equivalence and bisimulation join forces in probabilistic automata. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 247\u2013262. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-06410-9_18"},{"issue":"6","key":"5_CR22","doi-asserted-by":"crossref","first-page":"1662","DOI":"10.1137\/10080484X","volume":"40","author":"N Ferns","year":"2011","unstructured":"Ferns, N., Panangaden, P., Precup, D.: Bisimulation metrics for continuous Markov decision processes. SIAM J. Comput. 40(6), 1662\u20131714 (2011)","journal-title":"SIAM J. Comput."},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-319-06880-0_17","volume-title":"Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday","author":"N Ferns","year":"2014","unstructured":"Ferns, N., Precup, D., Knight, S.: Bisimulation for Markov decision processes through families of functional expressions. In: Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday. LNCS, vol. 8464, pp. 319\u2013342. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-06880-0_17"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-662-46678-0_15","volume-title":"Foundations of Software Science and Computation Structures","author":"D Gebler","year":"2015","unstructured":"Gebler, D., Larsen, K.G., Tini, S.: Compositional metric reasoning with probabilistic process calculi. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 230\u2013245. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46678-0_15"},{"key":"5_CR25","unstructured":"Giacalone, A., Jou, C., Smolka, S.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods, pp. 443\u2013458 (1990)"},{"issue":"4\u20136","key":"5_CR26","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 Aspects Comput. 24(4\u20136), 749\u2013768 (2012)","journal-title":"Formal Aspects Comput."},{"key":"5_CR27","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\u2013161 (1985)","journal-title":"J. ACM"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-662-44584-6_18","volume-title":"CONCUR 2014\u2013Concurrency Theory","author":"H Hermanns","year":"2014","unstructured":"Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249\u2013265. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-44584-6_18"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Huth, M., Kwiatkowska, M.Z.: Quantitative analysis and model checking. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, pp. 111\u2013122. IEEE Computer Society (1997)","DOI":"10.1109\/LICS.1997.614940"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G., Yi, W.: Probabilistic extensions of process algebras. In: Handbook of Process Algebra, pp. 685\u2013710. Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044482830-9\/50029-1"},{"issue":"7","key":"5_CR31","first-page":"52","volume":"13","author":"L Kantorovich","year":"1958","unstructured":"Kantorovich, L., Rubinshtein, G.: On a space of totally additive functions. Vestn Len. Univ. 13(7), 52\u201359 (1958)","journal-title":"Vestn Len. Univ."},{"key":"5_CR32","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-61550-4_167","volume-title":"Mathematical Foundations of Computer Science 1996","author":"M Kwiatkowska","year":"1996","unstructured":"Kwiatkowska, M., Norman, G.: Probabilistic metric semantics for a simple language with recursion. In: Penczek, W., Sza\u0142as, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 419\u2013430. Springer, Heidelberg (1996). doi: 10.1007\/3-540-61550-4_167"},{"key":"5_CR34","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":"5_CR35","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)"},{"key":"5_CR36","unstructured":"Norman, G.J.: Metric Semantics for Reactive Probabilistic Systems. Ph.D. thesis, University of Birmingham (1997)"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-44618-4_25","volume-title":"CONCUR 2000\u2014Concurrency Theory","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). doi: 10.1007\/3-540-44618-4_25"},{"key":"5_CR38","unstructured":"Raman, V.: Game Relations, Metrics and Refinements. Ph.D. thesis, University of California (2010)"},{"key":"5_CR39","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT (1995)"},{"key":"5_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-540-48654-1_35","volume-title":"CONCUR\u201994: Concurrency Theory","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). doi: 10.1007\/978-3-540-48654-1_35"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Song, L., Deng, Y., Cai, X.: Towards automatic measurement of probabilistic processes. In: Proceedings of QSIC 2007, pp. 50\u201359. IEEE (2007)","DOI":"10.1109\/QSIC.2007.4385480"},{"issue":"2:2","key":"5_CR42","first-page":"1","volume":"4","author":"F Breugel van","year":"2008","unstructured":"van Breugel, F., Sharma, B., Worrell, J.: Approximating a behavioural pseudometric without discount for probabilistic systems. Log. Methods Comput. Sci. 4(2:2), 1\u201323 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"5_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/3-540-44685-0_23","volume-title":"CONCUR 2001\u2014Concurrency Theory","author":"F Breugel","year":"2001","unstructured":"Breugel, F., Worrell, J.: An algorithm for quantitative verification of probabilistic transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 336\u2013350. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44685-0_23"},{"key":"5_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-48224-5_35","volume-title":"Automata, Languages and Programming","author":"F Breugel","year":"2001","unstructured":"Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. In: Orejas, F., Spirakis, P.G., Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 421\u2013432. Springer, Heidelberg (2001). doi: 10.1007\/3-540-48224-5_35"},{"issue":"1","key":"5_CR45","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.tcs.2004.09.035","volume":"331","author":"F Breugel van","year":"2005","unstructured":"van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331(1), 115\u2013142 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"1\/2","key":"5_CR46","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(01)00124-4","volume":"275","author":"M Ying","year":"2002","unstructured":"Ying, M.: Bisimulation indexes and their applications. Theor. Comput. Sci. 275(1\/2), 1\u201368 (2002)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47677-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:24:22Z","timestamp":1498335862000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47677-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319476766","9783319476773"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47677-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}