Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. In this paper, we conduct a systematic analysis of EC by which we gain a better understanding of this formalism and determine ways of augmenting its expressive power. The keystone of this endeavor is the definition of an extendible formal specification of its functionalities. This formalization has the effects of casting determination of MVIs as a model checking problem, of setting the ground for studying and comparing the expressiveness and complexity of various extensions of EC, and of establishing a semantic reference against which to verify the soundness and completeness of implementations. We extend the range of queries accepted by EC, which is limited to Boolean combinations of MVI verification or computation requests, to support arbitrary quantification over events and modal queries. We also admit specifications based on preconditions. We demonstrate the added expressive power by encoding a number of diagnosis problems. Moreover, we provide a systematic comparison of the expressiveness and complexity of the various extended event calculi against each other. Finally, we propose a declarative encoding of these enriched event calculi in the logic programming language lambda Prolog and prove the soundness and completeness of the resulting logic programs.
A Guided Tour Through some Extensions of the Event Calculus
FRANCESCHET, Massimo;MONTANARI, Angelo
2000-01-01
Abstract
Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. In this paper, we conduct a systematic analysis of EC by which we gain a better understanding of this formalism and determine ways of augmenting its expressive power. The keystone of this endeavor is the definition of an extendible formal specification of its functionalities. This formalization has the effects of casting determination of MVIs as a model checking problem, of setting the ground for studying and comparing the expressiveness and complexity of various extensions of EC, and of establishing a semantic reference against which to verify the soundness and completeness of implementations. We extend the range of queries accepted by EC, which is limited to Boolean combinations of MVI verification or computation requests, to support arbitrary quantification over events and modal queries. We also admit specifications based on preconditions. We demonstrate the added expressive power by encoding a number of diagnosis problems. Moreover, we provide a systematic comparison of the expressiveness and complexity of the various extended event calculi against each other. Finally, we propose a declarative encoding of these enriched event calculi in the logic programming language lambda Prolog and prove the soundness and completeness of the resulting logic programs.File | Dimensione | Formato | |
---|---|---|---|
ci.pdf
non disponibili
Tipologia:
Altro materiale allegato
Licenza:
Non pubblico
Dimensione
395.15 kB
Formato
Adobe PDF
|
395.15 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.