{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,9,24]],"date-time":"2022-09-24T16:52:11Z","timestamp":1664038331139},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.<\/jats:p>","DOI":"10.1007\/s00165-016-0366-2","type":"journal-article","created":{"date-parts":[[2016,3,18]],"date-time":"2016-03-18T19:40:51Z","timestamp":1458330051000},"page":"381-407","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Computing maximal weak and other bisimulations"],"prefix":"10.1145","volume":"28","author":[{"given":"Alexandre","family":"Boulgakov","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Gibson-Robinson","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Armstrong P Goldsmith M Lowe G Ouaknine J Palikareva H Roscoe AW Worrell J (2012) Recent developments in FDR. In: Computer aided verification. Springer pp 699\u2013704","DOI":"10.1007\/978-3-642-31424-7_52"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Boulgakov A Gibson-Robinson T Roscoe AW (2014) Computing maximal bisimulations. In: Formal methods and software engineering. Springer pp 11\u201326","DOI":"10.1007\/978-3-319-11737-9_2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80390-1"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0185-2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Blom S van de Pol J (2009) Distributed branching bisimulation minimization by inductive signatures. arXiv preprint arXiv:0912.2550","DOI":"10.4204\/EPTCS.14.3"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00361-X"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90071-K"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/367766.368168"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0244-z"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson T Armstrong P Boulgakov A Roscoe AW (2015) FDR3: a parallel refinement checker for CSP. Int J Softw Tools Technol Transf 1\u201319","DOI":"10.1007\/s10009-015-0377-y"},{"key":"e_1_2_1_2_11_2","first-page":"626","volume-title":"Automata, languages and programming, volume 443 of Lecture notes in computer science","author":"Groote JF","year":"1990"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Kanellakis PC Smolka SA (1983) CCS expressions finite state processes and three problems of equivalence. In: Proceedings of the 2nd annual ACM symposium on principles of distributed computing PODC \u201983 pp 228\u2013240 New York NY USA ACM","DOI":"10.1145\/800221.806724"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Mateescu R (2005) On-the-fly state space reductions for weak equivalences. In: Proceedings of the 10th international workshop on formal methods for industrial critical systems pp 80\u201389 ACM","DOI":"10.1145\/1081180.1081191"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Milner R (1981) A modal characterisation of observable machine-behaviour. In: CAAP\u201981. Springer pp 25\u201334","DOI":"10.1007\/3-540-10828-9_52"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/901178"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_2_1_2_18_2","unstructured":"Phillips ICC Ulidowski I (1996) Ordered SOS rules and weak bisimulation. Theory Formal Methods"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Roscoe AW Gardiner PHB Goldsmith MH Hulance JR Jackson DM Scattergood JB (1995) Hierarchical compression for model-checking CSP or how to check 10 20 dining philosophers for deadlock. In: Proceedings of TACAS 1995. BRICS","DOI":"10.1007\/3-540-60630-0_7"},{"key":"e_1_2_1_2_20_2","unstructured":"Roscoe AW (1994) Model-checking CSP. A classical mind: essays in honour of CAR Hoare"},{"key":"e_1_2_1_2_21_2","unstructured":"Roscoe AW (1998) The theory and practice of concurrency"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s002360050036"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268499"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/233551.233556"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Wimmer R Herbstritt M Hermanns H Strampp K Becker B (2006) Sigref\u2014a symbolic bisimulation tool box. In: Automated technology for verification and analysis. Springer pp 477\u2013492","DOI":"10.1007\/11901914_35"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0366-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0366-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0366-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:13:36Z","timestamp":1641485616000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0366-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["10.1007\/s00165-016-0366-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0366-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5]]}}}