Temporal Specification Optimisation for the Event Calculus

Abstract

Temporal pattern matching tasks require the detection of situations of interest based on streams of symbolic events. The Run-Time Event Calculus (RTEC) is a formal framework that represents situations of interest as time-varying properties called 'fluents'. Temporal patterns often express 'Boolean combinations' of situations; RTEC features two types of fluents that may model such patterns: 'simple' and 'statically determined'. A simple fluent representation, however, is exponentially larger and more expensive to reason with than the corresponding statically determined fluent one. We formally identify the class of simple fluent definitions that can be translated into statically determined fluent definitions. Moreover, we present a compiler for the translation, and a reproducible empirical evaluation on real applications.