Temporal Specification Optimisation for the Event Calculus

Temporal Specification Optimisation for the Event Calculus Periklis Mantenoglou1, Alexander Artikis1,2 1NCSR “Demokritos”, Greece 2University of Piraeus, Greece [email protected], [email protected] 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. Introduction Temporal pattern matching involves the detection of situations of interest based on streams of symbolic events. In composite event recognition, e.g., we need to reason over streams of time-stamped, symbolic events in order to detect instances of composite activities (Giatrakos et al. 2020). Temporal pattern matching requires a formal language that defines a set of operators between events and determines the syntactical form of the patterns defining situations of interest. These patterns often express ‘Boolean combinations’ of situations, featuring conjunction, disjunction and negation operators. In human activity recognition, e.g., we may say that two people are meeting when they are close to each other and one of them is ‘active’, i.e., moving her arms while in the same position. Another way of defining a situation of interest is through the law of inertia, i.e., the situation is initiated based on pattern satisfaction, and then persists through time, as long as a pattern terminating the situation is not satisfied. In the maritime domain, e.g., we may say that a vessel is performing a ‘trawling’ fishing activity if the vessel started performing sharp turns in a fishing area a short time ago, and has not left the fishing area since. There are several frameworks for temporal pattern matching that employ automata. CORE, e.g., is an automata-based system with highly efficient reasoning algorithms (Bucchi et al. 2022). CORE, however, does not support relational Copyright © 2025, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. concepts, and thus cannot express a ‘meeting’ activity between two persons. Furthermore, automata-based systems commonly model time implicitly (Giatrakos et al. 2020), complicating the representation of the law of inertia. There are also logic-based frameworks. MeTeoR extends a fragment of DatalogMTL with windows, but does not support negation (Walega et al. 2023). LARS (Beck et al. 2018) is a temporal specification language with several implementations (Beck et al. 2017; Bazoobandi et al. 2017; Eiter et al. 2019). LARS-based engines cannot express durative composite activity definitions, such as ‘trawling’. The Event Calculus is a logic programming formalism for representing and reasoning about events and their effects over time (Kowalski and Sergot 1986); it includes instantaneous events and time-varying properties called ‘fluents’. The Event Calculus supports durative and relational situations of interest, and a built-in representation of inertia. Several Event Calculus-based frameworks are found in the literature (Chittaro and Montanari 1996; Paschke and Bichler 2008; Chesani et al. 2013; Kafali et al. 2017; Baumgartner 2021; Arias et al. 2022). jREC, e.g., is a ‘reactive’ Event Calculus dialect that supports data streams (Montali et al. 2013; Falcionelli et al. 2019). The Run-Time Event Calculus (RTEC) extends the Event Calculus with optimisation techniques for data streams, such windowing, caching and indexing (Artikis et al. 2015; Mantenoglou et al. 2022, 2023), and has proven highly efficient in real applications (Tsilionis et al. 2022). In RTEC, it is possible to represent a situation of interest as a ‘simple’ or a ‘statically determined’ fluent. Simple fluents are defined in terms of their initiations and terminations, and the law of inertia. Statically determined fluents are defined as Boolean combinations of other fluents. While a simple fluent representation for such a Boolean combination is possible, it is exponentially larger and more expensive to reason with than the corresponding statically determined fluent definition. Therefore, whenever possible, a situation of interest should be defined as a statically determined fluent. Unfortunately, the knowledge engineer may not always employ the most efficient definition of a fluent. For instance, the engineer may be working on a knowledge base that was developed for an Event Calculus-based framework that does not feature statically determined fluents. In a legal contract verification framework (Sharifi et al. 2020; Parvizimosaed et al. 2022), e.g., the Event Calculus representation for the rights-holder of a contract can be optimised using a statically determined fluent definition. As another example, in a distributed authorisation policy management framework (Zahoor et al. 2022, 2023), the Event Calculus representations for policy conflicts and redundant policies can be re-written as statically determined fluents. Moreover, the engineer may detect only a portion of the composite activities that can be defined as statically determined fluents, resulting in inefficiencies when reasoning over the simple fluents that could have been written as statically determined ones. To address this issue, we propose a compiler that optimises temporal specifications in RTEC. Our contributions are the following. First, we formally identify the class of simple fluent definitions that can be translated into statically determined fluent definitions. Second, we provide a compiler for the translation and prove its correctness. Third, we present a reproducible empirical evaluation on knowledge bases and data streams of real applications, i.e., composite event recognition, legal contract verification, clinical guideline monitoring and distributed authorisation policy management. Our compiler reduced the size of these knowledge bases by orders of magnitude, leading to significant reasoning efficiency gains. The proofs of all propositions of the paper and the resources for reproducing our experiments are publicly available1. The Run-Time Event Calculus Representation. The language of RTEC is many-sorted, including sorts for representing time, instantaneous events and fluents. RTEC employs a linear time-line with non-negative integer time-points. A ‘fluent-value pair’ (FVP) F=Vdenotes that fluent Fhas value V.happensAt(E,T)signifies that event Eoccurs at time-point T.initiatedAt(F=V,T) (resp. terminatedAt(F=V,T)) expresses that a time period during which a fluent Fhas the value Vcontinuously is initiated (terminated) at T.holdsAt(F=V,T)states that F has value Vat T, while holdsFor(F=V,I)expresses that F=Vholds continuously in the intervals included in list I. A formalisation of the temporal specifications of a domain in RTEC is called event description. Definition 1 (Event Description).An event description is a set of: • ground happensAt(E,T)facts, expressing an input stream of event instances, • rules with head initiatedAt(F=V,T)or terminatedAt(F=V,T), expressing the effects of events on FVP F=V, and • rules with head holdsFor(F=V,I), defining FVP F=V based on other FVPs. ■ RTEC features two types of FVPs: ‘simple’ and ‘statically determined’. A simple FVP F=Vis defined via a set of initiatedAt(F=V,T)and terminatedAt(F=V,T)rules. Example 1 (‘Meeting’ as a Simple FVP).In human activity recognition, the task is to detect composite human activities of interest, such as illegal, suspicious and violent activ1https://github.com/periklismant/aaai2025 supplementary ities, based on streams containing symbolic representations of video feeds. We may use the fluent meeting(P1,P2)to express that people P1and P2are having a meeting, while the value of meeting(P1,P2)denotes the stage of the meeting. The simple FVP meeting(P1,P2) = interacting can be specified with the following rules: initiatedAt(meeting(P1,P2) = interacting,T)← happensAt(start(active(P1) = true),T), holdsAt(close(P1,P2) = true,T), not happensAt(end(close(P1,P2) = true),T). (1) initiatedAt(meeting(P1,P2) = interacting,T)← happensAt(start(close(P1,P2) = true),T), holdsAt(active(P1) = true,T), not happensAt(end(active(P1) = true),T). (2) initiatedAt(meeting(P1,P2) = interacting,T)← happensAt(start(active(P1) = true),T), happensAt(start(close(P1,P2) = true),T). (3) terminatedAt(meeting(P1,P2) = interacting,T)← happensAt(end(active(P1) = true),T).(4) terminatedAt(meeting(P1,P2) = interacting,T)← happensAt(end(close(P1,P2) = true),T).(5) According to rules (1)–(3), P1and P2start interacting when P1starts being ‘active’, while P1and P2remain close to each other (rule (1)), P1and P2come close to each other, while P1continues being active (rule (2)), or P1starts being active, and P1and P2start being close to each other at the same time (rule (3)). According to rules (4)–(5), P1and P2 stop interacting when P1stops being active (rule (4)), or when P1and P2stop being close to each other (rule (5)). ♢ The auxiliary start and end events allow for succinct event descriptions and reasoning optimisations. For a simple FVP F=V, these events are defined as follows: happensAt(start(F=V),T)← initiatedAt(F=V,T),not holdsAt(F=V,T).(6) happensAt(end(F=V),T)← terminatedAt(F=V,T),holdsAt(F=V,T).(7) Rule (6) states that start(F=V)takes place at time-point T if F=Vis initiated at Tand F=Vdoes not hold at T, i.e., start(F=V)marks the initiations of F=Vthat bring about a new time period where F=Vholds continuously. Similarly, based on rule (7), end(F=V)marks the terminations Tof F=Vfor which F=Vholds at T. Definition 2 (Syntax of Rules Defining Simple FVPs).Consider a simple FVP F=V. The initiatedAt(F=V,T)rules of the event description have the following syntax: initiatedAt(F=V,T)← happensAt(E1,T)[[,[not]happensAt(E2,T), . . . , [not]happensAt(En,T),[not]holdsAt(F1=V1,T), . . . , [not]holdsAt(Fk=Vk,T)]]. The first body literal of an initiatedAt rule is a positive happensAt predicate; this is followed by a possibly empty set, denoted by ‘[[ ]]’, of positive/negative happensAt and holdsAt predicates. ‘not’ expresses negation-by-failure (Clark 1977), while ‘[not]’ denotes that ‘not’ is optional. Ei, where i∈[1,n], denotes an event of the domain, or an auxiliary event start(F′=V′)or end(F′=V′), where F′=V′is an FVP. All (head and body) predicates are evaluated on the same time-point T. The bodies of terminatedAt(F=V,T) rules have the same form. ■ The definition of a simple FVP F=Vis a pair of sets (Rs,Re); set Rs(resp. Re) contains rules with head initiatedAt(F=V,T)(terminatedAt(F=V,T)). (Rs m,Re m), e.g., where Rs m(Re m) contains rules (1)–(3) (rules (4)–(5)), is a definition of meeting(P1,P2) = interacting. A statically determined FVP F=Vis defined via a rule with head holdsFor(F=V,I). Example 2 (‘Meeting’ as a Statically Determined FVP).We may define meeting(P1,P2) = interacting as a statically determined FVP using the following rule rm: holdsFor(meeting(P1,P2) = interacting,I)← holdsFor(active(P1) = true,Ia), holdsFor(close(P1,P2) = true,Ic), intersect all([Ia,Ic],I). (8) intersect all([Ia,Ic],I)is an interval manipulation construct, computing the list of maximal intervals Ias the intersection of all maximal intervals in lists Iaand Ic.rmstates that meeting(P1,P2) = interacting holds in the intervals where active(P1) = true and close(P1,P2) = true hold. ♢ Definition 3 (Syntax of Rules Defining Statically Determined FVPs).The definition of statically determined FVP F=Vis a rule that has the following syntax: holdsFor(F=V,In+m)← holdsFor(F1=V1,I1)[[,holdsFor(F2=V2,I2), . . . holdsFor(Fn=Vn,In),intervalConstruct(L1,In+1), . . . intervalConstruct(Lm,In+m)]]. The first body literal of a holdsFor rule defining F=Vis aholdsFor predicate expressing the maximal intervals of an FVP other than F=V. This is followed by a possibly empty list, denoted by ‘[[ ]]’, of holdsFor predicates and interval manipulation constructs, expressed by intervalConstruct. intervalConstruct(Lj,In+j)may be union all(Lj,In+j), intersect all(Lj,In+j)or relative complement all(Ik,Lj,In+j). Ik, where k<n+j, is a list of maximal intervals appearing earlier in the body of the rule, and list Ljcontains a subset of these lists. The output list In+mcontains the maximal intervals during which F=Vholds continuously. ■ union all(L,I)(resp. intersect all(L,I)) computes the list of maximal intervals Ias the union (intersection) of all lists of maximal intervals of list L.relative complement all(I′,L,I) computes the list of maximal intervals Iby removing from the maximal intervals of list I′all interval segments included in an interval of some list in L. The interval manipulation constructs of RTEC support the following type of definition: for all time-points T,F=V holds at Tif and only if some Boolean combination of FVPs holds at T. To aid the presentation, we often represent such Boolean combinations with ‘Boolean FVP definitions’, i.e., DNF formulas with literals that correspond to FVPs; these definitions are not in the language of RTEC. A Boolean FVP definition pmof meeting(P1,P2) = interacting, e.g., is: active(P1) = true ∧close(P1,P2) = true (9) In the following sections, we will show that pm,rm, i.e., rule (8), and (Rs m,Re m), i.e., rules (1)–(5), are equivalent definitions of meeting(P1,P2) = interacting. Reasoning. The key reasoning task of RTEC is the computation of holdsFor(F=V,I), i.e., the list of maximal intervals Iduring which each FVP holds continuously. For a statically determined FVP F=Vwith definition r, RTEC computes holdsFor(F=V,I)by evaluating the conditions of rule r. For a simple FVP F=Vwith definition (Rs,Re), RTEC operates as follows. First, RTEC computes the initiations and the terminations of F=V, by evaluating the rules in sets Rsand Re, respectively. Next, RTEC computes the maximal intervals of F=Vby matching each initiation Tsof F=Vwith the first termination Teof F=Vafter Ts, ignoring every intermediate initiation between Tsand Te. RTEC may then derive holdsAt(F=V,T)by checking whether Tbelongs to one of the maximal intervals of F=V. From Simple to Statically Determined FVPs In RTEC, a composite activity expressing a Boolean combination of other activities may be modelled as a simple or a statically determined FVP. The size of the resulting simple FVP definition, however, is exponential to the number of literals in the Boolean definition. The Boolean FVP definition of meeting(P1,P2) = interacting in formula (9), e.g., is a conjunction of 2 FVPs, i.e., active(P1) = true and close(P1,P2) = true. In order to specify the initiations of meeting(P1,P2) = interacting in rules (1)–(3), we had to explicitly declare the possible orders in which FVPs active(P1) = true and close(P1,P2) = true may come into effect, using one rule for each such order, leading to 3rules. In contrast, the equivalent statically determined FVP definition is 1rule with 3conditions (rule (8)). To express a conjunction of nFVPs with a simple FVP definition, we need 2n−1initiation rules, i.e., one rule for each subset of the FVPs in the conjunction that may start simultaneously; the equivalent statically determined FVP definition is 1rule with n+1conditions. Moreover, according to the complexity analysis of RTEC (Artikis et al. 2015), the worst-case cost of deriving the maximal intervals of a statically determined FVP is considerably lower than the cost of maximal interval computation for a simple FVP. These claims are further supported by our empirical evaluation, where we demonstrate that, in real applications, the use of statically determined FVPs leads to much more concise event descriptions and significantly more efficient reasoning than the use of simple FVPs. Therefore, whenever possible, a composite activity should be defined as a statically determined FVP. Previous work assumed that the event description developer was able to optimise an event description, by, e.g., identifying whether a composite activity can be expressed as a statically determined FVP (Artikis et al. 2015). Unfortunately, such as an assumption rarely holds in practice. Towards developing a compiler that automates event description development and addresses this issue, we formally iden- tify the class of simple FVP definitions that may be translated into equivalent statically determined FVP definitions. We use the following notion of FVP definition equivalence: Definition 4 (Equivalent FVP Definitions).Two definitions, D1and D2, for FVP F=Vare equivalent, if D1implies holdsAt(F=V,T)iff D2implies holdsAt(F=V,T).■ Proposition 1 (Equivalence between Statically Determined and Boolean FVP Definitions).For each statically determined FVP definition, there is an equivalent Boolean FVP definition, and vice versa. ♦ The statically determined FVP definition in rule (8), e.g., is equivalent with the Boolean FVP definition in formula (9). Proposition 1 states that every Boolean FVP definition can be translated into a statically determined FVP definition, and vice versa. Therefore, a simple FVP definition (Rs,Re) is translatable into a statically determined FVP definition iff there is a Boolean FVP definition that is equivalent with (Rs,Re). We outline, as an example, a proof demonstrating that simple FVP definition (Rs m,Re m)is translatable. Then, we present the class of translatable simple FVP definitions. Equivalence Proof for Running Example We prove that the simple FVP definition (Rs m,Re m), containing rules (1)–(5), and the Boolean FVP definition pm in formula (9) are equivalent, i.e., they compute the same holdsAt atoms for FVP meeting(P1,P2) = interacting. pmimplies holdsAt(meeting(P1,P2) = interacting,T) iff both active(P1) = true and close(P1,P2) = true hold at time-point T.(Rs m,Re m)implies the same holdsAt(meeting(P1,P2) = interacting,T)atoms as the program comprising rules (1)–(5) and the following formulation of the law of inertia: holdsAt(F=V,T)←initiatedAt(F=V,T−1).(10) holdsAt(F=V,T)←holdsAt(F=V,T−1), not terminatedAt(F=V,T−1).(11) Rule (10) states that F=Vholds at time-point Tif F=V is initiated at the previous time-point T−1. Rule (11) expresses that F=Vholds at Tif F=Vholds at T−1and F=Vis not terminated at T−1. We prove that (Rs m,Re m)and pmare equivalent with an inductive proof on time-point T. Below, we outline the inductive step for time-point T(equivalences (12)–(16)), assuming that (Rs m,Re m)and pmimply the same holdsAt atoms at time-point T−1. The base of the induction is presented in the technical appendix1. (Rs m,Re m)|=holdsAt(meeting(P1,P2) = interacting,T) ↔(initiatedAt(meeting(P1,P2) = interacting,T−1)(12) ∨(holdsAt(meeting(P1,P2) = interacting,T−1)∧ ¬terminatedAt(meeting(P1,P2) = interacting,T−1))) ↔(b(1)@T−1∨b(2)@T−1∨b(3)@T−1∨(13) (holdsAt(active(P1) = true,T−1)∧ ¬b(4)@T−1∧ holdsAt(close(P1,P2) = true,T−1)∧ ¬b(5)@T−1)) ↔((happensAt(start(active(P1) = true),T−1)∨(14) (holdsAt(active(P1) = true,T−1)∧ ¬happensAt(end(active(P1) = true),T−1)))∧ (happensAt(start(close(P1,P2) = true),T−1)∨ (holdsAt(close(P1,P2) = true,T−1)∧ ¬happensAt(end(close(P1,P2) = true),T−1)))) ↔(holdsAt(active(P1) = true,T)∧(15) holdsAt(close(P1,P2) = true,T)) ↔pm|=holdsAt(meeting(P1,P2) = interacting,T)(16) ‘D|=l’ expresses that lis true in all models of D, while ‘b(i)@T−1’ denotes (the conjunction of) the body condition(s) of rule (i), having T−1as their time argument. Equivalence (12) expresses the law of inertia, i.e., (Rs m,Re m) implies that meeting(P1,P2) = interacting holds at timepoint Tiff it is initiated at time-point T−1or it holds and is not terminated at T−1. Equivalence (13) includes a substitution of initiatedAt(meeting(P1,P2) = interacting,T−1) and terminatedAt(meeting(P1,P2) = interacting,T−1) using the bodies of rules (1)–(3) and the bodies of rules (4)–(5), respectively. Moreover, based on our inductive assumption, we have substituted holdsAt(meeting(P1,P2) = interacting,T−1)with the conjunction of holdsAt(active(P1) = true,T−1)and holdsAt(close(P1,P2) = true,T−1), following pm. Equivalence (14) distributes ∧over ∨, while equivalence (15) expresses the law of inertia for FVPs active(P1) = true and close(P1,P2) = true. Equivalences (14)–(15) are explained thoroughly in the technical appendix1. Equivalence (16) expresses pm, i.e., meeting(P1,P2) = interacting holds iff both active(P1) = true and close(P1,P2) = true hold. We have shown that definitions (Rs m,Re m)and pmimply the same holdsAt(meeting(P1,P2) = interacting,T) atoms. Therefore, definitions (Rs m,Re m)and pmare equivalent. Since pmis equivalent with statically determined FVP definition rm(rule (8)), it follows that definition (Rs m,Re m) is equivalent with, and translatable into, definition rm. The Class of Translatable Simple FVP Definitions We identify symmetries that are satisfied by a simple FVP definition iff it is translatable. Inertial Condition Symmetry. Before presenting the first symmetry, we define the inertial condition set of an FVP. Definition 5 (Inertial Condition Set).Consider an FVP literal l. If lis F=V, then the inertial condition set IClof l contains the following conditions: • ‘holdsAt(F=V,T),not happensAt(end(F=V),T)’. • ‘happensAt(start(F=V),T)’. If lis ¬(F=V), then IClcontains: • ‘not holdsAt(F=V,T),not happensAt(start(F=V),T)’. • ‘happensAt(end(F=V),T)’. ■ A simple FVP definition (Rs,Re)is translatable only if Rsand Reare inertial condition symmetric rule-sets. Definition 6 (Inertial Condition Symmetric Rule-Set).A rule-set Ris inertial condition symmetric if, ∀r∈R, for each inertial condition cin r, with FVP u, where cis not the only positive happensAt condition in r,∃r′∈R, such that r′differs from ronly by having a condition c′instead of c, where c′=cand c′∈ICu.■ Consider, e.g., rule-set Rs m, i.e., rules (1)–(3). Rules (1) and (3), and rules (2) and (3), differ only in the inertial condition of FVP close(P1,P2) = true and active(P1) = true, respectively. Thus, Rs mis inertial condition symmetric. Re m is also inertial condition symmetric; the rules in Re mcontain one inertial condition each, which is a positive happensAt. As a counter-example, consider set Rs− mwith rules (2) and (3). Rs− mis not inertial condition symmetric because there is no rule in Rs− mfor one of the orders in which the FVPs in its inertial conditions may come about, i.e., active(P1) = true starting to hold after close(P1,P2) = true (Definition 6). An inertial condition symmetric rule-set is minimal if it cannot be partitioned into more than one inertial condition symmetric rule-sets. Rs m, e.g., is minimal, while Re mis not minimal. A partition of an inertial condition symmetric ruleset is complete if it includes only minimal inertial condition symmetric sets. The partition of Re m, e.g., into sets Re1 mand Re2 m, with rule (4) and rule (5), respectively, is complete. Guard Condition Symmetry. A translatable simple FVP definition may optionally contain ‘guard conditions’; their role is to prevent the computation of redundant FVP initiations/terminations. Consider, e.g., definition (Rs m,R′e m), where R′e mcontains the following rules: terminatedAt(meeting(P1,P2) = interacting,T)← happensAt(end(active(P1) = true),T), holdsAt(close(P1,P2) = true,T). (17) terminatedAt(meeting(P1,P2) = interacting,T)← happensAt(end(close(P1,P2) = true),T), holdsAt(active(P1) = true,T). (18) We constructed rule (17), e.g., by adding guard condition holdsAt(close(P1,P2) = true,T)in rule (4), i.e., the rule in set Re1 mof the complete partition of Re m. This condition states that close(P1,P2) = true needs to be in effect when a rule in Re1 mfires; otherwise, the termination would be redundant, because meeting(P1,P2) = interacting would have been terminated already by a rule in the minimal inertial condition symmetric rule-set Re2 mof Re m, due to condition happensAt(end(close(P1,P2) = true),T)of Re2 m. We define the guard condition set of a rule-set as follows: Definition 7 (Guard Condition Set).Consider a minimal inertial condition symmetric rule-set Rand set U, containing the FVP literals corresponding to the inertial conditions in R. The guard condition set of Ris: G=Sl∈U{c}, where cis ‘not holdsAt(F=V,T)’, if lis F=V, and ‘holdsAt(F=V,T)’, if lis ¬(F=V).■ A simple FVP definition (Rs,Re)is translatable only if Rsand Reare guard condition symmetric rule-sets. Definition 8 (Guard Condition Symmetric Rule-Set).Consider a rule-set R.Ris guard condition symmetric if it is inertial condition symmetric, G1,G2,...,Gnare the guard condition sets of the sets R1,R2,...,Rnin the complete partition of R, and ∀i∈ {1,...,n},∀r∈Ri, for each guard condition cin r, where c∈Gj,j=i, it holds that ∀c′∈Gj, where c′=c,∃r′∈R, such that r′differs from ronly by having condition c′instead of c.■ R′e m, e.g., is inertial condition symmetric and its complete partition consists of sets R′e1 mand R′e2 m, containing rule (17) and rule (18), respectively. The guard condition sets G′e1 mand G′e2 mof R′e1 mand R′e2 mcontain one condition each, i.e., holdsAt(close(P1,P2) = true,T)and holdsAt(active(P1) = true,T), resp. Thus, following Definition 8, R′e mis guard condition symmetric. Moreover, Rs mand Re mare guard condition symmetric because they are inertial condition symmetric and contain no guard conditions. Boolean Representation Symmetry. Equivalence (14) stated that the bodies of the initiation and termination rules in (Rs m,Re m)need to include the conditions expressing the law of inertia for the conjunction of active(P1) = true and close(P1,P2) = true, and no other inertial conditions. This is only possible when sets Rs mand Re mare complementary in terms of inertial conditions. Towards specifying this type of relation, we define the Boolean representation of an inertial condition symmetric rule-set. Definition 9 (Boolean Representation of Inertial Condition Symmetric Rule-Set).Consider an inertial condition symmetric rule-set R, where R1,R2,...,Rnis a complete partition of R. Set Ui, where 1≤i≤n, contains the FVP literals corresponding to the inertial conditions in Ri. The Boolean representation of Ris: p=W1≤i≤n∧l∈Uil.■ The Boolean representation of the minimal inertial condition symmetric rule-set Rs m, e.g., is ‘active(P1) = true ∧ close(P1,P2) = true’, while the Boolean representation of rule-set Re m, with complete partition Re1 mand Re2 m, is ‘¬(active(P1) = true)∨ ¬(close(P1,P2) = true)’. A simple FVP definition (Rs,Re)is translatable only if it is Boolean representation symmetric. Definition 10 (Boolean Representation Symmetric Simple FVP Definition).A simple FVP definition (Rs,Re)is Boolean representation symmetric if sets Rsand Reare inertial condition symmetric and the Boolean representations pand pof Rsand Reare complementary. ■ (Rs m,Re m)is Boolean representation symmetric as the Boolean representations of Rs mand Re mare complementary. We formally identify the class of translatable simple FVP definitions with the following proposition. Proposition 2 (Translatable Simple FVP Definition).A simple FVP definition (Rs,Re)is translatable iff: 1. Rsand Reare guard condition symmetric, and 2. (Rs,Re)is Boolean representation symmetric. When (Rs,Re)is translatable, it is equivalent with the definition induced by the Boolean representation of Rs.♦ We have shown, e.g., that sets Rs mand Re mare guard condition symmetric, and that (Rs m,Re m)is Boolean representation symmetric. Thus, based on Proposition 2, simple FVP definition (Rs m,Re m)is translatable. Moreover, (Rs m,Re m)is equivalent with the Boolean FVP definition induced by the Boolean representation of Rs m, which is pm(formula (9)). Compiler We developed an open-source compiler1that optimises an event description by replacing all translatable simple FVP definitions with their equivalent statically determined FVP definitions. Our empirical analysis, presented in the following section, demonstrates that the compiled event descrip- Algorithm 1: compiler(Rs,Re) 1: if not guardSymm(Rs)or not guardSymm(Re)then 2: return false 3: p←BoolRepr(Rs),p←BoolRepr(Re) 4: if not complementary(p,p)then return false 5: hr←holdsFor(F=V,I),br←[ ] 6: for each disjunct diin pdo 7: for each literal lij in dido 8: if lij is Fij =Vij then 9: br.add(holdsFor(Fij =Vij ,Iij )) 10: else ▷lij is ¬(Fij =Vij ). 11: br.add(holdsFor(Fij =Vij ,I′ ij )) 12: br.add(relative complement all([iw],I′ ij ,Iij )) 13: if |di|>1then br.add(intersect all([Ii1 ,...,Iini],Ii)) 14: if |p|>1then br.add(union all([I1,...,Im],I)) 15: return r tions are considerably more succinct, and lead to significantly more efficient reasoning. Algorithm 1 outlines the steps of the compiler. For each input definition (Rs,Re)of a simple FVP F=V, the compiler works as follows. First, it identifies whether (Rs,Re)is translatable (lines 1–4). Second, if (Rs,Re)is translatable, it rewrites (Rs,Re)as an equivalent statically determined FVP definition (lines 5–14). We check whether (Rs,Re)is translatable by examining the symmetry conditions of Proposition 2. We start by checking whether sets Rsand Reare guard condition symmetric (lines 1–2). To do this, we first need to verify that Rs and Reare inertial condition symmetric (see Definition 8). For Rswe proceed as follows. For each rule rsi in Rs, we identify the FVPs in the inertial conditions of rsi and construct set Rsi , containing one rule for each combination of the inertial conditions of these FVPs with at least one positive happensAt condition. If ∀rsi ∈Rs, we have Rsi ⊆Rs, then Rsis inertial condition symmetric (Definition 6). The disjoint sets Rs1 ,...,Rsm are a complete partition of Rs. Then, we construct the guard condition sets Gs1 ,...,Gsm of Rs1 ,...,Rsm and, for each rule-set Rsi and guard condition set Gsj , where j=i, we verify that, if there is a rule rin Rsi with a guard condition c∈Gsj , then Rsi contains, for each c′∈Gsj , one rule that differs from ronly by having guard condition c′instead of c(Definition 8). The cost of these procedures is quadratic to the number of rule conditions in Rs. Afterwards, we construct Boolean representations pand pof Rsand Rebased their complete partitions Rs1 , ..., Rsm and Re1 , ..., Rem′, following Definition 9 (line 3), and check whether pand pare complementary (line 4). If they are, then (Rs,Re)is Boolean representation symmetric (Definition 10). If the above symmetries are satisfied, then (Rs,Re)is equivalent with Boolean FVP definition p, i.e., the Boolean representation of Rs. Algorithm 1 translates p, i.e., the Boolean FVP definition that is equivalent with (Rs,Re), into statically determined FVP definition r, with head holdsFor(F=V,I), in lines 5–14. For each disjunct diin p, we process each literal lij in di(lines 6–7). If lij is Fij =Vij , then we add condition holdsFor(Fij =Vij ,Iij )in the body brof r(lines 8–9). List Iij contains the maximal intervals during which Fij =Vij holds continuously. Otherwise, if lij is ¬(Fij =Vij ), then we are interested in the maximal intervals during which Fij =Vij does not hold. We express the list Iij that contains these intervals with conditions holdsFor(Fij =Vij ,I′ ij ) and relative complement all([iw],I′ ij ,Iij ), where interval iw expresses the window, i.e., the bounded portion of the stream currently being processed by RTEC (lines 10–12). If di contains more than one FVP literal, denoted by ‘|di|>1’, we add intersect all([Ii1 , . . . Iini],Ii)in br(line 13). This way, we express the list of maximal intervals Iiduring which all FVP literals in dihold. Finally, if pcontains more than one disjunct, denoted by ‘|p|>1’, we add union all([I1,...,Im],I)in br(line 14); list Icontains the maximal intervals during which at least one of the disjuncts of pis satisfied. For this reason, rimplies that F=Vholds at some time-point Tiff pis satisfied at T, i.e., definitions rand pare equivalent. Thus, ris equivalent with the input simple FVP definition (Rs,Re). Example 3 (Compiling a Simple FVP Definition of ‘Meeting’).Simple FVP definition (Rs m,Re m)is translatable into Boolean FVP definition pm(formula (9)). Our compiler verifies this in lines 1–4 of Algorithm 1, and then proceeds with the translation of pminto a rule r, with head holdsFor(meeting(P1,P2) = interacting,I) (line 5). pmhas one disjunct, d1, with two literals, l11 : active(P1) = true and l12 :close(P1,P2) = true. Based on these literals, we add holdsFor(active(P1) = true,I11 )and holdsFor(close(P1,P2) = true,I12 )in the body brof r(lines 8–9). Since d1contains two FVP literals, we need to express the maximal intervals during which both these literals hold. To do this, we add intersect all([I11 ,I12 ],I)in br(line 13). pmcontains one disjunct, and thus we do not add union all (line 14). The resulting rule ris the same as statically determined FVP definition rm(rule (8)). ♢ Proposition 3 (Compiler Correctness).Given a simple FVP definition (Rs,Re), if (Rs,Re)is translatable, then Algorithm 1 returns a statically determined FVP definition that is equivalent with (Rs,Re). Otherwise, it returns false.♦ Experimental Analysis Experimental Setup. We evaluated our compiler on handcrafted Event Calculus formalisations for composite event recognition (CER), legal contract verification, clinical guideline monitoring and distributed authorisation policy management. In all applications, the input event descriptions included only simple FVP definitions. Our compiler optimised the event descriptions, i.e., identified the translatable FVP definitions and expressed them as statically determined FVP definitions. Then, we compared the size of the input and compiled event descriptions, and the efficiency of RTEC when reasoning over each event description. Concerning CER, we tested our compiler on three tasks: human activity recognition, maritime situational awareness and city transport management. In human activity recognition, the input streams were symbolic representations of video feeds, including events that denote simple activities performed by one person and identified on individual video frames, such as ‘active’, as well as the coordinates and the orientation of the tracked people. The task was to compute the maximal intervals of ‘meeting’, ‘moving together’, ‘fighting’ and ‘leaving object’ activities. We used CAVIAR2, a benchmark activity recognition dataset. For maritime situational awareness, we used streams of events that were derived from Automatic Identification System (AIS) signals, containing information about vessels’ location, speed and heading. The task was to compute the maximal intervals of various types of dangerous, suspicious or illegal vessel activities, such as a ship-to-ship transfer of goods in the open sea (Pitsikalis et al. 2019). We used a publicly available dataset3, containing 18M AIS signals, emitted by 5K vessels sailing around the port of Brest, France, between October 2015–March 2016. In city transport management, we used streams of events concerning changes in the position, acceleration, in-vehicle temperature, noise level and passenger density of public transport vehicles. The task was to compute the maximal intervals of composite activities related to public transport vehicle punctuality, driving style and quality, and passenger and driver comfort and satisfaction. We used real data, collected from the public transport vehicles in Helsinki, Finland, in November 2011 (Artikis et al. 2015). We also evaluated our compiler on Event Calculus formalisations for tasks other than CER. For legal contract verification, we used an event description specifying the obligations and the powers of the parties in a contract (Sharifi et al. 2020; Parvizimosaed et al. 2022), while, for clinical guideline monitoring, we used an event description defining scenarios of non-conformance with clinical guidelines (Bottrighi et al. 2011; Bragaglia et al. 2012). Moreover, we employed event descriptions specifying authorisation policy conflicts in multi-cloud environments (Zahoor et al. 2022), and redundant authorisation policies in Kubernetes (Zahoor et al. 2023). Unfortunately, no datasets are available for these applications, and thus we could only compare the size of the input and compiled event descriptions. Our experiments are reproducible; our compiler, the input and compiled event descriptions, and the datasets are publicly available1. RTEC4operated on SWI-8.4 Prolog on a PC with Ubuntu 22, Ryzen 7 5700U and 16GB RAM. Experimental Results. The input event descriptions include only simple FVPs; Ei h,Ei m,Ei t,Ei l,Ei g,Ei cand Ei r are the event descriptions for human activity recognition, maritime situational awareness, city transport management, legal contract verification, clinical guideline monitoring, and the identification of authorisation policy conflicts and redundant authorisation policies. For each event description Ei x, our compiler generated an optimised event description Eo xby transforming the translatable simple FVP definitions in Ei xinto statically determined FVP definitions. In all cases, the compilation time did not exceed half a second. Figure 1 (top) shows the reduction in the number of rules and conditions in the compiled event descriptions. Compiling Ei h, e.g., 2https://tinyurl.com/caviardataset 3https://zenodo.org/record/1167595 4https://github.com/aartikis/rtec Ei hEo hEi mEo mEi tEo tEi lEo lEi gEo gEi cEo cEi rEo r 0 50 100 150 200 Number of Rules Input Optimised 569 71 1212 215 1030 75 469 182 108 39 150 45 120 29 26K 3K 46K 5K 91K 10K 183K 20K 1 101 102 103 104 105 106 Window size Reasoning time (ms) Eo hEi h 40K 3K 73K 5K 159K 10K 328K 20K Window size Eo mEi m 2K 3K 4K 5K 8K 10K 16K 20K Window size Eo tEi t Figure 1: Event description optimisation (top figure); the number above each bar denotes the total number of rule conditions. Reasoning over input and compiled/optimised event descriptions (bottom figure); the horizontal axes denote the avg number of input events (top) and the avg number of computed FVP intervals (bottom) per window. which includes 131 rules and 569 rule conditions in total, leads to Eo m, containing 17 rules, with a total of 71 conditions. Our results show that our compiler can transform event descriptions for real applications into a significantly more compact form, paving the way for code maintenance. We employed RTEC for CER, with event descriptions Ei h,Eo h,Ei m,Eo m,Ei tand Eo t. We could not run RTEC on the remaining event descriptions because no datasets for the corresponding applications were available to us. RTEC processes input streams using a sliding window. Figure 1 (bottom) shows the reasoning times of RTEC per window, as the window size increased. Each data point is the average of 30 queries. In all of our experiments, reasoning with an optimised event description led to the same FVP intervals as reasoning with the original event description. Our results demonstrate that reasoning with an optimised event description may lead to efficiency benefits of about 1-2 orders of magnitude. Due to the significant size reduction we observed when compiling Ei l,Ei g,Ei cand Ei r(see Figure 1 (top)), we expect that their optimisation will lead to comparable reasoning efficiency benefits with the ones of Figure 1 (bottom). Summary The Event Calculus is a formal computational framework used in a wide range of tasks, including CER, legal contract verification, clinical guideline monitoring and distributed authorisation policy management. Unfortunately, the knowledge engineer does not always employ the optimal Event Calculus representation. To address this issue, we identified the class of simple FVP definitions that can be translated into statically determined FVP definitions. We provided a compiler for the translation, and a reproducible empirical evaluation on real applications. Our compiler reduced the size of the event descriptions by orders of magnitude, leading to significant reasoning efficiency gains. Acknowledgements This work was supported by the EU-funded CREXDATA project (No 101092749). References Arias, J.; Carro, M.; Chen, Z.; and Gupta, G. 2022. Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming. Theory Pract. Log. Program., 22(1): 51–80. Artikis, A.; Sergot, M. J.; and Paliouras, G. 2015. An Event Calculus for Event Recognition. IEEE Trans. Knowl. Data Eng., 27(4): 895–908. Baumgartner, P. 2021. Combining Event Calculus and Description Logic Reasoning via Logic Programming. In FroCoS, 98–117. Bazoobandi, H. R.; Beck, H.; and Urbani, J. 2017. Expressive Stream Reasoning with Laser. In ISWC, volume 10587, 87–103. Beck, H.; Dao-Tran, M.; and Eiter, T. 2018. LARS: A Logicbased framework for Analytic Reasoning over Streams. Artif. Intell., 261: 16–70. Beck, H.; Eiter, T.; and Folie, C. 2017. Ticker: A system for incremental ASP-based stream reasoning. Theory Pract. Log. Program., 17(5-6): 744–763. Bottrighi, A.; Chesani, F.; Mello, P.; Montali, M.; Montani, S.; and Terenziani, P. 2011. Conformance Checking of Executed Clinical Guidelines in Presence of Basic Medical Knowledge. In Business Process Management Workshops, volume 100 of Lecture Notes in Business Information Processing, 200–211. Springer. Bragaglia, S.; Chesani, F.; Mello, P.; Montali, M.; and Torroni, P. 2012. Reactive Event Calculus for Monitoring Global Computing Applications. In Logic Programs, Norms and Action - Essays in Honor of Marek J. Sergot on the Occasion of His 60th Birthday, volume 7360, 123–146. Bucchi, M.; Grez, A.; Quintana, A.; Riveros, C.; and Vansummeren, S. 2022. CORE: a COmplex event Recognition Engine. Proc. VLDB Endow., 15(9): 1951–1964. Chesani, F.; Mello, P.; Montali, M.; and Torroni, P. 2013. Representing and monitoring social commitments using the event calculus. Auton. Agents Multi Agent Syst., 27(1): 85– 130. Chittaro, L.; and Montanari, A. 1996. Efficient Temporal Reasoning in the Cached Event Calculus. Comput. Intell., 12(3): 359–382. Clark, K. L. 1977. Negation as Failure. In Logic and Data Bases, 293–322. Plemum Press. Eiter, T.; Ogris, P.; and Schekotihin, K. 2019. A Distributed Approach to LARS Stream Reasoning (System paper). Theory Pract. Log. Program., 19(5-6): 974–989. Falcionelli, N.; Sernani, P.; de la Torre, A. B.; Mekuria, D. N.; Calvaresi, D.; Schumacher, M.; Dragoni, A. F.; and Bromuri, S. 2019. Indexing the Event Calculus: Towards practical human-readable Personal Health Systems. Artif. Intell. Medicine, 96: 154–166. Giatrakos, N.; Alevizos, E.; Artikis, A.; Deligiannakis, A.; and Garofalakis, M. N. 2020. Complex event recognition in the Big Data era: a survey. VLDB J., 29(1): 313–352. Kafali, ¨ O.; Romero, A. E.; and Stathis, K. 2017. Agentoriented activity recognition in the event calculus: An application for diabetic patients. Comput. Intell., 33(4): 899–925. Kowalski, R.; and Sergot, M. 1986. A Logic-Based Calculus of Events. New Gen. Computing, 4(1): 67–96. Mantenoglou, P.; Kelesis, D.; and Artikis, A. 2023. Complex Event Recognition with Allen Relations. In KR, 502–511. Mantenoglou, P.; Pitsikalis, M.; and Artikis, A. 2022. Stream Reasoning with Cycles. In KR, 544–553. Montali, M.; Maggi, F. M.; Chesani, F.; Mello, P.; and van der Aalst, W. M. P. 2013. Monitoring business constraints with the event calculus. ACM Trans. Intell. Syst. Technol., 5(1): 17:1–17:30. Parvizimosaed, A.; Sharifi, S.; Amyot, D.; Logrippo, L.; Roveri, M.; Rasti, A.; Roudak, A.; and Mylopoulos, J. 2022. Specification and analysis of legal contracts with Symboleo. Softw. Syst. Model., 21(6): 2395–2427. Paschke, A.; and Bichler, M. 2008. Knowledge Representation Concepts for Automated SLA Management. Decision Support Systems, 46(1): 187–205. Pitsikalis, M.; Artikis, A.; Dreo, R.; Ray, C.; Camossi, E.; and Jousselme, A. 2019. Composite Event Recognition for Maritime Monitoring. In DEBS, 163–174. Sharifi, S.; Parvizimosaed, A.; Amyot, D.; Logrippo, L.; and Mylopoulos, J. 2020. Symboleo: Towards a Specification Language for Legal Contracts. In IEEE RE, 364–369. Tsilionis, E.; Artikis, A.; and Paliouras, G. 2022. Incremental Event Calculus for Run-Time Reasoning. J. Artif. Intell. Res., 73: 967–1023. Walega, P. A.; Kaminski, M.; Wang, D.; and Grau, B. C. 2023. Stream reasoning with DatalogMTL. J. Web Semant., 76: 100776. Zahoor, E.; Chaudhary, M.; Akhtar, S.; and Perrin, O. 2023. A formal approach for the identification of redundant authorization policies in Kubernetes. Comput. Secur., 135: 103473. Zahoor, E.; Ikram, A.; Akhtar, S.; and Perrin, O. 2022. A Formal Approach for the Identification of Authorization Policy Conflicts within Multi-Cloud Environments. J. Grid Comput., 20(2): 18.