{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T18:41:41Z","timestamp":1757616101159,"version":"3.44.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171261"},{"type":"electronic","value":"9783030171278"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Unordered data Petri nets (UDPN) are an extension of classical Petri nets with tokens that carry data from an infinite domain and where transitions may check equality and disequality of tokens. UDPN are well-structured, so the coverability and termination problems are decidable, but with higher complexity than for Petri nets. On the other hand, the problem of reachability for UDPN is surprisingly complex, and its decidability status remains open. In this paper, we consider the continuous reachability problem for UDPN, which can be seen as an over-approximation of the reachability problem. Our main result is a characterization of continuous reachability for UDPN and polynomial time algorithm for solving it. This is a consequence of a combinatorial argument, which shows that if continuous reachability holds then there exists a run using only polynomially many data values.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_15","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"260-276","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Continuous Reachability for Unordered Data Petri Nets is in PTime"],"prefix":"10.1007","author":[{"given":"Utkarsh","family":"Gupta","sequence":"first","affiliation":[]},{"given":"Preey","family":"Shah","sequence":"additional","affiliation":[]},{"given":"S.","family":"Akshay","sequence":"additional","affiliation":[]},{"given":"Piotr","family":"Hofman","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0304-3975(78)90036-1","volume":"6","author":"C Rackoff","year":"1978","unstructured":"Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223\u2013231 (1978)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Rao Kosaraju, S.: Decidability of reachability in vector addition systems (preliminary version). In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing, San Francisco, California, USA, 5\u20137 May 1982, pp. 267\u2013281 (1982)","DOI":"10.1145\/800070.802201"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: 30th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, 6\u201310 July 2015, pp. 56\u201367 (2015)","DOI":"10.1109\/LICS.2015.16"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Cardoza, E., Lipton, R.J., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative semigroups: preliminary report. In: Proceedings of the 8th Annual ACM Symposium on Theory of Computing, Hershey, Pennsylvania, USA, 3\u20135 May 1976, pp. 50\u201354 (1976)","DOI":"10.1145\/800113.803630"},{"key":"15_CR6","unstructured":"Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary (extended abstract). CoRR, abs\/1809.07115 (2018)"},{"issue":"1","key":"15_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"WMP van der Aalst","year":"1998","unstructured":"van der Aalst, W.M.P.: The application of Petri nets to workflow management. J. Circ. Syst. Comput. 8(1), 21\u201366 (1998)","journal-title":"J. Circ. Syst. Comput."},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","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.: Decidability and complexity of Petri net problems \u2014 an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374\u2013428. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-65306-6_20"},{"key":"15_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526558","volume-title":"Free Choice Petri Nets","author":"J Desel","year":"1995","unstructured":"Desel, J., Esparza, J.: Free Choice Petri Nets. Cambridge University Press, New York (1995)"},{"key":"15_CR10","unstructured":"David, R., Alla, H.: Continuous Petri nets. In: Proceedings of the 8th European Workshop on Application and Theory of Petri Nets, Zaragoza, Spain, pp. 275\u2013294 (1987)"},{"issue":"1","key":"15_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2015-1168","volume":"137","author":"E Fraca","year":"2015","unstructured":"Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundam. Inform. 137(1), 1\u201328 (2015)","journal-title":"Fundam. Inform."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Blondin, M., Haase, C.: Logics for continuous reachability in Petri nets and vector addition systems with states. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, 20\u201323 June 2017, pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005068"},{"issue":"2","key":"15_CR13","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0005-1098(94)90024-8","volume":"30","author":"R David","year":"1994","unstructured":"David, R., Alla, H.: Petri nets for modeling of dynamic systems: a survey. Automatica 30(2), 175\u2013202 (1994)","journal-title":"Automatica"},{"key":"15_CR14","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1142\/S0218126698000079","volume":"8","author":"H Alla","year":"1998","unstructured":"Alla, H., David, R.: Continuous and hybrid Petri nets. J. Circ. Syst. Comput. 8, 159\u2013188 (1998)","journal-title":"J. Circ. Syst. Comput."},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s100090050020","volume":"2","author":"K Jensen","year":"1998","unstructured":"Jensen, K.: Coloured Petri nets - preface by the section editor. STTT 2(2), 95\u201397 (1998)","journal-title":"STTT"},{"key":"15_CR16","series-title":"The Kluwer International Series on Discrete Event Dynamic Systems","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-1-4615-5537-7_4","volume-title":"Timed Petri Nets: Theory and Application","author":"J Wang","year":"1998","unstructured":"Wang, J.: Timed Petri nets. Timed Petri Nets: Theory and Application. The Kluwer International Series on Discrete Event Dynamic Systems, vol. 9, pp. 63\u2013123. Springer, Boston (1998). https:\/\/doi.org\/10.1007\/978-1-4615-5537-7_4"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45740-2_5","volume-title":"Applications and Theory of Petri Nets 2001","author":"PA Abdulla","year":"2001","unstructured":"Abdulla, P.A., Nyl\u00e9n, A.: Timed Petri nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53\u201370. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45740-2_5"},{"issue":"3","key":"15_CR18","first-page":"251","volume":"88","author":"R Lazic","year":"2008","unstructured":"Lazic, R., Newcomb, T.C., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Inform. 88(3), 251\u2013274 (2008)","journal-title":"Fundam. Inform."},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/978-3-642-13675-7_12","volume-title":"Applications and Theory of Petri Nets","author":"F Rosa-Velardo","year":"2010","unstructured":"Rosa-Velardo, F., de Frutos-Escrig, D.: Forward analysis for Petri nets with name creation. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 185\u2013205. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13675-7_12"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-51046-0_8","volume-title":"Concurrency, Security, and Puzzles","author":"R Lazi\u0107","year":"2017","unstructured":"Lazi\u0107, R., Totzke, P.: What makes Petri nets harder to verify: stack or data? In: Gibson-Robinson, T., Hopcroft, P., Lazi\u0107, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 144\u2013161. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-51046-0_8"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-662-49630-5_26","volume-title":"Foundations of Software Science and Computation Structures","author":"P Hofman","year":"2016","unstructured":"Hofman, P., Lasota, S., Lazi\u0107, R., Leroux, J., Schmitz, S., Totzke, P.: Coverability trees for Petri nets with unordered data. In: Jacobs, B., L\u00f6ding, C. (eds.) FOSSACS 2016. LNCS, vol. 9634, pp. 445\u2013461. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_26"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Hofman, P., Leroux, J., Totzke, P.: Linear combinations of unordered data vectors. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, 20\u201323 June 2017, pp. 1\u201311 (2017)","DOI":"10.1109\/LICS.2017.8005065"},{"key":"15_CR23","unstructured":"Hofman, P., Lasota, S.: Linear equations with ordered data. In: 29th International Conference on Concurrency Theory, CONCUR 2018, Beijing, China, 4\u20137 September 2018, pp. 24:1\u201324:17 (2018)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/3-540-65306-6_19","volume-title":"Lectures on Petri Nets I: Basic Models","author":"M Silva","year":"1998","unstructured":"Silva, M., Terue, E., Colom, J.M.: Linear algebraic and linear programming techniques for the analysis of place\/transition net systems. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 309\u2013373. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-65306-6_19"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-662-49674-9_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Blondin","year":"2016","unstructured":"Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 480\u2013496. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_28"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/978-3-319-08867-9_40","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2014","unstructured":"Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P., Niksic, F.: An SMT-based approach to coverability analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 603\u2013619. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_40"},{"key":"15_CR27","unstructured":"Gupta, U., Shah, P., Akshay, S., Hofman, P.: Continuous reachability for unordered data Petri nets is in PTime. CoRR abs\/1902.05604 (2019). arxiv.org\/abs\/1902.05604"},{"issue":"34","key":"15_CR28","doi-asserted-by":"publisher","first-page":"4439","DOI":"10.1016\/j.tcs.2011.05.007","volume":"412","author":"F Rosa-Velardo","year":"2011","unstructured":"Rosa-Velardo, F., de Frutos-Escrig, D.: Decidability and complexity of Petri nets with unordered data. Theor. Comput. Sci. 412(34), 4439\u20134451 (2011)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17127-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T17:08:50Z","timestamp":1757092130000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}