Affiliations: DEIS, University of Bologna, V.le Risorgimento, 2, 40136 Bologna, Italy. {federico.chesani | paola.mello | marco.montali | paolo.torroni}@unibo.it
Note: [] Address for correspondence: University of Bologna โ V.le Risorgimento, 2 โ 40136 Bologna, Italy
Abstract: Since its introduction, the Event Calculus (โฐ๐) 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 โฐ๐ 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 โฐ๐ 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 โฐ๐, called โโฐ๐, 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.
