{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:08Z","timestamp":1740109088980,"version":"3.37.3"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2016,7,1]],"date-time":"2016-07-01T00:00:00Z","timestamp":1467331200000},"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,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Petri nets with name creation and management (\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"italic\">\u03bd<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            -PNs) have been recently introduced as an expressive model for dynamic (distributed) systems, whose dynamics are determined not only by how tokens flow in the system, but also by the pure names they carry. On the one hand, this extension makes the resulting nets strictly more expressive than P\/T nets: they can be exploited to capture a plethora of interesting systems, such as distributed systems enriched with channels and name passing, service interaction with correlation mechanisms, and resource-constrained workflow nets that explicitly account for process instances. On the other hand, fundamental properties like coverability, termination and boundedness are decidable for\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"italic\">\u03bd<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            -PNs. In this work, we go one step beyond the verification of such general properties, and provide decidability and undecidability results of model checking\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"italic\">\u03bd<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            -PNs against variants of first-order\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi mathvariant=\"italic\">\u03bc<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            -calculus, recently proposed in the area of data-aware process analysis. While this model checking problem is undecidable in the general case, decidability can be obtained by considering different forms of boundedness, which still give raise to an infinite-state transition system. We then ground our framework to tackle the problem of soundness checking over workflow nets enriched with explicit process instances and resources. Notably, our decidability results are obtained via a translation to data-centric dynamic systems, a recently devised framework for the formal specification and verification of data-aware business processes working over full-fledged relational databases with constraints. In this light, our results contribute to the cross-fertilization between the area of formal methods for concurrent systems and that of foundations of data-aware processes, which has not been extensively investigated so far.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0370-6","type":"journal-article","created":{"date-parts":[[2016,4,18]],"date-time":"2016-04-18T06:44:10Z","timestamp":1460961850000},"page":"615-641","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Model checking Petri nets with names using data-centric dynamic systems"],"prefix":"10.1145","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8021-3430","authenticated-orcid":false,"given":"Marco","family":"Montali","sequence":"first","affiliation":[{"name":"KRDB Research Centre for Knowledge and Data, Faculty of Computer Science, Free University of Bozen-Bolzano, Piazza Domenicani 3, 39100, Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrey","family":"Rivkin","sequence":"additional","affiliation":[{"name":"KRDB Research Centre for Knowledge and Data, Faculty of Computer Science, Free University of Bozen-Bolzano, Piazza Domenicani 3, 39100, Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abadi M Gordon AD (1997) A calculus for cryptographic protocols: the spi calculus. In: Proceedings of the 4th ACM conference on computer and communications security CCS \u201997 pp 36\u201347 New York NY USA. ACM","DOI":"10.1145\/266420.266432"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Anisimov NA Koutny M (1995) On compositionality and petri nets in protocol engineering. In: Piotr Dembinski and Marek Sredniawa editors PSTV vol. 38 of IFIP Conference Proceedings pp 71\u201386. Chapman & Hall","DOI":"10.1007\/978-0-387-34892-6_5"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bojanczyk M Braud L Klin B Lasota S (2012) Towards nominal computation. In Proceedings of POPL. ACM Press","DOI":"10.1145\/2103656.2103704"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bagheri Hariri B Calvanese D De Giacomo G Deutsch A Montali M (2013) Verification of relational data-centric dynamic systems with external services. In: Proceedings of PODS pp 163\u2013174. ACM","DOI":"10.1145\/2463664.2465221"},{"key":"e_1_2_1_2_5_2","unstructured":"Bagheri Hariri B Calvanese D Deutsch A Montali M (2014) State boundedness in data-aware dynamic systems. In: Proceedings of KR"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bagheri Hariri B Calvanese B Montali M De Giacomo G De Masellis R Felli P (2013) Description logic knowledge and action bases. J Artif Intell Res","DOI":"10.1613\/jair.3826"},{"key":"e_1_2_1_2_7_2","unstructured":"Belardinelli F Lomuscio A Patrizi F (2012) An abstraction technique for the verification of artifact-centric systems. In: Proceedings KR"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bojanczyk M Segoufin L Torunczyk S (2013) Verification of database-driven systems via amalgamation. In: Proceedings of PODS","DOI":"10.1145\/2463664.2465228"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Calvanese D De Giacomo G Montali M (2013) Foundations of data aware process analysis: a database theory perspective. In: Proceedings of PODS","DOI":"10.1145\/2463664.2467796"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Calvanese D De Giacomo G Montali M Patrizi F (2013) Verification and synthesis in description logic based dynamic systems. In: Proceedings of RR vol 7994 of LNCS. Springer New York","DOI":"10.1007\/978-3-642-39666-3_5"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Chandra A Harel D (1980) Computable queries for relational database systems. J Comput Syst Sci 21","DOI":"10.1016\/0022-0000(80)90032-X"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Decker G Weske M (2008) Instance isolation analysis for service-oriented architectures. In: Proceedings of SCC pp 249\u2013256. IEEE Computer Society","DOI":"10.1109\/SCC.2008.44"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Allen Emerson E (1996) Model checking and the Mu-calculus. In: Proceedings of the DIMACS symposium on descriptive complexity and finite models pp 185\u2013214. American Mathematical Society Press","DOI":"10.1090\/dimacs\/031\/06"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Esparza J (1994) On the decidability of model checking for several \u03bc-calculi and petri nets. In: Proceedings of CAAP vol 787 of LNCS pp 115\u2013129. Springer New York","DOI":"10.1007\/BFb0017477"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Gabbay M Pitts AM (2002) A new approach to abstract syntax with variable binding. Formal Asp Comput 13(3\u20135)","DOI":"10.1007\/s001650200016"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"H\u00fcchting R Majumdar R Meyer R (2013) A theory of name boundedness. In: Proceedings of CONCUR vol 8052 of LNCS pp 182\u2013196. Springer New York","DOI":"10.1007\/978-3-642-40184-8_14"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","DOI":"10.1007\/b95112","volume-title":"Coloured petri nets\u2014modelling and validation of concurrent systems","author":"Jensen K","year":"2009"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"K\u00f6hler M R\u00f6lke H (2004) Properties of object petri nets. In: Proceedings of ICATPN vol 3099 of LNCS pp 278\u2013297. Springer New York","DOI":"10.1007\/978-3-540-27793-4_16"},{"volume-title":"Elements of finite model theory, vol 7360 of LNCS, chapter fixed point logics and complexity classes","year":"2004","author":"Libkin L","key":"e_1_2_1_2_19_2"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.5555\/2366267.2366270"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Martos-Salgado M Rosa-Velardo F (2011) Dynamic soundness in resource-constrained workflow nets. In: Proceedings of FMOODS\/FORTE vol 6722 of LNCS pp 259\u2013273. Springer New York","DOI":"10.1007\/978-3-642-21461-5_17"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Needham RM (1989) Names. In: Mullender S (ed) Distributed systems pp 89\u2013101. ACM Press Wokingham","DOI":"10.1145\/90417.90741"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(80)90032-0"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-33278-4","volume-title":"Understanding petri nets: modeling techniques, analysis methods, case studies","author":"Reisig W","year":"2013"},{"issue":"3","key":"e_1_2_1_2_25_2","first-page":"329","article-title":"Name creation vs. replication in petri net systems","volume":"88","author":"Rosa-Velardo F","year":"2008","journal-title":"Fundam Inf"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.007"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Vardi MY (2005) Model checking for database theoreticians. In: Proceedings of ICDT vol 3363 of LNCS pp 1\u201316. Springer New York","DOI":"10.1007\/978-3-540-30570-5_1"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"van der Aalst WMP (1997) Verification of workflow nets. In: Proceedings of ICATPN vol 1248 of LNCS pp 407\u2013426. Springer New York","DOI":"10.1007\/3-540-63139-9_48"},{"key":"e_1_2_1_2_29_2","unstructured":"van der Aalst WMP (2005) Pi calculus versus petri nets: let us eat humble pie rather than further inflate the pi hype. BPTrends 3(5)"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"van der Aalst WMP Stahl C (2011) Modeling business processes\u2014a petri net-oriented approach. Cooperative Information Systems series. MIT Press","DOI":"10.7551\/mitpress\/8811.001.0001"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"van der Aalst WMP van Hee KM ter Hofstede AHM Sidorova N Verbeek HMW Voorhoeve M Thandar Wynn M (2011) Soundness of workflow nets: classification decidability and analysis. Formal Asp Comput 23(3):333\u2013363","DOI":"10.1007\/s00165-010-0161-4"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"van Hee KM Serebrenik A Sidorova N Voorhoeve M (2005) Soundness of resource-constrained workflow nets. In: Proceedings of ICATPN vol 3536 of LNCS pp 250\u2013267. Springer New York","DOI":"10.1007\/11494744_15"},{"issue":"2","key":"e_1_2_1_2_33_2","first-page":"243","article-title":"Resource-constrained workflow nets","volume":"71","author":"van Hee KM","year":"2006","journal-title":"Fundam Inf"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Vianu V (2009) Automatic verification of database-driven systems: a new frontier. In: Proceedings of ICDT pp 1\u201313","DOI":"10.1145\/1514894.1514896"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Westergaard M Maria Maggi F (2011) Modeling and verification of a protocol for operational support using coloured petri nets. In: Proceedings of Applications and theory of petri nets\u201432nd international conference PETRI NETS 2011 Newcastle UK June 20\u201324 2011 pp 169\u2013188","DOI":"10.1007\/978-3-642-21834-7_10"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0370-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0370-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0370-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:08:02Z","timestamp":1641485282000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0370-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,7]]}},"alternative-id":["10.1007\/s00165-016-0370-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0370-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,7]]}}}