HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs

1 Introduction

Temporal logics traditionally assume that the traces generated by the dynamic system of interest have infinite length. This does not match a variety of different settings where traces have an unbounded, but finite, length, such as planning [Baier and McIlraith, 2006; Baier et al., 2007; Gerevini et al., 2009] and Business Process Management (BPM) [Dumas et al., 2018; van der Aalst and others, 2011].

To specify and reason about temporal properties of finite traces, De Giacomo and Vardi (2013) studied two finitetrace variants of Linear Temporal Logic and Linear Dynamic Logic, namely LTLf and LDLf . These logics turned out to be particularly important in BPM: LTLf has become the formal basis for one of the most studied declarative process modeling notations [Pesic et al., 2007], while LDLf has been employed to realize advanced forms of process monitoring and runtime verification [De Giacomo et al., 2014]. Notably, these logics are not only interesting from the semantical point of view, but also bring an operational advantage over their infinite-trace counterparts, since reasoning can be carried out by directly manipulating finite-state automata, without appealing to automata over infinite objects [De Giacomo and Vardi, 2013; De Giacomo et al., 2014].

LTLf and LDLf express properties of single traces in isolation. However, especially in BPM it is also of interest to express properties that relate multiple traces at once (see, e.g., [van der Aalst et al., 2004; Weidlich et al., 2011; Rinderle-Ma et al., 2016]). Two specific settings arise in this spectrum. In the first setting, such traces belong to the overall, possibly infinite log of traces representing all the valid executions of a given process model. In this case, traces are implicitly represented in the form of a finite-state transition system or a bounded Petri net interpreted under interleaving semantics, which guarantee that the induced log forms a regular language. These logs not only capture any finite concrete process log, but also capture logs that can be inferred through sampling by model-learning and process mining techniques [Vaandrager, 2017; van der Aalst, 2011]. In the second setting, which is the typical one in business process management [van der Aalst and others, 2011], traces belong to a finite event log explicitly storing a set of observed process executions, representing a factual sample of all the traces that belong to an unknown process, which again is assumed to be regular.

In the case of infinite-traces, HyperLTL has been proposed to express "hyper" properties that quantify over multiple traces at once [Clarkson et al., 2014]. In this paper, motivated by BPM we introduce HyperLDLf and its fragment HyperLTLf : two extensions of LDLf andLTLf , respectively, that have the ability to express and verify hyper-properties of finite traces.

To handle the analysis of (finite and infinite) logs, we in particular focus on the very significant task of model checking: the task of verifying HyperLDLf formulas over a regular log, i.e., a (possibly infinite) set of traces forming a regular language. We study the HyperLDLf model checking problem in the key setting where the regular log is compactly described by a deterministic finite automaton. Specifically, we show that model-checking a HyperLDLf formula with k alternations of trace quantifiers is k-EXPSPACE-complete. Notably, we show the upper bound by presenting a sound and complete algorithm based on manipulation of regular automata that retains the good, practical computational characteristics already exploited in several reasoning tasks for LTLf /LDLf . Finally, we go back to our original motivation and discuss how HyperLTLf and HyperLDLf can be used to specify and verify relevant, sophisticated properties within BPM and process mining.

2 Automata and Languages

We recall some basic notions on alternating, nondeterministic, universal, and deterministic finite automata. All these automata capture regular languages but they have different characteristics that we will exploited later [Davis et al., 1994]. For a given set X, B+(X) is the set of positive Boolean formulas over X, that is Boolean formulas built from elements of X using ∧ and ∨, where we also allow true and false. A subset Y ⊆ X satisfies a Boolean formula χ ∈ B+(X) if the truth assignment assigning true to the elements in Y and false to the elements in X \ Y satisfies χ. Given an alphabet Σ, a finite word over it is a finite sequence w = σ0 · σ1 · . . . · σn of letters in Σ. By |w| = n+1 we denote the length of w. Moreover, by Σ∗ we denote the set of all possible finite words over Σ. An alternating finite automaton (AFA) on finite words is a tuple A =〈Σ, Q, q0, δ, F 〉 where Σ is the (finite) input alphabet, Q is a finite set of states with q0 ∈ Q being initial state, δ : Q×Σ → B+(Q) is a transition function and F ⊆ Q is a set of final states. Intuitively, the transition function δ(q, σ) describes the possible configurations that A can reach when reading the symbol σ while being in state q. The automaton A is nondeterministic (NFA), denoted N , or universal (UFA), denoted U, if δ(q, σ) contains only disjunctions or conjunctions, respectively. Finally, it is deterministic (DFA), denoted D, if the transition function maps each pair (q, σ) to a single state q′ .

