First Principles Simulations of MoS2 Towards the Non-Enzymatic Sensing of Cortisol

Gabriele Boschetto

Stefania Carapezzi, Aida Todri-Sanial CNRS-LIRMM, University of Montpellier, 34095 Montpellier, France gabriele.boschetto@lirmm.fr ; stefania.carapezzi@lirmm.fr ; aida.todri@lirmm.fr

Atomically thin two-dimensional (2D) materials have been -and are still currently beingextensively studied due to their unique mechanical, electrical, and optical properties, which, together with their ultra-thin size, enable the development of compact devices and innovative technologies. Within the vast chemical space of transition metal dichalcogenides (TMDs), single-layer molybdenum disulphide (MoS2) is with no doubt one of the most studied material due to its stability and its direct optical band gap of 1.8 eV, which make it the ideal candidate to be used in a wide range of nanoelectronic devices, going beyond conventional CMOS technology. [START_REF] Qiao | Fabricating molybdenum disulfide memristors[END_REF] Here we look at MoS2 in the context of biosensing, and we study such material as the core component of field-effect biosensors (Bio-FETs) for the detection of cortisol. Ultimately, the aim of this study is to design and integrate such biosensors in wearable health monitoring devices. [START_REF] Eu H | SmartVista project[END_REF] We want to bridge the gap between materials' properties and device physics and to do so, we carry out first-principles atomistic computer simulations in the framework of density functional theory (DFT). Our study constitutes the first step of a wider multi-scale modelling approach in which the goal is to construct a full atomistic-to-device level model. Recently, MoS2 has been studied as a sensing platform for detecting mainly gas and small biological molecules, such as glucose. [START_REF] Jeevanandham | Nickel oxide decorated MoS2 nanosheet-based nonenzymatic sensor for the selective detection of glucose[END_REF] Enzymatic biosensing is the most common approach, however, non-enzymatic sensing can provide higher sensor stability and prompt response at the expense of chemical selectivity. Here, we are interested in the non-enzymatic detection of cortisol in human sweat as a mean to monitor the risk of cardiovascular diseases. However, the mechanisms that govern the interaction between the analyte and MoS2 at the molecular level are far from being understood. Thus, we thoroughly explore the MoS2/cortisol interaction in terms of both structural, electronic, and charge transfer properties to assess viable sensing mechanisms. We study the impact of some of the most used metal dopants employed in lab-scale experiments, such as Ni, Pt, Pd, in order to modulate the sensing platform with respect to bare MoS2. In addition to single-atom doping, we also explore the use of metal nanoparticles (e.g., Pt and Au) to decorate the MoS2 layer as yet another mean to detect cortisol. Overall, our work ultimately aims to obtain a deep understanding of the properties of MoS2 when used as a sensor to drive the design of devices towards better performance.

October 26-29, 2021 Grenoble (France)


Thomas Chatain
email: chatain@lsv.fr

Mathilde Boltenhagen
email: boltenhagen@lsv.fr

Josep Carmona
email: jcarmona@cs.upc.edu

Anti-Alignments -Measuring The Precision of Process Models and Event Logs

Processes are a crucial artefact in organizations, since they coordinate the execution of activities so that products and services are provided. The use of models to analyse the underlying processes is a well-known practice. However, due to the complexity and continuous evolution of their processes, organizations need an effective way of analysing the relation between processes and models.

Conformance checking techniques asses the suitability of a process model in representing an underlying process, observed through a collection of real executions. One important metric in conformance checking is to asses the precision of the model with respect to the observed executions, i.e., characterize the ability of the model to produce behavior unrelated to the one observed. In this paper we present the notion of anti-alignment as a concept to help unveiling runs in the model that may deviate significantly from the observed behavior.

Using anti-alignments, a new metric for precision is proposed. The proposed anti-alignment based precision metric satisfies most of the required axioms highlighted in a recent publication. Moreover, a complexity analysis of the problem of computing anti-alignments is provided, which sheds light into the practicability of using anti-alignment to estimate precision. Experiments are provided that witness the validity of the concepts introduced in this paper.

Conformance Checking; Anti-Alignments; Precision.

Introduction

Relating observed and modelled process behavior is the lion's share of conformance checking [START_REF] Carmona | Conformance Checking -Relating Processes and Models[END_REF]. Observed behavior is often recorded in form of event logs, that store the footprints of process executions. Symmetrically, process models are representations of the underlying process, which can be automatically discovered or manually designed. With the aim of quantifying this relation, conformance checking techniques consider four quality dimensions: fitness, precision, generalization and simplicity [START_REF] Rozinat | Conformance checking of processes based on monitoring real behavior[END_REF]. For the first three dimensions, the alignment between a process model and an event log is of paramount importance, since it allows relating modeled and observed behavior [START_REF] Adriansyah | Aligning observed and modeled behavior[END_REF].

