{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T02:48:31Z","timestamp":1780627711778,"version":"3.54.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,2,19]],"date-time":"2018-02-19T00:00:00Z","timestamp":1518998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100002341","name":"Suomen Akatemia","doi-asserted-by":"publisher","award":["139402"],"award-info":[{"award-number":["139402"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002341","name":"Suomen Akatemia","doi-asserted-by":"publisher","award":["27752"],"award-info":[{"award-number":["27752"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/L025507\/1"],"award-info":[{"award-number":["EP\/L025507\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K001698\/1"],"award-info":[{"award-number":["EP\/K001698\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s10703-018-0316-0","type":"journal-article","created":{"date-parts":[[2018,2,19]],"date-time":"2018-02-19T15:54:46Z","timestamp":1519055686000},"page":"407-431","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Compact and efficiently verifiable models for concurrent systems"],"prefix":"10.1007","volume":"53","author":[{"given":"Hern\u00e1n","family":"Ponce\u00a0de\u00a0Le\u00f3n","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Mokhov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,2,19]]},"reference":[{"key":"316_CR1","unstructured":"ARM Ltd.: ARMv6-M Architecture Reference Manual (2010)"},{"key":"316_CR2","unstructured":"Berkeley Logic Synthesis and Verification Group: ABC: a System for Sequential Synthesis and Verification, Release 70930. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"issue":"3","key":"316_CR3","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/2984450.2984457","volume":"3","author":"S Brookes","year":"2016","unstructured":"Brookes S, O\u2019Hearn PW (2016) Concurrent separation logic. ACM SIGLOG News 3(3):47\u201365","journal-title":"ACM SIGLOG News"},{"key":"316_CR4","doi-asserted-by":"publisher","unstructured":"D\u2019Alessandro C, Mokhov A, Bystrov AV, Yakovlev A (2007) Delay\/phase regeneration circuits. In: 13th IEEE international symposium on asynchronous circuits and systems (ASYNC 2007), 12\u201314 March 2006, Berkeley, California, USA. IEEE Computer Society, pp 105\u2013116. https:\/\/doi.org\/10.1109\/ASYNC.2007.14","DOI":"10.1109\/ASYNC.2007.14"},{"key":"316_CR5","volume-title":"The book of traces","year":"1995","unstructured":"Diekert V, Rozenberg G (eds) (1995) The book of traces. World Scientific Publishing Co., Inc, Singapore"},{"key":"316_CR6","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/3-540-65306-6_20","volume-title":"Lectures on Petri Nets I: basic models","author":"J Esparza","year":"1998","unstructured":"Esparza J (1998) Decidability and complexity of petri net problem-an introduction. In: Rozenberg G, Reisig W (eds) Lectures on Petri Nets I: basic models. Springer, Berlin, pp 374\u2013428"},{"key":"316_CR7","unstructured":"Esparza J, Heljanko K (2008) Unfoldings\u2014a partial-order approach to model checking. In: Monographs in theoretical computer science. An EATCS series. Springer"},{"key":"316_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem","author":"P Godefroid","year":"1996","unstructured":"Godefroid P, Van Leeuwen J, Hartmanis J, Goos G, Wolper P (1996) Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem, vol 1032. Springer, Heidelberg"},{"key":"316_CR9","doi-asserted-by":"crossref","unstructured":"Haar S, Rodr\u00edguez C, Schwoon S (2013) Reveal your faults: it\u2019s only fair! In: ACSD, pp 120\u2013129","DOI":"10.1109\/ACSD.2013.15"},{"key":"316_CR10","doi-asserted-by":"publisher","unstructured":"K\u00e4hk\u00f6nen K, Heljanko K (2014) Testing multithreaded programs with contextual unfoldings and dynamic symbolic execution. In: 14th international conference on application of concurrency to system design, pp 142\u2013151. https:\/\/doi.org\/10.1109\/ACSD.2014.20","DOI":"10.1109\/ACSD.2014.20"},{"key":"316_CR11","doi-asserted-by":"crossref","unstructured":"Khomenko V, Mokhov A (2011) An algorithm for direct construction of complete merged processes. In: International conference on application and theory of Petri Nets and concurrency. Springer, pp 89\u2013108","DOI":"10.1007\/978-3-642-21834-7_6"},{"key":"316_CR12","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-56496-9_14","volume-title":"Computer aided verification","author":"K McMillan","year":"1993","unstructured":"McMillan K (1993) Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Probst DK, von Bochmann G (eds) Computer aided verification. Springer, Heidelberg, pp 164\u2013177"},{"key":"316_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A calculus of communicating systems","author":"R Milner","year":"1980","unstructured":"Milner R (1980) A calculus of communicating systems, vol 92. Springer, Berlin"},{"key":"316_CR14","doi-asserted-by":"crossref","unstructured":"Mokhov A (2009) Conditional partial order graphs. Ph.D. thesis, Newcastle University","DOI":"10.1109\/ACSD.2008.4574604"},{"issue":"4s","key":"316_CR15","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/2627351","volume":"13","author":"A Mokhov","year":"2014","unstructured":"Mokhov A, Khomenko V (2014) Algebra of parameterised graphs. ACM Trans Embed Comput Syst 13(4s):143","journal-title":"ACM Trans Embed Comput Syst"},{"issue":"11","key":"316_CR16","doi-asserted-by":"publisher","first-page":"1480","DOI":"10.1109\/TC.2010.58","volume":"59","author":"A Mokhov","year":"2010","unstructured":"Mokhov A, Yakovlev A (2010) Conditional partial order graphs: model, synthesis, and application. IEEE Trans Comput 59(11):1480\u20131493","journal-title":"IEEE Trans Comput"},{"issue":"6","key":"316_CR17","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1049\/iet-cdt.2010.0158","volume":"5","author":"A Mokhov","year":"2011","unstructured":"Mokhov A, Alekseyev A, Yakovlev A (2011) Encoding of processor instruction sets with explicit concurrency control. IET Comput Digital Tech 5(6):427\u2013439","journal-title":"IET Comput Digital Tech"},{"issue":"6","key":"316_CR18","doi-asserted-by":"publisher","first-page":"1552","DOI":"10.1109\/TC.2013.37","volume":"63","author":"A Mokhov","year":"2014","unstructured":"Mokhov A, Iliasov A, Sokolov D, Rykunov M, Yakovlev A, Romanovsky A (2014) Synthesis of processor instruction sets from high-level ISA specifications. IEEE Trans Comput 63(6):1552\u20131566. https:\/\/doi.org\/10.1109\/TC.2013.37","journal-title":"IEEE Trans Comput"},{"key":"316_CR19","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M Nielsen","year":"1981","unstructured":"Nielsen M, Plotkin GD, Winskel G (1981) Petri nets, event structures and domains, part I. Theoret Comput Sci 13:85\u2013108","journal-title":"Theoret Comput Sci"},{"key":"316_CR20","first-page":"505","volume-title":"Petri Nets and other models of concurrency","author":"I Poliakov","year":"2007","unstructured":"Poliakov I, Sokolov D, Mokhov A (2007) Workcraft: a static data flow structure editing, visualisation and analysis tool. In: Kleijn J, Yakovlev A (eds) Petri Nets and other models of concurrency. Springer, Berlin, pp 505\u2013514"},{"key":"316_CR21","unstructured":"Ponce de Le\u00f3n H, Mokhov A (2015) Building bridges between sets of partial orders. In: 9th international conference on language and automata theory and applications, LATA 2015, Nice, France, March 2\u20136, 2015, Proceedings, pp 145\u2013160"},{"key":"316_CR22","doi-asserted-by":"crossref","unstructured":"Ponce de Le\u00f3n H, Rodr\u00edguez C, Carmona J, Heljanko K, Haar S (2015) Unfolding-based process discovery. In: 13th international symposium on automated technology for verification and analysis, ATVA 2015, Shanghai, China, October 12\u201315, 2015, Proceedings, Lecture Notes in Computer Science, vol 9364. Springer, pp 31\u201347","DOI":"10.1007\/978-3-319-24953-7_4"},{"issue":"1","key":"316_CR23","first-page":"81","volume":"1","author":"JR Quinlan","year":"1986","unstructured":"Quinlan JR (1986) Induction of decision trees. Mach Learn 1(1):81\u2013106","journal-title":"Mach Learn"},{"key":"316_CR24","unstructured":"Rodr\u00edguez C, Sousa M, Sharma S, Kroening D (2015) Unfolding-based partial order reduction. In: 26th international conference on concurrency theory, CONCUR 2015, Madrid, Spain, September 1\u20134, 2015, pp 456\u2013469"},{"key":"316_CR25","unstructured":"Rykunov M (2013) Design of asynchronous microprocessor for power proportionality. Ph.D. thesis, Newcastle University"},{"issue":"2","key":"316_CR26","doi-asserted-by":"publisher","first-page":"45:1","DOI":"10.1145\/3012281","volume":"16","author":"O Saarikivi","year":"2017","unstructured":"Saarikivi O, Ponce de Le\u00f3n H, K\u00e4hk\u00f6nen K, Heljanko K, Esparza J (2017) Minimizing test suites with unfoldings of multithreaded programs. ACM Trans Embed Comput Syst 16(2):45:1\u201345:24","journal-title":"ACM Trans Embed Comput Syst"},{"key":"316_CR27","doi-asserted-by":"crossref","unstructured":"Valmari A (1998) The state explosion problem. In: Lectures on Petri nets I: basic models. Springer, pp 429\u2013528","DOI":"10.1007\/3-540-65306-6_21"},{"key":"316_CR28","doi-asserted-by":"crossref","unstructured":"van Beest NRTP, Dumas M, Garc\u00eda-Ba\u00f1uelos L, Rosa ML (2015) Log delta analysis: interpretable differencing of business process event logs. In: 13th international conference on business process management, BPM 2015, Innsbruck, Austria, August 31\u2013September 3, 2015, Proceedings, pp 386\u2013405","DOI":"10.1007\/978-3-319-23063-4_26"},{"key":"316_CR29","volume-title":"The complexity of boolean functions","author":"I Wegener","year":"1987","unstructured":"Wegener I (1987) The complexity of boolean functions. Johann Wolfgang Goethe-Universitat, Frankfurt"},{"key":"316_CR30","unstructured":"Workcraft webpage (2017) www.workcraft.org"},{"key":"316_CR31","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-45657-0_2","volume-title":"Computer aided verification","author":"L Zhang","year":"2002","unstructured":"Zhang L, Malik S (2002) The quest for efficient boolean satisfiability solvers. In: Brinksma D, Larsen KG (eds) Computer aided verification. Springer, Berlin, pp 17\u201336"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-018-0316-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0316-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-018-0316-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T08:54:52Z","timestamp":1603875292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-018-0316-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,19]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["316"],"URL":"https:\/\/doi.org\/10.1007\/s10703-018-0316-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,2,19]]},"assertion":[{"value":"19 February 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}