The concepts of run, accepting run, and accepted word for an automaton A are quite standard and we refer to [Leiss, 1985; Davis et al., 1994] for their formal definition. Let L(A) be the set of words accepted by the automaton A. Recall that every automaton A can be turned into an equivalent nondeterministic one N, that is, such that L(A) = L(N). Such operation is called nondeterminization and by Ndet(A) we denote the nondeterministic equivalent automaton. Analogously, we can turn an automaton A into a universal one, denoted Univ(A). Such operation is called universalization. Moreover, recall that if A is either alternating or universal, Ndet(A) can be of size exponential w.r.t. |A|. Analogously, if A is either alternating or nondeterministic, Univ(A) can be of size exponential w.r.t. |A| [Chandra et al., 1981; Davis et al., 1994].

3 HyperLDLf over Finite Traces

We start by defining the hyper-version of LDLf . We refer to [De Giacomo and Vardi, 2013] for details on LDLf itself.

Definition 1 (HyperLDLf syntax). For a set AP containing atomic propositions p and a set V of trace variables π, the syntax of HyperLDLf is the following:

φ := pπ | ¬pπ | φ ∧ φ | φ ∨ φ

Observe that the atomic propositions occurring in a HyperLDLf formula are typed over the trace (variable) on which they are evaluated. This is also the case for the propositional true and false predicate. In particular, we have trueπ .= pπ ∨ ¬pπ and falseπ .= ¬trueπ for every trace variable occurring in a HyperLDLf formula. Analogously, by trueP .= ∧π∈P trueπ and falseP .= ¬trueP we denote the propositional true and false over a set of traces. For convenience we use the abbreviation finishedπ .= [trueπ]ff to specify that a trace π is finished, and lastπ .= 〈trueπ〉finishedπ to specify the last element of the trace.

A log Log ⊆ (2AP)∗ is a (possibly infinite) subset of traces over the powerset of AP. Note that an element P of 2AP can be regarded also as a truth-assignment of AP, where every element in P takes the value true and every element not in P takes the value false. For a trace t ∈ Log, |t| denotes the length of t. By t[i] we denote the i-th element over t, with t[0] and t[|t|-1] being the first and last elements, respectively. For every i, j ∈ N with i ≤ j, by t[i, j], we denote the subtrace obtained from t by taking the elements form t[i] to t[j-1]. For the case of |t| ≤ i, the trace t[i, j] = ϵ is the empty trace. For the case i < |t| ≤ j, the trace t[i, j] = t[i, |t|-1] is the suffix of t starting from the i-th element. We also denote the suffix of t from element i with t[i, . . .].

A trace assignment (or simply assignment) Π : V → Log is a function mapping trace variables V to concrete traces in Log. By Π[π ← t] we denote the trace assignment that adheres with Π, except that Π[π ← t](π) = t, that is, t is assigned to π. By Π[i, j], for every i, j ∈ N, we denote the projection of assignment Π over the subtraces between i and j, i.e., such that Π[i, j](π) = Π(π)[i, j] for each π ∈ V . By Π[i, . . .], for every i ∈ N, we denote the projection of Π over the suffix from i, i.e., such that Π[i, . . .](π) = Π(π)[i, . . .] for each π ∈ V .

The semantics of a HyperLDLf formula over a set Log of traces, a trace assignment Π, and a natural number i ∈ N is given as follows:

