TY - JOUR
T1 - Verifying compliance of business processes with temporal answer sets
AU - D'Aprile, Davide
AU - Giordano, Laura
AU - Gliozzi, Valentina
AU - Martelli, Alberto
AU - Pozzato, Gian Luca
AU - Dupré, Daniele Theseider
PY - 2011
Y1 - 2011
N2 - In this paper we provide a framework for the specification and the verification of business processes, which is based on a temporal extension of answer set programming (ASP) and we address the problem of verifying the compliance of business processes to norms. The logical formalism we use, is a combination of Answer Set Programming and Dynamic Linear Time Temporal Logic (DLTL), and allows for a declarative specification of a business process, as well as the specification of norms, by means of a set of temporal rules and a set of temporal constraints. A notion of commitment, borrowed from the social approach to agent communication, is used to capture obligations within norms. Besides allowing for a declarative specification of business processes, the proposed framework can be used for encoding business processes specified in conventional workflow languages. The verification of temporal properties of a business process, expressed by temporal formulas, can be done by encoding bounded model checking techniques in ASP. Verifying compliance of a business process to norms consists, in particular, in verifying that there are no executions of the business process which leave commitments unfulfilled.
AB - In this paper we provide a framework for the specification and the verification of business processes, which is based on a temporal extension of answer set programming (ASP) and we address the problem of verifying the compliance of business processes to norms. The logical formalism we use, is a combination of Answer Set Programming and Dynamic Linear Time Temporal Logic (DLTL), and allows for a declarative specification of a business process, as well as the specification of norms, by means of a set of temporal rules and a set of temporal constraints. A notion of commitment, borrowed from the social approach to agent communication, is used to capture obligations within norms. Besides allowing for a declarative specification of business processes, the proposed framework can be used for encoding business processes specified in conventional workflow languages. The verification of temporal properties of a business process, expressed by temporal formulas, can be done by encoding bounded model checking techniques in ASP. Verifying compliance of a business process to norms consists, in particular, in verifying that there are no executions of the business process which leave commitments unfulfilled.
UR - http://www.scopus.com/inward/record.url?scp=84870620678&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:84870620678
SN - 1613-0073
VL - 810
SP - 147
EP - 161
JO - CEUR Workshop Proceedings
JF - CEUR Workshop Proceedings
T2 - 26th Italian Conference on Computational Logic, CILC 2011
Y2 - 31 August 2011 through 2 September 2011
ER -