TY - GEN
T1 - Temporal deontic action logic for the verification of compliance to norms in ASP
AU - Giordano, Laura
AU - Martelli, Alberto
AU - Dupré, Daniele Theseider
PY - 2013
Y1 - 2013
N2 - The verification of compliance of business processes to norms requires the representation of different kinds of obligations, including achievement obligations, maintenance obligations, obligations with deadlines and contrary to duty obligations. In this paper we develop a deontic temporal extension of Answer Set Programming (ASP) suitable for verifying compliance of a business process to norms involving such different types of obligations. To this end, we extend Dynamic Linear Time Temporal Logic (DLTL) with deontic modalities to define a Deontic DLTL. We then combine it with ASP to define a deontic action language in which until formulas and next formulas are allowed to occur within deontic modalities. We show that in the language we can model the different kinds of obligations which are useful in the verification of compliance to normative requirements. The verification can be performed by bounded model checking techniques.
AB - The verification of compliance of business processes to norms requires the representation of different kinds of obligations, including achievement obligations, maintenance obligations, obligations with deadlines and contrary to duty obligations. In this paper we develop a deontic temporal extension of Answer Set Programming (ASP) suitable for verifying compliance of a business process to norms involving such different types of obligations. To this end, we extend Dynamic Linear Time Temporal Logic (DLTL) with deontic modalities to define a Deontic DLTL. We then combine it with ASP to define a deontic action language in which until formulas and next formulas are allowed to occur within deontic modalities. We show that in the language we can model the different kinds of obligations which are useful in the verification of compliance to normative requirements. The verification can be performed by bounded model checking techniques.
KW - Compliance Verification
KW - Deontic Logic
KW - Reasoning about Actions
KW - Temporal Logic
UR - http://www.scopus.com/inward/record.url?scp=84883539004&partnerID=8YFLogxK
U2 - 10.1145/2514601.2514608
DO - 10.1145/2514601.2514608
M3 - Conference contribution
AN - SCOPUS:84883539004
SN - 9781450320801
T3 - Proceedings of the International Conference on Artificial Intelligence and Law
SP - 53
EP - 62
BT - Proceedings of the 14th International Conference on Artificial Intelligence and Law, ICAIL 2013
T2 - 14th International Conference on Artificial Intelligence and Law, ICAIL 2013
Y2 - 10 June 2013 through 14 June 2013
ER -