{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,28]],"date-time":"2025-08-28T12:47:17Z","timestamp":1756385237206},"reference-count":39,"publisher":"Cambridge University Press (CUP)","issue":"4-5","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"content-version":"unspecified","delay-in-days":86,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The paper provides a framework for the verification of business processes, based on an extension of answer set programming (ASP) with temporal logic and constraints. The framework allows to capture expressive fluent annotations as well as data awareness in a uniform way. It allows for a declarative specification of a business process but also for encoding processes specified in conventional workflow languages. Verification of temporal properties of a business process, including verification of compliance to business rules, is performed by bounded model checking techniques in Answer Set Programming, extended with constraint solving for dealing with conditions on numeric data.<\/jats:p>","DOI":"10.1017\/s1471068413000409","type":"journal-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T16:24:58Z","timestamp":1380126298000},"page":"641-655","source":"Crossref","is-referenced-by-count":5,"title":["Business process verification with constraint temporal answer set programming"],"prefix":"10.1017","volume":"13","author":[{"given":"LAURA","family":"GIORDANO","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ALBERTO","family":"MARTELLI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MATTEO","family":"SPIOTTA","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"DANIELE THESEIDER","family":"DUPR\u00c9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"key":"S1471068413000409_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/371316.371517"},{"key":"S1471068413000409_ref9","unstructured":"D'Aprile D. , Giordano L. , Gliozzi V. , Martelli A. , Pozzato G. L. and Theseider Dupr\u00e9 D. 2010. Verifying business process compliance by reasoning about actions. In CLIMA XI, 99\u2013116."},{"key":"S1471068413000409_ref13","unstructured":"Gebser M. , Ostrowski M. and Schaub T. 2009. Constraint answer set solving. In ICLP, 235\u2013249."},{"key":"S1471068413000409_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001790"},{"key":"S1471068413000409_ref16","unstructured":"Giordano L. , Martelli A. and Theseider Dupr\u00e9 D. 2012. Achieving completeness in bounded model checking of action theories in ASP. In Proc. KR 2012."},{"key":"S1471068413000409_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/11837862_18"},{"key":"S1471068413000409_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2004.02.002"},{"key":"S1471068413000409_ref30","unstructured":"Ostrowski M. 2012. What is this thing called \u201cclingcon\u201d? A language description. Available at potassco.sourceforge.net."},{"key":"S1471068413000409_ref20","doi-asserted-by":"publisher","DOI":"10.26686\/ajl.v4i0.1780"},{"key":"S1471068413000409_ref4","first-page":"118","article-title":"Bounded model checking.","volume":"58","author":"Biere","year":"2003","journal-title":"Advances in Computers"},{"key":"S1471068413000409_ref19","volume-title":"Third International Workshop on Requirements Engineering and Law","author":"Governatori","year":"2010"},{"key":"S1471068413000409_ref35","unstructured":"Singh M. P. 2000. A social semantics for Agent Communication Languages. Issues in Agent Communication, LNCS(LNAI) 1916, 31\u201345."},{"key":"S1471068413000409_ref34","unstructured":"Roman D. and Kifer M. 2008. Semantic web service choreography: Contracting and enactment. In International Semantic Web Conference, LNCS 5318, 550\u2013566."},{"key":"S1471068413000409_ref33","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/4074.001.0001","volume-title":"Knowledge in Action","author":"Reiter","year":"2001"},{"key":"S1471068413000409_ref25","doi-asserted-by":"crossref","unstructured":"Hoffmann J. , Weber I. and Governatori G. 2009. On compliance checking for clausal constraints in annotated process models. Information Systems Frontiers.","DOI":"10.1007\/s10796-009-9179-7"},{"key":"S1471068413000409_ref28","doi-asserted-by":"crossref","first-page":"325","DOI":"10.3233\/FI-2010-310","article-title":"Abductive logic programming as an effective technology for the static verification of declarative business processes.","volume":"102","author":"Montali","year":"2010","journal-title":"Fundamenta Informaticae"},{"key":"S1471068413000409_ref37","unstructured":"van der Aalst W. , van Hee K. , ter Hofstede A. , Sidorova N. , Verbeek H. , Voorhoeve M. and Wynn M. 2008. Soundness of workflow nets: Classification, decidability, and analysiss. BPM Center Report BPM-08-02, BPMcenter.org."},{"key":"S1471068413000409_ref21","unstructured":"Governatori G. and Sadiq S. 2009. The journey to business process compliance. Handbook of Research on BPM, IGI Global, 426\u2013454."},{"key":"S1471068413000409_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1380572.1380578"},{"key":"S1471068413000409_ref2","unstructured":"Alberti M. , Gavanelli M. , Lamma E. , Mello P. , Torroni P. and Sartor G. 2005. Mapping of deontic operators to abductive expectations. NORMAS, 126\u2013136."},{"key":"S1471068413000409_ref5","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"S1471068413000409_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.artmed.2009.09.003"},{"key":"S1471068413000409_ref7","unstructured":"Clarke E. , Kroening D. , Ouaknine J. and Strichman O. 2004. Completeness and complexity of bounded model checking. In VMCAI, 85\u201396."},{"key":"S1471068413000409_ref10","volume-title":"Constraint Processing","author":"Dechter","year":"2003"},{"key":"S1471068413000409_ref11","unstructured":"Deutsch A. , Hull R. , Patrizi F. and Vianu V. 2009. Automatic verification of data-centric business processes. In ICDT, 252\u2013267."},{"key":"S1471068413000409_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.datak.2011.01.004"},{"key":"S1471068413000409_ref14","volume-title":"Handbook of Knowledge Representation","author":"Gelfond","year":"2007"},{"key":"S1471068413000409_ref15","unstructured":"Ghose A. and Koliadis G. 2007. Auditing business process compliance. ICSOC, LNCS 4749, 169\u2013180."},{"key":"S1471068413000409_ref18","doi-asserted-by":"crossref","unstructured":"Giordano L. , Martelli A. and Theseider Dupr\u00e9 D. 2013b. Temporal deontic action logic for the verification of compliance to norms in ASP. In Proc. ICAIL 2013.","DOI":"10.1145\/2514601.2514608"},{"key":"S1471068413000409_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000639"},{"key":"S1471068413000409_ref22","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/978-94-009-6259-0_10","article-title":"Dynamic logic","volume":"2","author":"Harel","year":"1984","journal-title":"Handbook of Philosophical Logic"},{"key":"S1471068413000409_ref8","doi-asserted-by":"crossref","unstructured":"Damaggio E. , Deutsch A. and Vianu V. 2011. Artifact systems with data dependencies and arithmetic. In ICDT.","DOI":"10.1145\/1938551.1938563"},{"key":"S1471068413000409_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00039-6"},{"key":"S1471068413000409_ref26","unstructured":"Knuplesch D. , Ly L. T. , Rinderle-Ma S. , Pfeifer H. and Dadam P. 2010. On enabling data-aware compliance checking of business process models. In Proc. ER 2010, 29th International Conference on Conceptual Modeling, 332\u2013346."},{"key":"S1471068413000409_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.035"},{"key":"S1471068413000409_ref29","doi-asserted-by":"publisher","DOI":"10.1147\/sj.423.0428"},{"key":"S1471068413000409_ref31","first-page":"485","article-title":"ASP modulo CSP: The clingcon system.","volume":"12","author":"Ostrowski","year":"2012","journal-title":"TPLP"},{"key":"S1471068413000409_ref38","unstructured":"van der Aalst W. M. P. and Pesic M. 2006. Decserflow: Towards a truly declarative service flow language. In The Role of Business Processes in Service Oriented Architectures. Dagstuhl Seminar Proceedings, vol. 06291."},{"key":"S1471068413000409_ref39","doi-asserted-by":"crossref","unstructured":"Weber I. , Hoffmann J. and Mendling J. 2010. Beyond soundness: On the verification of semantic business process models. Distributed and Parallel Databases (DAPD).","DOI":"10.1007\/s10619-010-7060-9"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068413000409","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,13]],"date-time":"2024-05-13T09:29:13Z","timestamp":1715592553000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068413000409\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":39,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S1471068413000409"],"URL":"https:\/\/doi.org\/10.1017\/s1471068413000409","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}