Given a process model and a trace in the event log, an alignment provides the run in the model which mostly resembles the observed trace. When alignments are computed, the quality dimensions can be defined on top [START_REF] Adriansyah | Aligning observed and modeled behavior[END_REF][START_REF] Munoz-Gama | Conformance Checking and Diagnosis in Process Mining[END_REF]. In a way, alignments are optimistic: although observed behavior may deviate significantly from modeled behavior, it is always assumed that the least deviations are the best explanation (from the model's perspective) for the observed behavior.

In this paper we present a somewhat symmetric notion to alignments, denoted as anti-alignments. Given a process model and a log, an anti-alignment is a run of the model that mostly deviates from any of the traces observed in the log. The motivation for anti-alignments is precisely to compensate the optimistic view provided by alignments, so that the model is queried to return a highly deviating behavior that has not been seen in the log. In contexts where the process model should adhere to a certain behavior and not leave much room for exotic possibilities (e.g., banking, healthcare), the absence of highly deviating anti-alignments may be a desired property for a process model. Using anti-alignments one cannot only catch deviating behavior, but also use it to improve some of the current quality metrics considered in conformance checking. In this paper we highlight the strong relation of anti-alignments and the precision metric: a highly-deviating anti-alignment may be considered as a witness for a loss in precision. Some of the reference metrics for precision lack this ability of exploring the model behavior beyond what is observed in the log, thus being considered as short-sighted (e.g., [START_REF] Adriansyah | Measuring precision of modeled behavior[END_REF]).

We cast the problem of computing anti-alignments as the satisfiability of a Boolean formula, and provide high-level techniques which can for instance compute the most deviating anti-alignment for a certain run length, or the shortest anti-alignment for a given number of deviations.

Anti-alignments are related to the completeness of the log; a log is complete if it contains all the behavior of the underlying process [START_REF] Van Der Aalst | Process Mining -Data Science in Action[END_REF]. For incomplete logs, the alternatives for computing anti-alignments grow, making it difficult to tell the difference between behavior not observed but meant to be part of the process, and behavior not observed which is not meant to be part of the process.

Since there exists already some metrics to evaluate the completeness of an event log (e.g., [START_REF] Yang | Estimating completeness of event logs[END_REF]), we assume event logs have a high level of completeness before they are used for computing anti-alignments. Notice that in presence of an incomplete event log, anti-alignments can be used to interactively complete it: an anti-alignment that is certified by the stake-holder as valid process behavior can be appended to the event log to make it more complete. This work is an extension of recent publications related to anti-alignments: in [START_REF] Chatain | Anti-alignments in conformance checking -the dark side of process models[END_REF] we established for the first time the notion of anti-alignments based on the Hamming distance, and proposed a simple metric to estimate precision.

Then, the work in [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF] elaborated the notion of anti-alignments, heuristically computing them for the Levenshtein distance by adapting the A * search technique, and proposed two new notions for trace-based and log-based precision, that can be combined to estimate precision of process models. However, as it was claimed recently in a survey paper advocating for properties precision metrics should have [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF], it was not known the satisfiability of the properties for the aforementioned metrics.

The contributions of the paper with respect to our previous work are now enumerated.

• We show how anti-alignments can be computed in an optimal way for the Levenshtein distance, without increasing the complexity class of the problem. Moreover we relate the two available distance encodings (Hamming and Levenshtein), and show the implications of using each one for anti-alignment based precision.

• We adapt the precision metrics from [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF] to not depend on a particular length defined apriori.

• We prove the adherence of one of the new metrics proposed in this paper to most of the properties in [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF].

• A novel implementation is provided, with several improvements and heuristics, which makes it able to deal with larger instances.

• A new evaluation section is reported, that shows empirically the capabilities of the proposed technique for large and real-life instances.

The remainder of the paper is organized as follows: in the next section, a simple example is used to emphasize the importance of anti-alignments and their application to estimate precision is shown. Then in Section 3 the basic theory needed for the understanding of the paper is introduced. Section 4 provides the formal definition of anti-alignments, whilst Section 5 formalizes the encoding into SAT of the problem of computing anti-alignments. In Section 6, we define a new metric, based on anti-alignments, for estimating precision of process models.

Experiments are reported in Section 7, and related work in Section 8. Section 9 concludes the paper and gives some hints for future research directions.

A Motivating Example

Let us use the example shown in Figure 1 for illustrating the notion of antialignment. The example was originally presented in [START_REF] Vanden Broucke | Event-based real-time decomposed conformance analysis[END_REF], and in this paper we present a very abstract version of it in Figure 1 contains all sort of monetary checks, authority notifications, and logging mechanisms. The process is initiated when a new transaction is requested, opening a new instance in the system and registering all the components involved. The second step is to run a check on the person (or entity) origin of the monetary transaction. Then, the actual payment is processed differently, depending of the payment modality chosen by the sender (cash, cheque and payment). Later, the receiver is checked and the money is transferred. Finally, the process ends registering the information, notifying it to the required actors and authorities, and emitting the corresponding receipt.

Assume that a log covering all the three possible variants (corresponding to the three possible payment methods) with respect of the model in Figure 1(a) is given. The three different variants for this log will be: ort, cs, pcap, cr, tm, nct ort, cs, pchp, cr, tm, nct ort, cs, pep, cr, tm, nct where we use the acronym for each one of the actions performed, e.g., ort stands for open and register transaction.

For this pair of model and log, most of the current metrics for precision (e.g., [START_REF] Adriansyah | Measuring precision of modeled behavior[END_REF]) will rightly assess a very high precision. In fact, since no deviating anti-alignment can be obtained because every model run is in the log, the antialignment based precision metric from this paper will also assess a high (in our case, perfect) precision. Now assume that we modify a bit the model, adding a loop around the alternative stages for the payment. Intuitively, this (malicious) modification in the process model may allow to pay several times although only one transfer will be done. The modified high-level overview is shown in Figure 1(b). The aforementioned metric for precision will not consider this modification as a severe one: the precision of the model with respect to the log will be very similar to the one for the model in Figure 1(a).

Remarkably, this modification in the process model comes with a new highly deviating anti-alignment denoting a run of the model that contains more than one iteration of the payment: ort, cs, pcap, pchp, pchp, pep, pcap, cr, tm, nct Clearly, this model execution where five payments have been recorded is possible in the process of Figure 1(b). Correspondingly, the precision of this model in describing the log of only three variants will be significantly lowered in the metric proposed in this paper, since the anti-alignment produced is very different from any of the three variants recorded in the event log. [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF] is a tuple N = ⟨P, T, F, M 0 , M f , Σ, λ⟩, where P is the set of places, T is the set of transitions (with P ∩ T = ∅), F : (P × T ) ∪ (T × P ) → {0, 1} is the flow relation, M 0 is the initial marking, M f is the final marking, Σ is an alphabet of actions and λ : T → Σ labels every transition by an action.

Preliminaries Definition 1 ((Labeled) Petri net). A (labeled) Petri Net

A marking is an assignment of a non-negative integer to each place. If k is assigned to place p by marking M (denoted M (p) = k), we say that p is marked with k tokens. Given a node x ∈ P ∪ T , its pre-set and post-set are denoted by

∈ T * , u 2 ∈ T + , u 3 ∈ T * such that M 0 [u 1 ⟩M [u 2 ⟩M [u 3 ⟩M f .
An event log is a collection of traces, where a trace may appear more than once. Formally: Definition 2 (Event Log). An event log L (over an alphabet of actions Σ) is a multiset of traces σ ∈ Σ * .

Process mining techniques aim at extracting from a log L a process model N (e.g., a Petri net) with the goal to elicit the process underlying a system S. S is considered a language for the sake of comparison. By relating the behaviors of L, L(N ) and S, particular concepts can be defined [START_REF] Buijs | Quality dimensions in process discovery: The importance of fitness, precision, generalization and simplicity[END_REF]. A log is incomplete if

S \ L ̸ = ∅. A model N fits log L if L ⊆ L(N ). A model is precise in describing a log L if L(N ) \ L is small. A model N represents a generalization of log L with respect to system S if some behavior in S \ L exists in L(N ). Finally, a model
N is simple when it has the minimal complexity in representing L(N ), i.e., the well-known Occam's razor principle.

Anti-Alignments

The idea of anti-alignments is to seek in the language of a model N what are the runs which differ considerably with all the observed traces. Hence, this is the opposite of the notion of alignments [START_REF] Adriansyah | Aligning observed and modeled behavior[END_REF] which is central in process mining: for many tasks in conformance checking like process model repair or decision point analysis, one needs indeed to find the run which is the most similar to a given log trace [START_REF] Van Der Aalst | Process Mining -Data Science in Action[END_REF]. In this paper, we are focusing on precision and for this, traces which are not similar to any observed trace in the log serve as witnesses for bad precision. All these notions anyway depend on a definition of distance between two traces (typically a model trace, i.e. a run of the model, and an observed log trace). We assume a given distance function dist :

Σ * × Σ * → [0, 1]
computable in polynomial time and such that1

• for every γ ∈ Σ * , dist(γ, γ) = 0,

• for every σ ∈ Σ * , dist(γ, σ) converges to 1 when |γ| diverges to ∞.

Definition 3 (Anti-alignment).

For a distance threshold m ∈ [0, 1], an manti-alignment of a model N w.r.t. a log L is a full run γ ∈ L(N ) such that dist(γ, L) ≥ m, where dist(γ, L) is defined as the min σ∈L dist(γ, σ). 2For the following examples, we show anti-alignments w.r.t. two possible choices of distance dist: Levenshtein's distance and Hamming distance. Definition 4 (Levenshtein's edit distance dist L ). Levenshtein's edit distance dist L (γ, σ) between two traces γ, σ ∈ Σ * is based on the minimum number #edits(γ, σ) of deletions and insertions needed to transform γ to σ. In order to get a normalized distance between 0 and 1, we define Levenshtein's edit distance dist L (γ, σ) = #edits(γ,σ) max (1,|γ|+|σ|) .

L = {⟨a, b, c, f, g, h, k⟩, ⟨a, c, b, f, g, h, k⟩, ⟨a, c, b, f, h, g, k⟩, ⟨a, b, c, f, h, g, k⟩,
⟨a, e, f, i, k⟩, ⟨a, d, f, g, h, k⟩, ⟨a, e, f, h, g, k⟩} ,

Figure 2: A process model (taken from [START_REF] Van Der Aalst | Process discovery using localized events[END_REF]) and an event log. The full run ⟨a, b, c, f, i, k⟩ is a Example 1. Consider the Petri net and log shown in Figure 2. With Levenshtein's distance, the full run ⟨a, b, c, f, i, k⟩ is at distance 3 13 from the log trace ⟨a, b, c, f, g, h, k⟩ (two deletions and one insertion). It is at larger distance from the other log traces. Therefore, it is a 3 13 -anti-alignment.

Another interesting choice is Hamming distance. It is in general less informative than Levenshtein's distance for relating observed and modelled behavior, but it has the interest of being very simple to compute. Variants of Hamming distance can also provide good compromises. In Sections 5 and 6, we will show how to efficiently compute anti-alignments for Hamming distance using SAT solvers.

Definition 5 (Hamming distance dist H

). For two traces γ = γ 1 . . . γ n and

σ = σ 1 . . . σ n , of same length n > 0, define dist H (γ, σ) := 1 n • { i ∈ {1 . . . n} | γ i ̸ = σ i } . For γ longer than σ, we define dist H (γ, σ) := dist H (γ, σ • w |γ|-|σ| ),
where w ̸ ∈ Σ is a special padding symbol (w for 'wait'); we proceed symmetrically when γ is shorter than σ.

Lemma 1. Observe that, for every γ and σ (assuming one of them at least is nonempty), dist L (γ, σ) ≤ dist H (γ, σ).

Proof. Assume w.l.o.g.

0 < |γ| < |σ|. Let n := { i ∈ {1 . . . |γ|} | γ i ̸ = σ i } .
We Proof. If the model has finitely many full runs, then one of them must be a maximal anti-alignment.

Conversely, if N is finite and has infinitely many runs, then there must exist arbitrary long full runs; more formally, there exists an infinite sequence of full runs (γ i ) i∈N of strictly increasing length. For every σ ∈ L, the sequence of (dist(γ i , σ)) i∈N converges to 1. Since there are finitely many σ ∈ L,

(min σ∈L dist(γ i , σ)) i∈N converges to 1 as well. 2
Maximal anti-alignments will be used in Section 6 to define our precision metric.

The case of models with executable loops will be discussed in Subsection 6.1.1.

Lemma 3.

The problem of deciding, given a finite model N and a log L, whether there exists a 0-anti-alignment of N w.r.t. L, has the same complexity as reachability for Petri nets.

Proof. This is equivalent to checking whether L(N

) ̸ = ∅, i.e. whether M f is reachable from M 0 . 2
By definition, a 0-anti-alignment of N w.r.t. L is a full run γ ∈ L(N ) satisfying the trivial inequality dist(γ, L) ≥ 0. The same problem with a strict inequality is also of interest. We will need it in Section 6.1.1. The problem of reachability in Petri nets is known to be decidable, but nonelementary [START_REF] Czerwinski | The reachability problem for petri nets is not elementary[END_REF]. Yet, the complexity drops to NP if a bound is given on the length of the anti-alignment.

Lemma 5. The problem of deciding, for a Petri net N , a log L, a rational distance threshold m ∈ Q and a bound n ∈ N, if there exists an m-anti-alignment γ such that |γ| ≤ n, is NP-complete. We assume that n is encoded in unary. 3 Proof. The problem is clearly in NP: checking that a run γ is a m-antialignment of N w.r.t. L takes polynomial time (remember that we consider distance functions computable in polynomial time).

For NP-hardness, we propose a reduction from the problem of reachability of a marking M f in a 1-safe acyclic 4 Petri net N , known to be NP-complete [START_REF] Stewart | Reachability in some classes of acyclic Petri nets[END_REF][START_REF] Cheng | Complexity results for 1-safe nets[END_REF]. Notice that, since N is acyclic, each transition can fire only once; hence, the length of the firing sequences of N is bounded by the number of transitions 3 Since n has typically the same order of magnitude as the length of the longest traces in the log, encoding n in unary does not significantly affect the size of the problem instances. 4 a Petri net is acyclic if the transitive closure F + of its flow relation is irreflexive.

|T |. Finally, M f is reachable in N iff

SAT-encoding of Anti-Alignments

In this section, we give hints on how SAT solvers can help to find antialignments. We detail the construction of a SAT formula Φ n m (N, L), where N is a Petri net, L a log, n and m two integers. This formula will be used in the search of anti-alignments of N w.r.t. L for Hamming distance (see Section 5.3 for the encoding using the Levenshtein distance). The formula Φ n m (N, L) characterizes precisely the full runs γ = λ(t 1 ) . . . λ(t n ) ∈ L(N ) of N of length n which differ in at least m positions with every log trace in L.

Coding Φ n m (N, L) Using Boolean Variables

The formula Φ n m (N, L) is coded using the following Boolean variables:

• τ i,t for i = 1 . . . n, t ∈ T (remind that w is the special symbol used to pad the log traces, see Definition 5) means that transition t i = t.

• m i,p for i = 0 . . . n, p ∈ P means that place p is marked in marking M i (remind that we consider only safe nets, therefore the m i,p are Boolean variables).

• δ i,σ,k for i = 1 . . . n, σ ∈ L, k = 1, . . . , m means that the k th mismatch with the observed trace σ is at position i.

The total number of variables is

O(n × (|T | + |P | + |L| × m)).
Let us decompose the formula Φ n m (N, L).

• The fact that γ = λ(t 1 ) . . . λ(t n ) ∈ L(N ) is coded by the conjunction of the following formulas:

-Initial marking:   ∧ p∈M0 m 0,p   ∧   ∧ p∈P \M0 ¬m 0,p   -Final marking:   ∧ p∈M f m n,p   ∧   ∧ p∈P \M f ¬m n,p  
-One and only one t i for each i:

n ∧ i=1 ∨ t∈T (τ i,t ∧ ∧ t ′ ∈T ¬τ i,t ′ )
-The transitions are enabled when they fire:

n ∧ i=1 ∧ t∈T (τ i,t =⇒ ∧ p∈ • t m i-1,p )
-Token game (for safe Petri nets):

n ∧ i=1 ∧ t∈T ∧ p∈t • (τ i,t =⇒ m i,p ) n ∧ i=1 ∧ t∈T ∧ p∈ • t\t • (τ i,t =⇒ ¬m i,p ) n ∧ i=1 ∧ t∈T ∧ p∈P,p̸ ∈ • t,p̸ ∈t • (τ i,t =⇒ (m i,p ⇐⇒ m i-1,p ))
• Now, the constraint that γ deviates from the observed traces (for every

σ ∈ L, dist(γ, σ) ≥ m) is coded as: ∧ σ∈L m ∧ k=1 n ∨ i=1 δ i,σ,k
with the δ i,σ,k correctly affected w.r.t. λ(t i ) and σ i :

∧ σ∈L m ∧ k=1 n ∧ i=1 ( δ i,σ,k ⇐⇒ ∨ t∈T, λ(t)̸ =σi τ i,t
)

and that for k ̸ = k ′ , the k th and k ′th mismatch correspond to different i's (i.e. a given mismatch cannot serve twice):

∧ σ∈L n ∧ i=1 m-1 ∧ k=1 m ∧ k ′ =k+1 ¬(δ i,σ,k ∧ δ i,σ,k ′ )

Size of the Formula

In the end, the first part of the formula

(γ = λ(t 1 ) . . . λ(t n ) ∈ L(N )) is coded by a Boolean formula of size O(n × |T | × |N |), with |N | := |T | + |P |.
The second part of the formula (for every

σ ∈ L, dist(γ, σ) ≥ m) is coded by a Boolean formula of size O(n × m 2 × |L| × |T |).
The total size for the coding of the formula

Φ n m (N, L) is O ( n × |T | × ( |N | + m 2 × |L|
)) .

SAT-encoding of Anti-Alignments for Levenshtein's Edit Distance

Our SAT-encoding of anti-alignments for Levenshtein's edit distance uses the same boolean variables as the SAT-encoding of anti-alignments for Hamming distance of the previous section, completed with δ variables used to encode the edit distance.

Our encoding is based on the same relations that are used by the classical dynamic programming recursive algorithm for computing the edit distance between two words u = ⟨u 1 , . . . ,

u n ⟩ and v = ⟨v 1 , . . . , v m ⟩:                            dist(⟨u 1 , . . . , u i ⟩, ϵ) = i dist(ϵ, ⟨v 1 , . . . , v j ⟩) = j dist(⟨u 1 , . . . , u i+1 ⟩, ⟨v 1 , . . . , v j+1 ⟩) =          dist(⟨u 1 , . . . , u i ⟩, ⟨v 1 , . . . , v j ⟩) if u i+1 = v j+1 1 + min(dist(⟨u 1 , . . . , u i+1 ⟩, ⟨v 1 , . . . , v j ⟩), dist(⟨u 1 , . . . , u i ⟩, ⟨v 1 , . . . , v j+1 ⟩)) if u i+1 ̸ = v j+1
We encode this computation in a SAT formula ϕ over variables δ i,j,d , for i = 0, . . . , n, j = 0, . . . , m and d = 0, . . . , n + m. Formula ϕ will have exactly one solution, in which each variable δ i,j,d is true iff ⟨u 1 . . . u i ⟩ and ⟨v 1 . . . v j ⟩ differ by at least d edits.

In order to test equality between the u i and v j , we use variables λ i,a and λ ′ j,a , for i = 0, . . . , n, j = 0, . . . , m and a ∈ Σ, and we set their value such that λ i,a is true iff u i = a, and λ ′ j,a is true iff v j = a. Hence, the test u i+1 = v j+1 becomes in our formulas:

∨ a∈Σ (λ i+1,a ∧λ ′ j+1,a ). For readability of the formulas, we refer to this coding by [u i+1 = v j+1 ]. We also write similarly

[u i+1 ̸ = v j+1 ].
In the following, we describe the different clauses of the formula ϕ of our SAT encoding of the edit distance.

δ 0,0,0 ∧ ∧ d>0 ¬δ 0,0,d (1)
∧ d ∧ n i=0 (δ i+1,0,d+1 ⇔ δ i,0,d ) (2) ∧ d ∧ m j=0 (δ 0,j+1,d+1 ⇔ δ 0,j,d ) (3) ∧ d n ∧ i=0 m ∧ j=0 [u i+1 = v j+1 ] ⇒ (δ i+1,j+1,d ⇔ δ i,j,d ) (4)
∧ d n ∧ i=0 m ∧ j=0 [u i+1 ̸ = v j+1 ] ⇒ (δ i+1,j+1,d+1 ⇔ (δ i+1,j,d ∧ δ i,j+1,d )) (5)
Example 3. At instants i = 1 and j = 1 of words u = ⟨s, g, c⟩ and v = ⟨s, b, c, a⟩, the letters are the same, then, by ( 4), the distance is only higher or equal to 0 :

(u 1 = v 1 ) ⇒ (δ 1,1,0 ⇔ δ 0,0,0 ).
However at instants i = 2 and j = 2, the letters u 2 and v 2 are different.

A step before, δ 1,2,1 and δ 2,1,1 are true because of the length of the subwords.

Then, by [START_REF] Augusto | Split miner: Discovering accurate and simple business process models from event logs[END_REF], the distance at instants i = 2 and j = 2 is higher or equal to 2 :

δ 2,2,2 .
The result is understandable because the edit distance costs the deletion of g and the addition of b to transform u to v.

In order to insert this encoding of Leventshein's edit distance into our formulas for anti-alignments, we need to compute the edit distance between the expected anti-alignment and every trace of the log, which requires to use variables δ i,σ,j,k for i = 0 . . . n, σ ∈ L, j = 0 . . . |σ|, k = 0, . . . , max(n, |σ|) to represent the fact that u 1 . . . u i and v 1 . . . v j differ by at least k edits.

Solving the Formula in Practice

In practice, the coding of the formula Φ n m (N, L) can be done using the Boolean variables τ i,t , m i,p and δ i,σ,k .

Then we need to transform the formula in conjunctive normal form (CNF) in order to pass it to the SAT solver. We use Tseytin's transformation [START_REF] Tseytin | On the complexity of derivation in propositional calculus[END_REF] to get a formula in conjunctive normal form (CNF) whose size is linear in the size of the original formula. The idea of this transformation is to replace recursively the disjunctions ϕ 1 ∨ • • • ∨ ϕ n (where the ϕ i are not atoms) by the following equivalent formula:

∃x 1 , . . . , x n                x 1 ∨ • • • ∨ x n ∧ x 1 =⇒ ϕ 1 ∧ . . . ∧ x n =⇒ ϕ n
where x 1 , . . . , x n are fresh variables.

In the end, the SAT solver tells us if there exists a run γ = λ(t 1 ) . . . λ(t n ) ∈ L(N ) which differs by at least m edits with every observed trace σ ∈ L. If a solution is found, we extract the run γ using the values assigned by the SAT solver to the Boolean variables τ i,t .

Using Anti-Alignments to Estimate Precision

In this section we show how to use anti-alignments to estimate precision of process models. Remarkably, we show how to modify the definitions of [START_REF] Chatain | Anti-alignments in conformance checking -the dark side of process models[END_REF][START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF] so that the new metric does not depend on a predefined length. In Section 6.2 we dive into the adherence of the metric with respect to a recent proposal for properties of precision metrics [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF].

Precision

Our precision metric is an adaptation of our previous versions presented in [START_REF] Chatain | Anti-alignments in conformance checking -the dark side of process models[END_REF][START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF]. It relies on anti-alignments to find the model run that is as distant as possible to the log traces. Like anti-alignments, the definition of precision is parameterized by a distance dist. In the examples, we will specify each time if we use Levenshtein's edit distance (Definition 4) or Hamming distance (Definition 5).

Definition 6 (Precision).

Let L be an event log and N a model. We define precision as follows:

P aa (N, L) := 1 -sup γ∈L(N ) dist(γ, L) .
For instance, consider the model and log shown in Figure 2. With Levenshtein's distance, the full run ⟨a, b, c, f, i, k⟩ is a maximal anti-alignment. It is at distance 3 13 to any of the log traces, and hence P aa (N, L) = 1 -3 13 = 0.77.

Handling Process Models with Loops

Notice that a model with arbitrary long runs (i.e., a process model that contains loops) may cause the formula in Definition 6 to converge to 0. This is a natural artifact of comparing a finite language (the event log), with a possibly infinite language (the process model). Since process models in reality contain loops, an adaptation of the metric is done in this section, so that it can also handle this type of models without penalizing severely the loops.

Definition 7 (Precision for Models with Loops). Let L be an event log

and N a model. We define ϵ-precision as follows:

P ϵ aa (N, L) := 1 -sup γ∈L(N ) dist(γ, L) (1 + ϵ) |γ|
with some ϵ ≥ 0 which is a parameter of this definition.

Informally, the formula computes the anti-alignment that provides maximal distance with any trace in the log, and at the same time tries to minimize its length. The penalization for the length is parametrized over the ϵ 5 . Observe that P 0 aa (N, L) is precisely the precision P aa (N, L) of Definition 6. By making Definition 7 not dependant on a predefined length, it deviates from the log-based precision metrics defined in previous work [START_REF] Chatain | Anti-alignments in conformance checking -the dark side of process models[END_REF][START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF].

Let us now consider the model of Figure 4, and the log ⟨a,b,c,d⟩,⟨a,f,g,h⟩,⟨a,b,i,b,c,d⟩]. Assume that ϵ = 0.05. A possible anti-alignment is γ 1 = ⟨a, c, b, e⟩ which is at least at Levenshtein's distance 1 2 to any of the log traces. For γ 1 the value of the formula is 1 - Another possible anti-alignment is c,b,i,b,i,b,i,b,i,b, e⟩ which is at least at distance 10 18 to any of the log traces. For γ 2 the value of the formula is 1 -10 18

L = [⟨a⟩,
γ 2 = ⟨a,
(1.05) 12 = 0.691. Hence, since the anti-alignment that maximizes the second term of the formula is γ 1 , the precision computed is P 0.05 aa (N, L) = 0.589. If instead, ϵ is set to a lower value, e.g., ϵ = 0.02, the corresponding value of the formula for the anti-alignment ⟨a, c, b, i, b, i, b, i, b, i, b, i, b, i, b, i, b, e⟩ will be the mainimal, and therefore it will be selected as the anti-alignment resulting in P 0.02 aa (N, L) = 0.533.

Computing P ϵ aa

By incorporating the ϵ parameter in the definition of precision, now the metric can deal with models containing loops without predefining the length of the anti-alignment. In this section we show that the proposed extension is well-defined and can be computed, and provide some complexity results of the algorithms involved.

Lemma 6. For every finite model N , log L and ϵ > 0, the supremum in the definition of P ϵ aa is reached, i.e. there exists a full run γ ∈ L(N ) such that

P ϵ aa (N, L) = 1 -dist(γ,L) (1+ϵ) |γ| .
Proof. Two cases have to be distinguished: if L(N ) ⊆ L, then the supremum equals 0, is obviously reached by any γ ∈ L(N ), and P ϵ aa (N, L) = 1; otherwise, let γ 0 ∈ L(N ) \ L and let m := dist(γ0,L) (1+ϵ) |γ 0 | ; we show that the supremum in the definition of P ϵ aa becomes now a maximum over a finite set of runs, bounded by a given length n that depends on m and ϵ:

sup γ∈L(N ) dist(γ, L) (1 + ϵ) |γ| = max γ∈L(N ),|γ|≤n dist(γ, L) (1 + ϵ) |γ| , with n := ⌊ -log m log(1+ϵ)

⌋

. Indeed, for every γ strictly longer than n, we have

dist(γ,L) (1+ϵ) |γ| ≤ 1 (1+ϵ) n+1 = exp(-(n + 1) • log(1 + ϵ)) ≤ exp(log m) = m, which also shows that |γ 0 | ≤ n.
Hence γ 0 is considered in our max, and then

max γ∈L(N ),|γ|≤n dist(γ,L) (1+ϵ) |γ| ≥ m > sup γ∈L(N ),|γ|>n dist(γ,L) (1+ϵ) |γ| . 2
Lemma 6 gives us the key for an algorithm to compute P ϵ aa .

Algorithm 1. Algorithm for computing P ϵ aa (N, L): • else return 1 (the model has perfect precision).

• if L(N ) ̸ ⊆ L, then -select γ 0 ∈ L(N ) \ L -let m := dist(γ0,L) (1+ϵ) |γ 0 | -explore
The correctness of this algorithm follows directly from Lemma 6. Its complexity resides essentially in the initial test, which corresponds to simply deciding if P ϵ aa (N, L) < 1, whose complexity is given by the following lemma:

Lemma 7. The problem of deciding, for a finite model N and a log L, if

P ϵ aa (N, L) < 1, is equivalent to deciding reachability in Petri nets.
Proof. We simply observe that P ϵ aa (N, L) < 1 iff L(N ) ̸ ⊆ L. Deciding this is equivalent to deciding reachability in Petri nets, as showed in Lemma 4. 2

However, in practice, one would generally skip the first check and jump directly to the exploration until some depth n, possibly computed for a given threshold m, like the one given by the γ 0 in Algorithm 1. Notice that the algorithm explores less deep (i.e. n is smaller) when m is large (close to 1), i.e. γ 0 is close to the optimal anti-alignment. We can summarize this with the following variation of Algorithm 1:

Algorithm 2. Algorithm for estimating P ϵ aa (N, L) using a threshold 0 < m ≤ 1 as input:

• explore the reachability graph of N until depth n :=

⌊ -log m log(1+ϵ) ⌋ • if the exploration finds a full run γ ∈ L(N ) \ L • then output "P ϵ aa (N, L) = 1 -max γ∈L(N ),|γ|≤n dist(γ,L) (1+ϵ) |γ| " • else output "P ϵ aa (N, L) ≥ 1 -m".
Lemma 8. For any fixed ϵ > 0, the problem of deciding, for a finite model N , a log L and a rational constant m > 0, if

P ϵ aa (N, L) < 1 -m, is NP-complete.
Proof. The proof is similar to the one of Lemma 6; here, the bound m is given directly, and we have the same equality

sup γ∈L(N ) dist(γ, L) (1 + ϵ) |γ| = max γ∈L(N ),|γ|≤n dist(γ, L) (1 + ϵ) |γ| , with n := ⌊ -log m log(1+ϵ)

⌋

. This means, in order to check that P ϵ aa (N, L) < 1 -m, it suffices to guess a full run γ of length |γ| ≤ n, where n depends linearly on the size of the representation of m (number of bits in the numerator and denominator). Then one can check in polynomial time that dist(γ,L) (1+ϵ) |γ| > m. For completeness, we proceed like in Lemma 5: we reduce reachability of

M f in a 1-safe acyclic Petri net N to P ϵ aa (N, L) < 1 -m with L = ∅ and m = 1 (1+ϵ) |T |+1 . 2

Discussion about Reference Properties for Precision

Recently, an effort to consolidate a set of desired properties for precision metrics has been proposed [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF]. Five axioms are described that establish different features of a precision metric prec(N, L). Summarizing, the axioms proposed in [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF] are:

• A1: A precision metric should be a function, i.e. it should be deterministic.

• A2: If a process model N 2 allows for more behavior not seen in a log L than another model N 1 does, then N 2 should have a lower precision than

N 1 regarding L: L ⊆ L(N 1 ) ⊆ L(N 2 ) =⇒ prec(N 1 , L) ≥ prec(N 2 , L)
• A3: Let N 1 be a model that allows for the behavior seen in a log L, and at the same time its behavior is properly included in a model N 2 whose language is Σ *6 (called a flower model). Then the precision of N 1 on L should be strictly greater than the one for N 2 .

• A4: The precision of a log on two language equivalent models should be equal:

L(N 1 ) = L(N 2 ) =⇒ prec(N 1 , L) = prec(N 2 , L)
• A5: Adding fitting traces to a fitting log can only increase the precision of a given model with respect to the log:

L 1 ⊆ L 2 ⊆ L(N ) =⇒ prec(N, L 1 ) ≤ prec(N, L 2 )
In the aforementioned paper, it is shown that the previous version of our antialignment-based precision metric (from [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF]) does not satisfy axiom A5 (the satisfaction of the rest of axioms are declared as unknowns in the paper). With the new version of the metric presented in this paper, we here provide proofs for these axioms, except for A3. But at the same time, we show that any precision metric can be adapted in order to satisfy A3.

Lemma 9. The metric P ϵ aa (for any fixed ϵ) satisfies A1.

Proof. Everything in our definitions is functional. 2 Lemma 10. The metric P ϵ aa satisfies A2.

Proof. Let L ⊆ L(N 1 ) ⊆ L(N 2 ). The definitions take the sup γ∈L(N ) of an expression which does not depend on the model. Since L(N 1 ) ⊆ L(N 2 ), the sup γ∈L(N2) ranges over a ⊆-larger set than the sup γ∈L(N1) . Therefore the result cannot be smaller, and we get prec(N 1 , L) ≥ prec(N 2 , L). 2

Our metrics may not satisfy the strict inequality required by A3: they satisfy only a weaker version of A3 with non-strict inequality, but, as observed in [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF],

this is then simply subsumed by A2. The authors of [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF] precisely introduced A3 after arguing that, in case of a flower model, a strict inequality should be required.

Anyway, we show in Lemma 11 that any precision metric prec can be modified so that it satisfies this requirement of strict inequality for the flower models.

Lemma 11. Let prec be any precision metric. It is possible to define a metric

prec ′ from prec such that prec ′ satisfies A3: it suffices to set the precision of the flower models to a value smaller than all the other precision values (after possibly extending the target set of the function). This guarantees A3 and preserves all the other axioms.

Proof. The new metric prec ′ satisfies A3 by construction. Moreover, if prec is deterministic (A1), then prec ′ also is. For preservation of A 2 , A 4 and A 5 , it suffices to study the different cases (separate flower model and others) to show that the equality and non-strict inequalities are preserved. 2

We consider that satisfying A3 is a very artificial issue. However, if really the transformation defined in Lemma 11 had to be implemented, it would imply that, in order to compute the precision, one would have to decide if the model N is a flower model, i.e. if L(N ) = Σ * . This is known as the universality problem. This problem is, in theory, highly intractable 7 . But again, this is very artificial: in practice it suffices to explore at a very short finite horizon to detect many many non-flower models.

Lemma 12. The metric P ϵ aa satisfies A4.

Proof. This trivially holds since both metrics are behaviorally defined. Also, we copied this axiom A4 from [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF], but observe that it is a simple corollary of

A2 as soon as L ⊆ L(N 1 ) = L(N 2 ). 2
Lemma 13. Metrics P ϵ aa (for any ϵ) satisfies A5.

Proof. With L 1 ⊆ L 2 , for every γ ∈ L(N ), we have dist(γ, L 1 ) ≥ dist(γ, L ), so the sup γ∈L(N ) cannot be smaller for L 1 than for L 2 . The rest does not depend on the log. 2

Heuristics

Due to the complexity of the problem, we present two heuristics to approximate anti-alignment based precision.

Prefix Limitation

Anti-alignment based precision requires the computation of a run of the process model that maximizes the minimal distance to the log traces. A first approximation is then to compute only a prefix of it.

Definition 8 (Prefixes of Petri net). A Prefix of size n for a

Petri net N = ⟨P, T, F, M 0 , M f , Σ, λ⟩ is a firing sequence M 0 [u 1 ⟩ . . . M n-1 [u n ⟩M n , starting
from the initial marking M 0 and of maximal length n.

For example, the prefixes of size 3 for the model of Fig. 4 are the firing sequences: (NFSA) [START_REF] Krötzsch | Complexity of universality and related problems for partially ordered NFAs[END_REF], and here the NFSA to consider would be the reachability graph of N (for N k-bounded), which is exponential in the size of N . Hence, deciding universality for k-bounded labeled Petri nets is in EXPSPACE.

{p 0 }[a⟩{p 1 , p 2 }[
Similarly, the log traces are also truncated.

For instance, for n = 3 and log L = [⟨a⟩, ⟨a, b, c, d⟩, ⟨a, f, g, h⟩, ⟨a, b, i, b, c, d⟩],

the prefixes of size 3 of the model will be compared with the truncated log traces

[⟨a⟩, ⟨a, b, c⟩, ⟨a, f, g⟩, ⟨a, b, i⟩].
Solving the problem of anti-alignment on prefixes dramatically improves efficiency, and already gives very relevant results in practice (see experimental Section 7.4).

Furthermore, the optimal prefix based anti-alignment brings a lower bound for model precision under the assumption that the model is a sound workflow net, i.e., every prefix can be completed to reach the final marking. The intuition is that the most misaligned full run that we can expect is the optimal anti-alignment found on the prefixes, completed with a sequence of perfectly misaligned actions. Following this intuition, one can deduce a lower bound on the precision for the full model and full log. This lower bound is quite tedious to compute in the general case but we illustrate it in a restricted case. We explain it in a simplified case of a model N and a log L where all log traces and full runs have the same length 2n.

Proof. Let γ ′ be an anti-alignment found for the prefixes of size n, i.e. γ ′ is a prefix of size n for N , maximizing the dist(γ ′ , L ′ ) where L ′ is the truncated log.

Let This means that there exists a log trace σ ∈ L whose prefix σ 1 of size n satisfies #edits(γ 1 , σ 1 ) ≤ #edits(γ ′ , σ ′ ). From this we deduce that

σ ′ ∈ L ′ achieving dist(γ ′ , L ′ ), such that dist(γ ′ , L ′ ) = dist(γ ′ ,
#edits(γ, σ) ≤ #edits(γ ′ , σ ′ ) + 2n
Indeed, one way to edit γ to σ is to delete all the suffix γ 2 (n deletions), then edit γ 1 to σ 1 (≤ #edits(γ ′ , σ ′ ) actions), and finally complete σ 1 to σ (n insertions).

It follows that

dist(γ, L) ≤ #edits(γ ′ , σ ′ ) + 2n 4n = 1 2
( #edits(γ ′ , σ ′ ) 2n + 1 ) = 1 2 (dist(γ ′ , σ ′ ) + 1)
and

P ϵ aa (N, L) ≥ 1 - dist(γ ′ , σ ′ ) + 1 2(1 + ϵ) 2n .
2

Notice that we did not compute this lower bound in the experiment part because the general case (where traces and runs have various lengths) is tedious to obtain.

In section 7.4, we give the prefix-based anti-alignments and the precision of those prefixes only, i.e., we reduce the problem to the set of prefixes. Definition 7 is then given by

P /n aa (N, L, n) = 1 - sup γ∈Prefixes(N,n) dist(γ, Truncate(L, n))
where Prefixes(N, n) denotes the set of prefixes of length n for the process model N , and Truncate(L, n) denotes the log L with all traces truncated to length n.

This precision on prefixes can already help one to analyze the beginning of a process model.

Maximal Number of Edits

The SAT encoding of the Levenshtein distance between two words u and

                           dist max_d (⟨u 1 , . . . , u i ⟩, ϵ) = min(d, i) dist max_d (ϵ, ⟨v 1 , . . . , v j ⟩) = min(d, j) dist max_d (⟨u 1 , . . . , u i+1 ⟩, ⟨v 1 , . . . , v j+1 ⟩) =          dist max_d (⟨u 1 , . . . , u i ⟩, ⟨v 1 , . . . , v j ⟩) if u i+1 = v j+1 min(d, 1 + min(dist max_d (⟨u 1 , . . . , u i+1 ⟩, ⟨v 1 , . . . , v j ⟩), dist max_d (⟨u 1 , . . . , u i ⟩, ⟨v 1 , . . . , v j+1 ⟩))) if u i+1 ̸ = v j+1 Lemma 14. For every u and v, dist max_d (u, v) ≤ dist(u, v). Moreover, if dist(u, v) ≤ d then dist max_d (u, v) = dist(u, v).
Proof. Both parts come naturally by strong induction on i + j. 2

Hence, the maximal number of edits heuristic gives a lower bound of the Levenshtein distance. From Definition 7 of the precision metric P ϵ aa defined by 1 -sup γ∈L(N ) dist(γ,L) (1+ϵ) γ , we conclude that the heuristic returns a upper-bound of the precision value based on L.

Tool Support and Experiments

In this section we present the tools implementing the results of this paper, and both a qualitative and quantitative evaluation on state-of-the-art benchmarks from the literature. To compare the different distances based results, we denoted Leventshein distance based anti-alignment precision by P L,ϵ aa and Hamming distance based anti-alignment precision by P H,ϵ aa .

da4py: A Python Library Supporting Anti-Alignments

Several tools implement anti-alignments. Darksider, an Ocaml command line software, has already been presented in [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF]. It creates the SAT formulas and calls the solver Minisat+ [START_REF] Eén | An extensible sat-solver[END_REF] to get the result. ProM software [START_REF] Verbeek | Prom 6: The process mining toolkit[END_REF] also has an anti-alignment plugin that computes anti-alignments in a brute force way. Recently, we have created a Python library in order to make our technique more accessible: da4py8 . Thanks to the use of the SAT library PySAT [START_REF] Ignatiev | PySAT: A Python toolkit for prototyping with SAT oracles[END_REF],

da4py allows one to run different state-of-the-art SAT solvers. Moreover, this SAT library uses an implementation of the RC2 algorithm [START_REF] Ignatiev | Rc2: a python-based maxsat solver[END_REF] in order to get

MaxSAT solutions, a variant that improves a lot the efficiency of computing anti-alignments. Finally, da4py is compatible with the library pm4py [START_REF] Berti | Process Mining for Python (PM4Py): Bridging the Gap Between Process-and Data Science[END_REF], and uses the same data objects.

Remarkably, in order to deal with large logs (as the ones shown in the quantitative evaluation part), da4py has two variants of the precision metric. The first one, used in the first experiments, computes the exact precision as it is introduced in Definition 7 with a search of best anti-alignments (Algorithm 1).

For the quantitative evaluations, Definitions 8 and P /n aa precision are used, thus alleviating the complexity by not requiring a full run but only a prefix. Accordingly, the corresponding precision measure is then a variant, that is normalized by the size of the prefix. Furthermore, for anti-alignments based on Levenshtein's distance, the simplification to add a threshold on the number of edits (presented in Section 6.3.2) is also experimented below. We then discuss the limitations of this heuristic.

Qualitative Comparison of Precision Metrics

A set of examples are taken from page 64 of [START_REF] Rozinat | Process Mining: Conformance and Extension[END_REF], and consist of the simple event log shown in Table 1 aligned with 10 different process models. The log consists of only five different traces, with various frequencies. The models in (introduced in [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF] and modified in [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF]).

The outer loop can be started at any point and then either exited one transition before completing the loop either finished the run. Table 2 compares some precision metrics for the models in Figures 5 to 14

Model

with the two possible metrics proposed in this paper: P H,ϵ aa and P L,ϵ aa , representing the precision for the Hamming and Levenshtein distance. The values of P a are defined as in [START_REF] Adriansyah | Aligning observed and modeled behavior[END_REF]. The precision values in P ET and P ET C are defined in [START_REF] Adriansyah | Measuring precision of modeled behavior[END_REF]. The value P ne denotes the precision metric from [START_REF] Vanden Broucke | Determining process model precision and generalization with weighted artificial negative events[END_REF]. Finally, the values M AP 3 and M AP 7 are defined in [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF] 9 .

Clearly, the existing precision metrics do not agree on all models and do not always agree with the intuition for precision. While all methods rank the All-parallel model just after the Flower model, our AA-based precisions position the Round-Robin model in second place instead. This is due to the fact that our method found the anti-alignment ⟨τ, τ ⟩ which is far from the log traces. In fact, this run does not exist in the first version of this model in [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF] for which the situation would not occur.

Figure 8, which consists of all the traces in separate paths, is considered to have a low precision by the P ET C metric while all the other methods describe this model as perfectly precise.

We observe that our methods give higher precisions than the rest for the flower model. This is due to the requirement of the τ transitions in order to get a full run of the model, thus alleviating the distance to the traces. A similar situation, with the same antidote, happens with the parallel model.

More generally, we note that our method, due to the parameter ϵ, gives a good balance for models with loops. The precision of those models are very mixed. We see on one side P ET , P ET C , P a and P ne are from 0.947 to 0.720 and on the other side, M AP gives a precision close to zero. However, all the methods agree on the ranking of the loops compared to the parallel model. Now, notice that model 5 and 9 are considered to be equally precise with the anti-alignment precision, which is not the case for the other metrics. Model 9 contains the behaviors of model 5 plus some permutation and skip activities between G and H, thus adding runs in the models. The fact that our method finds the same precision is a consequence of the input log. Model precision is defined in accordance to the log. In this case, there is not anti-alignment of Fig. 9 that is further to the log traces than the anti-alignment of Fig. 5 their are more anti-alignments.

Finally, we would like to point out the practical aspect of the parameter ϵ.

See precisions of

Qualitative Experiment on Prefix Heuristic

To deal with large logs, our library has a variant of precision that works on a fixed size of prefix. In this sub-section, we show and discuss the consequences of using only a prefix of anti-alignment. This can be notified for models with loops for which anti-alignments do not reach the final marking. As the size of the run is fixed, parameter ϵ, used to limit the size of the run, is not required and corresponds to ϵ = 0.

In most cases, results for distance to 10 and 15 are similar. However, we remark two types of differences. When using a small size of prefix, a model with a loop is qualified as more precise than when the size of prefix is large, thus alleviating the use of the loop. For well precise model, reducing the size of the prefix can induce a decrease of the metric. For instance, for Fig. 5 the transitions F and I are well presented in the traces and do not raise the distances, thus raising the denominator of the normalization of the precision.

The comparison between Hamming and Levenshtein distances interestingly

shows some cases where anti-alingments are equal or very similar, which validates the use of the former (whose SAT encoding is simpler) as alternative for the latter. Also notice that, for a same size of run, P H,/n aa ≤ P L,/n aa as a consequence of Lemma 1.

Finally, we invite readers to compare anti-alignment prefix based precision (Table 3) to exact anti-alignment precision (Table 2). We see that for most models, approximated precision tends to be close to optimal one.

As a conclusion of this section, we motivate users to use the prefix based method, which is more time efficient. A preliminary study of the length of full runs of the models can help one to set the size of the prefix.

Qualitative Experiment for Maximal Number of Edits Heuristic

A second heuristic, used for large logs, is to reduce the maximal number of edits max_d of the Levenshtein distance in order to considerably reduce the size of the SAT formula (Section 6.3.1).

We present in Table 4 a concrete example of the consequences of this parameter. For log of Table 1, model of Fig. 10 and a prefix of run to 10, the maximal number of edits is 17 (the maximal length in log is 7). The first row of Table 4 shows the exact anti-alignment which is at distance 11 to any log trace. When we reduce the number of edits, the tool might still find the same anti-alignment. Indeed for next row of the table, max_d to 5, the tool finds anti-alignment ⟨A, C, G, G, G, G, G, G, G, G⟩ which is indeed at least at distance 5 to any log trace. In fact, this anti-alignment is optimal and it is at distance 11, but has been returned by chance. In fact, for max_d to 5, the tool also returned the two last lines of the table where the optimal anti-alignment has not been found. For them, the correct distance to the log is not 11 which implies a difference in precision.

Quantitative Comparison

In this section, we evaluate the techniques of this paper for 12 available real-life logs of varying sizes, and which have been recently used for benchmarking process discovery methods [START_REF] Augusto | Automated discovery of process models from event logs: Review and benchmark[END_REF] presented in [START_REF] Leemans | Discovering block-structured process models from event logs-a constructive approach[END_REF], and Split Miner [START_REF] Augusto | Split miner: Discovering accurate and simple business process models from event logs[END_REF]. We compare the performance of computing our metric against the one required for the M AP metric [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF], which is known to be the most recent precision contribution, and which as in our case, satisfies the axioms described in [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF].

Given that our methods are known to incur into a high complexity (specially in terms of memory footprint),we use samples of size 10 and 100 of the initial log. We present charts of runtimes in Fig. 15 and Fig. 16. The notation P

/n=10 aa

indicates that we use the simpler prefix variant of anti-alignments (see Section 7.4). As explained in Section 6.3.1, a second parameter, max_d, helps to reduce complexity of the SAT formula by bounding the number of maximal differences: in all but the precision using the Levenshtein distance and 100 traces, we use max_d = 20 which is optimal for a prefix of size 10. For 100 traces and the Levenshtein distance, we set max_d to 10, due to the computational requirements of that last set of benchmarks.

Discussion

By relying on approximations of anti-alignments (with prefixes instead of full runs, but also by limiting the maximal number of differences), our approach tends to run in reasonable time. We compare our method against M AP 3 which is also behavioral, satisfies the axioms and is also biased towards a pessimistic positioning of precision 11 . Also, in [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF] the method has shown good performances.

From Fig. 15, we see that neither the size of the model in term of nodes, neither the log size is correlated to runtimes of M AP 3 . In opposite, and as excepted, our methods fully rely on the size of the models. The complexity of computing the Levenshtein based anti-alignment is very well highlighted by the two Figures 15 and16. Moreover the charts show that Hamming based precision, which gives an approximation of Levenshtein based precision, is often the quicker approach.

Despite that method of [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF] is quite insensitive to the log size, which admittedly is not the case of our approach, we remark a between runtime of M AP 3 for when process models are learned with the Inductive miner and the Split mine. This measure is sensitive to the state-space and the Inductive miner creates many choice structure. The peak that appears in the charts of Fig. 15 corresponds to a model that contains a choice between 30 transitions. In our metric, this structure is encoded in a SAT clause and does not influence the runtime compare to other aspect like run size. Finally, it should be stressed that several engineering efforts can be incorporated into our current tool, to drastically reduce part of its computational demands. But we see that for the first time, our tool can deal with larger instances, when it is compared to the previous implementations.

Related Work

The seminal work in [START_REF] Rozinat | Conformance checking of processes based on monitoring real behavior[END_REF] was the first one in relating observed behavior (in form of a set of traces), and a process model. In order to asses how far can the model deviate from the log, the follows and precedes relations for both model and log are computed, storing for each relation whereas it always holds or only sometimes. In case of the former, it means that there is more variability. Then, log and model follows/precedes matrices are compared, and in those matrix cells

where the model has a sometimes relation whilst the log has an always relation 11 The selection of k = 3 was advised by the authors of [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF] in a personal communication. indicate that the model allows for more behavior, i.e., a lack of precision. This technique has important drawbacks: first, it is not general since in the presence of loops in the model the characterization of the relations is not accurate [START_REF] Rozinat | Conformance checking of processes based on monitoring real behavior[END_REF].

Second, the method requires a full state-space exploration of the model in order to compute the relations, a stringent limitation for models with large or even infinite state spaces.

In order to overcome the limitations of the aforementioned technique, a different approach was proposed in [START_REF] Munoz-Gama | Conformance Checking and Diagnosis in Process Mining[END_REF]. The idea is to find escaping arcs, denoting those situations where the model starts to deviate from the log behavior, i.e., events allowed by the model not observed in the corresponding trace in the log.

The exploration of escaping arcs is restricted by the log behavior, and hence the complexity of the method is always bounded. By counting how many escaping arcs a pair (model, log) has, one can estimate the precision of a model. Although being a sound estimation for the precision metric, it may hide the problems we are considering in this paper, i.e., models containing escaping arcs that lead to a large behavior.

Less related is the work in [START_REF] Vanden Broucke | Determining process model precision and generalization with weighted artificial negative events[END_REF], where the introduction of weighted artificial negative events from a log is proposed. Given a log L, an artificial negative event is a trace σ ′ = σ • a where σ ∈ L, but σ ′ / ∈ L. Algorithms are proposed to weight the confidence of an artificial negative event, and they can be used to estimate the precision and generalization of a process model [START_REF] Vanden Broucke | Determining process model precision and generalization with weighted artificial negative events[END_REF]. Like in [START_REF] Munoz-Gama | Conformance Checking and Diagnosis in Process Mining[END_REF],

by only considering one step ahead of log/model's behavior, this technique may not catch serious precision/generalization problems.

Finally, an automata-based technique is presented in [START_REF] Leemans | Scalable process discovery and conformance checking[END_REF]. The technique projects event log and process model onto all subsets of activities of size k, and generates minimal deterministic finite automata that conjunctively represents both perspectives, so that precision can be estimated by confronting the model and the conjunction automata.

As we mentioned in Section 6.2, a recent study elaborated on the guarantees provided by the aforementioned precision metrics [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF]. The study shows that none of the precision metrics up to that moment (including an earlier version of the metrics described in this paper [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF]) was able to satisfy all the properties together. Recently, however, a metric was proposed in [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF] which satisfies the 5 axioms. Likewise to the metric in [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF], the new precision metric proposed in this paper is shown to satisfy either these properties, or a weaker version of them. The metric in [START_REF] Augusto | Abstract-and-compare: A family of scalable precision measures for automated process discovery[END_REF] relies on behavioral abstractions which are based on refinements of the directly-follows graph [START_REF] Leemans | Discovering block-structured process models from event logs-a constructive approach[END_REF]. Due to this, they can dramatically overestimate the behavior of the model, thus have a tendency to be pessimistic.

The Hidden Bias of Anti-Alignment Based Precision

To conclude this section on related work, we would like to emphasize that, as it happens with some of the aforementioned metrics of this section, antialignment based precision checking presented in this paper may provide unintuitive values for certain, extreme case, situations. Let us use a very simple example to illustrate this.

Consider a model that has two main parts, that are in conflict: the first part is the single activity a, whilst the second part is a set of n concurrent activities, all different from a. Moreover, consider a log that consists of all the traces corresponding to the interleaving of the n concurrent activities of the second part of the model. Anti-alignment ⟨a⟩ is then at normalized distance 1 to any log trace (the normalized distance counts edits in the run, and edits in the trace and normalizes it by the length of both). This induces a precision of the model to be 0. However, when removing the transition labeled by a in the process model, the precision of the new model raises from 0 to 1. Hence, on this regard, the precision metric arising from anti-alignments can be sometimes too pessimistic (if one thinks on the initial model, a slight edit has made it to change completely its precision). We will consider in the future ways for compensating this pessimistic bias, perhaps by incorporating the number of available anti-alignments in the metric.

Conclusions and Future Work

Conformance checking is becoming an important tool to certify the correct execution of processes in organizations. Quality metrics for conformance checking are crucial to evaluate quantitatively process models, and among the four dimensions to attain this task, precision is an important one. This paper proposes anti-alignments as a crucial artefact to compute an accurate metric for precision. In contrast to existing metrics, anti-alignment based precision metrics satisfy most of the properties for precision described in [START_REF] Tax | The imprecisions of precision measures in process mining[END_REF].

As future work, we plan to explore new algorithms to compute antialignments so that the complexity of the problem can be alleviated in practice.

Also, we will consider new areas for the application of anti-alignments, like process model comparison or novel ways of computing the generalization of process models (we already suggested one such approach in a recent paper [START_REF] Van Dongen | A unified approach for measuring precision and generalization based on anti-alignments[END_REF]).

We see potential for other notions of anti-alignments, for instance antialignments can be generalized between two nets: to find behavior of the former that cannot be found in the latter. The application of this generalization goes beyond the field of process mining: it can be used, for instance, to allow generating behavior that is not possible in a model, by simply aligning the net that allows for all the possible behaviors with the original net. This way, one can compute the most deviating trace of a net with respect to its own behavior, up to a given length. A second application of anti-alignments between two nets is for assessing behavioral process model similarity: this way, example behavior that is in one model and not in the other can be provided as a hint on the dissimilarity between two models. Previous techniques focus on the differences on either the causal relations, or those parts of the models that are different [START_REF] Armas-Cervantes | Behavioral comparison of process models based on canonically reduced event structures[END_REF][START_REF] Dijkman | Diagnosing differences between business process models[END_REF][START_REF] Polyvyanyy | The 4c spectrum of fundamental behavioral relations for concurrent systems[END_REF][START_REF] Weidlich | Efficient consistency measurement based on behavioral profiles of process models[END_REF][START_REF] Weidlich | Causal behavioural profiles -efficient computation, applications, and evaluation[END_REF].

  (a): The modeled process describes a realistic transaction process within a banking context. The process

Figure 1 :

 1 Figure 1: Example (adapted from [31]). (a) Initial process model, (b) Modified process model.

3 13 -

 13 anti-alignment for Levenshtein's distance and a 3 7 -anti-alignment for Hamming distance.

Lemma 4 .Figure 3 :

 43 Figure 3: A deterministic Petri net representing the log L = {⟨a⟩, ⟨a, b⟩, ⟨a, a⟩, ⟨b⟩}, for the alphabet of actions Σ = {a, b}. Place pesc is reached only by the runs which do not appear in the log.

  there exists a γ of length less or equal to |T | which is a 0-anti-alignment of N (with M f as final marking) w.r.t. the empty log. 2

1 2 ( 1 .

 121 05) 4 = 0.589.

Figure 4 :

 4 Figure 4: Example from [2]

⌊ 1 -

 1 the reachability graph of N until depth n := max γ∈L(N ),|γ|≤n dist(γ,L) (1+ϵ) |γ| ;

  σ ′ ). Consider now any full run γ of N . Let γ 1 and γ 2 be the prefix and suffix respectively of size n of γ, such that γ = γ 1 • γ 2 and |γ 1 | = |γ 2 | = n. By assumption, the distance between γ 1 and the truncated log L ′ is less or equal to dist(γ ′ , L ′ ).

  v, presented in Section 5.1, uses boolean variables δ i,j,d for i = 0, . . . , |u| , j = 0, . . . , |v| and d = 0, . . . , |u| + |v|. The maximal number of edits max_d heuristic is an approximation of the SAT formula that aims at reducing the size of the formula by removing some clauses. Optimal formula of Levenshtein distance between words u and v requires boolean variables for |u| + |v| edits (parameter d of δ i,j,d ). The maximal number of edits heuristic uses variables δ i,j,d only with d smaller than some bound max_d < |u| + |v|. This way, it reduces also the size of the formula and the computation time to solve it.The heuristic precisely encodes the computation of the following value dist max _d (u, v) defined by slightly modifying the definition of Levenshtein's distance (compare with the definition of dist(u, v) in Section 5.3):

Figure 5 :

 5 Figure 5: The ideal model. Fitting, fairly precise and properly generalizing.

Figure 6 :

 6 Figure 6: Most frequent trace. Precise, but not fitting or generalizing.

Figure 7 :

 7 Figure 7: The flower model. Fitting and generalizing, but very imprecise.

Figure 8 :

 8 Figure 8: All traces separate. Fitting, precise, but not generalizing.

Figure 9 :

 9 Figure 9: A model with G and H in parallel.

Figure 10 :Figure 11 :

 1011 Figure 10: A model with G and H in selfloops

Figure 13 :

 13 Figure 13: A model where C and F are in a loop, but need to be executed equally often to reach the final marking.

Figure 14 :

 14 Figure 14: Modified Round-robin model

Figures 5 to 8

 8 Figures 5 to 8 are four examples of models often used to show the differences between fitness, precision and generalization. The model in Figure 5 shows the "ideal" process discovery result, i.e. the model that is fitting, fairly precise and properly generalizing. The models in Figures 9 to 12 present the same set of activities with varying loop and/or parallel constructs. Two new process models that describe particularly different routing logic from the previous models are depicted in Figures 13 and 14.

  Figure 10 for ϵ = 0.05 and ϵ = 0.01. The score considerably drops from P L,0.05 aa = 0.780 to P L,0.01 aa = 0.496. For large ϵ values, traces with a thousand G's is possible in the model and our anti-alignment can penalizes it a lot by allowing long runs.

Figure 15 :

 15 Figure 15: Runtimes Comparision of M AP 3 , P H,/n=10 aa and P L,/n=10 aa for 10 traces (left) and 100 traces (right) of Models discovered using Inductive Miner for the 12 Real-life Logs. For 100 traces, P L,/n=10 aa is given for max_d = 10.

Figure 16 :

 16 Figure 16: Runtimes Comparision of M AP 3 , P H,/n=10 aa and P L,/n=10 aa for 10 traces (left) and 100 traces (right) of Models discovered using Split Miner for the 12 Real-life Logs. For 100 traces, P L,/n=10 aa is given max_d = 10.

For

  instance, for well chosen values of k, M AP k would use the same abstraction for two models N 1 and N 2 having languages L(N 1 ) = a * b 3 c * |d * b 3 e * and L(N 2 ) = (a * |d * )b 3 (c * |e * ) and assign them the same precision. Intuitively, this is not satisfactory: assume that the log contains only traces in L(N 1 ), then model N 1 should score much better than N 2 .

  • respectively. A transition t is enabled in a marking M when all places in • t are marked.When a transition t is enabled, it can fire by removing a token from each place in • t and putting a token to each place in t• . A marking M ′ is reachable from M ifthere is a sequence of firings t 1 . . . t n that transforms M into M ′ , denoted by M [t 1 . . . t n ⟩M ′ . We define the language of N as the set of full runs defined by L(N ) := {λ(t 1 ) . . . λ(t n ) | M 0 [t 1 . . . t n ⟩M f }. A Petri net is k-bounded if no reachable marking assigns more than k tokens to any place. A Petri net is bounded if there exist a k for which it is k-bounded. A Petri net is safe if it is 1-bounded. A bounded Petri net has an executable loop if it has a reachable marking M and sequences of transitions u 1

• x and x

k⟩ (i and k do not match with g and h, and γ is shorter than σ, which counts for the third mismatch). It is at larger distance from the other log traces. Therefore, it is a 3 7 -anti-alignment.

	have, dist H (γ, σ) = n+|σ|-|γ| |σ|	. We have also dist L (γ, σ) ≤ 2n+|σ|-|γ| |γ|+|σ|	because
	one way to transform γ to σ is to replace γ i by σ i (one deletion and one insertion)
	at each position i ≤ |γ| where they differ (2n edits), and then to insert the letters
	σ |γ|+1 . . . σ |σ| (|σ| -|γ| edits). It remains to see that n ≤ |γ|, which implies
	n(|σ| -|γ|) ≤ |γ|(|σ| -|γ|)
	n|σ| ≤ |γ|(n + |σ| -|γ|)
	n|σ| + (n + |σ| -|γ|)|σ| ≤ |γ|(n + |σ| -|γ|) + (n + |σ| -|γ|)|σ|
	(2n + |σ| -|γ|)|σ| ≤ (|γ| + |σ|)(n + |σ| -|γ|)
	2n + |σ| -|γ| |γ| + |σ|	≤	(n + |σ| -|γ|) |σ|
	dist L (γ, σ) ≤ dist H (γ, σ) .
				2
	Example 2. Consider the Petri net and log shown in Figure 2. With Hamming
	distance, the full run γ = ⟨a, b, c, f, i, k⟩ is at distance 3 7 from the log trace
	σ = ⟨a, b, c, f, g, h, Lemma 2. For every log L and finite model N , we have:
	1. if the model has finitely many full runs, then there exists (at least) one
	maximal anti-alignment γ of N w.r.t. L, i.e. γ that maximizes the distance
	dist(γ, L);
	2. if the model has infinitely many full runs, then there exist anti-alignments
	γ with dist(γ, L) arbitrarily close to 1. Yet, there may not exist any 1-
	anti-alignment, i.e. there is no guarantee that the limit dist(γ, L) = 1 is
	reached for any γ.

  b⟩{p 2 , p 3 }[c⟩{p 3 , p 4 } and {p 0 }[a⟩{p 1 , p 2 }[f ⟩{p 1 , p 6 }[g⟩{p 1 , p 7 } and give the runs ⟨a, b, c⟩ and ⟨a, f, g⟩.

Table 1 :

 1 An example event log.

	Trace
	⟨A, B, D, E, I⟩
	⟨A, C, D, G, H, F, I⟩
	⟨A, C, G, D, H, F, I⟩
	⟨A, C, H, D, F, I⟩
	⟨A, C, D, H, F, I⟩

Table 2 :

 2 Precision measures of artificial models

			PET	PET C	Pa	Pne	M AP 3 M AP 7	P H,.05 aa	P L,.05 aa	P L,.01 aa
	Fig. 5	Generating model	0.992	0.994	0.982 0.995	0.880	0.852	0.797	0.945	0.928
	Fig. 6	Single trace	1.000	1.000	1.000 0.893	1.000	1.000	1.000	1.000	1.000
	Fig. 7	Flower model	0.136	0.119	0.142 0.117	0.003	0.000	0.408	0.352	0.295
	Fig. 8	Separate traces	1.000	0.359	1.000 0.985	1.000	1.000	1.000	1.000	1.000
	Fig. 9	G,H in parallel	0.894	0.936	0.947 0.950	0.564	0.535	0.797	0.945	0.928
	Fig. 10	G,H as self-loops	0.884	0.889	0.947 0,874	0.185	0.006	0.570	0.780	0.496
	Fig. 11	D as self-loop	0.763	0.760	0.797 0.720	0.349	0.069	0.506	0.759	0.469
	Fig. 12	All parallel	0.273	0.170	0.336 0.158	0.006	0.000	0.468	0.468	0.420
	Fig. 13	C,F equal loop	0.820	0.589	0.839 0.600	-	-	0.751	0.881	0.845
	Fig. 14	Round-robin	0.579	0.185	0.889 0.194	0.496	0.274	0.456	0.352	0.300

  , despite

	Model		Size of	Hamming distance Anti-alignments	Edit distance Anti-alignments	P H,/n aa	P L,/n aa
			Prefix
			5	⟨A, C, G, H, D⟩	⟨A, C, G, H, D⟩	0.600	0.800
	Fig. 5	Generating model	10	⟨A, C, G, H, D, F, I⟩	⟨A, C, G, H, D, F, I⟩	0.714	0.923
			15	⟨A, C, G, H, D, F, I⟩	⟨A, C, G, H, D, F, I⟩	0.714	0.923
			5	⟨A, B, D, E, I⟩	⟨A, B, D, E, I⟩	1.000	1.000
	Fig. 6	Single	10	⟨A, B, D, E, I⟩	⟨A, B, D, E, I⟩	1.000	1.000
			15	⟨A, B, D, E, I⟩	⟨A, B, D, E, I⟩	1.000	1.000
			5	⟨τ, G, F, B, C⟩	⟨τ, G, G, E, B⟩	0.200	0.300
	Fig. 7	Flower model	10	⟨τ, C, I, C, C, C, C, F, E, I⟩	⟨τ, G, G, G, G, G, G, G, G, G⟩	0.100	0.176
			15	⟨τ, D, E, B, B, B, B, B, E, E, B, H, B, B, C⟩	⟨τ, G, G, G, G, G, G, G, G, G, G, G, G, G, G⟩	0.067	0.136
			5	⟨A, B, D, E, I⟩	⟨A, C, D, G, H, F, I⟩	1.000	1.000
	Fig. 8	Separate traces	10	⟨A, B, D, E, I⟩	⟨A, C, D, G, H, F, I⟩	1.000	1.000
			15	⟨A, B, D, E, I⟩	⟨A, C, D, G, H, F, I⟩	1.000	1.000
			5	⟨A, C, H, G, D⟩	⟨A, C, τ, D, τ ⟩	0.600	0.800
	Fig. 9	G,H in parallel	10	⟨A, C, τ, H, D, F, I⟩	⟨A, C, D, τ, τ, F, I⟩	0.714	0.923
			15	⟨A, C, G, H, D, F, I⟩	⟨A, C, τ, D, G, F, I⟩	0.714	0.929
			5	⟨A, C, D, F, I⟩	⟨A, C, G, G, G⟩	0.600	0.600
	Fig. 10	G,H as self-loops	10	⟨A, C, H, H, D, H, H, G, H, H⟩	⟨A, C, G, G, G, G, G, G, G, G⟩	0.300	0.353
			15	⟨A, C, H, H, G, D, G, H, G, H, H, G, G, G, G⟩	⟨A, C, G, G, G, G, G, G, G, G, G, G, G, G, G⟩	0.200	0.272
			5	⟨A, B, E, I⟩	⟨A, B, D, D, D⟩	0.400	0.600
	Fig. 11	D as self-loop	10	⟨A, B, D, D, D, D, D, D, E, I⟩	⟨A, C, D, D, D, D, D, D, D, D⟩	0.300	0.375
			15	⟨A, B, D, D, D, D, D, D, D, D, D, D, D, E, I⟩	⟨A, C, D, D, D, D, D, D, D, D, D, D, D, D, D⟩	0.200	0.286
			5	⟨τ, G, E, I, C⟩	⟨τ, G, C, E, B⟩	0.200	0.300
	Fig. 12	All parallel	10	⟨τ, I, F, B, G, A, E, H, C, D⟩	⟨τ, D, I, F, B, H, A, G, C, E⟩	0.100	0.313
			15	⟨τ, G, B, A, D, E, F, H, I, C, τ ⟩	⟨τ, F, H, G, C, I, E, D, B, A, τ ⟩	0.091	0.353
	Fig. 13	C,F equal loop	5 10	⟨A, τ, τ, H, D⟩ ⟨A, C, B, D, E, F, I⟩	⟨A, C, τ, D, τ ⟩ ⟨A, C, B, D, E, F, I⟩	0.400 0.714	0.600 0.833
			15	⟨A, C, B, D, E, F, I⟩	⟨A, C, B, D, E, F, I⟩	0.667	0.833
	Fig. 14	Round-robin	5 10	⟨τ, I, A, B, C⟩ ⟨τ, I, A, B, C, D, E, F, G, H⟩	⟨τ, D, E, F, G⟩ ⟨τ, E, F, G, H, I, A, B, C, D⟩	0.200 0.100	0.500 0.529
			15	⟨τ, A, B, C, D, E, F, G, H, I, A, B, C, D, E⟩	⟨τ, B, C, D, E, F, G, H, I, A, B, C, D, E, F ⟩	0.067	0.500

Table 3 :

 3 Anti-alignments prefix of size 5, 10 and 15 for all artificial models

Table 3

 3 With the use of prefix only, the method does not require full runs.

	figures, for the artificial models, prefix anti-alignment of a size of
	prefix to 5, 10 and 15 and the corresponding adapted precision P aa given in /n

Table 4 :

 4 Consequences of the Threshold on Number of Edits of Leventshein Distance for logof Table1, model of Fig.10and a prefix of run to 10. The last line is forced to reach the final marking.

	Parameter max_d,	Returned Anti-alignment	Returned Threshold	Correct	Precision
	Threshold on the		Lower Bound	Minimal
	Number of Edits		Distance to Log	Distance to Log
	17	⟨A, C, G, G, G, G, G, G, G, G⟩	11	11	0.353
	5	⟨A, C, G, G, G, G, G, G, G, G⟩	5	11	0.353
	5	⟨A, C, D, G, G, G, G, G, H, H⟩	5	7	0.588
	5	⟨A, C, D, H, G, H, G, G, G, F ⟩	5	5	0.706

Table 5 .

 5 They cover different fields, ranging from finance through to healthcare and government. The logs are publicly available at the 4DTU Data Center 10 . The demonstrations have

	been executed on a virtual machine with Debian 3.16.43-2+deb8u2 system, 12
	CPU Intel Xeon 2.67GHz and 50GB RAM.
	7.5.1. Benchmark Description
	For each of the twelve logs, we compute precision for the models automati-
	cally discovered with two state-of-the-art discovery algorithms: Inductive Miner

Table 5 :

 5 Quantitative Benchmark Descriptions of the 12 real-life Logs

Actually, we do not require that dist satisfies the usual properties of distance functions like symmetry or triangle inequality.

Since the function dist takes its values in [0, 1], we define by convention dist(γ, ∅) := 1.

Although, admittedly, ϵ is a parameter that should be decided apriori, in practice one can use a particular value to this parameter thorough several instances, without impacting significantly the insights obtained through this metric.

Actually,[START_REF] Tax | The imprecisions of precision measures in process mining[END_REF] writes "L(N 1 ) ⊂ P(Σ * )", with P for powerset, but we believe this is a mistake.

This universality problem is PSPACE-complete for non-deterministic finite state automata

https://github.com/BoltMaud/da4py, a Python version of Darksider

Notice that the metrics M AP[START_REF] Armas-Cervantes | Behavioral comparison of process models based on canonically reduced event structures[END_REF] and M AP[START_REF] Berti | Process Mining for Python (PM4Py): Bridging the Gap Between Process-and Data Science[END_REF] are not applicable for one of the benchmarks of this paper, due to the existence of unbounded constructs.

https://data.4tu.nl/repository/collection:event_logs_real

Acknowledgments.

This work has been partially supported by funds from ENS Paris-Saclay (project ProMAut of the Farman institute), the Spanish Ministry for Economy and Competitiveness (MINECO) and the European Union (FEDER funds) under grant GRAMM (TIN2017-86727-C2-1-R).