{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T05:55:05Z","timestamp":1757310905098},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,4,1]],"date-time":"2016-04-01T00:00:00Z","timestamp":1459468800000},"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,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Partial order reduction has been very successful at combatting the state explosion problem for lower-level formalisms, but has thus far made hardly any impact for model checking higher-level formalisms such as B, Z or TLA\n            <jats:sup>+<\/jats:sup>\n            . This paper attempts to remedy this issue in the context of Event-B, with its much more fine-grained events and thus increased potential for event-independence and partial order reduction. In this work, we provide a detailed description of a partial order reduction for explicit state model checking in ProB. The technique is evaluated on a variety of models. The implementation of the method is discussed, which is based on new constraint-based analyses. Further, we give a comprehensive description for elaborating the implementation into the LTL model checker of ProB for checking LTL\n            <jats:sub>\n              \u2212\n              <jats:italic>X<\/jats:italic>\n            <\/jats:sub>\n            formulae.\n          <\/jats:p>","DOI":"10.1007\/s00165-015-0351-1","type":"journal-article","created":{"date-parts":[[2016,1,15]],"date-time":"2016-01-15T16:48:47Z","timestamp":1452876527000},"page":"295-323","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Optimising the ProB model checker for B using partial order reduction"],"prefix":"10.1145","volume":"28","author":[{"given":"Ivaylo","family":"Dobrikov","sequence":"first","affiliation":[{"name":"Institut f\u00fcr Informatik, Heinrich-Heine Universit\u00e4t D\u00fcsseldorf, Universit\u00e4tstr. 1, 40225, D\u00fcsseldorf, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Heinrich-Heine Universit\u00e4t D\u00fcsseldorf, Universit\u00e4tstr. 1, 40225, D\u00fcsseldorf, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Ait-Sadoune I Ait-Ameur Y (2009) A proof based approach for modelling and verifying web services compositions. In: ICECCS \u201909 Washington DC USA. IEEE Computer Society pp 1\u201310","DOI":"10.1109\/ICECCS.2009.48"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Abrial J-R Butler M Hallertede S Voisin L (2006) An open extensible tool environment for Event-B. In: ICFEM 2006. LNCS vol 4260. Springer pp 588\u2013605","DOI":"10.1007\/11901433_32"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bene N Brim L \u010cern\u00e1 I Sochor J Va\u0159ekov\u00e1 P Zimmerova B (2009) Partial order reduction for state\/event LTL. In: iFM 2009. LNCS vol 5423. Springer Berlin pp 307\u2013321","DOI":"10.1007\/978-3-642-00255-7_21"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Barnat J Brim L Havel V Havl\u00ed\u010dek J Kriho J Len\u010do M Ro\u010dkai P \u0160till V Weiser J (2013) DiVinE 3.0\u2014an explicit-state model checker for multithreaded C & C++ programs. In: CAV. LNCS vol 8044. Springer Berlin pp 863\u2013868","DOI":"10.1007\/978-3-642-39799-8_60"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Barnat J Brim L Rockai P (2010) Parallel partial order reduction with topological sort proviso. In: SEFM. IEEE Computer Society pp 222\u2013231","DOI":"10.1109\/SEFM.2010.35"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0260-5"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bendisposto J Leuschel M (2009) Proof assisted model checking for B. In: ICFEM. LNCS vol 5885 pp 504\u2013520 Springer Berlin","DOI":"10.1007\/978-3-642-10373-5_26"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Bendisposto J Leuschel M (2011) Automatic flow analysis for Event-B. In: FASE. LNCS vol 6603. Springer Berlin pp 50\u201364","DOI":"10.1007\/978-3-642-19811-3_5"},{"key":"e_1_2_1_2_11_2","volume-title":"Principles of model checking","author":"Baier C","year":"2008"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0093-y"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Chaki S Clarke EM Ouaknine J Sharygina N Sinha N (2004) State\/event based software model checking. In: iFM. LNCS vol 2999 pp 128\u2013147","DOI":"10.1007\/978-3-540-24756-2_8"},{"key":"e_1_2_1_2_14_2","unstructured":"Clarke Jr Edmund M Grumberg O Peled DA (1999) Model checking. MIT Press Cambridge"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050035"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Dobrikov I Leuschel M (2014) Optimising the ProB model checker for B using partial order reduction. In: SEFM LNCS vol 8702 pp 220\u2013234","DOI":"10.1007\/978-3-319-10431-7_16"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Esparza J Lammich P Neumann R Nipkow T Schimpf A Smaus J-G (2013) A fully verified executable LTL model checker. In: CAV. LNCS vol 8044. Springer Berlin pp 463\u2013478","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"e_1_2_1_2_18_2","volume-title":"Partial-order methods for the verification of concurrent systems\u2014an approach to the state-explosion problem. LNCS, vol 1032","author":"Godefroid P","year":"1996"},{"key":"e_1_2_1_2_19_2","unstructured":"Godefroid P Pirottin D (993) Refining dependencies improves partial-order verification methods. In: CAV. LNCS vol 697. Springer Berlin"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Godefroid P Wolper P (1991) Using partial orders for the efficient verification of deadlock freedom and safety properties. In: CAV. LNCS vol 575 pp 332\u2013342. Springer Berlin","DOI":"10.1007\/3-540-55179-4_32"},{"key":"e_1_2_1_2_21_2","volume-title":"Spin model checker, the: primer and reference manual","author":"Holzmann G","year":"2003","edition":"1"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Holzmann G Peled D (1994) An improvement in formal verification. In: Proceedings FORTE pp 197\u2013211","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Kant G Laarman A Meijer J van de Pol J Blom S van Dijk T (2015) LTSmin: high-performance language-independent model checking. In: TACAS. LNCS vol 9035. Springer Berlin pp 692\u2013707","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"e_1_2_1_2_24_2","unstructured":"Leuschel M (2008) The high road to formal validation: model checking high-level versus low-level specifications. In: ABZ. LNCS vol 5238. Springer Berlin pp 4\u201323"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Butler M Spermann C Turner E (2007) Symmetry reduction for B by permutation flooding. In: Proceedings B\u20192007. LNCS vol 4355. Springer Berlin pp 79\u201393","DOI":"10.1007\/11955757_9"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Bendisposto J (2010) Directed model checking for B: an evaluation and new techniques. In: SBMF\u2019 2010. LNCS vol 6527. Springer Berlin pp 1\u201316","DOI":"10.1007\/978-3-642-19829-8_1"},{"key":"e_1_2_1_2_28_2","unstructured":"Leuschel M Massart T (2007) Efficient approximative verification for B via symmetry markers. In: Proceedings international symmetry conference pp 71\u201385 January"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Lichtenstein O Pnueli A (1985) Checking that finite state concurrent programs satisfy their linear specifications. In: POPL\u201985 New York NY USA ACM pp 97\u2013107","DOI":"10.1145\/318593.318622"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Laarman A Wijs A (2014) Partial-order reduction for multi-core LTL model checking. In: HVC 2014. LNCS vol 8855. Springer Berlin pp 267\u2013283","DOI":"10.1007\/978-3-319-13338-6_20"},{"key":"e_1_2_1_2_31_2","volume-title":"Isabelle\/HOL-A proof assistant for Higher-Order Logic","author":"Nipkow T","year":"2002"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of 18th IEEE symposium on foundations of computer science (SFCS \u201977). IEEE Computer Society Press pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Peled D (1994) Combining partial order reduction with on-the-fly model-checking. In: Proceedings of the sixth workshop on CAV. LNCS vol 818. Springer Berlin pp 377\u2013390","DOI":"10.1007\/3-540-58179-0_69"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-009-0132-3"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(97)00133-6"},{"key":"e_1_2_1_2_36_2","unstructured":"Rosa CD Merz S Quinson M (2010) A simple model of communication APIs\u2014application to dynamic partial-order reduction. ECEASST 35"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Sun J Liu Y Dong JS (2008) Model checking CSP revisited: introducing a process analysis toolkit. In: Proceedings of ISoLA. Springer Berlin pp 307\u2013322","DOI":"10.1007\/978-3-540-88479-8_22"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Turner E Leuschel M Spermann C Butler M (2007) Symmetry reduced model checking for B. In: TASE. IEEE pp 25\u201334","DOI":"10.1109\/TASE.2007.50"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Valmari A (1989) Stubborn sets for reduced state space generation. In: Applications and theory of petri nets pp 491\u2013515","DOI":"10.1007\/3-540-53863-1_36"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Valmari A (1989) Eliminating redundant interleavings during concurrent program verification. In: PARLE. LNCS vol 366 Springer Berlin pp 89\u2013103","DOI":"10.1007\/3-540-51285-3_35"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Valmari A (1990) A stubborn attack on state explosion. In: CAV pp 156\u2013165","DOI":"10.1007\/BFb0023729"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Valmari A (1996) Stubborn set methods for process algebras. In: DIMACS vol 29 pp 213\u2013231","DOI":"10.1090\/dimacs\/029\/12"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Wehrheim H (1999) Partial order reductions for failures refinement. In: Proceedings of the 6th international workshop on expressiveness in concurrency Electronic notes in theoretical computer science vol 27 pp 71\u201384","DOI":"10.1016\/S1571-0661(05)80296-8"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Zheng M San\u00e1n D Sun J Liu Y Dong JS Gu Y (2013) State space reduction for sensor networks using two-level partial order reduction. In: VMCAI pp 515\u2013535","DOI":"10.1007\/978-3-642-35873-9_30"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-015-0351-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-015-0351-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-015-0351-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:48Z","timestamp":1641538488000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-015-0351-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1007\/s00165-015-0351-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-015-0351-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4]]}}}