Evaluating Compliance : From LTL to Abductive Logic Programming

• Autorzy: Chesani F. , Gavanelli M. , Lamma E. , Mello P. , Montali M.

Identyfikatory

DOI

10.3233/FI-2018-1657

• Konferencja: Convegno Italiano di Logica Computazionale : CILC 2015 (30th; 01-03.07.2015; University of Genoa, Italy)
• Języki publikacji: EN

Abstrakty

EN

The compliance verification task amounts to establishing if the execution of a system, given in terms of observed happened events, does respect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to assess compliance in different domains, such as normative multi-agent systems, business process management and service oriented computing. In this work we review the LTL and SCIFF frameworks in the light of compliance evaluation, and formally investigate the relationship between the two approaches. We define a notion of compliance within each approach, and then we show that an arbitrary LTL formula can be expressed in SCIFF, by providing a translation procedure from LTL to SCIFF which preserves compliance.

Słowa kluczowe

EN

linear temporal logic; abductive logic programming; compliance verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 159, nr 1/2
• Strony: 35--63
• Opis fizyczny: Bibliogr. 53 poz.

Twórcy

autor

Chesani F.

• University of Bologna, V.le Risorgimento 2, 40136 Bologna, Italy

autor

Gavanelli M.

• University of Ferrara, Via Saragat 1, 44122 Ferrara, Italy

autor

Lamma E.

• University of Ferrara, Via Saragat 1, 44122 Ferrara, Italy

autor

Mello P.

• University of Bologna, V.le Risorgimento 2, 40136 Bologna, Italy

autor

Montali M.

• Free Universty of Bozen-Bolzano, Piazza Domenicani 3, I-39100 Bolzano, Italy

Bibliografia

