{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:43Z","timestamp":1760202763739,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2018,2,24]],"date-time":"2018-02-24T00:00:00Z","timestamp":1519430400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001809","name":"the National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61532019","61472473"],"award-info":[{"award-number":["61532019","61472473"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"name":"the National 973 Program","award":["2014CB340701"],"award-info":[{"award-number":["2014CB340701"]}]},{"DOI":"10.13039\/501100005231","name":"the CAS\/SAFEA International Partnership Program for Creative Research Team","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005231","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2018,9]]},"DOI":"10.1007\/s00236-018-0313-1","type":"journal-article","created":{"date-parts":[[2018,2,24]],"date-time":"2018-02-24T05:30:01Z","timestamp":1519450201000},"page":"461-488","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Probabilistic bisimulation for realistic schedulers"],"prefix":"10.1007","volume":"55","author":[{"given":"Lijun","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pengfei","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lei","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Eisentraut","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David N.","family":"Jansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens Chr.","family":"Godskesen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,2,24]]},"reference":[{"issue":"2","key":"313_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. 200(2), 149\u2013214 (2005)","journal-title":"Inf. Comput."},{"key":"313_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. 546, 63\u201392 (2014)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"313_CR3","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1287\/moor.27.4.819.297","volume":"27","author":"DS 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. 27(4), 819\u2013840 (2002)","journal-title":"Math. Oper. Res."},{"issue":"2","key":"313_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 Secur. Comput. 7(2), 128\u2013143 (2010)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"313_CR5","unstructured":"Brengel, M.: Probabilistic weak transitions. Bachelor\u2019s thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2013)"},{"key":"313_CR6","doi-asserted-by":"crossref","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: CONCUR, pp. 371\u2013385 (2002)","DOI":"10.1007\/3-540-45694-5_25"},{"key":"313_CR7","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the $$\\text{PowerScale}^{{\\rm TM}}$$ PowerScale 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":"313_CR8","unstructured":"De Alfaro, L.: The verification of probabilistic systems under memoryless partial-information policies is hard. Technical report, DTIC document (1999)"},{"key":"313_CR9","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. Inf. Comput. 222, 139\u2013168 (2013)","journal-title":"Inf. Comput."},{"key":"313_CR10","doi-asserted-by":"crossref","unstructured":"Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes. In: CONCUR, pp. 274\u2013288 (2009)","DOI":"10.1007\/978-3-642-04081-8_19"},{"issue":"2","key":"313_CR11","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 $$\\text{ pCTL }^{\\text{* }}$$ pCTL * . Inf. Comput. 208(2), 203\u2013219 (2010). https:\/\/doi.org\/10.1016\/j.ic.2009.11.002","journal-title":"Inf. Comput."},{"issue":"2","key":"313_CR12","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 $$\\text{ pCTL }^{\\text{* }}$$ pCTL * . Inf. Comput. 208(2), 203\u2013219 (2010)","journal-title":"Inf. Comput."},{"issue":"3","key":"313_CR13","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. 19(3), 549\u2013563 (2008)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"313_CR14","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: CONCUR, pp. 21\u201339 (2010)","DOI":"10.1007\/978-3-642-15375-4_3"},{"key":"313_CR15","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":"313_CR16","doi-asserted-by":"publisher","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11\u201314 July 2010, pp 342\u2013351. IEEE Computer Society, Edinburgh (2010). https:\/\/doi.org\/10.1109\/LICS.2010.41","DOI":"10.1109\/LICS.2010.41"},{"key":"313_CR17","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J., Zhang, L.: A semantics for every GSPN. In: PETRI NETS. Lecture Notes in Computer Science, vol. 7927, pp. 90\u2013109. Springer (2013)","DOI":"10.1007\/978-3-642-38697-8_6"},{"key":"313_CR18","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Kraemer, J., Turrini, A., Zhang, L.: Deciding bisimilarities on distributions. In: QEST. Lecture Notes in Computer Science, vol. 8054, pp. 72\u201388. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-40196-1_6"},{"key":"313_CR19","unstructured":"Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Late weak bisimulation for Markov automata. CoRR arXiv:1202.4116 (2014)"},{"key":"313_CR20","unstructured":"Eisentraut, C.G.: Principles of Markov automata. Ph.D. thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2017)"},{"key":"313_CR21","doi-asserted-by":"publisher","unstructured":"Feng, Y., Zhang, L.: When equivalence and bisimulation join forces in probabilistic automata. In: FM, Lecture Notes in Computer Science, vol. 8442, pp. 247\u2013262. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_18","DOI":"10.1007\/978-3-319-06410-9_18"},{"key":"313_CR22","doi-asserted-by":"crossref","unstructured":"Feng, Y., Song, L., Zhang, L.: Distribution-based bisimulation and bisimulation metric in probabilistic automata. CoRR arXiv:1512.05027 (2015)","DOI":"10.1007\/978-3-319-06410-9_18"},{"key":"313_CR23","doi-asserted-by":"crossref","unstructured":"Giro, S., D\u2019Argenio, P.R.: Quantitative model checking revisited: neither decidable nor approximable. In: FORMATS. Lecture Notes in Computer Science, vol. 4763, pp. 179\u2013194. Springer (2007)","DOI":"10.1007\/978-3-540-75454-1_14"},{"key":"313_CR24","doi-asserted-by":"publisher","unstructured":"Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An $$o(m \\log n)$$ o ( m log n ) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. (2017). https:\/\/doi.org\/10.1145\/3060140 , article 13","DOI":"10.1145\/3060140"},{"key":"313_CR25","doi-asserted-by":"crossref","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of Markov reward automata. In: ATVA. Lecture Notes in Computer Science, vol. 8837, pp. 168\u2013184. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_13"},{"key":"313_CR26","volume-title":"Measure Theory","author":"PR Halmos","year":"1974","unstructured":"Halmos, P.R.: Measure Theory, vol. 1950. Springer, New York (1974)"},{"key":"313_CR27","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\/2676726.2676998"},{"issue":"4\u20136","key":"313_CR28","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. Form. Asp. Comput. 24(4\u20136), 749\u2013768 (2012)","journal-title":"Form. Asp. Comput."},{"key":"313_CR29","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, Berlin (2002)"},{"key":"313_CR30","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J.: Probabilistic bisimulation: naturally on distributions. In: CONCUR. Lecture Notes in Computer Science, vol. 8704. Springer (2014)","DOI":"10.1007\/978-3-662-44584-6_18"},{"key":"313_CR31","doi-asserted-by":"crossref","unstructured":"Honda, K., Tokoro, M.: On asynchronous communication semantics. In: Object-Based Concurrent Computing, pp. 21\u201351 (1991)","DOI":"10.1007\/3-540-55613-3_2"},{"key":"313_CR32","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: TACAS, Lecture Notes in Computer Science, vol. 6015, pp. 23\u201337. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"313_CR33","doi-asserted-by":"crossref","unstructured":"Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: CONCUR, pp. 334\u2013349 (2000)","DOI":"10.1007\/3-540-44618-4_25"},{"key":"313_CR34","volume-title":"Real and Complex Analysis","author":"W Rudin","year":"2006","unstructured":"Rudin, W.: Real and Complex Analysis. Tata McGraw-Hill Education, Delhi (2006)"},{"key":"313_CR35","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. Inf. Comput. 237, 151\u2013173 (2014)","journal-title":"Inf. Comput."},{"key":"313_CR36","doi-asserted-by":"crossref","unstructured":"Segala, R.: A compositional trace-based semantics for probabilistic automata. In: CONCUR. Lecture Notes in Computer Science, vol. 962, pp. 234\u2013248. Springer (1995)","DOI":"10.1007\/3-540-60218-6_17"},{"key":"313_CR37","unstructured":"Segala, R.: Modeling and verification of randomized distributed realtime systems. Ph.D. thesis, MIT (1995)"},{"key":"313_CR38","unstructured":"Song, L., Feng, Y., Zhang, L.: Decentralized bisimulation for multiagent systems. In: AAMAS\u201915: Autonomous Agents and Multiagent Systems, pp. 209\u2013217. ACM, New York (2015)"},{"key":"313_CR39","doi-asserted-by":"crossref","unstructured":"Timmer, M., van de Pol, J., Stoelinga, M.: Confluence reduction for Markov automata. In: FORMATS. Lecture Notes in Computer Science, vol. 8053, pp. 243\u2013257. Springer (2013)","DOI":"10.1007\/978-3-642-40229-6_17"},{"issue":"3","key":"313_CR40","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, P.W.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996). https:\/\/doi.org\/10.1145\/233551.233556","journal-title":"J. ACM"},{"key":"313_CR41","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-65765-3_10","volume-title":"Formal Modeling and Analysis of Timed Systems: FORMATS. Lecture Notes in Computer Science","author":"P Yang","year":"2017","unstructured":"Yang, P., Jansen, D.N., Zhang, L.: Distribution-based bisimulation for labelled Markov processes. In: Abate, A., Geeraerts, G. (eds.) Formal Modeling and Analysis of Timed Systems: FORMATS. Lecture Notes in Computer Science, vol. 10419, pp. 170\u2013186. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-65765-3_10"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-018-0313-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-018-0313-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-018-0313-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,14]],"date-time":"2022-08-14T21:10:44Z","timestamp":1660511444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-018-0313-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,24]]},"references-count":41,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,9]]}},"alternative-id":["313"],"URL":"https:\/\/doi.org\/10.1007\/s00236-018-0313-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2018,2,24]]},"assertion":[{"value":"23 May 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 January 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 February 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}