{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:34:27Z","timestamp":1743140067283,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_16","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"248-264","source":"Crossref","is-referenced-by-count":3,"title":["Probabilistic Bisimulation for Realistic Schedulers"],"prefix":"10.1007","author":[{"given":"Christian","family":"Eisentraut","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens Chr.","family":"Godskesen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"16_CR1","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. Inf. Comput.\u00a0200(2), 149\u2013214 (2005)","journal-title":"Inf. Comput."},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/j.tcs.2014.03.001","volume":"546","author":"M. Bernardo","year":"2014","unstructured":"Bernardo, M., De Nicola, R., Loreti, M.: Relating strong behavioral equivalences for processes with nondeterminism and probabilities. Theor. Comput. Sci.\u00a0546, 63\u201392 (2014)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"16_CR3","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1287\/moor.27.4.819.297","volume":"27","author":"D.S. Bernstein","year":"2002","unstructured":"Bernstein, D.S., Givan, R., Immerman, N., Zilberstein, S.: The complexity of decentralized control of Markov decision processes. Math. Oper. Res.\u00a027(4), 819\u2013840 (2002)","journal-title":"Math. Oper. Res."},{"issue":"2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H. Boudali","year":"2010","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Sec. Comput.\u00a07(2), 128\u2013143 (2010)","journal-title":"IEEE Trans. Dependable Sec. Comput."},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45694-5_25","volume-title":"CONCUR 2002 - Concurrency Theory","author":"S. Cattani","year":"2002","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 371\u2013385. Springer, Heidelberg (2002)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and Verification of the PowerScale$^{\\scriptsize{\\mbox{TM}}}$ bus arbitration protocol: An industrial experiment with lotos. In: FORTE, pp. 435\u2013450 (1996)","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"16_CR7","unstructured":"De Alfaro, L.: The verification of probabilistic systems under memoryless partial-information policies is hard. Technical report, DTIC Document (1999)"},{"key":"16_CR8","doi-asserted-by":"publisher","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. Information and Computation\u00a0222, 139\u2013168 (2013)","journal-title":"Information and Computation"},{"key":"16_CR9","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., van Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 274\u2013288. Springer, Heidelberg (2009)"},{"issue":"2","key":"16_CR10","doi-asserted-by":"publisher","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.\u00a0208(2), 203\u2013219 (2010)","journal-title":"Inf. Comput."},{"issue":"3","key":"16_CR11","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1142\/S0129054108005814","volume":"19","author":"L. Doyen","year":"2008","unstructured":"Doyen, L., Henzinger, T.A., Raskin, J.: Equivalence of labeled Markov chains. Int. J. Found. Comput. Sci.\u00a019(3), 549\u2013563 (2008)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"16_CR12","unstructured":"Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Late Weak Bisimulation for Markov Automata. CoRR, abs\/1202.4116 (2014), \n                        http:\/\/arxiv.org\/abs\/1202.4116"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-38697-8_6","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"C. Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J.-P., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol.\u00a07927, pp. 90\u2013109. Springer, Heidelberg (2013)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-40196-1_6","volume-title":"Quantitative Evaluation of Systems","author":"C. Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Kr\u00e4mer, J., Turrini, A., Zhang, L.: Deciding bisimilarities on distributions. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol.\u00a08054, pp. 72\u201388. Springer, Heidelberg (2013)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-15375-4_3","volume-title":"CONCUR 2010 - Concurrency Theory","author":"C. Eisentraut","year":"2010","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 21\u201339. Springer, Heidelberg (2010)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351 (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"16_CR17","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.\u00a08442, pp. 247\u2013262. Springer, Heidelberg (2014)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-540-75454-1_14","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Giro","year":"2007","unstructured":"Giro, S., D\u2019Argenio, P.R.: Quantitative model checking revisited: neither decidable nor approximable. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol.\u00a04763, pp. 179\u2013194. Springer, Heidelberg (2007)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-11936-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"D. Guck","year":"2014","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol.\u00a08837, pp. 168\u2013184. Springer, Heidelberg (2014)"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Halmos, P.R.: Measure theory, vol.\u00a01950. Springer (1974)","DOI":"10.1007\/978-1-4684-9440-2"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"He, F., Gao, X., Wang, B., Zhang, L.: Leveraging weighted automata in compositional reasoning about concurrent probabilistic systems. In: POPL, pp. 503\u2013514. ACM (2015)","DOI":"10.1145\/2775051.2676998"},{"issue":"4-6","key":"16_CR22","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 Asp. Comput.\u00a024(4-6), 749\u2013768 (2012)","journal-title":"Formal Asp. Comput."},{"key":"16_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov chains: and the quest for quantified quality","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov chains: and the quest for quantified quality. Springer, Heidelberg (2002)"},{"key":"16_CR24","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 \u2013 Concurrency 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.\u00a08704, pp. 249\u2013265. Springer, Heidelberg (2014)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-55613-3_2","volume-title":"Object-Based Concurrent Computing","author":"K. Honda","year":"1992","unstructured":"Honda, K., Tokoro, M.: On asynchronous communication semantics. In: Zatarain-Cabada, R., Wang, J. (eds.) ECOOP-WS 1991. LNCS, vol.\u00a0612, pp. 21\u201351. Springer, Heidelberg (1992)"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-12002-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Kwiatkowska","year":"2010","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 23\u201337. Springer, Heidelberg (2010)"},{"key":"16_CR27","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 - Concurrency 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.\u00a01877, pp. 334\u2013349. Springer, Heidelberg (2000)"},{"key":"16_CR28","unstructured":"Rudin, W.: Real and complex analysis. Tata McGraw-Hill Education (2006)"},{"key":"16_CR29","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/j.ic.2014.02.001","volume":"237","author":"J. Schuster","year":"2014","unstructured":"Schuster, J., Siegle, M.: Markov automata: Deciding weak bisimulation by means of non-navely vanishing states. Information and Computation\u00a0237, 151\u2013173 (2014)","journal-title":"Information and Computation"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-60218-6_17","volume-title":"CONCUR \u201995 Concurrency Theory","author":"R. Segala","year":"1995","unstructured":"Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 234\u2013248. Springer, Heidelberg (1995)"},{"key":"16_CR31","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Realtime Systems. PhD thesis. MIT (1995)"},{"key":"16_CR32","unstructured":"Song, L., Feng, Y., Zhang, L.: Decentralized bisimulation for multiagent systems. In: AAMAS, pp. 209\u2013217. IFAAMAS (2015)"},{"key":"16_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-40229-6_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Timmer","year":"2013","unstructured":"Timmer, M., van de Pol, J., Stoelinga, M.I.A.: Confluence reduction for markov automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol.\u00a08053, pp. 243\u2013257. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T08:23:07Z","timestamp":1676017387000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}