• [1] Prior AN. Past, Present and Future. Oxford University Press, 1967.
• [2] Emerson EA. Temporal and Modal Logic. In: van Leeuwen J (ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. Elsevier and MIT Press. 1990. ISBN: 0-444-88074-7, 0-262-22039-3.
• [3] Holzmann G. The model checker SPIN. Software Engineering, IEEE Transactions on. 1997;23(5):279-295. doi:10.1109/32.588521.
• [4] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma E, Larsen KG (eds.), CAV, volume 2404 of Lecture Notes in Computer Science. Springer, 2002 pp. 359-364. ISBN: 3-540-43997-8.
• [5] Pesic M, Schonenberg H, van der Aalst WMP. DECLARE: Full Support for Loosely-Structured Processes. In: Proceedings of the 11th IEEE International Enterprise Distributed Object Computing Conference (EDOC 2007). IEEE Computer Society, 2007 pp. 287-300. doi:10.1109/EDOC.2007.14.
• [6] Pesic M, van der Aalst WMP. A Declarative Approach for Flexible Business Processes Management. In: Eder J, Dustdar S (eds.), Proceedings of the BPM 2006 Workshops (BPD, BPI, ENEI, GPWW, DPM, semantics4ws), volume 4103 of Lecture Notes in Computer Science. Springer, 2006 pp. 169-180. URL https://doi.org/10.1007/11837862_18.
• [7] Pesic M. Constraint-Based Workflow Management Systems: Shifting Controls to Users. Ph.D. thesis, Beta Research School for Operations Management and Logistics, Eindhoven, 2008.
• [8] Montali M. Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach, volume 56 of Lecture Notes in Business Information Processing. Springer, 2010. doi:10.1007/978-3-642-14538-4_1.
• [9] Awad A, Decker G, Weske M. Efficient Compliance Checking Using BPMN-Q and Temporal Logic. In: Dumas M, Reichert M, Shan MC (eds.), 6th International Conference on Business Process Management (BPM 2008), volume 5240 of Lecture Notes in Computer Science. Springer, 2008 pp. 326-341. URL https://doi.org/10.1007/978-3-540-85758-7_24.
• [10] van der Aalst W, de Beer H, van Dongen B. Process Mining and Verification of Properties: An Approach based on Temporal Logic. In: Meersman R, Tari Z (eds.), Proceedings of the OTM 2005 Confederated International Conferences CoopIS, DOA, and ODBASE, volume 3760 of Lecture Notes in Computer Science. Springer, 2005 pp. 130-147. URL https://doi.org/10.1007/11575771_11.
• [11] Artikis A, Sergot M, Pitt J. Specifying Norm-Governed Computational Societies. ACM Transactions on Computational Logic, 2009;10(1):1-42. doi:http://doi.acm.org/10.1145/1459010.1459011.
• [12] Fornara N, Colombetti M. Specifying Artificial Institutions in the Event Calculus. In: Dignum [53], 2009 pp. 335-366.
• [13] Roman D, Kifer M. Semantic Web Service Choreography: Contracting and Enactment. In: Sheth AP, Staab S, Dean M, Paolucci M, Maynard D, Finin TW, Thirunarayan K (eds.), Proceedings of the 7th International Semantic Web Conference (ISWC 2008), volume 5318 of Lecture Notes in Computer Science. Springer, 2008 pp. 550-566. URL https://doi.org/10.1007/978-3-540-88564-1_35.
• [14] Baldoni M, Baroglio C, Martelli A, Patti V. Reasoning about Interaction Protocols for Customizing Web Service Selection and Composition. Journal of Logic and Algebraic Programming, special issue on Web Services and Formal Methods, 2007;70(1):53-73. URL https://doi.org/10.1016/j.jlap.2006.05.005.
• [15] De Nicola A, Missikoff M, Proietti M, Smith F. A Logic-Based Method for Business Process Knowledge Base Management. In: Bergamaschi S, Lodi S, Martoglia R, Sartori C (eds.), 8th Italian Symposium on Advanced Database Systems. Rimini, Italy, 2010 pp. 170-181.
• [16] Alberti M, Chesani F, Gavanelli M, Lamma E, Mello P, Torroni P. Verifiable agent interaction in abductive logic programming: the SCIFF framework. ACM Transactions on Computational Logic, 2008;9(4):29:1-29:43. doi:10.1145/1380572.1380578.
• [17] Alberti M, Gavanelli M, Lamma E, Mello P, Torroni P, Sartor G. Mapping deontic operators to abductive expectations. Computational & Mathematical Organization Theory, 2006;12(2-3):205-225. URL https://doi.org/10.1007/s10588-006-9544-8.
• [18] Chesani F, Mello P, Montali M, Torroni P. Commitment Tracking via the Reactive Event Calculus. In: Boutilier C (ed.), Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009), 2009 pp. 91-96. URL http://dl.acm.org/citation.cfm?id=1661445.1661461.
• [19] Alberti M, Cattafi M, Chesani F, Gavanelli M, Lamma E, Mello P, Montali M, Torroni P. A Computational Logic Application Framework for Service Discovery and Contracting. Int. J. Web Service Res., 2011;8(3):1-25. doi:10.4018/IJWSR.2011070101. URL https://doi.org/10.4018/IJWSR.2011070101.
• [20] Montali M, Pesic M, van der Aalst WMP, Chesani F, Mello P, Storari S. Declarative Specification and Verification of Service Choreographies. ACM Transactions on the Web, 2010;4(1):3-1-3-62. doi:10.1145/1658373.1658376.
• [21] Montali M, Torroni P, Chesani F, Mello P, Alberti M, Lamma E. Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business Processes. Fundamenta Informaticae, 2010;102(3-4):325-361. URL http://dl.acm.org/citation.cfm?id=1890507.1890512.
• [22] Fung TH, Kowalski RA. The IFF Proof Procedure for Abductive Logic Programming. Logic Programming, 1997;33(2):151-165. URL https://doi.org/10.1016/S0743-1066(97)00026-5.
• [23] Dumas M, Rosa ML, Mendling J, Reijers HA. Fundamentals of Business Process Management. Springer, 2013. ISBN: 978-3-642-33142-8. doi:10.1007/978-3-642-33143-5. URL http://dx.doi.org/10.1007/978-3-642-33143-5.
• [24] Chopra AK, Singh MP. Producing Compliant Interactions: Conformance, Coverage, and Interoperability. In: Proceedings of the 4th International Conference on Declarative Agent Languages and Technologies, DALT’06. Springer-Verlag, Berlin, Heidelberg, 2006 pp. 1-15. ISBN: 3-540-68959-1, 978-3-540-68959-1. doi:10.1007/11961536n_1. URL http://dx.doi.org/10.1007/11961536_1.
• [25] Governatori G, Rotolo A. Norm Compliance in Business Process Modeling. In: RuleML 2010, Procs., volume 6403 of LNCS. Springer, 2010 pp. 194-209. ISBN: 978-3-642-16288-6.
• [26] Governatori G, Hashmi M, Lam H, Villata S, Palmirani M. Semantic Business Process Regulatory Compliance Checking Using LegalRuleML. In: EKAW 2016, Procs., volume 10024 of LNCS. Springer, 2016 pp. 746-761. ISBN: 978-3-319-49003-8.
• [27] Fisher M, Dixon C, Peim M. Clausal Temporal Resolution. ACM Transactions on Computational Logic, 2001;2(1):12-56. doi:10.1145/371282.371311.
• [28] Montali M, Torroni P, Alberti M, Chesani F, Gavanelli M, Lamma E, Mello P. Verification from Declarative Specifications Using Logic Programming. In: de la Banda MG, Pontelli E (eds.), Logic Programming, 24th International Conference, ICLP 2008, Udine, Italy, December 9-13 2008, Proceedings, volume 5366 of Lecture Notes in Computer Science. Springer, 2008 pp. 440-454. ISBN: 978-3-540-89981-5, doi:10.1007/978-3-540-89982-2_39. URL http://dx.doi.org/10.1007/978-3-540-89982-2_39.
• [29] Kakas AC, Kowalski RA, Toni F. Abductive Logic Programming. Journal of Logic and Computation, 1993;2(6):719-770.
• [30] Lloyd JW. Foundations of Logic Programming. Springer, 2nd edition, 1987. doi:10.1007/978-3-642-83189-8.
• [31] Jaffar J, Maher MJ. Constraint Logic Programming: a Survey. Logic Programming, 1994;19-20:503-582. URL https://doi.org/10.1016/0743-1066(94)90033-7.
• [32] Torroni P, Chesani F, Yolum P, Gavanelli M, Singh MP, Lamma E, Alberti M, Mello P. Modelling Interactions via Commitments and Expectations. In: Dignum [53], 2009 pp. 263-284.
• [33] Kunen K. Negation in Logic Programming. J. Log. Program., 1987;4(4):289-308. URL https://doi.org/10.1016/0743-1066(87)90007-0.
• [34] Clark KL. Negation as Failure. In: Gallaire H, Minker J (eds.), Logic and Data Bases, pp. 293-322. Plenum Press, 1978.
• [35] Jaffar J, Maher MJ, Marriott K, Stuckey PJ. The Semantics of Constraint Logic Programs. J. Log. Program., 1998;37(1-3):1-46. URL https://doi.org/10.1016/S0743-1066(98)10002-X.
• [36] Evans C, Kakas AC. Hypothetico-deductive Reasoning. In: Fifth Generation Computer Systems. IOS Press, 1992 pp. 546-554.
• [37] Alberti M, Gavanelli M, Lamma E, Mello P, Torroni P. Abduction with hypotheses confirmation. In: Giunchiglia F (ed.), IJCAI-05 Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence. Professional Book Center, USA, 2005 pp. 1545-1546. ISBN: 0-938075-93-4.
• [38] Montali M. Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach. Ph.D. thesis, University of Bologna, 2009.
• [39] Heljanko K, Niemelä I. Bounded LTL model checking with stable models. TPLP, 2003;3(4-5):519-550. doi:10.1017/S1471068403001790. URL http://dx.doi.org/10.1017/S1471068403001790.
• [40] Delzanno G, Podelski A. Constraint-based deductive model checking. STTT, 2001;3(3):250-270. doi:10.1007/s100090100049. URL http://dx.doi.org/10.1007/s100090100049.
• [41] Ramakrishna YS, Ramakrishnan CR, Ramakrishnan IV, Smolka SA, Swift T, Warren DS. Efficient Model Checking Using Tabled Resolution. In: Grumberg O (ed.), Computer Aided Verification, 9th International Conference, CAV ’97, Haifa, Israel, June 22-25, 1997, Proceedings, volume 1254 of Lecture Notes in Computer Science. Springer, 1997 pp. 143-154. ISBN: 3-540-63166-6. doi:10.1007/3-540-63166-6_16. URL http://dx.doi.org/10.1007/3-540-63166-6_16.
• [42] Nilsson U, Lübcke J. Constraint Logic Programming for Local and Symbolic Model-Checking. In: Lloyd JW, Dahl V, Furbach U, Kerber M, Lau K, Palamidessi C, Pereira LM, Sagiv Y, Stuckey PJ (eds.), Computational Logic - CL 2000, First International Conference, London, UK, 24-28 July, 2000, Proceedings, volume 1861 of Lecture Notes in Computer Science. Springer, 2000 pp. 384-398. ISBN: 3-540-67797-6. doi:10.1007/3-540-44957-4_26. URL http://dx.doi.org/10.1007/3-540-44957-4_26.
• [43] Smith F, Proietti M. Rule-based Behavioral Reasoning on Semantic Business Processes. In: Filipe J, Fred ALN (eds.), ICAART 2013 - Proceedings of the 5th International Conference on Agents and Artificial Intelligence, Volume 2, Barcelona, Spain, 15-18 February, 2013. SciTePress, 2013 pp. 130-143. ISBN: 978-989-8565-39-6.
• [44] Giordano L, Martelli A, Spiotta M, Dupré DT. Business process verification with constraint temporal answer set programming. TPLP, 2013;13(4-5):641-655. doi:10.1017/S1471068413000409. URL http://dx.doi.org/10.1017/S1471068413000409.
• [45] Henriksen JG, Thiagarajan PS. Dynamic Linear Time Temporal Logic. Ann. Pure Appl. Logic, 1999;96(1-3):187-207. doi:10.1016/S0168-0072(98)00039-6. URL http://dx.doi.org/10.1016/S0168-0072(98)00039-6.
• [46] Havelund K, Rosu G. Testing Linear Temporal Logic Formulae on Finite Execution Traces. Technical Report TR 01-08, RIACS Technical Report, 2001.
• [47] Gelfond M, Lobo J. Authorization and Obligation Policies in Dynamic Systems. In: De La Banda MG, Pontelli E (eds.), 24th International Conference on Logic Programming (ICLP), number 5366 in Lecture Notes in Computer Science. Springer, 2008 pp. 22-36. URL https://doi.org/10.1007/978-3-540-89982-2_7.
• [48] Xanthakos I. Semantic Integration of Information by Abduction. Ph.D. thesis, Imperial College London, 2003.
• [49] Fisher M. Implementing Temporal Logics: Tools for Execution and Proof (Tutorial Paper). In: Toni F, Torroni P (eds.), CLIMA VI, volume 3900 of Lecture Notes in Computer Science. Springer. 2005 pp. 129-142. ISBN: 3-540-33996-5.
• [50] Gupta G, Pontelli E. A constraint-based approach for specification and verification of real-time systems. In: IEEE Real-Time Systems Symposium. IEEE Computer Society, 1997 pp. 230-239. doi:10.1109/REAL.1997.641285.
• [51] De Giacomo G, De Masellis R, Montali M. Reasoning on LTL on Finite Traces: Insensitivity to Infiniteness. In: Brodley CE, Stone P (eds.), Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI). AAAI Press/The MIT Press, 2014 pp. 1027-1033. ISBN: 978-1-57735-661-5. URL http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8575.
• [52] Bauer A, Leucker M, Schallhart C. Comparing LTL Semantics for Runtime Verification. Logic and Computation, 2010;20(3):651-674. doi:10.1093/logcom/exn075.
• [53] Dignum V (ed.). Handbook of Research on Multi-Agent Systems: Semantics and Dynamics of Organizational Models. IGI Global, 2009. ISBN: 1605662569.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).