TY - GEN
T1 - Verifying business process compliance by reasoning about actions
AU - D'Aprile, Davide
AU - Giordano, Laura
AU - Gliozzi, Valentina
AU - Martelli, Alberto
AU - Pozzato, Gian Luca
AU - Theseider Dupré, Daniele
N1 - Funding Information:
This work has been partially supported by Regione Piemonte, Project “ICT4LAW - ICT Converging on Law: Next Generation Services for Citizens, Enterprises, Public Administration and Policymakers”.
PY - 2010
Y1 - 2010
N2 - In this paper we address the problem of verifying business process compliance with norms. To this end, we employ reasoning about actions in a temporal action theory. The action theory is defined through a combination of Answer Set Programming and Dynamic Linear Time Temporal Logic (DLTL). The temporal action theory allows us to formalize a business process as a temporal domain description, possibly including temporal constraints. Obligations in norms are captured by the notion of commitment, which is borrowed from the social approach to agent communication. Norms are represented using (possibly) non monotonic causal laws which (possibly) enforce new obligations. In this context, verifying compliance amounts to verify that no execution of the business process leaves some commitment unfulfilled. Compliance verification can be performed by Bounded Model Checking.
AB - In this paper we address the problem of verifying business process compliance with norms. To this end, we employ reasoning about actions in a temporal action theory. The action theory is defined through a combination of Answer Set Programming and Dynamic Linear Time Temporal Logic (DLTL). The temporal action theory allows us to formalize a business process as a temporal domain description, possibly including temporal constraints. Obligations in norms are captured by the notion of commitment, which is borrowed from the social approach to agent communication. Norms are represented using (possibly) non monotonic causal laws which (possibly) enforce new obligations. In this context, verifying compliance amounts to verify that no execution of the business process leaves some commitment unfulfilled. Compliance verification can be performed by Bounded Model Checking.
UR - https://www.scopus.com/pages/publications/77956540824
U2 - 10.1007/978-3-642-14977-1_10
DO - 10.1007/978-3-642-14977-1_10
M3 - Conference contribution
AN - SCOPUS:77956540824
SN - 3642149766
SN - 9783642149764
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 99
EP - 116
BT - Computational Logic in Multi-Agent Systems - 11th International Workshop, CLIMA XI, Proceedings
T2 - 11th International Workshop on Computational Logic in Multi-Agent Systems, CLIMA XI
Y2 - 16 August 2010 through 17 August 2010
ER -