{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:36Z","timestamp":1760202696685,"version":"3.37.3"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2016,3,1]],"date-time":"2016-03-01T00:00:00Z","timestamp":1456790400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Sino-German Center (CDZ)","award":["GZ 1023"],"award-info":[{"award-number":["GZ 1023"]}]},{"name":"DFG\/NWO","award":["ROCKS"],"award-info":[{"award-number":["ROCKS"]}]},{"name":"DFG","award":["SFB\/TR 14"],"award-info":[{"award-number":["SFB\/TR 14"]}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"crossref","award":["295261"],"award-info":[{"award-number":["295261"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["318490"],"award-info":[{"award-number":["318490"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002367","name":"Chinese Academy of Sciences","doi-asserted-by":"publisher","award":["2015VTC029"],"award-info":[{"award-number":["2015VTC029"]}],"id":[{"id":"10.13039\/501100002367","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61472473"],"award-info":[{"award-number":["61472473"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CAS\/SAFEA","award":["International Partnership Program for Creative Research Team"],"award-info":[{"award-number":["International Partnership Program for Creative Research Team"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61550110249"],"award-info":[{"award-number":["61550110249"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Weak probabilistic bisimulation on probabilistic automata can be decided by an algorithm that needs to check a polynomial number of linear programming problems encoding weak transitions. It is hence of polynomial complexity. This paper discusses the specific complexity class of the weak probabilistic bisimulation problem, and it considers several practical algorithms and linear programming problem transformations that enable an efficient solution. We then discuss two different implementations of a probabilistic automata weak probabilistic bisimulation minimizer, one of them employing SAT modulo linear arithmetic as the solver technology. Empirical results demonstrate the effectiveness of the minimization approach on standard benchmarks, also highlighting the benefits of compositional minimization.<\/jats:p>","DOI":"10.1007\/s00165-016-0356-4","type":"journal-article","created":{"date-parts":[[2016,2,19]],"date-time":"2016-02-19T10:40:34Z","timestamp":1455878434000},"page":"109-143","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Deciding probabilistic automata weak bisimulation: theory and practice"],"prefix":"10.1145","volume":"28","author":[{"given":"Luis Mar\u00eda","family":"Ferrer Fioriti","sequence":"first","affiliation":[{"name":"Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vahid","family":"Hashemi","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany"},{"name":"Max Planck Institute for Informatics, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Turrini","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.4086\/toc.2012.v008a006"},{"volume-title":"Network flows: theory, algorithms, and applications","year":"1993","author":"Ahuja RK","key":"e_1_2_1_2_2_2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1137\/S1052623497323194"},{"issue":"4","key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1007\/s00453-001-0049-z","article-title":"Exact algorithms for linear programming over algebraic extensions","volume":"31","author":"Beling PA","year":"2001","journal-title":"Algorithmica"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","first-page":"1173","DOI":"10.1007\/s11590-011-0356-5","article-title":"A network simplex based algorithm for the minimum cost proportional flow problem with disconnected subnetworks","volume":"6","author":"Bah\u00e7eci U","year":"2012","journal-title":"Optim Lett"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2008.102"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0273-0979-1989-15750-9"},{"key":"e_1_2_1_2_8_2","unstructured":"Barrett C Stump A Tinelli C (2010) The SMT-LIB standard: version 2.0. In SMT"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/548834"},{"issue":"3","key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1016\/S0377-2217(02)00505-2","article-title":"Network simplex algorithm for the general equal flow problem","volume":"150","author":"Calvete HI","year":"2002","journal-title":"Eur J Oper Res"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chehaibar G Garavel H Mounier L Tawbi N Zulian F (1996) Specification and verification of the PowerScaleregistered bus arbitration protocol: an industrial experiment with LOTOS. In: FORTE pp 435\u2013450","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Crouzen P Hermanns H (2010) Aggregation ordering for massively compositional models. In: ACSD pp 171\u2013180","DOI":"10.1109\/ACSD.2010.28"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Coste N Hermanns H Lantreibecq E Serwe W (2009) Towards performance prediction of compositional models in industrial GALS designs. In: CAV. LNCS vol 5643 pp 204\u2013218","DOI":"10.1007\/978-3-642-02658-4_18"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Christiano P Kelner JA M\u00b8dry A Spielman D (2011) Electrical flows laplacian systems and faster approximation of maximum flow in undirected graphs. In: STOC pp 273\u2013282","DOI":"10.1145\/1993636.1993674"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Crouzen P Lang F (2011) Smart reduction. In FASE. LNCS vol 6603 pp 111\u2013126","DOI":"10.1007\/978-3-642-19811-3_9"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Cattani S Segala R (2002) Decision algorithms for probabilistic bisimulation. In: CONCUR of LNCS vol 2421 pp 371\u2013385","DOI":"10.1007\/3-540-45694-5_25"},{"key":"e_1_2_1_2_17_2","unstructured":"Deng Y (2005) Axiomatisations and types for probabilistic and mobile processes. PhD thesis \u00c9cole des Mines de Paris"},{"key":"e_1_2_1_2_18_2","unstructured":"Derman C (1970) Finite state markovian decision processes. Academic Press Inc New York"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Mendon\u00e7a de Moura L Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS. LNCS vol 4963 pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Eisentraut C Hermanns H Schuster J Turrini A Zhang L (2013) The quest for minimal quotients for probabilistic automata. In: TACAS. LNCS vol 7795 pp 16\u201331","DOI":"10.1007\/978-3-642-36742-7_2"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Eisentraut C Hermanns H Zhang L (2010) Concurrency and composition in a stochastic world. In: CONCUR. LNCS vol 6269 pp 21\u201339","DOI":"10.1007\/978-3-642-15375-4_3"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Eisentraut C Hermanns H Zhang L (2010) On probabilistic automata in continuous time. In: LICS pp 342\u2013351","DOI":"10.1109\/LICS.2010.41"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Gebler D Hashemi V Turrini A (2014) Computing behavioral relations for probabilistic concurrent systems. In: Stochastic model checking. Rigorous dependability analysis using model checking techniques for stochastic systems. LNCS vol 8453. Springer Berlin Heidelberg pp 117\u2013155","DOI":"10.1007\/978-3-662-45489-3_5"},{"key":"e_1_2_1_2_24_2","unstructured":"GNU linear programming kit. http:\/\/www.gnu.org\/software\/glpk\/."},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211911"},{"key":"e_1_2_1_2_26_2","unstructured":"Hansson HA (1991) Time and probability in formal design of distributed systems. PhD thesis Uppsala University"},{"key":"e_1_2_1_2_27_2","first-page":"66","article-title":"On the efficiency of deciding probabilistic automata weak bisimulation","volume":"66","author":"Hashemi V","year":"2012","journal-title":"ECEASST, vol"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Helgason RV Kennington JL (1995) Primal simplex algorithms for minimum cost network flows. In: Network models. Handbooks in operations research and management science vol 7 chapter 2. Elsevier Amsterdam pp 85\u2013113","DOI":"10.1016\/S0927-0507(05)80119-7"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00019-2"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539793251876"},{"key":"e_1_2_1_2_31_2","unstructured":"Jonsson B Larsen KG (1991) Specification and refinement of probabilistic processes. In: LICS pp 266\u2013277"},{"volume-title":"In: Encyclopedia of mathematics and its applications.","year":"1980","author":"Jones WB","key":"e_1_2_1_2_32_2"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579150"},{"issue":"1","key":"e_1_2_1_2_34_2","first-page":"191","article-title":"A polynomial algorithm in linear programming","volume":"20","author":"Khachyan LG","year":"1979","journal-title":"Sov Math Doklady"},{"key":"e_1_2_1_2_35_2","unstructured":"Katoen J-P Kemna T Zapreev IS Jansen DN (2007) Bisimulation minimisation mostly speeds up probabilistic model checking. In: TACAS. LNCS vol 4424 pp 76\u201392"},{"key":"e_1_2_1_2_36_2","unstructured":"Klee V Minty GJ (1972) How good is the simplex algorithm? In: Inequalities vol III pp 159\u2013175. Defense Technical Information Center USA"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Krimm J-P Mounier L (2000) Compositional state space generation with partial order reductions for asynchronous communicating systems. In: TACAS. LNCS vol 1785 pp 266\u2013282","DOI":"10.1007\/3-540-46419-0_19"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: CAV. LNCS vol 6806 pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Kanellakis PC Smolka SA (1990) CCS expressions finite state processes and three problems of equivalence. I&C. 86(1):43\u201368","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"e_1_2_1_2_40_2","unstructured":"LpSolve mixed integer linear programming solver. http:\/\/lpsolve.sourceforge.net."},{"volume-title":"Communication and concurrency","year":"1989","author":"Milner R","key":"e_1_2_1_2_41_2"},{"issue":"1","key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1287\/ijoc.1110.0485","article-title":"A network simplex algorithm for the equal flow problem on a generalized network","volume":"25","author":"Morrison DR","year":"2011","journal-title":"INFORMS J Comput"},{"issue":"3","key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","first-page":"801","DOI":"10.1007\/s11590-013-0634-5","article-title":"An algorithm to solve the proportional network flow problem","volume":"8","author":"Morrison DR","year":"2013","journal-title":"Optim Lett"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Philippou A Lee I Sokolsky O (2000) Weak bisimulation for probabilistic systems. In: CONCUR. LNCS vol 1877 pp 334\u2013349","DOI":"10.1007\/3-540-44618-4_25"},{"key":"e_1_2_1_2_45_2","unstructured":"PRISM model checker. http:\/\/www.prismmodelchecker.org\/"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Parma A Segala R (2004) Axiomatization of trace semantics for stochastic nondeterministic processes. In: QEST pp 294\u2013303","DOI":"10.1109\/QEST.2004.1348043"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"publisher","DOI":"10.1016\/0305-0548(89)90017-8"},{"volume-title":"In: Algorithms and combinatorics, vol 24.","year":"2003","author":"Schrijver A","key":"e_1_2_1_2_49_2"},{"key":"e_1_2_1_2_50_2","unstructured":"Segala R (1995) Modeling and verification of randomized distributed real-time systems. PhD thesis MIT"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Segala R (2006) Probability and nondeterminism in operational models of concurrency. In: CONCUR. LNCS vol 4137 pp 64\u201378","DOI":"10.1007\/11817949_5"},{"issue":"3","key":"e_1_2_1_2_52_2","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1287\/mnsc.33.3.301","article-title":"The efficiency of the simplex method: a survey","volume":"33","author":"Shamir R","year":"1987","journal-title":"Manag Sci"},{"issue":"2","key":"e_1_2_1_2_53_2","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Segala R","year":"1995","journal-title":"Nordic J Comput"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Turrini A Hermanns H (2015) Polynomial time decision algorithms for probabilistic automata. I&C 244:134\u2013171","DOI":"10.1016\/j.ic.2015.07.004"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Vardi MY (1985) Automatic verification of probabilistic concurrent finite-state programs. In: FOCS pp 327\u2013338","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Vazirani VV (2004) Approximation algorithms. Springer Berlin","DOI":"10.1007\/978-3-662-04565-7"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0356-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0356-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0356-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:18:38Z","timestamp":1641485918000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0356-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3]]},"references-count":56,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,3]]}},"alternative-id":["10.1007\/s00165-016-0356-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0356-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,3]]}}}