Wyniki wyszukiwania - BazTech

1

Evaluating Compliance : From LTL to Abductive Logic Programming

Chesani F., Gavanelli M., Lamma E., Mello P., Montali M.

Fundamenta Informaticae

|

2018

|

Vol. 159, nr 1/2

35--63

EN

The compliance verification task amounts to establishing if the execution of a system, given in terms of observed happened events, does respect a given property. In the past both the frameworks of Temporal Logics and Logic Programming have been extensively exploited to assess compliance in different domains, such as normative multi-agent systems, business process management and service oriented computing. In this work we review the LTL and SCIFF 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 providing a translation procedure from LTL to SCIFF which preserves compliance.

2

Compliance in Business Processes with Incomplete Information and Time Constraints : a General Framework based on Abductive Reasoning

Chesani F., Mello P., Montali M., Tessaris S., De Masellis R., Di Francescomarino C., Ghidini C.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 1/2

75--111

EN

The capability to store data about Business Process (BP) executions in so-called Event Logs has brought to the identification of a range of key reasoning services (consistency, compliance, runtime monitoring, prediction) for the analysis of process executions and process models. Tools for the provision of these services typically focus on one form of reasoning alone. Moreover, they are often very rigid in dealing with forms of incomplete information about the process execution. While this enables the development of ad hoc solutions, it also poses an obstacle for the adoption of reasoning-based solutions in the BP community. In this paper, we introduce the notion of Structured Processes with Observability and Time (SPOT models), able to support incompleteness (of traces and logs), and temporal constraints on the activity duration and between activities. Then, we exploit the power of abduction to provide a flexible, yet computationally effective framework able to reinterpret key reasoning services in terms of incompleteness and observability in a uniform way.

3

A Logic-Based, Reactive Calculus of Events

Chesani F., Mello P., Montali M., Torroni P.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 1/2

135-161

EN

Since its introduction, the Event Calculus (EC) has been recognized for being an excellent framework to reason about time and events, and it has been applied to a variety of domains. However, its formalization inside logic-based frameworks has been mainly based on backward, goal-oriented reasoning: given a narrative (also called execution trace) and a goal, logic-based formalizations of EC focus on proving the goal, i.e., establishing if a property (called fluent) holds. These approaches are therefore unsuitable in dynamic environments, where the narrative typically evolves over time: indeed, each occurrence of a new event requires to restart the reasoning process from scratch. Ad-hoc, procedural methods and implementations have been then proposed to overcome this issue. However, they lack a strong formal basis and cannot guarantee formal properties. As a consequence, the applicability of EC has been somehow limited in large application domains such as run-time monitoring and event processing, which require at the same time reactivity features as well as formal properties to provide guarantees about the computed response. We overcome the highlighted issues by proposing a Reactive and logic-based axiomatization of EC, called REC, on top of the SCIFF Abductive Logic Programming framework. Our solution exhibits the features of a reactive verification facility, while maintaining a solid formal background.

4

Abductive Logic Programming as an Effective Technology for the Static Verification of Declarative Business Processes

Montali M., Torroni P., Chesani F., Mello P., Alberti M., Lamma E.

Fundamenta Informaticae

|

2010

|

Vol. 102, nr 3/4

325-361

EN

We discuss the static verification of declarative Business Processes. We identify four desiderata about verifiers, and propose a concrete framework which satisfies them. The framework is based on the ConDec graphical notation for modeling Business Processes, and on Abductive Logic Programming technology for verification of properties. Empirical evidence shows that our verification method seems to perform and scale better, in most cases, than other state of the art techniques (model checkers, in particular). A detailed study of our framework's theoretical properties proves that our approach is sound and complete when applied to ConDec models that do not contain loops, and it is guaranteed to terminate when applied to models that contain loops.