• Log,Π, i |= ∃πϕ if there exists t ∈ Log such that Log,Π[π ← t], i |= ϕ;
• Log,Π, i |= ∀πϕ if for each t ∈ Log it holds that Log,Π[π ← t], i |= ϕ;
• Log,Π, i |= tt;
• Log,Π, i ̸|= ff;
• Log,Π, i |= ¬ψ if Log,Π, i ̸|= ψ;
• Log,Π, i |= ψ1 ∧ ψ2 if both Log,Π, i |= ψ1 and Log,Π, i |= ψ2;
• Log,Π, i |= ψ1 ∨ ψ2 if either Log,Π, i |= ψ1 or Log,Π, i |= ψ2;
• Log,Π, i |= 〈ρ〉ψ if there exists j ≥ i such that (i, j) ∈ RΠ(ρ) and Log, Π, j |= ψ;
• Log,Π, i |= [ρ]ψ if for each j ≥ i such that (i, j) ∈ RΠ(ρ) it holds that Log,Π, j |= ψ,

where the relation RΠ(ρ) contains all pairs of indexes (i, j) so that Π(π)[i, j] conforms to ρ for each π that appears as an index of a proposition in ρ, defined as follows:

• (i, j) ∈ RΠ(pπ) if j = i + 1, Π(π)[i, j] ̸= ϵ, and p ∈ Π(π)[i];
• (i, j) ∈ RΠ(¬pπ) if j = i + 1, Π(π)[i, j] ̸= ϵ, and p /∈ Π(π)[i];

• (i, j) ∈ RΠ(ψ1 ∧ ψ2) if (i, j) ∈ RΠ(ψ1) and (i, j) ∈ RΠ(ψ2);
• (i, j) ∈ RΠ(ψ1 ∨ ψ2) if (i, j) ∈ RΠ(ψ1) or (i, j) ∈ RΠ(ψ2);
• (i, j) ∈ RΠ(ψ? ) if j = i and Log,Π, j |= ψ;
• (i, j) ∈ RΠ(ρ1+ρ2) if either (i, j) ∈ RΠ(ρ1) or (i, j) ∈ RΠ(ρ2);
• (i, j) ∈ RΠ(ρ1; ρ2) if there exists k ∈ [i, j] such that (i, k) ∈ RΠ(ρ1) and (k, j) ∈ RΠ(ρ2);
• (i, j) ∈ RΠ(ρ∗ ) if j = i or there exists k ∈ [i + 1, j] such that (i, k) ∈ RΠ(ρ) and (k, j) ∈ RΠ(ρ∗ ).

By Log, Π |= ϕ we denote the fact that Log, Π, 0 |= ϕ.

A variable π in ϕ is free if it occurs out of the scope of either ∃π or ∀π. By free(ϕ) we denote the set of free variables in ϕ. Formula ϕ is closed if free(ϕ) = ∅. Observe that the semantics of a closed formula ϕ replaces all the traces in the assignment Π, which then becomes irrelevant. Thus, we can denote by Log |= ϕ the fact that Log, Π, 0 |= ϕ for some Π.

Note how the semantics allows to consider the evolution of multiple traces at once, in a synchronous fashion. Indeed, RΠ(ρ) includes all the pairs (i, j) so that the synchronous execution described by Π(π)[i, j] conforms to ρ, for each π appearing in the regular expression. As a result, while evaluating formulas of the form 〈ρ〉ψ or [ρ]ψ, all the traces in Log that are assigned through Π to trace variables appearing in ρ are synchronously executed.

Similarly to HyperLDLf , we can define the hyper-version of LTLf [De Giacomo and Vardi, 2013].

Definition 2 (HyperLTLf syntax). For a set AP containing atomic propositions p and a set V of trace variables π, the syntax of HyperLTLf is the following:

