Quickening Data-Aware Conformance Checking through Temporal Algebras ^†

Intrusion detection for cyber security aims at auditing an environment for identifying potential flaws that can be remedied and fixed later. While anomaly-based approaches raise an alarm if the observed behaviour differs significantly from the expected one, signature-based approaches check whether attack patterns might be recognised from the environment. The latter are often used to mitigate the high false-alarm rates of the former [10]. Expected behaviour might be encoded as process models expressed in LTL_f, which, when violated, lead to the detection of an attack: such a language can be directly exploited to represent several different kinds of attacks, such as Denial Of Service, Buffer Overflows, and Password Guessing [10]. In his dissertation [11], Ray shows how malware can be detected by determining LTL_f formulae discriminating between system–calls patterns generated by malicious software from expected run-time behaviour. Recent developments [12,13] showed that it is possible to perform prediction (and therefore reasoning) on potentially infinite sequences by analysing a finite subsequence of the overall behaviour within a sliding window; Buschjäger et al. [12] predict future events not covered by the sliding window by correlating them to the patterns observed in such a window. By associating a positive label to each finite subsequence preceding or containing an attack, and a negative one otherwise, we can also extract temporal models detecting subsequences containing attacks [14]. This entails that real-time verification boils down, to some extent, to offline monitoring, as we guarantee that it is sufficient to analyse currently-observed behaviours to predict and detect an attack. The learned model, once validated, can be exploited in the aforementioned real-time verification systems [10].

On blockchains, each trace event represents a proper blockchain event, thus including function or event invocations issued by one or more smart contracts. In particular, smart contracts are sets of conditions specified in self-executing programs [15], which include protocols within which the parties will fulfil some promises [16]. Given that smart contracts can also be seen as postconditions activated upon the occurrence of specified pre-conditions [17], they are also exploited as security measures reducing malicious and accidental exceptions [15]. As per previous considerations, we can directly encode the smart contract premises in LTL_f, as well as represent the whole smart contract as a whole LTL_f formula under the assumption that the blockchain guarantees its execution [17]. Therefore, we can perform post-mortem analysis checking whether a given run-time abides by the rules imposed by the system.

Smart factories enable the collection and analysis of data through advanced sensors and embedded software for better decision-making. These enable monitoring each phase of the entire production process in both real-time and domain-specific applications where the safety of both autonomous cyber-physical systems as well as human workers is at stake [18]. This is of the uttermost importance, as both humans and machines cooperate in the same environment where a minimal violation of safety requirements might damage the overall production process, thus reflecting in maintenance costs. This calls for logical-based formal methods providing correctness guarantees [19]. Run-time verification [19] and prediction [13] have started gaining momentum against customary static analysis tools: in fact, real complex systems such as factories are often hard to predict and analyse before execution. As run-time verification can be deployed as a permanent testing condition on the environment, Mao et al. [19] show that this approach is complete, thus reducing the complicated model-checking problem into a simpler conformance checking one. Programmable Logic Controllers (PLC) are at the heart of this mechanism, where controllers can make decisions over previously-observed events. PLC work is similar to smart contracts in the previous scenario: at each “scan cycle”, the controllers perceive through sensors the status change of the environment (e.g., variations of temperature and pressure). This information is then fed to the internal logic, which, on the other hand, might decide to intervene directly in the environment by sending signals to some actuators (e.g., controlling the pressure and temperature on the system). Due to the similarity of PLC to smart contracts, these might also exploit LTL_f for determining security requirements: when a safety condition is violated, the PLC might activate an alarm while ensuring that the system works within safe operation ranges [19]. Please observe that ptLTL, also defined in [19], is a version of LTL allowing reasoning on past events so as to avoid semi-decidable computations for traces of infinite length, might be still represented through an equivalent LTL_f formula evaluated over a finite sliding window [13] bounded by the first and the latest event. Please observe that the difference between LTL and LTL_f  is that only the latter considers traces of finite length.

