{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,10]],"date-time":"2024-08-10T09:51:54Z","timestamp":1723283514377},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"5-6","license":[{"start":{"date-parts":[[2015,11,1]],"date-time":"2015-11-01T00:00:00Z","timestamp":1446336000000},"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":[[2015,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Substantial research efforts have been expended to deal with the complexity of concurrent systems that is inherent to their analysis, e.g., works that tackle the well-known state space explosion problem. Approaches differ in the classes of properties that they are able to suitably check and this is largely a result of the way they balance the trade-off between analysis time and space employed to describe a concurrent system. One interesting class of properties is concerned with behavioral characteristics. These properties are conveniently expressed in terms of computations, or\n            <jats:italic>runs<\/jats:italic>\n            , in concurrent systems. This article introduces the theory of\n            <jats:italic>untanglings<\/jats:italic>\n            that exploits a particular representation of a collection of runs in a concurrent system. It is shown that a representative untangling of a bounded concurrent system can be constructed that captures all and only the behavior of the system. Representative untanglings strike a unique balance between time and space, yet provide a single model for the convenient extraction of various behavioral properties. Performance measurements in terms of construction time and size of representative untanglings with respect to the original specifications of concurrent systems, conducted on a collection of models from practice, confirm the scalability of the approach. Finally, this article demonstrates practical benefits of using representative untanglings when checking various behavioral properties of concurrent systems.\n          <\/jats:p>","DOI":"10.1007\/s00165-014-0329-4","type":"journal-article","created":{"date-parts":[[2015,1,12]],"date-time":"2015-01-12T06:27:45Z","timestamp":1421044065000},"page":"753-788","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Untanglings: a novel approach to analyzing concurrent systems"],"prefix":"10.1145","volume":"27","author":[{"given":"Artem","family":"Polyvyanyy","sequence":"first","affiliation":[{"name":"Queensland University of Technology, GPO Box 2434, P Block (Level 8), Gardens Point Campus, 4001, Brisbane, QLD, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcello","family":"La Rosa","sequence":"additional","affiliation":[{"name":"Queensland University of Technology, GPO Box 2434, P Block (Level 8), Gardens Point Campus, 4001, Brisbane, QLD, Australia"},{"name":"NICTA Queensland Lab, Brisbane, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chun","family":"Ouyang","sequence":"additional","affiliation":[{"name":"Queensland University of Technology, GPO Box 2434, P Block (Level 8), Gardens Point Campus, 4001, Brisbane, QLD, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arthur H. M.","family":"ter Hofstede","sequence":"additional","affiliation":[{"name":"Queensland University of Technology, GPO Box 2434, P Block (Level 8), Gardens Point Campus, 4001, Brisbane, QLD, Australia"},{"name":"Eindhoven University of Technology, Eindhoven, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01888220"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Desel J Esparza J (1995) Free choice Petri nets. Cambridge tracts in theoretical computer science vol 40. Cambridge University Press Cambridge","DOI":"10.1017\/CBO9780511526558"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Desel J (2000) Validation of process models by construction of process nets. In: Business process management (BPM). LNCS vol 1806. Springer Berlin pp 110\u2013128","DOI":"10.1007\/3-540-45594-9_8"},{"key":"e_1_2_1_2_4_2","unstructured":"Esparza J Heljanko K (2008) Unfoldings: a partial-order approach to model checking. Monographs in theoretical computer science. An EATCS series. Springer Berlin"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014746130920"},{"key":"e_1_2_1_2_6_2","unstructured":"Fahland D (2010) From Scenarios to Components. PhD thesis Humboldt-Universit\u00e4t zu Berlin Berlin Germany"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.datak.2011.01.004"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80040-0"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383879"},{"key":"e_1_2_1_2_10_2","unstructured":"Hack M (1975) Decidability questions for Petri nets. Outstanding dissertations in the computer sciences. Garland Publishing New York"},{"key":"e_1_2_1_2_11_2","unstructured":"Khomenko V (2003) Model checking based on prefixes of Petri net unfoldings. PhD thesis University of Newcastle upon Tyne School of Computing Science Newcastle upon Tyne UK"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-006-0023-y"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Khomenko V Mokhov A (2011) An algorithm for direct construction of complete merged processes. In: Petri nets. LNCS vol 6709. Springer Berlin pp 89\u2013108","DOI":"10.1007\/978-3-642-21834-7_6"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.736561"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"McMillan KL (1992) Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: Computer aided verification (CAV). LNCS vol 663. Springer Berlin pp 164\u2013177","DOI":"10.1007\/3-540-56496-9_14"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384314"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Melzer S R\u00f6mer S (1997) Deadlock checking using net unfoldings. In: Computer aided verification (CAV). LNCS vol 1254. Springer Berlin pp 352\u2013363","DOI":"10.1007\/3-540-63166-6_35"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"e_1_2_1_2_20_2","unstructured":"Petri CA (1977) Non-sequential processes. Translation of a Lecture given at the IMMD Jubilee Colloquium on \u201cParallelism in Computer Science\u201d Unversit\u00e4t Erlangen-N\u00fcrnberg. Translated by Philip Krause and John Low Petri CA St. Augustin: Gesellschaft fnr Mathematik und Datenverarbeitung Bonn Interner Bericht ISF-77-5"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Polyvyanyy A La Rosa M ter Hofstede AHM (2014) Indexing and efficient instance-based retrieval of process models using untanglings. In: Advanced information systems engineering (CAiSE). LNCS vol 8484. Springer International Publishing Berlin pp 439\u2013456","DOI":"10.1007\/978-3-319-07881-6_30"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: annual symposium on foundations of computer science (FOCS). IEEE Computer Society pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_23_2","unstructured":"Polyvyanyy A Weidlich M (2013) Towards a compendium of process technologies: the jBPT library for process model analysis. In: CAiSE forum. CEUR workshop proceedings vol 998. CEUR-WS.org pp 106\u2013113"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Polyvyanyy A Weidlich M Conforti R La Rosa M ter Hofstede AHM (2014) The 4C spectrum of fundamental behavioral relations for concurrent systems. In: Petri nets. LNCS vol 8489. Springer International Publishing Berlin pp 210\u2013232","DOI":"10.1007\/978-3-319-07734-5_12"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Reisig W(2013) Understanding Petri nets: modeling techniques analysis methods case studies. Springer Berlin","DOI":"10.1007\/978-3-642-33278-4"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez C Schwoon S Khomenko V. (2013) Contextual merged processes. In: Petri nets. LNCS vol 7927. Springer Berlin pp 29\u201348","DOI":"10.1007\/978-3-642-38697-8_3"},{"issue":"1","key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/S0304-3975(96)80710-9","article-title":"Models for concurrency: towards a classification","volume":"170","author":"Sassone V","year":"1996","journal-title":"Theor Comput Sci"},{"key":"e_1_2_1_2_29_2","unstructured":"Tarasyuk IV (1997) Equivalence notions for models of concurrent and distributed systems. PhD thesis A.P. Ershov Institute of Informatics Systems Siberian Division of the Russian Academy of Sciences Novosibirsk Russia"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"van der Aalst WMP (1997) Verification of workflow nets. In: Petri nets. LNCS vol 1248. Springer Berlin pp 407\u2013426","DOI":"10.1007\/3-540-63139-9_48"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"van Glabbeek RJ Vaandrager FW (1987) Petri net models for algebraic theories of concurrency. In: Parallel architectures and languages Europe (PARLE). LNCS vol 259. Springer Berlin pp 224\u2013242","DOI":"10.1007\/3-540-17945-3_13"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0329-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0329-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0329-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:08:18Z","timestamp":1641485298000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0329-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11]]},"references-count":31,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["10.1007\/s00165-014-0329-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0329-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,11]]}}}