Evaluating compliance: from LTL to abductive logic programming

The compliance verification task amounts to establishing if the execution of a system, given in terms of observed events, does re- spect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to as- sess compliance. In this work we review the LTL and the Abductive Logic Programming 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 pro- viding an automatic translation procedure from LTL to SCIFF which preserves compliance.