In fact, HyperLDLf can express the classic linear-temporal logic operators over finite traces such as next (X) and until (U) and so to have HyperLTLf defined as a syntactic fragment of HyperLDLf .Indeed, the next and weak next operators can be encoded in HyperLDLf by Xψ .= 〈truefree(ψ)〉ψ and ~Xψ .= ¬X¬ψ, respectively. Note that the propositional true in the diamond operator refers only to the traces that are free in ψ. That is, we do not impose any condition on the rest of the traces, which may or may not terminate (or may have terminated already) at the current execution step. Analogously, for the until operator, we have that ψ1Uψ2 .= 〈(ψ1? ; truefree(ψ2))∗ 〉ψ2. Note that in this case it is sufficient to impose the propositional true only on the traces occurring in ψ2 since, for those occurring in ψ1, this is automatically imposed by evaluating ψ1 at each step of the execution specified in the regular expression of the diamond operator. Clearly, we can define the finally and globally operators as usual as Fψ .= truefree(ψ)Uψ and Gψ .= ¬F¬ψ. These shortcut definitions for the temporal operators automatically induce the semantics of HyperLTLf .

Note that, we can impose two traces to be of equal length by |π1| = |π2| .= G(lastπ1 ↔ lastπ2 ). Analogously, we can say that π1 is not longer than π2 by |π1| ≤ |π2| .= (¬lastπ2 )Ulastπ1 . Finally, we can also compare the content of traces. For example, we can say that π1 and π2 evaluate a subset L ⊆ AP in the same way: equalL(π1, π2) .= |π1| = |π2| ∧ G ∧p∈L(pπ1 ↔ pπ2 ).

4 Model Checking HyperLDLf

We are interested in model checking HyperLDLf properties over a log. In particular we focus on a quite general class of logs: those that are regular, i.e., the set of traces in the log can be recognized by a deterministic finite automaton, which we call the Log DFA D, i.e., Log = L(D). We denote D, Π, i |= ϕ the fact that L(D),Π, i |= ϕ, and by D |= ϕ the fact that D, Π, 0 |= ϕ for some trace assignment Π. Therefore, model checking in our context is defined as follows.

Definition 3. For a given Log DFA D and a closed HyperLDLf formula ϕ, the model-checking problem is the problem of deciding whether D |= ϕ.

We solve the model-checking problem by reducing it to the emptiness problem of a suitably defined regular automaton. Consider a quantifier free HyperLDLf formula ψ and let V = {π1, . . . , πn} = free(ψ). Thus, ψ can be regarded as an LDLf formula over ⋃π∈V APπ, where APπ denotes the alphabet AP relativized with variable π, i.e., APπ = {pπ : p ∈ AP}. However, we need to consider its semantics in the context of HyperLDLf , which provides, at once, traces of different length. In order to use the LDLf automata construction, we restrict to trace assignments that map every variable in traces all of the same length. To do this, consider the function tail mapping a trace assignment Π to another tail(Π) over the same set V of traces, in which each Π(π) is replaced with tail(Π)(π) = Π(π)·end length(Π)-|Π(π)|+1 π 1 . Intuitively, every trace in the codomain of Π is appended with a tail of symbols endπ in a way that each of them has the same length.

By Θπ = 2APπ we denote the set of possible truthassignments over the set APπ and by Θend π = Θπ ∪ {endπ}, the set of assignments augmented with the corresponding endπ symbol. Observe that the symbol endπ differs from the empty assignment, setting every propositional variable false, but rather mean that the trace is finished. Indeed, it will hold that both endπ ̸|= 〈pπ〉tt and endπ ̸|= 〈¬pπ〉tt.

By Θend V = ⋃π∈V Θend π we denote the union set of assignments over the atomic propositions typed with π ∈ V . Note that the sets of truth-assignments are pairwise disjoint. Therefore, a truth-assignment in Θend V can be uniquely identified with a list of assignments in Θend π , one for each π ∈ V . At this point, every trace assignment tail(Π) of this form can be regarded as a single trace over the set Θend V , to which a quantifier-free HyperLDLf formula can be interpreted as an LDLf one. We have the following proposition.

Proposition 1. For a given quantifier-free HyperLDLf formula ϕ and a trace assignment Π, it holds that Π |= ϕ if, and only if, tail(Π) |= ϕ. 2

