{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:21:54Z","timestamp":1750220514748,"version":"3.41.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T00:00:00Z","timestamp":1619740800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003593","name":"CNPq","doi-asserted-by":"crossref","award":["441952\/2014-3"],"award-info":[{"award-number":["441952\/2014-3"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100002322","name":"CAPES","doi-asserted-by":"crossref","award":["877\/2017"],"award-info":[{"award-number":["877\/2017"]}],"id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004586","name":"FAPERJ","doi-asserted-by":"crossref","award":["247709"],"award-info":[{"award-number":["247709"]}],"id":[{"id":"10.13039\/501100004586","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2021,4,30]]},"abstract":"<jats:p>Petri Nets are a widely used formalism to deal with concurrent systems. Dynamic Logics (DLs) are a family of modal logics where each modality corresponds to a program. Petri-PDL is a logical language that combines these two approaches: it is a dynamic logic where programs are replaced by Petri Nets. In this work we present a clausal resolution-based calculus for Petri-PDL. Given a Petri-PDL formula, we show how to obtain its translation into a normal form to which a set of resolution-based inference rules are applied. We show that the resulting calculus is sound, complete, and terminating. Some examples of the application of the method are also given.<\/jats:p>","DOI":"10.1145\/3441655","type":"journal-article","created":{"date-parts":[[2021,5,15]],"date-time":"2021-05-15T19:27:02Z","timestamp":1621106822000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning about Petri Nets: A Calculus Based on Resolution and Dynamic Logic"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1204-0176","authenticated-orcid":false,"given":"Bruno","family":"Lopes","sequence":"first","affiliation":[{"name":"Universidade Federal Fluminense, Brazil"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9792-5346","authenticated-orcid":false,"given":"Cl\u00e1udia","family":"Nalon","sequence":"additional","affiliation":[{"name":"Universidade de Bras\u00edlia, Brazil"}]},{"given":"Edward Hermann","family":"Haeusler","sequence":"additional","affiliation":[{"name":"Pontif\u00edcia Universidade Cat\u00f3lica do Rio de Janeiro, Brazil"}]}],"member":"320","published-online":{"date-parts":[[2021,5,15]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"23","article-title":"Proving properties in ordinary Petri Nets using LoRes logical language","volume":"57","author":"de Almeida Eliana S.","year":"1999","unstructured":"Eliana S. de Almeida and Edward Hermann Haeusler . 1999 . Proving properties in ordinary Petri Nets using LoRes logical language . Petri Net Newsletter 57 (1999), 23 \u2013 36 . Eliana S. de Almeida and Edward Hermann Haeusler. 1999. Proving properties in ordinary Petri Nets using LoRes logical language. Petri Net Newsletter 57 (1999), 23\u201336.","journal-title":"Petri Net Newsletter"},{"volume-title":"Application and Theory of Petri Nets and Concurrency","author":"Amparore Elvio Gilberto","key":"e_1_2_1_2_1","unstructured":"Elvio Gilberto Amparore , Marco Beccuti , and Susanna Donatelli . 2014. (Stochastic) model checking in Great SPN. In Application and Theory of Petri Nets and Concurrency , Gianfranco Ciardo and Ekkart Kindler (Eds.). Springer International Publishing , Cham , 354\u2013363. Elvio Gilberto Amparore, Marco Beccuti, and Susanna Donatelli. 2014. (Stochastic) model checking in GreatSPN. In Application and Theory of Petri Nets and Concurrency, Gianfranco Ciardo and Ekkart Kindler (Eds.). Springer International Publishing, Cham, 354\u2013363."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAE.2010.5451406"},{"key":"e_1_2_1_4_1","first-page":"1","article-title":"Sequential and distributed model checking of Petri","volume":"7","author":"Bell Alexander","year":"2005","unstructured":"Alexander Bell and Boudewijn R. Haverkort . 2005 . Sequential and distributed model checking of Petri Nets. Int. J. Softw. Tools Technol. Transf. 7 , 1 (Feb. 2005), 43\u201360. DOI:https:\/\/doi.org\/10.1007\/s10009-003-0129-2 10.1007\/s10009-003-0129-2 Alexander Bell and Boudewijn R. Haverkort. 2005. Sequential and distributed model checking of Petri Nets. Int. J. Softw. Tools Technol. Transf. 7, 1 (Feb. 2005), 43\u201360. DOI:https:\/\/doi.org\/10.1007\/s10009-003-0129-2","journal-title":"Nets. Int. J. Softw. Tools Technol. Transf."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.01.007"},{"volume-title":"Model checking of persistent Petri nets","author":"Best Eike","key":"e_1_2_1_6_1","unstructured":"Eike Best and Javier Esparza . 1992. Model checking of persistent Petri nets . In Computer Science Logic, Egon B\u00f6rger, Gerhard J\u00e4ger, Hans Kleine B\u00fcning, and Michael M. Richter (Eds.). Springer , Berlin ,35\u201352. Eike Best and Javier Esparza. 1992. Model checking of persistent Petri nets. In Computer Science Logic, Egon B\u00f6rger, Gerhard J\u00e4ger, Hans Kleine B\u00fcning, and Michael M. Richter (Eds.). Springer, Berlin,35\u201352."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1093\/bib\/bbm029"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1119439.1119443"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58216-9_30"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(96)00024-3"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5626\/JCSE.2015.9.1.9"},{"volume-title":"A false history of true concurrency: From Petri to tools","author":"Esparza Javier","key":"e_1_2_1_12_1","unstructured":"Javier Esparza . 2010. A false history of true concurrency: From Petri to tools . In Model Checking Software, Jaco van de Pol and Michael Weber (Eds.). Springer , Berlin ,180\u2013186. Javier Esparza. 2010. A false history of true concurrency: From Petri to tools. In Model Checking Software, Jaco van de Pol and Michael Weber (Eds.). Springer, Berlin,180\u2013186."},{"key":"e_1_2_1_13_1","first-page":"143","article-title":"Decidability Issues for Petri Nets - A survey","volume":"30","author":"Esparza Javier","year":"1994","unstructured":"Javier Esparza and Mogens Nielsen . 1994 . Decidability Issues for Petri Nets - A survey . Journal of Information Processing and Cybernetics 30 , 3 (1994), 143 -- 160 . Javier Esparza and Mogens Nielsen. 1994. Decidability Issues for Petri Nets - A survey. Journal of Information Processing and Cybernetics 30, 3 (1994), 143--160.","journal-title":"Journal of Information Processing and Cybernetics"},{"key":"e_1_2_1_14_1","volume-title":"12th IFAC Symposium on Transportation Systems. Elsevier, Redondo Beach, 513\u2013518","author":"Abu Farha A.","year":"2009","unstructured":"A. Abu Farha and Eckehard Schneider . 2009 . Modelling of traffic safety and operation in urban networks using DSTPN . In 12th IFAC Symposium on Transportation Systems. Elsevier, Redondo Beach, 513\u2013518 . A. Abu Farha and Eckehard Schneider. 2009. Modelling of traffic safety and operation in urban networks using DSTPN. In 12th IFAC Symposium on Transportation Systems. Elsevier, Redondo Beach, 513\u2013518."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijhydene.2016.05.138"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"volume-title":"First-order Logic and Automated Theorem Proving","author":"Fitting Melvin","key":"e_1_2_1_17_1","unstructured":"Melvin Fitting . 1990. First-order Logic and Automated Theorem Proving . Springer-Verlag New York, Inc. , New York, NY . Melvin Fitting. 1990. First-order Logic and Automated Theorem Proving. Springer-Verlag New York, Inc., New York, NY."},{"volume-title":"Petri Nets for Systems Engineering: A Guide to Modeling, Verification and Applications","author":"Girault Claude","key":"e_1_2_1_18_1","unstructured":"Claude Girault and R\u00fcdiger Valk . 2001. Petri Nets for Systems Engineering: A Guide to Modeling, Verification and Applications . Springer-Verlag , Berlin . Claude Girault and R\u00fcdiger Valk. 2001. Petri Nets for Systems Engineering: A Guide to Modeling, Verification and Applications. Springer-Verlag, Berlin."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.06.006"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzu010"},{"volume-title":"Trends in Practical Applications of Agents, Multi-Agent Systems and Sustainability, Javier Bajo, Josefa Z","author":"Lopes Bruno","key":"e_1_2_1_21_1","unstructured":"Bruno Lopes , Mario Benevides , and Edward Hermann Haeusler . 2015. Reasoning about multi-agent systems using stochastic Petri Nets . In Trends in Practical Applications of Agents, Multi-Agent Systems and Sustainability, Javier Bajo, Josefa Z . Hern\u00e1ndez, Philippe Mathieu, Andrew Campbell, Antonio Fern\u00e1ndez-Caballero, Mar\u00eda N. Moreno, Vicente Juli\u00e1n, Amparo Alonso-Betanzos, Mar\u00eda Dolores Jim\u00e9nez-L\u00f3pez, and Vicente Botti (Eds.). Springer International Publishing , Salamanca , 75\u201386. Bruno Lopes, Mario Benevides, and Edward Hermann Haeusler. 2015. Reasoning about multi-agent systems using stochastic Petri Nets. In Trends in Practical Applications of Agents, Multi-Agent Systems and Sustainability, Javier Bajo, Josefa Z. Hern\u00e1ndez, Philippe Mathieu, Andrew Campbell, Antonio Fern\u00e1ndez-Caballero, Mar\u00eda N. Moreno, Vicente Juli\u00e1n, Amparo Alonso-Betanzos, Mar\u00eda Dolores Jim\u00e9nez-L\u00f3pez, and Vicente Botti (Eds.). Springer International Publishing, Salamanca, 75\u201386."},{"key":"e_1_2_1_22_1","unstructured":"William McCune. 2009. Prover9 and Mace4. Accessed February 1 2019 from https:\/\/www.cs.unm.edu\/\u223cmccune\/prover9\/.  William McCune. 2009. Prover9 and Mace4. Accessed February 1 2019 from https:\/\/www.cs.unm.edu\/\u223cmccune\/prover9\/."},{"volume-title":"Logics in Artificial Intelligence, Michael Fisher, Wiebe van der Hoek","author":"Nalon Cl\u00e1udia","key":"e_1_2_1_23_1","unstructured":"Cl\u00e1udia Nalon and Clare Dixon . 2006. Anti-prenexing and prenexing for modal logics . In Logics in Artificial Intelligence, Michael Fisher, Wiebe van der Hoek , Boris Konev, and Alexei Lisitsa (Eds.), Vol. 4160 . Springer , Berlin , 333\u2013345. Cl\u00e1udia Nalon and Clare Dixon. 2006. Anti-prenexing and prenexing for modal logics. In Logics in Artificial Intelligence, Michael Fisher, Wiebe van der Hoek, Boris Konev, and Alexei Lisitsa (Eds.), Vol. 4160. Springer, Berlin, 333\u2013345."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.04.008"},{"key":"e_1_2_1_25_1","first-page":"319","article-title":"Fundamentals of a theory of asynchronous information flow","volume":"5","author":"Petri Carl Adam","year":"1962","unstructured":"Carl Adam Petri . 1962 . Fundamentals of a theory of asynchronous information flow . Commun. ACM 5 , 6 (1962), 319 \u2013 319 . Carl Adam Petri. 1962. Fundamentals of a theory of asynchronous information flow. Commun. ACM 5, 6 (1962), 319\u2013319.","journal-title":"Commun. ACM"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_29_1","volume-title":"The E Theorem Prover. Retrieved","author":"Schulz Stephan","year":"2019","unstructured":"Stephan Schulz . 2013. The E Theorem Prover. Retrieved February 1, 2019 , from http:\/\/wwwlehre.dhbw-stuttgart.de\/ sschulz\/E\/E.html. Stephan Schulz. 2013. The E Theorem Prover. Retrieved February 1, 2019, from http:\/\/wwwlehre.dhbw-stuttgart.de\/ sschulz\/E\/E.html."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ins.2016.01.036"},{"key":"e_1_2_1_31_1","volume-title":"Automation of Logic: SPASS. Retrieved","author":"Team The SPASS","year":"2019","unstructured":"The SPASS Team . 2010. Automation of Logic: SPASS. Retrieved February 1, 2019 , from http:\/\/www.spass-prover.org\/. The SPASS Team. 2010. Automation of Logic: SPASS. Retrieved February 1, 2019, from http:\/\/www.spass-prover.org\/."},{"key":"e_1_2_1_32_1","volume-title":"Proceedings (Cat. No.03TH8696)","volume":"2","author":"Tolba Ch\u00e9rif","year":"2003","unstructured":"Ch\u00e9rif Tolba , Philippe Thomas , Abdellah El Moudni , and Dimitri Lefebvre . 2003 . Performances evaluation of the traffic control in a single crossroad by Petri nets. In 2003 IEEE Conference on Emerging Technologies and Factory Automation . Proceedings (Cat. No.03TH8696) (EFTA\u201903), Vol. 2 . IEEE, Lisbon, 157\u2013160. DOI:https:\/\/doi.org\/10.1109\/ETFA. 2003.1248688 10.1109\/ETFA.2003.1248688 Ch\u00e9rif Tolba, Philippe Thomas, Abdellah El Moudni, and Dimitri Lefebvre. 2003. Performances evaluation of the traffic control in a single crossroad by Petri nets. In 2003 IEEE Conference on Emerging Technologies and Factory Automation. Proceedings (Cat. No.03TH8696) (EFTA\u201903), Vol. 2. IEEE, Lisbon, 157\u2013160. DOI:https:\/\/doi.org\/10.1109\/ETFA.2003.1248688"},{"volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part II","author":"Tseitin G. S.","key":"e_1_2_1_33_1","unstructured":"G. S. Tseitin . 1968. On the complexity of derivations in the propositional logics . In Studies in Constructive Mathematics and Mathematical Logic, Part II , A. O. Slisenko (Ed.). Vol. 8 . Nauka , Leningrad, Otdel , 234\u2013259. G. S. Tseitin. 1968. On the complexity of derivations in the propositional logics. In Studies in Constructive Mathematics and Mathematical Logic, Part II, A. O. Slisenko (Ed.). Vol. 8. Nauka, Leningrad, Otdel, 234\u2013259."},{"key":"e_1_2_1_34_1","volume-title":"Vampire theorem prover. Retrieved","author":"Voronkov Andrei","year":"2019","unstructured":"Andrei Voronkov . 1994. Vampire theorem prover. Retrieved February 1, 2019 , from http:\/\/www.vprover.org. Andrei Voronkov. 1994. Vampire theorem prover. Retrieved February 1, 2019, from http:\/\/www.vprover.org."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0031826"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3441655","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3441655","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:30Z","timestamp":1750195470000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3441655"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,30]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4,30]]}},"alternative-id":["10.1145\/3441655"],"URL":"https:\/\/doi.org\/10.1145\/3441655","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2021,4,30]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-05-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}