In some other industrial scenarios, we might be interested in detecting unexpected variations in time series reflecting the fluctuation of some perceived variables (e.g., variations in temperature and pressure). The latest developments [13] showed that (industrial) time series could also be represented as traces: we might assign to each event an activity label $\varpi$ if the current event has a data payload whose values upper bound the ones from immediately preceding event’s payload, and $\neg \varpi$ otherwise. Consequently, we can encode disparate data variation patterns in LTL_f reflecting different types of data volatility or steep increases/decreases [13]. This shows how LTL_f can also represent anomaly-based problems by reducing them to the identification of anomaly patterns [20].

A medical process describes clinical-related procedures as well as organisational management ones (e.g., registration, admission, and discharge) [21]. The renowned openEHR (https://www.openehr.org/ accessed the 5 March 2023) standard distinguishes the former in four main archetypes: an observation, recording patients’ clinical symptoms (e.g., body temperature, blood pressure); an evaluation, providing preliminary diagnosis and assessing the patient’s health based on the former results; and an instruction, the execution of the treatment plan proposed by a physician (e.g., prescribing, examining, and testing). An action describes the way to intervene or treat medical patients according to the treatment plan (e.g., drug administration, blood matching). Once encoded as such, each process representing an instantiation of a medical process, i.e., a patient’s clinical course, can be then collected and represented in a log. As such, each action is going to be represented as a distinct activity label of a given event [22] that might contain relevant payload information recording the outcome of the clinical procedures, as well as demographical information related to the patient [21] for future socio-clinical analyses [23].

Declarative temporal languages such as Declare can then be exploited to provide a descriptive approach specifying temporal constraints among activities without strictly enforcing their order of completion, thus restricting the order of application of a specific set of activities [21]. As these models come with temporal semantics expressed in LTL_f, these are, for all intents and purposes, process models. As such, these might be applied to detect discrepancies between clinical guidelines, expressed by the aforementioned model, and the actual process executions collected in a log. This is of the utmost concern as often deviations represent errors compromising the patient recovery [22], which, if efficiently and identified in advance, lead to an increased patient satisfaction as well a reduction of healthcare costs (e.g., due to mismanagement) [21].

First, we discuss the base operators directly accessing the tables. These might have an associated marker specifying whether the event of interest is considered an activation (A) or a target (T) condition; if none is required, the mark can be omitted from the operator. The ${\mathtt{Activity}}^{\tau }{\left(\mathtt{a}\right)}_{\mathtt{A}/T}^{\mathcal{L}}$ operator lists all of the events associated with an activation label $\mathtt{a}$. As the ${\mathtt{ActivityTable}}_{\mathcal{L}}$ directly provides this information, this operator is defined as follows:

We can also make similar considerations for single elementary interval representable as an LTL_f compound condition $\mathtt{a}\wedge \mathit{lower}\le \kappa \le \mathit{upper}$, which can be run as a single range query over an ${\mathtt{AttributeTable}}_{\mathcal{L}}^{\kappa }$. As each of its records has an offset $\pi$ to the ${\mathtt{ActivityTable}}_{\mathcal{L}}$, this resolves the trace id and event id information required for the intermediate result. This operator can therefore be formalised as follows:

If we want to list all of the initial (or terminal) events of a trace, we can directly access the ActivityTable and provide a linear scan over the number of the possible traces through its associated secondary index. If we are not interested in whether the trace starts with a specific activity label, then we can define the ${\mathtt{First}}_{\mathtt{A}}^{\mathcal{L},\tau }$ (and ${\mathtt{Last}}_{\mathtt{A}}^{\mathcal{L},\tau }$) operators as follows:

On the other hand, $\mathtt{Init}$ (and $\mathtt{Ends}$) are the specific refinements of the former operators if we are also interested in retrieving events with a specific activity label. These can be defined as follows:

Given a natural number n, $\mathtt{Exists}{(\mathtt{a},n)}_{\mathtt{A}}^{\mathcal{L}}$ lists the traces containing at least n events with an activity label $\mathtt{a}$. As $\mathtt{Absence}{(\mathtt{a},n)}_{\mathtt{A}}^{\mathcal{L}}$ is the substantial negation of the former, this lists the traces containing at most $n-1$ events with an activity label $\mathtt{a}$. Please observe that these operators directly provide the formal semantics for the homonym Declare template. As the CountingTable precisely contains the counting information required to solve this query, these operators can be formalised as follows for $n\in {\mathbb{N}}_{>0}$:

The following paragraph shows how these last two operators can be generalised for counting the salient event information returned by any sub-expression returning an operand $\rho$.

The unary xtLTL_f operators come in two flavours: the first ones extend some of the former operators for compound conditions or atoms not necessarily associated with activity labels, while the second ones directly extend the unary operators from LTL_f.

Base Operators’ generalisations. We extend the definition of Init/Ends or Exists/Absence for any possible set of events of interest listed in an intermediate result $\rho$, not necessarily associated with the same activity label. We first define Exists and Absence operator as such: instead of exploiting the counting table, we now actually need to count the events returned in $\rho$ for each trace and return an intermediate result triplet iff. they satisfy the counting condition. These can be then defined as follows for $n\in {\mathbb{N}}_{>0}$:

Similarly, while the operators accessing the CountingTable (Exists/Absence) return the result by linearly scanning such a table, their generalised counterparts require scanning their operand $\rho$ as returned from a subexpression of choice, and then creaming them off depending on how many events per trace were in $\rho$. As we might observe, we might exploit the previously provided operators when we want to evaluate conditions only associated with activity labels, while we might need to exploit the former if we are interested in results associated with compound conditions whose evaluation is returned in $\rho$.

Finally, we refine Init and Ends for a given operand $\rho$, to keep only the events at the beginning or end of a given trace:

Further details on our intended notion of these operators’ generality if compared to the corresponding base operators can be found in Appendix A.1.

LTL_fextensions. The unary xtLTL_f operators work differently from the corresponding ones in LTL_f: while the latter compute the semantics from the first occurring operator appearing in the formula towards the leaves, the former assume to receive intermediate results from the leaves.

This structural difference also imposes an explicit distinction between timed and untimed operators. This is required as each operator is completely agnostic from the semantics associated with the upstream operator, and therefore the downstream operator has to combine the incoming intermediate results appropriately. This motivates why LTL_f operators do not have to provide such an explicit distinction from their syntactical standpoint.

Such a premise motivates the counter-intuitive definition of the timed ${\mathtt{Next}}^{\tau }$ operator if compared to the homonym in LTL_f: as this needs to return the events for which desired temporal constraints happen immediately after them, it needs to assume that the desired forthcoming temporal behaviour is the one received as an input $\rho$, for which all the events preceding the ones listed in $\rho$ are the ones of interest. As per the previous statement, it also follows that this operator shall never possess an equivalent untimed flavour. From these considerations, ${\mathtt{Next}}^{\tau }$ is formally defined as follows: where L fulfils the role of preserving the information of the events satisfying an activation, target, or correlation condition independently from the event stated in the second component of the intermediate representation record. Therefore, $\langle i,j,L\rangle$ shall be interpreted as follows: ${\sigma }_j^i$ witnesses the satisfaction of any activation, target, or correlation condition by the events collected in L.

We now discuss the definition of “globally”. As per previous considerations, checking that all of the events in a trace satisfy a given condition corresponds to retrieving all of the events satisfying such a condition, for then counting if the length of the returned events corresponds to the trace length. Similarly, the timed version of the same operator shall test the same condition for each possible event and return the points in the trace after which the desired condition always happens in the future. These operators are therefore defined as follows:

The operators expressing the eventuality that a condition shall happen in the future undergo similar considerations, with the only difference that these do not require to test that all of the trace events from a given point in time will satisfy a given condition, as it suffices that at least one event will satisfy it. The $\mathtt{Future}$ operator with its timed counterpart are then formally defined as follows:

Timed and untimed negations are implemented dissimilarly by design. While the timed negation returns all of the events that are in the log but which were not returned in the previous computation $\rho$, the untimed version returns the traces containing no events associated with the provided input. These operators are therefore defined as follows:

Differently from the LTL_f binary operators, the xtLTL_f binary operators are specifically tailored to express data correlation conditions $\Theta$ between activation and target payloads. This requires that one of the two operands, either $\rho$ or ${\rho }^{\prime }$, returns activated events while the other provides targeted ones. Supplement I discusses the formal definition of predicates assessing whether an event $\langle i,j,L\rangle \in \rho$ matches with another event $\langle i,j^{\prime },L^{\prime }\rangle \in {\rho }^{\prime }$ on the basis of their matched and activated events in L and $L^{\prime }$. After this, we have the definition of our required binary operators.

The until operators work similarly to the other LTL_f-derived unary operators. The timed until returns all of the events within the trace satisfying the until condition, expressed by returning all of the “activated” events ${\sigma }_j^i$ listed in the right operand (as they trivially satisfy the until condition) alongside all of the “targeted’ events ${\sigma }_j^i$ from the left operand with $k<j$ at a distance $j-k+1$ from the second operand’s event while guaranteeing that all the events in ${\sigma }_k^i,\cdots ,{\sigma }_{j-1}^i$ appear in the first operand while satisfying the matching condition within this temporal window. The untimed version of this operator performs such considerations only from the beginning of the trace. These are defined as follows: where ${\mathcal{T}}_{\Theta }^{A,i}$ performs (Please see Supplement I for more details.) the correlation tests and returns the set of the matches if any and, if no match was successful, it returns False. Differently from Until${}_{\Theta }^{\tau }$ and Until${}_{\Theta }$, the rest of the binary operators assume to receive “activated” (or “targeted”) events from the left (right) operand. The timed conjunction states that a join condition effectively happens in a given event ${\sigma }_j^i$ if both operands return such an event and their associated activation and target conditions match. Thus, we only care for activation and target conditions at the same event ${\sigma }_j^i$. For its untimed counterpart, we state that a trace satisfies the conjunction of events if at least one activation condition from the left operand matching with a target from the right operand, if any, exists; this corresponds to coalescing the activations and target conditions on the first event while requiring that at least one of them occurs. These two operators can then be defined as follows:

The disjunctive version of the timed conjunctive operator returns either the result of the conjunctive operator or the events that did not temporally match from each respective operator. The only difference with its untimed version is that the latter merges all potential activation or target conditions from either of the two operands:

As we will see, the choice of characterizing Or with an $E_{\Theta }^i$ match while coalescing the activation and target conditions on the first trace event allows us to express the Choice template from Declare with one single operator while preserving its expected LTL_f semantics.

Similarly to relational algebra, we can now compose some frequently occurring operators together for enhancing the overall time complexity associated with the execution of frequently appearing subqueries in Declare.

Appendix A.3 will show that computing these operators is equivalent to computing their semantically equivalent xtLTL_f expression containing multiple operators.

For easing the pseudocode readability, we can also define an ${\mathtt{Atom}}_{A/T}^{\mathcal{L},\tau }\left(p_i\right)$ operator computing the conjunction of all of the compound conditions characterizing each atom:

Properties of thextLTL_f Algebra. We furnish the previous definitions with some formal proofs, which, so as not to burden the reader, are postponed to the Appendix A. We show that xtLTL_f is as expressive as traditional LTL_f, as we can show that each LTL_f expression evaluated over a finite and non-empty trace $\sigma$ corresponds to an xtLTL_f expression evaluated over the representation of such a trace within the proposed logical model; as the proofs of Lemmas A5 and A6 in Appendix A.2 are constructive, they show the translation process from LTL_f formulæ  to equivalent xtLTL_f expressions.

Next, we also show that the timed and untimed operators correspond to the intended semantics: that is, for each timed operator having a corresponding untimed operator if the former states that the timed formula is satisfied by the i-th trace starting from time j, it follows that the sub-trace of i starting from time j will satisfy the corresponding untimed formula. This shows the correctness of the untimed operators concerning their timed definitions (Lemma A7).

In Appendix A.3, we show that the Declare template $\mathtt{Choice}$ can be fully implemented by exploiting an untimed $\mathtt{Or}$ operator (Corollary A1) while the latter still abides to the rules of LTL_f semantics. We also motivate the need of the derived operators in terms of equivalence to the intended xtLTL_f expressions (Lemmas A9 and A10) as well as in terms of improved computational complexity (Section 6.4) and run time (Section 7.1). The latter is discussed after describing the physical model in more detail alongside the algorithms associated with each operator, which is introduced in the following section.