{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,11]],"date-time":"2024-07-11T22:27:33Z","timestamp":1720736853750},"reference-count":25,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2016,8,31]],"date-time":"2016-08-31T00:00:00Z","timestamp":1472601600000},"content-version":"vor","delay-in-days":1491,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1016\/j.tcs.2012.04.046","type":"journal-article","created":{"date-parts":[[2012,5,9]],"date-time":"2012-05-09T21:12:57Z","timestamp":1336597977000},"page":"2-22","source":"Crossref","is-referenced-by-count":24,"special_numbering":"C","title":["Efficient unfolding of contextual Petri nets"],"prefix":"10.1016","volume":"449","author":[{"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Bruni","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Corradini","sequence":"additional","affiliation":[]},{"given":"Barbara","family":"K\u00f6nig","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Rodr\u00edguez","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2012.04.046_br000005","series-title":"Unfoldings \u2014 A Partial-Order Approach to Model Checking","author":"Esparza","year":"2008"},{"key":"10.1016\/j.tcs.2012.04.046_br000010","unstructured":"K. Heljanko, Combining symbolic and partial-order methods for model-checking 1-safe Petri nets, Ph.D. Thesis, Helsinki University of Technology, 2002."},{"key":"10.1016\/j.tcs.2012.04.046_br000015","doi-asserted-by":"crossref","unstructured":"W. Vogler, A.L. Semenov, A. Yakovlev, Unfolding and finite prefix for nets with read arcs, in: Proc. of CONCUR\u201998, in: LNCS, vol. 1466, 1998, pp. 501\u2013516.","DOI":"10.1007\/BFb0055644"},{"key":"10.1016\/j.tcs.2012.04.046_br000020","unstructured":"G. Ristori, Modelling systems with shared resources via Petri nets, Ph.D. Thesis, Department of Computer Science, University of Pisa, 1994."},{"key":"10.1016\/j.tcs.2012.04.046_br000025","series-title":"Dagstuhl Seminar 9301","first-page":"280","article-title":"Contextual occurrence nets and concurrent constraint programming","volume":"vol. 776","author":"Montanari","year":"1994"},{"key":"10.1016\/j.tcs.2012.04.046_br000030","doi-asserted-by":"crossref","unstructured":"R. Janicki, M. Koutny, Invariant semantics of nets with inhibitor arcs, in: Proc. Concur, in: LNCS, vol. 527, 1991, pp. 317\u2013331.","DOI":"10.1007\/3-540-54430-5_97"},{"key":"10.1016\/j.tcs.2012.04.046_br000035","unstructured":"P. Baldan, A. Corradini, U. Montanari, An event structure semantics for P\/T contextual nets: Asymmetric event structures, in: Proc. FoSSaCS, in: LNCS, vol. 1378, 1998, pp. 63\u201380."},{"issue":"1\u20132","key":"10.1016\/j.tcs.2012.04.046_br000040","first-page":"235","article-title":"Reachability in contextual nets","volume":"51","author":"Winkowski","year":"2002","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/j.tcs.2012.04.046_br000045","series-title":"ToPNoC 1","first-page":"199","article-title":"McMillan\u2019s complete prefix for contextual nets","volume":"vol. 5100","author":"Baldan","year":"2008"},{"key":"10.1016\/j.tcs.2012.04.046_br000050","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1023\/A:1014746130920","article-title":"An improvement of McMillan\u2019s unfolding algorithm","volume":"20","author":"Esparza","year":"2002","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/j.tcs.2012.04.046_br000055","unstructured":"C. Rodr\u00edguez, Cunf, http:\/\/www.lsv.ens-cachan.fr\/~rodriguez\/tools\/cunf\/."},{"key":"10.1016\/j.tcs.2012.04.046_br000060","unstructured":"S. Schwoon, Mole, http:\/\/www.lsv.ens-cachan.fr\/~schwoon\/tools\/mole\/."},{"key":"10.1016\/j.tcs.2012.04.046_br000065","doi-asserted-by":"crossref","unstructured":"P. Baldan, A. Bruni, A. Corradini, B. K\u00f6nig, S. Schwoon, On the computation of McMillan\u2019s prefix for contextual nets and graph grammars, in: Proc. ICGT\u201910, in: LNCS, vol. 6372, 2010, pp. 91\u2013106.","DOI":"10.1007\/978-3-642-15928-2_7"},{"key":"10.1016\/j.tcs.2012.04.046_br000070","doi-asserted-by":"crossref","unstructured":"C. Rodr\u00edguez, S. Schwoon, P. Baldan, Efficient contextual unfolding, in: Proc. Concur, in: LNCS, vol. 6901, 2011, pp. 342\u2013357.","DOI":"10.1007\/978-3-642-23217-6_23"},{"key":"10.1016\/j.tcs.2012.04.046_br000075","doi-asserted-by":"crossref","unstructured":"C. Rodr\u00edguez, S. Schwoon, P. Baldan, Efficient contextual unfolding, Tech. Rep. LSV-11-14, LSV, ENS de Cachan, 2011.","DOI":"10.1007\/978-3-642-23217-6_23"},{"key":"10.1016\/j.tcs.2012.04.046_br000080","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1995.1153","article-title":"Semantics of inhibitor nets","volume":"123","author":"Janicki","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/j.tcs.2012.04.046_br000085","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits, in: Proc. CAV, in: LNCS, vol. 663, 1992, pp. 164\u2013177.","DOI":"10.1007\/3-540-56496-9_14"},{"key":"10.1016\/j.tcs.2012.04.046_br000090","doi-asserted-by":"crossref","unstructured":"V. Khomenko, Model checking based on prefixes of Petri net unfoldings, Ph.D. Thesis, School of Computing Science, Newcastle University, 2003.","DOI":"10.1007\/3-540-45657-0_49"},{"key":"10.1016\/j.tcs.2012.04.046_br000095","unstructured":"V. Khomenko, Punf, http:\/\/homepages.cs.ncl.ac.uk\/victor.khomenko\/tools\/punf\/."},{"key":"10.1016\/j.tcs.2012.04.046_br000100","doi-asserted-by":"crossref","unstructured":"K. Heljanko, Deadlock and reachability checking with finite complete prefixes, Licentiate\u2019s Thesis, Helsinki University of Technology, 1999.","DOI":"10.1007\/3-540-44618-4_10"},{"key":"10.1016\/j.tcs.2012.04.046_br000105","unstructured":"C. Rodr\u00edguez, Implementation of a complete prefix unfolder for contextual nets, Rapport de master, Master Parisien de Recherche en Informatique, Paris, France, Sep. 2010."},{"issue":"3","key":"10.1016\/j.tcs.2012.04.046_br000110","doi-asserted-by":"crossref","first-page":"247","DOI":"10.3233\/FI-1999-37304","article-title":"Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets","volume":"37","author":"Heljanko","year":"1999","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/j.tcs.2012.04.046_br000115","unstructured":"C. Schr\u00f6ter, Halbordnungs- und Reduktionstechniken f\u00fcr die automatische Verifikation von verteilten Systemen, Ph.D. Thesis, Universit\u00e4t Stuttgart, 2006."},{"key":"10.1016\/j.tcs.2012.04.046_br000120","series-title":"PPDP","first-page":"255","article-title":"A declarative encoding of telecommunications feature subscription in SAT","author":"Codish","year":"2009"},{"key":"10.1016\/j.tcs.2012.04.046_br000125","doi-asserted-by":"crossref","unstructured":"J. Esparza, K. Heljanko, Implementing LTL model checking with net unfoldings, in: Proc. SPIN, in: LNCS, vol. 2057, 2001, pp. 37\u201356.","DOI":"10.1007\/3-540-45139-0_4"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397512004318?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397512004318?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,7,7]],"date-time":"2020-07-07T06:54:04Z","timestamp":1594104844000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397512004318"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":25,"alternative-id":["S0304397512004318"],"URL":"http:\/\/dx.doi.org\/10.1016\/j.tcs.2012.04.046","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2012,8]]}}}
