Temporal deontic action logic for the verification of compliance to norms in ASP

The verification of compliance of business processes to norms re- quires the representation of different kinds of obligations, includ- ing 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 re- quirements. The verification can be performed by bounded model checking techniques.