Hence, without loss of generality, we assume the trace assignments to map traces of the same length and then to regard them as a single trace over Θend V . This allows us to apply the DFA construction for LDLf [De Giacomo and Vardi, 2013; Brafman et al., 2018]:

1 Where we pose length(Π) = maxπ∈V {|Π(π)|}.

2 Note that the set Log is irrelevant for quantified free formulas, as it just needs to include the traces mapped to in Π.

Proposition 2. For every quantifier free HyperLDLf formula ψ there exists an alternating finite automaton Aψ of size polynomial in |ψ| such that, for every trace assignment Π, it holds that Π |= ψ if, and only if, Π ∈ L(Aψ).

Next we focus on regular logs. First, recall that the set Log of valid traces over AP is described in terms of a DFA D = 〈Σ,Q, q0, δ, F〉 with Σ = 2AP, that is Log = L(D). In our model-checking technique, we may need to read traces that are tailed with the end symbol a finite but unbounded number of times. This is done by amending the automaton and defining Dtail = 〈Σ′ ,Q′ , q0, δ′ , F ′ 〉, where Σ′ = Σ ∪ {end}, Q′ = Q∪{acc, rej}, F ′ = F ∪{acc} and δ′ extends δ as follows:

• δ′ (q, end) = {acc if q ∈ F
• δ′ (acc, σ) = {acc, if σ = end rej otherwise ;
• δ′ (rej, σ) = rej.

rej otherwise ;

Intuitively, Dtail is as D until the end of trace is reached. From that point on, it accepts only if both the trace is accepted by D and the rest is made by an arbitrarily long sequence of end symbols. The following trivially holds.

Proposition 3. For every DFAD, the automaton Dtail is such that L(Dtail ) = {w; endn : w ∈ L(D) and n ∈ N}.

Finally we deal with the quantifiers of HyperLDLf . To do so we make use of the classic notions of existential and universal projection (see e.g. [David E. Muller and Paul E. Schupp, 1995]).

Definition 4 (Automata projection). For a given automaton A =〈Σ, Q, q0, δ, F 〉 such that Σ = 2X and P ⊆ X:

• If A is nondeterministic, then the existential projection of A over P is the automaton A∃P = 〈Σ,Q, q0, δ∃P , F〉 with δ∃P (q, σ) = ∨σ′P ∈2P δ(q, σX\P ∪ σ′P ) 3
• If A is universal, then the universal projection of A over P is the automaton A∀P =〈Σ, Q, q0, δ∀P , F〉 where δ∀P (q, σ) = ∧σ′P ∈2P δ(q, σX\P ∪ σ′P )

Observe that, by using the Ndet and Univ, we can compute the existential and universal projections of any kind of automaton A. However this might require an exponential blow-up in its size, as nondeterminization and universalization are involved. For simplicity, we use the notation A∃P , in place of (Ndet(A))∃P , to denote the existential projection for every automaton. Analogously, A∀P denotes the universal projection for every automaton. Intuitively, the existential projection A∃P accepts words w for which there exists a replacement of the variables in P that make the resulting word w′ accepted by A. The universal projection, instead, A∀P accepts words w for which every possible replacement of the variable evaluation in P is a word w′ accepted by A. This is formalized in the following theorem which adapts a key result in [David E. Muller and Paul E. Schupp, 1995] for infinite words to finite ones.

3 Note that σ is a subset of X and that, for some Y ⊆ X, σY .=

σ ∩ Y denotes the projection over Y .

Theorem 1. For a given automaton A over the alphabet 2X and a subset P ⊆ X, the two following propositions hold:

1. For every word w ∈ (2X )∗ , w ∈ L(A∃P ) iff there exists a word w′ s.t. |w′ | = |w|, w′ (i)X\P = w(i)X\P for every i < |w|, and w′ ∈ L(A).
2. For every word w ∈ (2X )∗ , w ∈ L(A∀P ) iff for every word w′ such that |w′ | = |w| and w′ (i)X\P = w(i)X\P for every i < |w|, it holds that w′ ∈ L(A).

For a given DFA D reading words over an alphabet Σ = 2AP, the π-typification of D, denoted Dπ is obtained by renaming every proposition p in AP to pπ. By APπ = {pπ : p ∈ AP} we denote the set of typed variables from AP.

We are now ready to present our algorithm that, given a Log DFA D and a HyperLDLf formula ϕ, constructs an automaton Automaton(D, ϕ) whose nonemptiness problem is equivalent to check whether D |= ϕ. We first define Algorithm 1 for generating the automaton Automaton(D, ϕ).

Algorithm 1 Automata construction Automaton(·, ·). Input: HyperLDLf formula ϕ and Log DFA D. Output: The automaton Automaton(D, ϕ). if ϕ is quantifier free then return Aϕ ∩ ⋂π∈free(ϕ) Dtail π if ϕ = ∃πϕ′ then return (Automaton(D, ϕ′ ))∃APπ if ϕ = ∀πϕ′ then return (Automaton(D, ϕ′ ))∀APπ

Algorithm 1 recursively scans the formula on a top-tobottom fashion, handling its quantifiers one by one. At each recursive call, it removes the outermost quantifier of ϕ and computes the automata projection that corresponds to the quantification modality. For an existential quantification it applies an existential projection, whereas for a universal quantification, it applies a universal one. Algorithm 1 makes use of a polynomial operation: the typification of the alphabet.

Theorem2. For everyHyperLDLf formulaϕand a LogDFA D it holds that L(Automaton(D, ϕ)) = {Π : V → L(D) : D, Π, 0 |= ϕ}.

Proof sketch. By induction on the structure of ϕ, the base case handles the quantifier free formulas, for which the algorithm returns the DFA construction of Aϕ intersected with a suitable number of copies of Dtail APπ to make sure the selected traces are in the log. The inductive cases handle the quantifiers by means of automata projection. The correctness of such procedure follows from Theorem 1.

We can now solve model-checking of D and ϕ by checking the nonemptiness of Automaton(D, ϕ), see Algorithm 2.

The correctness of Algorithm 2 is a direct consequence of Theorem 2. Algorithm 2 gives us an upper-bound on the computational complexity of the problem.

Algorithm 2 Model checking HyperLDLf over Log DFAs.

Input: HyperLDLf formula ϕ and Log DFA D.

Output: YES, if D |= ϕ. NO, otherwise.

Compute A = Automaton(D, ϕ) by Alg. 1

if L(A) ̸= ∅ then

return YES

else

return NO

Theorem 3. The model checking problem for a HyperLDLf formula ϕ with quantifier alternation depth k over a Log DFA D can be solved in k-EXPSPACE in both ϕ and D.

Proof sketch. For quantified free formulas ϕ, Algorithm 2 checks the nonemptiness of a polynomial sized alternating automaton, whose complexity is PSPACE. For all the other cases, at each automata projection, the size of the automaton increases by one exponential, thus requiring an extra exponent in space complexity to check for its nonemptiness.

This bound is tight since we prove a matching lower-bound for the model-checking of both HyperLDLf and HyperLTLf .

Theorem 4. The model checking problem for a HyperLTLf (and so HyperLDLf ) formula ϕ with quantifier alternation depth k over a Log DFA D is k-EXPSPACE-Hard.

Proof sketch. Through an encoding from Turing machines. The proof adapts the argument for proving the lower-bound of the satisfiability problem for QPTL in [Sistla et al., 1987].

We observe that our technique is based on automata constructions involving projection (existential projection) and determinization and complementation (universal projection, considering that ∀ϕ ≡ ¬∃¬ϕ). Note that these operations are computationally dominated by determinization (projection is polynomial as is complementation after deteminization). In fact the alternation of quantifiers is directly related to the number of required determinization steps (after projection). This is what makes the tower of exponential directly related to quantifier alternations. On the other hand there is evidence that determinization in the case of regular nondeterministic automata, while worst case exponential, is often polynomial in practice for minimized DFAs [Tabakov and Vardi, 2005] and this often gives rise to scalable algorithms in spite of the worst case computational complexity [Zhu et al., 2017; Zhu et al., 2020; Tabajara and Vardi, 2020]. For this reason Algorithm 1 and 2 are indeed promising also in practice.

5 HyperLDLf and BPM

We illustrate how HyperLDLf can be used to capture a variety of interesting properties within Business Process Management (BPM). An operational process consists of a collection of activities that are executed in coordination [Dumas et al., 2018]. The process is instantiated multiple times, and each instance represents the execution of the process on a specific, so-called case object (an order, a claim, . . . ), moving it from the initial state of the process to one of its final states. This happens through the application of finitely many activities to the case object, in agreement with the ordering constraints imposed by the process control-flow. This setting perfectly matches HyperLDLf , thanks to the ability of the logic to express hyper-properties over the finite traces induced by multiple process instances.

We fix a set A of activities. Given a trace π over A, we assume that at each step, at most one activity is executed. The case where no activity is executed, which we represent for convenience using formula nopπ = ∧a∈A ¬aπ, represents an idle step in the execution. With this notions at hand, we concentrate on three relevant aspects in the BPM spectrum.

Process Mining is a family of techniques used to get insights about operational processes, and to improve processes based on event data obtained from actual executions [van der Aalst and others, 2011]. Process mining techniques range from the discovery of process models from event data to checking whether an event log conforms to a process model (either manually crafted or automatically discovered from data). To do so, they need to inspect and relate different traces that are contained in the event log or that can be generated by the process model (two notions that in our setting homogeneously map to the HyperLDLf notion of regular log). Specifically, several process mining techniques do not directly work with raw traces, but rather use all the traces at hand to establish behavioral relations between activities, in turn using them as a succinct, abstract representation.

As a representative example, we consider here the reference ordering relations introduced in one of the seminal works on process discovery [van der Aalst et al., 2004]. Such ordering relations capture whether, according to the log, two activities directly follow each other, are mutually exclusive, or concurrent. For example, a log Log indicates that activities a and b directly follow each other, that is, are in a strict sequencing (written a→Logb in [van der Aalst et al., 2004]), if: (i) there exists a trace in Log where a is followed by b without any other activity in between; (ii) in none of the traces from Log the converse happens, that is, b is followed by a without any other activity in between. While these two properties separately quantify over traces, they have to holds simultaneously in Log to infer that a and b are in a strict sequencing, hence calling for the hyper-features of HyperLDLf . Indeed, we can check whether a→Logb by:

The other ordering relations can be formalized analogously.

Instance-Spanning Constraints are behavioral constraints that span across multiple instances of a given process, and thus inherently require to related multiple traces at once. In [Rinderle-Ma et al., 2016], a multitude of instance-spanning constraints is collected from different application scenarios, from logistics to healthcare and security. Interestingly, previous formalization attempts in this spectrum either failed or required to combine all distinct traces in a single stream equipping events with trace identifiers [Rinderle-Ma et al., 2016], an approach that is not applicable when the (possibly infinite) log to be considered is generated by a process model. Differently from those attempts, thanks to its hyperfeatures HyperLDLf has the direct ability to elegantly capture instance-spanning constraints.

Consider for example an activity propagation constraint dictating that whenever an activity a occurs in a trace π of the log, then b has to occur later on in all traces π′ related to π. By assuming that the fact that π is related to π′ is expressed through a domain-specific HyperLDLf formula rel(π1, π2) having π and π′ as free variables, we can formalize in HyperLDLf this activity propagation constraint as: ∀π1, π2 rel(π1, π2) → G(aπ1 → XFbπ2 ). This formula can be instantiated to capture that whenever a package shipped via truck is detected as contaminated, then all the packages traveling in the same truck need to be later inspected.

Alternative behaviors in a process. We finally consider the use of HyperLDLf to express sophisticated properties on alternative behaviors exhibited by a process that cannot be captured using branching-time logics. To illustrate this, we first partition the activities A into observable activities AO (public activities executed by or visible to external actors), and unobservable activities AU (private activities). We want to express a variety of outcome property capturing that whenever the process can produce a trace π1 satisfying a desired behavioral pattern (a regular expression ρ) and leading to a given outcome (a final, observable activity), then it is also able to produce a different trace π2 that (i) mimics π1 by exhibiting the same observable behavior, and (ii) satisfies the same desired pattern ρ leading to an alternative outcome.

Intuitively, by "mimicking" we mean that two traces are equal once all unobservable activities are projected out. Additionally, observable activities are not required to happen at the same time: an observable activity happening in either trace is replicated by the other with an arbitrary delay by adding unobservable activities in between. Until this happens, however, no other observable activity can be executed in either trace. Note that the role of mimicking and of being mimicked can be exchanged among π1 and π2 at each observable activity: it can happen that an observable activity of π1 may be mimicked by π2 with a certain delay, and that the next observable activity of π2 is then mimicked by π1 with some other delay. This requirement cannot be captured by a simple branchingtime formula but is indeed a hyper property that requires the ability to compare observable projections of traces.

This can be used, for example, to check that the process is so that whenever a customer properly follows a sequence of public steps required by a payment system, if the payment is ultimately rejected then there is an alternative execution, with the same public steps but with possibly different unobservable ones (in type or number), where the payment is accepted.

To formalize this, we assume that in each step at most one task is executed. Let ρπ be a regular expression over the set A in π, and a, b ∈ AU respectively denote the actual and alternative outcomes. Then property can be captured as:

where mimics(π1, π2) formalizes that π2 mimics π1. Since π1 and π2 may have a different length, we write mimics(π1, π2) = |π1|≤ |π2|∧mimicsObs(π1, π2) ∨ |π1|> |π2|∧mimicsObs(π2, π1), and then formalize this notion of mimicking via mimicsObs(πs, πl), taking advantage from the fact that πs is of equal or shorter length than πl. To do so, we define a support formula: given a set T of trace variables, unT = ∧π∈T (nopπ ∨ (∨u∈AU uπ)) captures an unobservable step jointly performed in all traces from T. Using this, we write ϕskip = (un{πs,πl})∗ to indicate an arbitrary sequence of possibly different unobservable steps simultaneously performed by πs and πl. As a result, mimicsObs(πs, πl) =

6 RelatedWork on Infinite Traces

To deal with multiple traces at once, a specific extension of LTL, called HyperLTL, has been originally introduced in the infinite traces setting. HyperLTL supports explicit quantification over traces, as well as hyper-properties that inspect and relate multiple traces at once [Clarkson et al., 2014]. In [Clarkson et al., 2014], HyperLTL and HyperCTL∗ are introduced as extensions of LTL and CTL∗ to reason about a set of (infinite) traces all at once. A hyper extension of PDL, namely HyperPDL-∆, is considered in [Gutsfeld et al., 2020]. The model-checking and satisfiability problems for HyperLTL and these extensions have been investigated and solved [Clarkson et al., 2014; Finkbeiner and Hahn, 2016; Gutsfeld et al., 2020; Mascle and Zimmermann, 2020]. Their solutions are based on automata on infinite objects (traces), and provide a similar complexity hierarchy as the one in Theorem 3. Our technique avoids the manipulation of automata on infinite objects, sidestepping the difficulties of complementation of such automata, in favor of standard automata for regular languages, which have better computational characteristics in practice, see the discussion at the end of Section 4.

7 Conclusion

We have introduced HyperLDLf a logic for expressing hyper properties over logs, which are of particular interest, e.g., in BPM. Specifically, we have proposed a technique for modelchecking of regular logs that takes full advantage of the relationship between LTLf /LDLf and regular automata. For this reason, such a technique promises to be easily implementable and effective in practice in spite of the high worstcase complexity of the problem. It is also of interest to study other problems such as synthesis of a log satisfying certain HyperLDLf properties, which is related to satisfiability, or synthesis of controller generating a log with desired HyperLDLf properties, cfr. [Pnueli and Rosner, 1989].

Acknowledgments

Research partially supported by the ERC Advanced Grant WhiteMech (No. 834228) and by the EU ICT-48 2020 project TAILOR (No. 952215).