Martín Escarrá

Petar Maksimović

Alan Schmitt

HOCore in Coq

We consider a recent publication on higher-order process calculi [13] and describe how its main results have been formalized in the Coq proof assistant. We highlight several important technical issues that we have uncovered in the original publication. We believe these issues are not unique to the paper under consideration and require particular care to be avoided. Our ultimate goal is to show that it is possible to build a solid, high-confidence setting for formal reasoning on higher-order process calculi.

Introduction

Computer-aided verification has reached a point where it can be applied to state-of-the-art research domains, including compilers, programming languages, and mathematical theorems. Our goal is to contribute to this growing effort by formalizing a recent paper on process calculi.

Our main motivation is the increasing complexity of proofs in this domain. Simply put, researchers are forced to pay very close attention to a great number of details, some of which may remain implicit or go unnoticed, leaving room for imprecision or errors in the proofs. To overcome such issues, we argue a more formal treatment is needed. With our formalization, we strive for a deeper understanding of the proving process and a precise exposition of the overlooked details. Moreover, we show that it is possible to build a solid, high-confidence setting for formal reasoning on higher-order process calculi.

The paper that we are examining is [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], by Lanese et al. It introduces HOCore-a minimal higher-order process calculus, which features input-prefixed processes, output processes, and parallel composition. Its syntax is as follows:

P ::= a(x).P | a⟨P ⟩ | P ∥ P | x | 0.
HOCore is minimal, in the sense that it features only the operators strictly necessary for higherorder communication. For one, there are no continuations following output messages. More importantly, there is no restriction operator, rendering all channels global and the dynamic creation of new channels impossible. The semantics of HOCore is presented in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] in the form of a labeled transition system and it is shown that HOCore is a Turing-complete calculus. On the other hand, its observational equivalence is proven to be decidable. In fact, the main forms of strong bisimilarity considered in the literature (contextual equivalence, barbed congruence, higher-order bisimilarity, context bisimilarity, and normal bisimilarity [START_REF] Cao | More on bisimulations for higher order pi-calculus[END_REF][START_REF] Jeffrey | Contextual equivalence for higher-order pi-calculus revisited[END_REF][START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF][START_REF] Thomsen | Calculi for Higher Order Communicating Systems[END_REF]) all coincide in HOCore. Moreover, their synchronous and asynchronous versions coincide as well. It is thus possible to decide that two processes are equivalent, yet it is impossible, in the general case, to decide whether or not they terminate. In addition, the authors give in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] a sound and complete axiomatization of observational equivalence, and show that its decidability breaks in the presence of four static restrictions. Our formalization focuses on the subset of [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] addressing the decidability of observational equivalence and the coincidence of synchronous bisimilarities, but also includes an initial effort towards the formalization of the soundness and completeness of the axiomatization of HOCore.

Our theorem prover of choice for this development is Coq [START_REF]The Coq proof assistant reference manual[END_REF]. Coq allows the user to describe concepts such as mathematical theories or programming languages, state properties related to these concepts, and verify that such properties hold. Proofs produced using Coq-and interactive theorem provers in general-have a higher degree of reliability when compared to pen-and-paper proofs. They rely on a trusted core-the code on which the theorem prover is based-upon which all subsequent inferences are made. Coq supports inductive and co-inductive reasoning, offers a variety of tactics to build proofs, provides a comprehensive library, and permits extraction of a certified program from the constructive proof of its formal specification. Its typical applications include the formalization of programming languages semantics (e.g., the CompCert compiler certification project [START_REF] Leroy | Formal verification of a realistic compiler[END_REF]), the formalization of mathematics (e.g., the formal proof of the four color theorem [START_REF] Gonthier | A computer-checked proof of the four colour theorem[END_REF]), and teaching [START_REF] Pierce | Software Foundations[END_REF].

Contributions. We present a formalization of HOCore, both the calculus itself and its behavioral theory. We first introduce the syntactic and semantic concepts of HOCore: processes, freshness of variables and channels, structural congruence, and the labeled transition system (Section 2). We focus in particular on how to model bound variables using the canonical approach of Pollack et al. [START_REF] Pollack | A canonical locally named representation of binding[END_REF]. We then turn to the formalization of the various strong bisimilarities used in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]: higher-order, context, normal, open normal, and IO-bisimilarity (Section 3).

The main contributions of the paper are the formal proofs that these five bisimilarities coincide and that they are decidable. We detail the errors, inaccuracies, and implicit assumptions made in the pen-and-paper proofs, and show how to correct them (Section 4). These issues are not unique to the paper under consideration, and require particular care to be avoided.

Finally, we strive to execute the formalization so as to preserve a high degree of both visual and technical correspondence between the formulations of theorems and proofs on paper and their counterparts in Coq. We also gained valuable insights into the interplay between the flexibility of process calculi and the rigidity of a formal verification environment. We summarize what we have learned in the process in Section 6.

The formalization of the calculus, in particular our choice of binding technology, and the decidability of IO bisimilarity have been presented in [START_REF] Boulier | Formalisation de hocore en coq[END_REF]. They are recalled here so that the paper be self-contained. This paper extends that work to cover all the results of [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] regarding bisimulations.

The complete formalization, available online,1 consists of approximately 4 thousands of lines of code (kloc) of specification and 13 kloc of proofs. It was developed intermittently over a period of three years by the three authors and Simon Boulier. In the rest of the paper, we use the symbols as links to relevant definitions or lemmas in the online Coq code. Our Coq development heavily relies on the TLC library, developed by Arthur Chargueraud. 2 TLC is a general purpose Coq library that offers many tactics for proof automation.

Formalizing HOCore

Syntax

HOCore is a minimal higher-order process calculus, based on the core of well-known calculi such as CHOCS [START_REF] Thomsen | A calculus of higher order communicating systems[END_REF], Plain CHOCS [START_REF] Thomsen | Plain CHOCS: A second generation calculus for higher order processes[END_REF], and Higher-Order π-calculus [START_REF] Sangiorgi | Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms[END_REF][START_REF] Sangiorgi | Bisimulation for higher-order process calculi[END_REF][START_REF] Sangiorgi | π-calculus, internal mobility and agent-passing calculi[END_REF]. The main syntactic categories of HOCore are channels (a, b, c), variables (x, y, z), and processes (P, Q, R). Channels and variables are atomic, whereas processes are defined inductively.

P, Q ::= a⟨P ⟩ output process | a(x).P input prefixed process | x process variable | P ∥ Q parallel composition | 0 empty process
An input-prefixed process a(x).P awaits to receive a process, for example Q, on some channel a; it then replaces every occurrence of the variable x in the process P with Q (similarly to a λabstraction). An output process3 a⟨Q⟩ emits the process Q on channel a. Parallel composition enables the interaction between the senders and the receivers.

The only binding in HOCore occurs for variables in input processes. We denote the free variables of a process P by fv(P ), and the bound ones by bv(P ). In [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], processes are identified up to the renaming of bound variables. Processes that do not contain free variables are closed whereas those that do are open. If a variable x does not occur either free or bound within a process P , we say that it is fresh with respect to that process, and denote this in the Coq development by x♯P . We denote lists with the symbol : a list of variables is, for instance, denoted by x.

Structural congruence. The structural congruence relation, written ≡, is the smallest congruence relation on processes for which parallel composition is associative, commutative, and has 0 as the neutral element. In our formalization, we distinguish a single step of structural congruence from its reflexive-transitive closure, denoted by ≡ * .

P ∥ Q ≡ Q ∥ P P ∥ (Q ∥ R) ≡ (P ∥ Q) ∥ R P ∥ 0 ≡ P
Canonical representation of terms. The first step of our formalization addresses the treatment of bound variables and α-conversion. We have opted for the locally named approach, as described by Pollack et al. in [START_REF] Pollack | A canonical locally named representation of binding[END_REF]. In this approach, the set of variables is explicitly divided into two distinct subsets: free (global) variables, denoted by X, Y, Z, and bound (local) variables, denoted by x, y, z.

The main idea is to dispense with α-equivalence altogether by calculating the value of a local variable canonically at the time of its binding. For this calculation, we rely on a height function f , taking as arguments the global variable X and the term P within which it is to be bound, and computing the value of the corresponding local variable x. We then replace every occurrence of X with x in P . As an illustration, let us examine the process a(x).(x ∥ x). This process is α-equivalent to the process a(y).(y ∥ y), for any local variable y, and we would like to be able to choose a canonical representative for this entire family of processes. To that end, we start from the process X ∥ X, where the variable X is free, calculate x = f X (X ∥ X), and take this x to be our canonical representative. In the following, we write a[X] f .P for a(f X (P )).[f X (P )/X]P .

The height function needs to meet several criteria so that it does not, for one, return a local variable already used in a binding position around the global variable to be replaced, thus resulting in a capture. We use the three criteria required by the authors in [START_REF] Pollack | A canonical locally named representation of binding[END_REF] that guarantee that the height function is well-defined. ( ) ( ) ( ) Although it is not strictly necessary to choose a particular height function f that satisfies these criteria, it is important to demonstrate that such a function exists, which we do, using the following function and representing local variables as integers. ( ) ( ) In this definition, chan, lvar, and var are types representing channels, local variables, and global variables, respectively. 4 We can then define the substitution operation without any complications arising from the renaming of variables. We write [Q/X]P for the substitution of the variable X with the process Q in P , and [ Q/ X]P for the simultaneous substitution of distinct variables X with processes Q in P . In this paper, we use the same notation for both operations; the Coq version uses two distinct notations. ( ) ( )

f X (X) = 1 f X (y) = 0 f X (0) = 0 f X (Y ) = 0 if X ̸ = Y f X (a⟨P ⟩) = f X (P ) f X (P ∥ Q) = max(f X (P ), f X (Q)) f X (a(y).P ) = { f X (P ) if f X (P ) =
[P /X]X = P [P /x]x = P [P /X]Y = Y if X ̸ = Y [P /x]y = y if x ̸ = y [P /X]x = x [P /x]X = X [P /X]0 = 0 [P /x]0 = 0 [P /X](Q ∥ R) = [P /X]Q ∥ [P /X]R [P /x](Q ∥ R) = [P /x]Q ∥ [P /x]R [P /X]a⟨Q⟩ = a⟨[P /X]Q⟩ [P /x]a⟨Q⟩ = a⟨[P /x]Q⟩ [P /X]a(y).Q = a(y).[P /X]Q [P /x]a(y).Q = a(y).[P /x]Q if x ̸ = y [P /x]a(x).Q = a(x).Q
Well-formed processes. Given a height function f , we now define well-formed processes as processes in which all local variables are bound5 and are computed using f . We refer to them as wf-processes. We thus define the predicate wf that inductively characterize well-formed processes. ( ) Since all of the subsequent definitions, such as those of the labeled transition system, congruence, and bisimulations, take into consideration wf-processes only, we define a dependent type corresponding to wf-processes, by pairing processes with the proof that they are well-formed.

Record wfprocess : Set := mkWfP {proc :> process; wf_cond : wf proc}.

A wfprocess is a record with one constructor, mkWfP. This record contains two fields: a process, named proc, and a proof that proc is well-formed, named wf_cond. This type is dependent because the type of the second field (the type of a proof that proc is well-formed, i.e., wf proc) depends on the value of the first field. The notation proc :> process is a coercion: it automatically transforms a wfprocess into a process through the proc field when needed.

This approach allows us to directly reason about wf-processes without having to carry additional hypotheses in lemmas or definitions. Each time a wf-process is constructed, however, we are required to provide a proof of its well-formedness. To this end, we introduce well-formed counterparts for all of the process constructors. For instance, to express parallel composition of wf-processes, we use the following definition: Definition wfp_Par (p q : wfprocess) := mkWfP (Par p q) (WfPar p q (wf_cond p) (wf_cond q)).

where the constructor WfPar is used to build the proof of well-formedness of parallel processes:

| WfPar : forall (p q : process), wf p -> wf q -> wf (Par p q).

Our initial development did not use dependent types, but instead relied on additional wellformedness hypotheses for most lemmas. We found out that, in practice, it is much more convenient to bundle processes and well-formedness together. We can, for instance, use Coq's built-in notion of reflexive relations without having to worry about relating non well-formed processes. Also, we can define transitions and congruence directly on well-formed processes, thus streamlining the proofs by removing a significant number of lines of code otherwise required to show that processes obtained and constructed during the proofs are indeed well-formed.

Semantics

The original semantics of HOCore is expressed via a labeled transition system (LTS) applied to a calculus with α-conversion. It features the following transition types: internal transitions P τ --→ P ′ , input transitions P a(x)

---→ P ′ , where P receives on the channel a a process that is to replace a local variable x in the continuation P ′ , and output transitions P a⟨P ′′ ⟩ -----→ P ′ , where P emits the process P ′′ on channel a and evolves to P ′ . This LTS is not satisfactory because the input transition mentions the name of its bound variable. For instance, the following transition needs to be prevented to avoid name capture: x ∥ a(x).x a(x) ---→ x ∥ x. To this end, side conditions are introduced and the entire semantics is defined "up-to α-conversion" to make sure terms do not get stuck because of the choice of a bound name. To obtain a simpler formalization, we restate it using abstractions.

Abstractions and agents. An agent A is either a process or an abstraction F . ( ) An abstraction can be viewed as a λ-abstraction inside a context. ( )

A ::= P | F F ::= (x).P | F ∥ P | P ∥ F
We call these abstractions localized, because the binder (x) does not move (the usual approach to abstractions involves "lifting" the binder so that the abstraction always remains of the form (x).P ). Our approach, similar to the one in [START_REF] Tiu | Proof search specifications of bisimulation and modal logics for the picalculus[END_REF], allows us to avoid the recalculation of bound variables.

The application of an abstraction to a process, denoted by F • Q, follows the inductive definition of abstractions. ( )

((x).P ) • Q = [Q/x]P (F ∥ P ) • Q = (F • Q) ∥ P (P ∥ F ) • Q = P ∥ (F • Q)
Removal transitions. To simplify the definition of bisimulations that allow an occurrence of a free variable to be deleted from related processes, we also add transitions X X --→ 0, where a global variable dissolves into an empty process.

The Labeled Transition System. The LTS consists of the following seven rules.

Inp a(x).P

a --→ (x).P Out a⟨P ⟩ a⟨P ⟩ ----→ 0 Rem X X --→ 0 Act1 If P α --→ A, then P ∥ Q α --→ A ∥ Q. Act2 If Q α --→ A, then P ∥ Q α --→ P ∥ A. Tau1 If P a⟨P ′′ ⟩ -----→ P ′ and Q a --→ F , then P ∥ Q τ --→ P ′ ∥ (F • P ′′ ). Tau2 If P a --→ F and Q a⟨P ′′ ⟩ -----→ Q ′ , then P ∥ Q τ --→ (F • P ′′ ) ∥ Q ′ .
In these rules, α denotes an arbitrary transition label. In Coq, we represent transitions inductively, providing a constructor for each of the rules. ( ) To illustrate, we present the constructors that correspond to the rules Out and Rem. For better legibility of the code, we introduce a special notation for transitions.

Notation "{ p --l ->> ap }" := (transition p l ap) (at level 60).

Formalizing Bisimulations

We present several forms of strong bisimilarity commonly used in higher-order process calculi and describe their formalization in Coq. We first define a number of basic bisimulation clauses, as in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF].

Definition 1. A relation R on HOCore processes is:

• a variable relation, if when P R Q and P X --→ P ′ , there exists a process

Q ′ , such that Q X --→ Q ′ and P ′ R Q ′ . ( )
• an input relation, if when P R Q and P a --→ F , there exists an abstraction F ′ , such that Q a --→ F ′ , and for all global variables X fresh in P and Q, it holds that

(F • X) R (F ′ • X). ( )
• an input normal relation, if when P R Q and P a --→ F , there exists an abstraction F ′ , such that Q a --→ F ′ , and for all channels m fresh in P and

Q it holds that (F • m⟨0⟩) R (F ′ • m⟨0⟩). ( ) • a τ -relation, if when P R Q and P τ --→ P ′ , then there exists a process Q ′ , such that Q τ --→ Q ′ and P ′ R Q ′ . ( ) • an output relation, if when P R Q and P a⟨P ′′ ⟩ -----→ P ′ , then there exist processes Q ′ and Q ′′ , such that Q a⟨Q ′′ ⟩ -----→ Q ′ , P ′ R Q ′ and P ′′ R Q ′′ . ( )
• an output normal relation, if when P R Q and P a⟨P ′′ ⟩ -----→ P ′ , then there exist processes

Q ′ and Q ′′ , such that Q a⟨Q ′′ ⟩ -----→ Q ′ ,
and for all channels m fresh in P and Q and all global variables X fresh in P ′′ and Q ′′ , it holds that (m[X] f .P

′′ ∥ P ′ ) R (m[X] f .Q ′′ ∥ Q ′ ). ( )
• an output context relation, if when P R Q and P a⟨P ′′ ⟩ -----→ P ′ , then there exist processes Q ′ and Q ′′ , such that Q a⟨Q ′′ ⟩ -----→ Q ′ , and for all global variables X and processes S, such that fv(S) ⊆ {X}, it holds that ([

P ′′ /X]S ∥ P ′ ) R ([Q ′′ /X]S ∥ Q ′ ). ( )
• closed, if when P R Q and P a --→ F , then there exist a process Q ′ and an abstraction F ′ , such that Q a --→ F ′ , and for all closed processes R, it holds that

(F • R) R (F ′ • R). ( )
Definition var_relation (R : RelWfP) : Prop := forall (p q : wfprocess), (R p q) -> forall (X : var) (p' : wfprocess), {p --LabRem X ->> (AP p')} -> exists (q' : wfprocess), {q --LabRem X ->> (AP q')} /\ (R p' q').

There are two main differences between these definitions and the ones presented in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]. The first one, as mentioned before, is the use of abstractions in place of variables in input transitions. The second difference is found in the definition of a variable relation; we use the transition Rem, while the one in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] uses structural congruence:

• A symmetric relation R on HOCore processes is a variable bisimulation if when P R Q and P ≡ x ∥ P ′ , then there exists

Q ′ such that Q ≡ x ∥ Q ′ and P ′ R Q ′ .
This particular change was motivated by the fact that we have chosen to define bisimulations semantically, in terms of processes that are capable of executing transitions. In that context, preserving the definition of a variable relation from [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] and involving structural congruence would be inconsistent. Moreover, working under the hypothesis that two processes are structurally congruent is very inconvenient, as their structure may be completely different.

Using these clauses, we define the five forms of strong bisimulation: higher-order (∼ HO ), context For each of these bisimulations, we also consider a corresponding bisimilarity, i.e., the union of all corresponding bisimulations, and each of these bisimilarities is proven to be a bisimulation itself. Bisimilarity can naturally be viewed as a co-inductive notion, but its co-inductive aspects can also be expressed in a set-theoretic way, as follows:

Definition IObis (p q : wfprocess) : Prop := exists R, (IO_bisimulation R) /\ (R p q).

To compare the set-theoretic and the native Coq co-inductive versions of bisimilarity, we have also defined the latter ( ) and proven it equivalent to the set-theoretic one by using a variation of Park's principle [START_REF] Gimenez | A Tutorial on Recursive Types in Coq[END_REF]. We can use these two definitions interchangeably, depending on which one can is easier to use in a given proof. For instance, the co-inductive definition is more convenient when proving statements in which the candidate relations are very simple and follow the formulation of the statement, as there is thus no need to supply the relation during the proof process. In the cases where the candidate relations are more complicated, however, we find it more natural and closer to the paper proofs to use the set-theoretic definition.

We also define the extensions of ∼ HO , ∼ CON , and ∼ NOR to open processes by adding abstractions that bind all free variables, and denote these extensions by ∼ ⋆ HO , ∼ ⋆ CON , and ∼ ⋆ NOR , respectively. ( ) ( ) ( ) Definition 3. Let R be a bisimilarity on closed HOCore processes. The extension of R to open HOCore processes, denoted by R ⋆ , is defined by

R ⋆ = {(P, Q) : a[x 1 ] f . . . . a[x n ] f .P R a[x 1 ] f . . . . a[x n ] f .Q} where f v(P ) ∪ f v(Q) = {x 1 . . . x n }.
Relations and Bisimilarities "up-to". An important tool used in our development is the notion that two processes P and Q are in a relation R up to another relation R ′ : assuming the processes are related by R before a transition, they are related by R ′ RR ′ after the transition.

More formally, we have the following (giving only one example definition in each category, the remaining ones being formulated analogously).

Definition 4. A relation R on HOCore processes is:

• a τ -relation up to R ′ , if when P R Q and P τ --→ P ′ , there exists a process

Q ′ , such that Q τ --→ Q ′ and P ′ R ′ RR ′ Q ′ . ( )

• an IO-bisimulation up to R ′ if it is symmetric, and if it is an input relation, an output relation, and a variable relation up to R ′ . ( )

Further, we establish the following connection between bisimilarities and bisimilarities "up-to", illustrated here only for open normal bisimilarity, but holding for all five. Lemma 1. Let R ′ be an equivalence relation that is also an open normal bisimulation. Then, p ∼ o NOR q if and only if p ∼ o NOR q up to R ′ . ( ) We mainly use this technique to reason up to structural congruence. We prove that structural congruence is an equivalence relation ( ), and that it is, for instance, an open normal bisimulation ( ). By Lemma 1, we may reason up to structural congruence to show that processes are open normal bisimilar. This allows us to consider bisimulation candidates that are small, and use structural congruence after a transition to get back in the candidate. Alternatively, one could close the candidate relation under structural congruence, but this would yield much larger candidates, for which related processes would have completely different structures and formal proofs would become much more complicated.

Existential vs. Universal Quantification of freshness. The definitions of input, input normal, and output normal relations all feature universal quantification on some channel and/or variable that have to be fresh. The formalization in Coq has revealed that this condition leads to major problems in a number of proofs, including the one for transitivity of open normal bisimilarity, the proof of Lemma 1, and the proof of Lemma 7; these problems were not explicitly addressed in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]. Transitivity provides the simplest example: assume P ∼ Q and Q ∼ R, where ∼ is a bisimulation relying on a property on fresh variables. To show P ∼ R, one has to show the property holds for every variable fresh in P and R. However, we do not know whether every such variable is fresh in Q, so we cannot infer the property from P ∼ Q nor Q ∼ R. Using an existential approach would not work either: the variable witness for P ∼ Q may differ from the one for Q ∼ R. The solution is to show the universal and existential versions of the bisimulations coincide, use the existential version for P ∼ R (we need to find a variable), and rely on the universal version for the hypotheses (allowing to freely choose a variable to be fresh for P , Q, and R). Intuitively, the identity of fresh variables does not matter: if one works, any will. We have shown this is the case for the IO, normal, and open normal bisimilarity ( ) ( ) ( ). To achieve this, we have shown that related processes have the same multiset of free variables and the same multiset of channels used for input or output.

Again, as for bisimulations "up-to", we could consider closing the candidate relation under variable freshness, but this would again complicate the formal proof substantially. However, and much more importantly, existentially-quantified IO-bisimulation cannot be avoided in the formalization of the decidability procedure.

Formalizing Decidability & Coincidence of Bisimilarities

We now present the formalization of the bisimilarity decidability and bisimilarity coincidence theorems of HOCore. We emphasize that, in order to arrive at those results, it was necessary to prove a number of auxiliary lemmas about structural congruence, substitution, multiple substitution, and transitions that were implicitly considered true in the original paper. Some of these lemmas were purely mechanical, while others required a substantial effort. One of the latter is Lemma 2, presented below and used later in the proof of Lemma 8. Although its correctness is intuitively clear-when substituting several variables with empty messages, the substitution order does not matter-it required a relatively complex proof by complete induction on the length of X.

Lemma 2. Let P be a wf-process, X and X ′ lists of variables, and M and M ′ lists of messages with arguments 0. Further, let X and X ′ have no duplicate elements, and let the lengths of X and M , as well as the lengths of X ′ and M ′ be equal. Let ( X, M ) and ( X ′ , M ′ ), respectively, denote the list of ordered pairs obtained by joining X and M , and X ′ and M ′ . Finally, let us assume that for all X ∈ fv(P ) and arbitrary m, it holds that (X, m⟨0⟩) ∈ ( X, M ) if and only if (X, m⟨0⟩) ∈ ( X ′ , M ′ ). Then, it also holds that [ M / X]P = [ M ′ / X ′ ]P . ( ) IO-bisimilarity. The first bisimilarity we studied is IO-bisimilarity. Its simplicity lets us show directly that not only it is a congruence, but that it is also decidable. Lemma 3. The following properties concerning ∼ o IO hold: To show decidability, we specify a brute force algorithm that tests every possible transition for the two processes, up to a given depth. ( ) As IO-bisimilarity testing always results in smaller processes (there is no τ clause in this bisimilarity), we can show that this algorithm decides IO-bisimilarity, if the depth considered is large enough ( ) ( ). This allows us to conclude: Theorem IObis_constructive_decidable : forall p q, {p ≈ q} + {~(p ≈ q)}.

1. ∼ o IO is a congruence: if P ∼ o IO P ′ , then: (1) a[X] f .P ∼ o IO a[X] f .P ′ ; ( ) (2) for all Q, P ∥ Q ∼ o IO P ′ ∥ Q; ( )
We should note here that the brute force algorithm would not be applicable to the definition of IO-bisimilarity as stated in Definition 2, because we would need to consider universal quantification on the fresh variable X in the case of an input transition. However, since we have proven the equivalence of universally-and existentially-quantified IO-bisimilarities, it is sufficient to check bisimilarity for only one arbitrary fresh X. More importantly, we strongly emphasize that, although the TLC library is based on classical logic, the decidability procedure that we have formalized is fully constructive.

General Properties of Bisimilarities. Next, we turn to properties of the other bisimilarities that are required to show they all coincide. The last claim is proven using induction on the combined measure m(P ) that takes into account both the structural size of P (s(P )) and the number of output actions in it (o(P )). This is necessary since an additional input process is produced in the output normal bisimulation clause of ∼ o NOR . Thus, in the induction step, the size of the process cannot be guaranteed to decrease. However, the number of output actions becomes smaller, and the combined measure suffices.

Coincidence of Bisimilarities in HOCore. We finally present the formalization of the coincidence of bisimilarities. First, we address one of the two most technically challenging lemmas of the development (Lemma 4.15 of [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]) ( ) ( ).

Lemma 7. If (m[X] f .P ′ ) ∥ P ∼ o NOR (m[X] f .Q ′ ) ∥ Q for some fresh m, then P ∼ o NOR Q and P ′ ∼ o NOR Q ′ .
Proof. In order to show the first part of the lemma, we show that the relation

S= ∞ ∪ j=1    (P, Q) :   ∏ k∈1..j m k [X k ] f .P k   ∥ P ∼ o NOR   ∏ k∈1..j m k [X k ] f .Q k   ∥ Q    is an existential ∼ o NOR -bisimulation, where {P i } ∞ 1 , {Q i } ∞ 1 are arbitrary processes, {m i } ∞ 1 are channels fresh with respect to P , Q, {P i } ∞
1 , and {Q i } ∞ 1 , and each variable X i is fresh with respect to P i and Q i . The proof proceeds as in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], by examining possible transitions of P and showing that these transitions are matched by Q. To this end, we study processes of the form ( ∏ k∈1..j m k [X k ] f .P k ) ∥ P ( ), proving several lemmas about their properties in relation to transitions and structural congruence. The original proof silently relies on the use of existentially-quantified open normal bisimilarity and up-to structural congruence proof techniques for this bisimilarity (up-to techniques are proven, but only for IO-bisimilarity). These assumed results were not trivial to formally establish.

For the second part of the lemma, we have determined that it is not necessary to formalize the informal, highly intuitive procedure to consume open-normal-bisimilar processes, as presented in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]. Instead, it is sufficient to proceed by induction on m(P ) and make use of the already proven first part, reducing the formal proof to a technical exercise. Moreover, we believe that the formalization of such a consumption procedure would have been very difficult and would require a substantial amount of time and effort. This illustrates the insights one can gain through formal proving when it comes to proof understanding and simplification.

We are now ready to state and prove the coincidence of bisimilarities.

Theorem 1. The five strong bisimilarities in HOCore coincide.

Proof. We prove the following implications, the direct corollary of which is our goal:

(1) ∼ o IO implies ∼ ⋆ HO ( ); (2) ∼ ⋆ HO implies ∼ ⋆ CON ( ); (3) ∼ ⋆ CON implies ∼ ⋆ NOR ( ); (4) ∼ ⋆ NOR implies ∼ o NOR ( ); (5) ∼ o NOR implies ∼ o IO ( ).
The only major auxiliary claim that needs to be proven here is that an open normal bisimulation also satisfies the output relation clause; this is an immediate consequence of Lemma 7.

In addition, we have proven that IO-bisimilarity is correct with respect to barbed congruence ( ), which, given Theorem 1, means that the forms of bisimilarity that we are considering are all correct w.r.t. barbed congruence. The other direction (completeness) involves properties of asynchronous bisimulations that remain to be formalized.

Next, we focus on the lemma that corresponds to the right-to-left direction of Lemma 4.14 of [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], stating that higher order bisimilarity implies IO-bisimilarity. Interestingly, this claim was included in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] although it is not necessary to prove the coincidence of bisimilarities. Its proof was the most challenging to formalize, and this formalization has led us to several important insights.

Lemma 8. ∼ ⋆ HO implies ∼ o IO . Discussion. It is sufficient to prove that the relation R = {(P, Q) | [ M / X]P ∼ ⋆ HO [ M / X]
Q} is an IO-bisimulation, where X and M are, respectively, lists of variables and messages carrying 0 on fresh channels. We show R is an input ( ), an output ( ), and a variable relation ( ). The proofs of all three cases in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF] share the same structure that relies on the application of both directions of Lemma 4.

First, the unguarded variables7 are substituted with processes of the form m⟨0⟩. Then, the remaining free variables are substituted with arbitrary closed processes R, using Lemma 4 left-toright to show that the result is still in R. Next, the processes do a transition, and it is proposed to apply Lemma 4 right-to-left to conclude. This last step is not justified, as we now explain. The main idea is to show that the bisimulation diagrams are closed under multiple substitution, i.e., that for all processes P and Q, all global variables X, and all closed processes R, given

[ R/ X]P ∼ HO [ R/ X]Q and [ R/ X]P α --→ [ R/ X]P ′ , there exists a Q ′ such that [ R/ X]Q α --→ [ R/ X]Q ′ and [ R/ X]P ′ ∼ HO [ R/ X]Q ′ .
Then, the idea is to apply Lemma 4 right-to-left to obtain P ′ ∼ ⋆ HO Q ′ . This is accomplished by first showing that there exists an S, such that [ R/ X]Q α --→ S and [ R/ X]P ′ ∼ HO S, and then showing that there exists a Q ′ , such that S = [ R/ X]Q ′ . The crucial mistake is that Q ′ here depends on R, unless proven otherwise. Thus, the requirement for a unique Q ′ with a universal quantification on R of Lemma 4 right-to-left is not satisfied, and the lemma cannot be applied.

Our initial attempt at this proof followed this approach, which failed when Coq refused to let us generalize R since Q ′ depended on it. We thus proceeded differently, by first substituting every free variable with processes of the form m⟨0⟩, using Lemma 4 left-to-right to show that we remain in the relation. We then applied Lemma 2 and another auxiliary lemma ( ) to finish the proof.

To conclude this summary, we note another error that we have discovered in Section 6.1 of [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], that concerns the axiomatization of HOCore. Namely, in the proof of the cancellation lemma:

For all processes P, Q, R, if P ∥ R ∼ o IO Q ∥ R, then also P ∼ o IO Q.
the authors attempt to re-use the proof from [START_REF] Milner | Unique decomposition of processes[END_REF], that proceeds by induction on the sum of sizes of P , Q, and R. However, this is not possible, as that proof was designed for a calculus with operators structurally different than the ones used in HOCore. Instead, we need to use the candidate relation R, parameterized by a natural number n, such that P R Q at level n if and only if there exists a process R such that s(P ) + s(Q) + s(R) ≤ n and P ∥ R ∼ o IO Q ∥ R, and prove that this candidate relation is an IO-bisimulation.

Related Work

We first discuss alternative approaches to the handling of binding and α-conversion, starting from Nominal Isabelle [START_REF] Urban | Nominal techniques in isabelle/hol[END_REF][START_REF] Huffman | A new foundation for nominal isabelle[END_REF][START_REF] Urban | General bindings and alpha-equivalence in nominal isabelle[END_REF]. This extension of the Isabelle proof assistant features nominal datatypes that represent α-equivalence classes. It has been used successfully in a number of research efforts concerning formalization of various calculi that feature binders [START_REF] Parrow | Higher-order psi-calculi[END_REF][START_REF] Bengtson | Psi-calculi in isabelle[END_REF][START_REF] Urban | Mechanizing the metatheory of LF[END_REF], and taking advantage of it would probably reduce the size of our development. However, since one of our main results is the formalization of the decidability procedure for IO-bisimulation, and since stating decidability in Isabelle is not a trivial task, we have ultimately opted to use Coq.

The locally nameless approach [START_REF] Aydemir | Engineering formal metatheory[END_REF][START_REF] Charguéraud | The locally nameless representation[END_REF] is the one most similar to the one we are using. There, variables are also split into two categories-local and global-but local variables are calculated by using de Bruijn indices instead of a height function. We find this approach to be both equally viable and equally demanding-freshness and well-formedness would both have to be defined, albeit differently, the proofs would retain their level of complexity, and the amount of code required would not be reduced substantially.

In the Higher-Order-Abstract-Syntax (HOAS), binders of the meta-language are used to encode the binding structure of the object language. In some settings, HOAS can streamline the development and provide an elegant solution for dealing with α-conversion, but in the case of process calculi it also brings certain drawbacks. As stated in [START_REF] Honsell | pi-calculus in (co)inductive-type theory[END_REF], there are difficulties with HOAS in dealing with metatheoretic issues concerning names, especially when it comes to the opening of processes, to the extent that certain meta-theoretic properties that involve substitution and freshness of names inside proofs and processes cannot be proven inside the framework and must be postulated instead.

In light of everything previously stated in this section and since HOCore does not have a restriction operator, we have decided to use the canonical locally named approach [START_REF] Pollack | A canonical locally named representation of binding[END_REF] for variables bound by the input operator. We have not yet considered more general approaches for name binding, such as [START_REF] Pouillard | A fresh look at programming with names and binders[END_REF]. In fact, our development may easily be adapted to other models for binders, as long as binders remain canonical (α-convertibility is equality).

We now turn to works related to the formalization of process calculi and their properties. To the best of the authors' knowledge, there have been no formalizations of the higher-order π-calculus so far. There are, however, many formalizations of the π-calculus in various proof assistants, including Coq, such as [START_REF] Hirschkoff | A full formalisation of pi-calculus theory in the calculus of constructions[END_REF] (where the author uses de Bruijn indices) and [START_REF] Honsell | pi-calculus in (co)inductive-type theory[END_REF] (where the authors use HOAS). The work closest to ours is the recently published formalization in Isabelle of higher-order Psi-calculi [START_REF] Parrow | Higher-order psi-calculi[END_REF], an extension to the higher-order setting of [START_REF] Bengtson | Psi-calculi in isabelle[END_REF]. We have developed our own formalization because we wanted to stay as close to the paper proofs as possible, in particular when it came to the handling of higher-order and the definitions of the many bisimulations involved. Although we feel that translating HOCore and its bisimulations into a higher-order psi-calculus constitutes a very interesting problem, it is beyond the scope of this paper.

A preliminary version of this paper has appeared in [START_REF] Boulier | Formalisation de hocore en coq[END_REF]. It contained the initial results of the effort, which included the locally nameless technique for dealing with binders, the correction of the semantics, and the results on decidability. With respect to that version, the contributions of this paper are the new and more solid treatment of well-formed processes as records, the proof of the coincidence of bisimilarities, and the discovery and correction of several errors and imprecisions made in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF].

Finally, we have not fully used the automation that Coq offers. In particular, we could benefit from integrating recent libraries that manipulate binary relations algebraically [START_REF] Braibant | Deciding kleene algebras in coq[END_REF].

Lessons Learned and Conclusions

The formalization of HOCore in Coq has given us a deeper understanding of both the calculus itself and the level of precision required for proving properties of bisimulations. We have identified one major flaw in the proofs, namely the improper generalization of an hypothesis in the proof of Lemma 8. This flaw was particularly insidious, as it was due to a lapse in the tracking of the context inside which a property is derived. Such tracking is precisely where proof assistants excel. We have also identified two missing results required by some lemmas. The first concerns existentially-quantified bisimulations: certain properties of bisimulations cannot be proven if the variables or channels featured in freshness conditions of bisimulation clauses are universally quantified. We solved this by introducing bisimulations with existential quantification and showing they are equivalent to the universally quantified ones. We have also discovered that existentially-quantified bisimulations are necessary for the formulation of the decidability procedure. The second missing result is about the transitivity of bisimulations, required to prove that open normal and existential open normal bisimilarities coincide. Proving transitivity is not a trivial claim that required the use of reasoning on bisimulations up to structural congruence, which was also missing for some bisimilarities.

Nevertheless, we were able to prove the decidability of IO-bisimilarity, the main coincidence theorem, and their supporting lemmas. We found that some of the lemmas of the paper are actually not needed, such as Lemma 8. Additionally, we significantly simplified some proofs. For instance, the proof of Lemma 7 (Lemma 4.15 in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]) does not require the consumption procedure described in [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]; induction on the combined measure m(P ) is sufficient and more elegant.

As a side effect of our precise treatment of bound variables, we have detected and corrected an error in the original semantics of HOCore, making it more streamlined in the process. Labels for input transitions no longer mention the variable to be substituted, but instead evolve to an abstraction. Since we do not need to lift the binders, we have decided to make these abstractions local. We have also introduced the operation that deletes a variable as a transition in the LTS, removing a special case in the definition of the bisimulations and avoiding the use of structural congruence.

In fact, many choices made during the formalization were guided by the intent to avoid structural congruence. Although it is very convenient to be able to freely change the structure of a process, doing so interferes with local reasoning. There were cases, however, where we could not avoid it, in particular when proving properties of normal bisimulation. In those cases, we have used "up-to structural congruence" techniques to keep the bisimulation candidates small enough. We have discovered that the discord between the rigid syntax of a formal process and the intuition that it models a "soup" where processes can freely move around and interact with each other made the formalizations of some of the proofs more difficult than anticipated.

We also proved that the co-inductive and set-theoretic definitions of IO-bisimilarity are equivalent, and used them depending on the complexity of the candidate relation at hand.

As for further work, our immediate aim is to formalize the results presented in Section 6 of [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF], pertaining to the soundness and completeness of the axiomatization of HOCore. At this point, we have the proof of the existence and uniqueness of prime decomposition of processes ( ), as well as an initial description of processes in normal form ( ) and a proof that normalization terminates ( ). Afterwards, we plan to extend the formalization of HOCore with name restriction, before tackling more complex features such as passivation.

In conclusion, we hope that the experience described in this paper will serve as a motivational step towards a more systematic use of proof assistants in the domain of process calculi.

|

  TrOut : forall a p, (transition (Send a p) (LabOut a p) (AP Nil)) | TrRem : forall X, (transition (Gvar X) (LabRem X) (AP Nil))

  (∼ CON ), normal (∼ NOR ), IO (∼ o IO ), and open normal (∼ o NOR ) bisimulations. Due to space restrictions, we present here only the ones that differ from those in [13]. Definition 2. A relation R on HOCore processes is: • an IO-bisimulation (∼ o IO ) if it is symmetric, an input relation, an output relation, and a variable relation; ( ) • an open normal bisimulation (∼ o NOR ) if it is symmetric, a τ -relation, an input relation, an output normal relation, and a variable relation. ( ) Definition IO_bisimulation (R : RelWfP) : Prop := (Symmetric R) /\ (in_relation R) /\ (out_relation R) /\ (var_relation R).

  and (3) a⟨P ⟩ ∼ o IO a⟨P ′ ⟩. ( ) 2. IO-bisimilarity and existential IO-bisimilarity coincide. ( ) 3. IO-bisimilarity and IO-bisimilarity up to ≡ * coincide. ( ) 4. ∼ o IO is a τ -bisimulation. ( ) 5. ∼ o IO is decidable. ( ) ( )

  Lemma 4. P ∼ ⋆ HO Q if and only if for all closed R, [ R/ X]P ∼ HO [ R/ X]Q, where X = fv(P ) ∪ fv(Q). (Lemma 4.13 of [13]). ( ) While the proof of this claim takes only several lines on paper, its Coq version amounts to more than three hundred lines of code, requiring a number of auxiliary lemmas that appear evident in a pen-and-paper context. These lemmas mostly deal with with permutations of elements inside a list and the treatment of channels in the "opening" of ∼ HO . Lemma 5. The following properties concerning ∼ NOR and ∼ ⋆ NOR hold: 1. Normal bisimilarity and existential normal bisimilarity coincide. ( ) 2. P ∼ ⋆ NOR Q if and only if there exists a list M of messages on distinct, fresh channels, each carrying 0 and such that [ M / X]P ∼ NOR [ M / X]Q, where X = fv(P ) ∪ fv(Q). 6 ( ) Lemma 6. The following properties concerning ∼ o NOR hold: 1. Open normal and existential open normal bisimilarity coincide. ( ) 2. Open normal bisimilarity and open normal bisimilarity up to ≡ * coincide. ( ) 3. If P ∼ o NOR Q, then P and Q have the same multiset of variables and channels. ( ) ( )

http://www.irisa.fr/celtique/aschmitt/research/hocore/

http://www.chargueraud.org/softs/tlc/

We will also refer to an output process as an output message or, more simply, a message.

To be precise, chan and lvar are aliases for Coq's type for natural numbers (nat), while var is the type for global variables provided by the TLC library.

Here we have a slight overloading of terminology when it comes to free and bound variables-while local variables are intended to model the bound variables of the object language, they can still appear free with respect to our adjusted syntax. For example, x is free in the process Lvar x, and we do not consider this process to be well-formed.

The proof of this claim, unlike its ∼HO counterpart, requires the use of the equivalence between normal and existential normal bisimilarity.

Variables that appear in an execution context, i.e., variables that are not "guarded" by an input.


Paul Brunet

Damien Pous

Decidability of Identity-free Relational Kleene Lattices

Families of binary relations are important interpretations of regular expressions, and the equivalence of two regular expressions with respect to their relational interpretations is decidable: the problem reduces to the equality of the denoted regular languages.

Putting together a few results from the literature, we first make explicit a generalisation of this reduction, for regular expressions extended with converse and intersection: instead of considering sets of words (i.e., formal languages), one has to consider sets of directed and labelled graphs.

We then focus on identity-free regular expressions with intersection-a setting where the above graphs are acyclic-and we show that the corresponding equational theory is decidable. We achieve this by defining an automaton model, based on Petri Nets, to recognise these sets of acyclic graphs, and by providing an algorithm to compare such automata.

Introduction

Binary relations appear everywhere in mathematics and computer science, together with the operations of union (∪), intersection (∩), composition (○), converse (. ∨ ), reflexive-transitive closure (. ⋆ ), and the constants identity (Id) and empty relation (∅). As such, an algorithm for deciding the equivalence of expressions built with these operators with respect to their relational interpretations is a very desirable goal. However such an algorithm has yet to be found.

Regular expressions [START_REF] Conway | Regular algebra and finite machines[END_REF], where only the operators ∪, ○, . ⋆ , Id, and ∅ are allowed, are the most famous example of a decidable fragment [START_REF] Kleene | Representation of Events in Nerve Nets and Finite Automata[END_REF]. In this setting, it is now well-known that the equivalence of two expressions in all relational interpretations is equivalent to the equality of the regular languages denoted by these expressions in the usual sense (the letter x is interpreted as {x}). Several equational or semi-equational theories are known to be complete for this fragment [START_REF] Kozen | On Kleene Algebras and closed semirings[END_REF][START_REF] Kozen | A completeness theorem for Kleene Algebras and the algebra of regular events[END_REF][START_REF] Krob | A Complete System of B-Rational Identities[END_REF].

The converse operation can also be added to regular expressions, and the resulting theory remains decidable (see [START_REF] Bloom | Notes on equational theories of relations[END_REF][START_REF] Ésik | Equational properties of Kleene algebras of relations with conversion[END_REF] or [START_REF] Brunet | Kleene algebra with converse[END_REF]). In this case, decidability is obtained by 1) reducing the problem of equivalence of two expressions to the equality of some regular sets of words over an extended alphabet, and 2) defining automata constructions to recognise these sets.

Freyd and Scedrov sketched an algorithm for representable allegories [8, page 208], that is, expressions with composition, intersection, converse, and identity, but without union or reflexivetransitive closure. Similar constructions were given independently by Andréka and Bredikhin [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF], in a more comprehensive way. The key idea is the following: if we restrict ourselves to the above syntax (variables, composition, intersection, converse, identity), we get what is called ground terms. Such a term u can be represented as labelled directed graphs G(u) with two distinguished vertices called the input and the output. A variable a corresponds to a graph with one edge labelled by a linking the input to the output. The identity is represented by the graph with a single vertex and no edges, The composition of two graphs with disjoints sets of vertices can be performed by identifying the output of the first graph and the input of the second one. The operation corresponding to the intersection consists in merging the inputs of the two graphs, as well as their outputs. And finally, converse is obtained by swapping the inputs and the outputs. Some examples are given in Figure 1.

These graphs can be endowed with a preorder relation G ◂ F , defined by the existence of a graph homomorphism from F to G (preserving inputs and outputs). For instance the graph corresponding to (a ⋅ (b ∧ c)) ∧ d is smaller than the graph of (a ⋅ b) ∧ (a ⋅ c), thanks to the homomorphism depicted in Figure 2 using dotted arrows. Notice that this preorder has nothing to do with the respective sizes of the graphs: a graph may very well be smaller (in the sense of ◂) than another while having more vertices (and vice versa). The key result from Freyd and Scedrov [8, page 208], or Andréka and Bredikhin [2, Theorem 1], is that for any two ground terms u, v, u is contained in v under any relational interpretation if and only if

G(u) ◂ G(v).
This is for ground terms; to handle the whole syntax, we need to add union and reflexive-transitive closure. It suffices for that to consider sets of graphs: to each expression e, one can associate a set of graphs G(e). Writing X ◂ for the downward closure of a set of graphs X by the relation ◂, we obtain the following generalisation of the above result: for any two expressions e and f , e is contained in f under any relational interpretation if and only if G(e) ⊆ G(f ) ◂ . (Theorem 6 in the sequel-this result is almost there in the work by Andréka et al. [START_REF] Andréka | The equational theory of Kleene lattices[END_REF], but this explicit formulation is new, to the best of our knowledge.)

This result encompasses the case of plain regular expressions, whose graphs are just words and for which the preorder ◂ reduces to isomorphism, but also the case of regular expressions with converse, whose graphs are words over a duplicated alphabet and for which the preorder ◂ can be reformulated in terms of the rewriting system proposed by Ésik et al. [START_REF] Bloom | Notes on equational theories of relations[END_REF][START_REF] Ésik | Equational properties of Kleene algebras of relations with conversion[END_REF].

Our main contribution is then to exploit this characterisation to obtain decidability for identityfree regular expressions with intersection, whose equational theory has been studied by Andréka et al. [START_REF] Andréka | The equational theory of Kleene lattices[END_REF]. The reason why we need to exclude identity and converse is that in presence of intersection, they yield cyclic graphs, and we do not know how to handle such graphs. We hope to get rid of this assumption in future work.

The key concept which we introduce is a new kind of finite automaton, allowing us to recognise sets of graphs that are downward-closed w.r.t. the graph embedding relation ◂. To give some intuition about this automaton model, let us look at the example from Figure 2, and try to build sequentially a morphism

h from F = G((a ⋅ b) ∧ (a ⋅ c)) to G = G((a ⋅ (b ∧ c)) ∧ d).
• We start by placing a token α ○ on A. We know that for h to be a morphism, it has to preserve the input of the graph, so we map A to position 0 in G. • There are two outgoing edges from A, both labelled by a. We split token α ○ into β ○ and γ ○, and move β ○ to position B and γ ○ to position C. We then map the positions of both tokens to position 1 in G, which is consistent with h being a morphism, thanks to the arc (0, a, 1).

• Now we try to move β ○. B has one outgoing edge, labelled by b. We may move β ○ to D, and using the arc (1, b, 2) in G we map D to position 2.

• Then we can look at γ ○. We have to move it to position D, and thanks to the arc (1, c, 2) we can confirm the map of D to 2, and merge back β ○ and γ ○.

At the end, we have only one token, placed on the output of F , and during the procedure we have mapped all positions in F to positions in G, while preserving all labelled edges. This kind of procedure is reminiscent of Petri nets [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF][START_REF] Petri | Fundamentals of a theory of asynchronous information flow[END_REF][START_REF] Petri | Kommunikation mit Automaten[END_REF]: at each step we relate tokens to positions in G, and fire transitions according to the edges of G. This is the basic idea behind the notion of Petri automata which we introduce in Section 2. For instance the Petri automaton we will construct for the term (a ⋅ b) ∧ (a ⋅ c) is depicted in Figure 3, and the procedure sketched above can then be formally described as a reading of the graph G in this automaton.

Given an expression e, we show in Section 3 how to build a Petri automaton that recognises exactly the graphs in G(e) ◂ . We then show in Section 4 how to compare Petri automata. Several difficulties arise, that do not appear with classical word automata. Our solution nevertheless uses a standard coinductive approach, where we define an appropriate notion of simulation.

Expressions and languages

In this section we consider the full signature ⟨∧, ∨, ⋅, ⋅ ⋆ , ⋅ ∨ , 0, 1⟩ of Kleene lattices with conversion. We fix a set X of variables, and we denote by Reg ∨∧ X the set of expressions build from variables in X with these connectives. These expressions are meant to be interpreted in relational models: ⋅ corresponds to the composition of relations; ∨ to the union; ∧ to the intersection; R * to the reflexive transitive closure of a relation R; and R ∨ to the converse of R. The constants 0 and 1 are respectively interpreted as the empty relation and the identity relation. For any set S, we write P (S) ∶= {P P ⊆ S } for the set of subsets of S. Let A → B be the functions from A to B and A ⇢ B the partial maps from A to B. dom (f ) denotes the domain of a partial map f . If σ ∶ X → P (S × S) is an interpretation of the alphabet X into some space of relations, we write σ for the unique homomorphism extending σ from Reg ∨∧ X to P (S × S). We say that two expressions e and f are relationally equivalent, written Rel ⊧ e = f , if for any relational interpretation σ we have σ(e) = σ(f ). Similarly, we write Rel ⊧ e ⩽ f if σ(e) ⊆ σ(f ) holds for any σ.

The ground terms are defined by the following sub-syntax:

u, v, w ∈ W X ∶∶= x ∈ X w ⋅ w w ∧ w w ∨ 1 .
We let G range over 2-pointed labelled directed graphs, which we simply call graphs in the sequel.

Those are tuples ⟨V, E, ι, o⟩ with V a finite set of vertices, E ⊆ V × X × V a set of edges labelled with X, and ι, o ∈ V the two distinguished vertices, respectively called input and output. To each ground term w, we associate such a graph G(w). The graph for 1 has only one vertex, both input and output. The graph of a has one edge labelled by a linking its input to its output. The composition of two graphs with disjoint sets of vertices can be performed by identifying the output of the first graph and the input of the second one. The intersection on graphs consists in merging their inputs and merging their outputs. The converse consists simply in exchanging the input and the output of a graph. See Figure 4 for a graphical description of this construction. Those graphs were introduced independently by Freyd and Scedrov [8, page 208], and Andréka and Bredikhin [START_REF] Andréka | The equational theory of union-free algebras of relations[END_REF].

G(1) ∶= G(a) ∶= a G(w ∨ ) ∶= G(w) G(u ⋅ v) ∶= G(u) G(v) G(u ∧ v) ∶= G(u) G(v)
Another useful notion is the notion of morphism between graphs:

Definition 1 (Graph morphism, preorder on ground terms)

A graph morphism from ⟨V 1 , E 1 , ι 1 , o 1 ⟩ to ⟨V 2 , E 2 , ι 2 , o 2 ⟩ is a map h ∶ V 1 → V 2 such that h(ι 1 ) = ι 2 , h(o 1 ) = o 2 , and (p, x, q) ∈ E 1 entails (h(p), x, h(q)) ∈ E 2 .
We denote by ◂ the relation on graphs defined by G ◂ G ′ if there exists a graph morphism from G ′ to G. This relation gives rise to a preorder on ground terms, written ⊲ and defined by u

⊲ v if G(u) ◂ G(v). *
Given a set S of graphs, we write S ◂ for its downward closure w.r.t. ◂:

S ◂ ∶= {G G ◂ G ′ , G ′ ∈ S }.
Similarly, we write S ⊲ for the downward closure of a set of ground terms w.r.t. ⊲.

As explained in the introduction, the above preorder on ground terms precisely characterises inclusion under arbitrary relational interpretations: [8, page 208]). For all ground terms u, v ∈ W X , we have

Theorem 2 ( [2, Theorem 1], or
Rel ⊧ u ⩽ v ⇔ u ⊲ v .
To extend this result to the expressions we consider in this paper, we introduce the following generalisation of the language of a regular expression. Sets of words become sets of ground terms.

Definition 3 (Term language of an expression)

The term language denoted by an expression e ∈ Reg ∨∧ X , written e , is the set of ground terms defined inductively as follows:

x ∶= {x} e ⋅ f ∶= {w ⋅ w ′ w ∈ e and w ′ ∈ f } e ∨ f ∶= e ∪ f e ∧ f ∶= {w ∧ w ′ w ∈ e and w ′ ∈ f } e ⋆ ∶= ⋃ n∈◆ {w 1 ⋅ ⋯ ⋅ w n ∀i, w i ∈ e } e ∨ ∶= {w ∨ w ∈ e } 1 ∶= {1} 0 ∶= ∅ . *
We need a slight refinement of a lemma established by Andréka, Mikulás, and Németi [START_REF] Andréka | The equational theory of Kleene lattices[END_REF]:

Lemma 4. For all expression e ∈ Reg ∨∧ X X, and all relational interpretations σ ∶ X → P (S × S), we have

σ(e) = ⋃ w∈ e σ(w) = ⋃ w∈ e ⊲ σ(w) .
Proof. The first equality is exactly [1, Lemma 2.1]; for the second one, we use the fact that σ(w) ⊆ σ(u) whenever w ⊲ u, thanks to Theorem 2 (i.e., [2, Theorem 1]).

The above definitions make it possible to characterise inclusion under all relational interpretation in terms of downward-closed term languages. To obtain decidability, we need to go one step further, by considering graph languages.

Definition 5 (Graph language of an expression)

The graph language of an expression e, denoted by G(e) is the set of graphs associated to the ground terms in e : G(e) ∶= {G(w) w ∈ e }. *

We finally obtain the following characterisation, which allows us to reduce validity in Rel to an equality of graph languages. Theorem 6. The following properties are equivalent, for all expressions e, f ∈ Reg ∨∧ X :

(i) Rel ⊧ e = f , (ii) e ⊲ = f ⊲ , (iii) G(e) ◂ = G(f ) ◂ .
Proof. The implication (ii) ⇒ (i) follows easily from Lemma 4, and (iii) ⇒ (ii) is a matter of unfolding definitions. For (i) ⇒ (iii), we mainly use [2, Lemma 3].

The above statement can also be reformulated in terms of inclusions, to match the result announced in the introduction:

Rel ⊧ e ⩽ v if and only if e ⊆ f ⊲ if and only if G(e) ⊆ G(f ) ◂ .
Also notice that while by definition G(e) only contains graphs emanating from ground terms, this is not the case for its closure G(e) ◂ . For instance, G((a ⋅ b) ∧ (c ⋅ d)) ◂ contains the following graph, which is not the graph of any ground term. The above result holds for the whole syntax of regular expressions with converse and intersection. However, in the remainder of the paper, we have to focus on expressions without converse and identity. This is because in combination with intersection, these two operations introduce cycles in the graphs associated to ground terms. Consider for instance the graphs for a ∧ 1 and a ∧ b ∨ :

G(a ∧ 1) = a ; G(a ∧ b ∨ ) = a b .
Since reflexive-transitive closure (⋅ ⋆ ) implicitly contains an occurrence of the identity, we also have to replace this operator with transitive closure (⋅ + ). We thus work we expressions from Reg ∧- X , defined with the following syntax: e, f ∈ Reg ∧- X ∶∶= x ∈ X e ∧ f e ∨ f e ⋅ f e + 0. Accordingly, ground terms are restricted to the following syntax: u, v, w ∈ W - X ∶∶= x ∈ X w ⋅ w w ∧ w.

Petri Automata

Before getting to our definition of automata, we recall the standard notion of Petri net.

Definition 7 (Petri Net) A Petri Net is a structure N = ⟨P, T, F, W, M 0 ⟩ where:

• P and T are finite disjoints sets, respectively of places and transitions;

• F ⊆ (P × T ) ∪ (T × P ) is a set of arcs, called the flow relation;

• W ∶ (P × T ) ∪ (T × P ) → ◆ is a weight function, such that W (f ) = 0 if f ∈ F ; • M 0 ∶ P → ◆ is the initial marking.
Given A Petri net is said to be one-bounded if in any accessible marking M , no place is marked with more than one token. Such markings can be seen as finite sets of places; we call them configurations in the sequel, and we let ξ, Ξ range over them. Bounded nets form an interesting class of nets, because many problems which are undecidable in the general case become decidable in this setting: whereas general Petri nets have an infinite set of accessible markings, they are finitely many in a bounded net.

Our notion of Petri Automata is defined below. The main difference with regular Petri nets is the labelling with letters from the alphabet X of all arcs coming out of transitions. Note that this slightly differs from the usual notion of labelled Petri net, where the labels are put on transitions.

Definition 8 (Petri Automaton)

A Petri automaton is a structure ⟨N, L, F ⟩ where:

• N = ⟨P, T, F, W, M 0 ⟩ is a one-bounded Petri net such that:
the weight W (f ) of all arcs f that appear in F is equal to 1; -all transitions τ ∈ T , have at least one incoming arc and one outgoing arc, meaning that there are places p, q ∈ P such that (p, τ ) ∈ F and (τ, q) ∈ F ;

there is an initial place ι such that M 0 contains only one token, placed in ι.

• L ∶ (T × P ) ∩ F → X is a labelling function;

• F ⊆ P (P ) is a set of final configurations. *

A transition τ in a Petri automaton can be alternatively described by a pair [τ ] = (s, t) where:

• s = {p (p, τ ) ∈ F } is the input of τ , often denoted by • τ , and

• t = {(x, q) (τ, q) ∈ F and x = L(τ, q) } is the output of τ . Notice that this differs from the usual notion of output of a transition in a Petri net: in the usual setting τ • is just the set of places reachable from the τ . Here we add to each place the label of the arc reaching it. For commodity reasons, we will thus define Petri automata using quadruples A = ⟨P, T , ι, F ⟩ with ι the initial place and

T = {(s, t) ∃τ ∈ T ∶ [τ ] = (s, t) }.
Graphical representations of such automata are given in Figures 3 and5. In these drawings a final configuration is represented by a dotted rectangle around the places contained in this configuration. Now we explain how to use Petri automata to define languages of graphs. We first describe what is a run of an automaton, and then how to use runs to read graphs.

Let A = ⟨P, T , ι, F ⟩ be a Petri automaton. We write ξ τ → A ξ ′ when the configuration ξ ′ can be obtained by firing some transition τ in the configuration ξ. A set of transitions T ⊆ T is called compatible if their inputs are pairwise disjoint. If furthermore all transitions in T are enabled in a configuration ξ, one can observe that the configuration ξ ′ reached after firing them successively does not depend on the order in which they are fired. In that case we write ξ (Note that a run ξ is uniquely determined by ξ 0 and the sequence (τ k ): all subsequent configurations can be computed deterministically.)

T → A ξ ′ .
Example 10 (An accepting run in the automaton from Figure 5) Consider the run ξ = ⟨(ξ 0 , ξ 1 , ξ 2 , ξ 3 , ξ 4 , ξ 5 , ξ 6 ) , (τ 0 , τ 1 , τ 2 , τ 3 , τ 4 , τ 5 )⟩, with

ξ 0 ={A} , ξ 1 ={B, G} , ξ 2 = ξ 4 ={C, E, G} , ξ 3 = ξ 5 ={D, E, G} , ξ 6 ={F, G} . τ 0 =({A} , {(b, B), (a, G)}) , τ 1 =({B} , {(c, C), (b, E)}) , τ 2 = τ 4 =({C} , {(a, D)}) , τ 3 =({D, E} , {(c, C), (b, E)}) , τ 5 =({D, E} , {(d, F )}) .
We can easily check, using the firing rules of a Petri net that:

{A} τ0 / / {B, G} τ1 / / {C, E, G} τ2 / / {D, E, G} τ3 / / {C, E, G} τ4 / / {D, E, G} τ5 / / {F, G} .
As {A} is the initial configuration and {F, G} ∈ F , this run is accepting. It can be represented graphically as in Figure 6. ∎

As in finite-state automata, we now need to specify how to read a graph in an automaton. This is done by linking the intermediate configurations of a run to vertices in the graph, and by imposing conditions to match transitions with labelled edges of the graph. Definition 11 (Reading along a run, parallel reading, language of a run) A reading of G = ⟨V, E, ι, o⟩ along a run ξ = ⟨(ξ k ) 0⩽k⩽n , (s k , t k ) 0⩽k<n ⟩ is a sequence (ρ k ) 0⩽k⩽n such that for all k, ρ k is a map from ξ k to V w , ρ 0 (ξ 0 ) = {ι}, ρ n (ξ n ) = {o}, and ∀k < n, the following holds:

• all tokens in the input of the transition are mapped to the same vertex in the graph:

∀p, q ∈ s k , ρ k (p) = ρ k (q);
• the images of tokens in ξ k that are not in the input of the transition are unchanged:

∀p ∈ ξ k ∖ s k , ρ k (p) = ρ k+1 (p),
• each pair in the output of the transition can be mapped to an edge of the graph with the same label: ∀p ∈ s k , ∀(x, q) ∈ t k , (ρ k (p), x, ρ k+1 (q)) ∈ E.

Similarly, we define a parallel reading ρ along some parallel run Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T k ) 0⩽k<n ⟩ by requiring that: ρ 0 (Ξ 0 ) = {ι}, ρ n (Ξ n ) = {o}, and ∀k < n the following holds:

• ∀p ∈ Ξ k ∖ ⋃ (s,t)∈T k s, ρ k+1 (p) = ρ k (p); • ∀(s, t) ∈ T k , ∀p, q ∈ s, ρ k (p) = ρ k (q); • ∀(s, t) ∈ T k , ∀p ∈ s, ∀(x, q) ∈ t, (ρ k (p), x, ρ k+1 (q)) ∈ E.
The language of a run ξ, denoted by L (ξ) is the set of graphs that can be read along ξ. *

The language of a Petri automaton is finally obtained by considering all accepting runs.

Definition 12 (Language recognised by a Petri automaton)

The language recognised by A , written L (A ), is the following set of graphs:

L (A ) ∶= ⋃ ξ accepting in A L (ξ) . *
The language of a run ξ can be characterised using a single graph which we call the trace of ξ: graphs are accepted by ξ exactly when they are smaller than the trace of ξ, according to ◂ (Lemma 14 below). For instance the trace of the run presented in Figure 6 is shown in Figure 7.

This trace is constructed by creating a vertex k for each transition τ k = (s k , t k ) of the run, plus a final vertex n. We add an edge (k, x, l) whenever there is some place q such that (x, q) ∈ t k , and τ l is the first transition after τ k in the run with q among its inputs, or l = n if there is no such transition in the run. Formally: Definition 13 (Trace of a run) Let ξ = ⟨(ξ k ) 0⩽k⩽n , (s k , t k ) 0⩽k<n ⟩ be run. For an index k ⩽ n and a place q, let ν(k, q) be either the smallest index l such that k ⩽ l and q ∈ s l , or n if there is no such index. The trace of ξ is the graph Tr (ξ) ∶= ⟨{0, . . . , n} , E ξ , 0, n⟩ with E ξ ∶= {(k, x, ν(k + 1, q)) (x, q) ∈ t k }. We write Tr (A ) for the set of traces associated to the accepting runs of A . * Lemma 14. For any accepting run ξ, we have G ∈ L (ξ) if and only if G ◂ Tr (ξ).

Proof. Suppose there exists a graph morphism h from Tr (ξ) to G. Then we can build a reading by defining ρ k (p) = h(ν(k, p)) for 0 ⩽ k ⩽ n and p ∈ ξ k . On the other hand, if we have a reading (ρ k ) 0⩽k⩽n of G, we can build a morphism h by letting h(k) = ρ k (p) for any p ∈ s k . As (ρ k ) k is a reading, h is well defined.

As a corollary, we obtain the following characterisation of the language of a Petri automaton.

Corollary 15. L (A ) = Tr (A ) ◂ .
The left-hand side language is defined through readings along accepting runs, which is a local and incremental notion and which allows us to define simulations in Section 4. By contrast, the right-hand side language is defined globally, which eases the following construction of an automaton recognising the language of an expression.

From expressions to automata

We now show how to associate to any expression e ∈ Reg ∧- X an automaton A (e) that recognises the language G(e) ◂ . In fact the produced automaton has an even stronger connection with e: the graphs in G(e) are exactly the traces of accepting runs in A (e).

Definition 16

To each expression e ∈ Reg ∧- X , we associate a Petri automaton A (e) defined inductively as follows:

• A (x) ∶= ⟨{0, 1} , {({0} , {(x, 1)})} , 0, {{1}}⟩ • A (0) ∶= ⟨{0} , ∅, 0, ∅⟩ • A (e 1 ∨ e 2 ) ∶= ⟨P 1 ∪ P 2 , T , ι 1 , F 1 ∪ F 2 ⟩ with T ∶= T 1 ∪ T 2 ∪ {({ι 1 } , t) ({ι 2 } , t) ∈ T 2 }. • A (e 1 ⋅ e 2 ) ∶= ⟨P 1 ∪ P 2 , T , ι 1 , F 2 ⟩ with T ∶= T 1 ∪ T 2 ∪ {(f, t) f ∈ F 1 and ({ι 2 } , t) ∈ T 2 }. • A (e + 1 ) ∶= ⟨P 1 , T , ι 1 , F 1 ⟩ with T ∶= T 1 ∪ {(f, t) f ∈ F 1 and ({ι 1 } , t) ∈ T 1 }. • A (e 1 ∧ e 2 ) ∶= ⟨P 1 ∪ P 2 , T , ι 1 , F ⟩ with F ∶= {f 1 ∪ f 2 f 1 ∈ F 1 , f 2 ∈ F 2 } and T ∶= {(s, t) i ∈ {1, 2} , (s, t) ∈ T i , ι i ∉ s } ∪ {({ι 1 } , t 1 ∪ t 2 ) ({ι 1 } , t 1 ) ∈ T 1 , ({ι 2 } , t 2 ) ∈ T 2 } (In the inductive cases, we assume that A (e i ) = ⟨P i , T i , ι i , F i ⟩ for i ∈ {1, 2}, with P 1 ∩ P 2 = ∅.) *
We prove by induction on e that A (e) is indeed a Petri automaton; for the one-boundedness assumption, we add to the induction hypothesis the fact that for any configuration ξ accessible in A (e), if there is a final configuration f ∈ F such that f ⊆ ξ, then f = ξ. Another invariant is that the initial place never appears in a final configuration, nor in the outputs of any transition. Note that the place ι 2 becomes unreachable by construction in the cases for union, composition and intersection, so that it could safely be removed, together with the associated transitions. One can also check that the number of places in the produced automaton is linear in the size of the input expression.

Theorem 17 (Correctness). For all expression e ∈ Reg ∧- X , L (A (e)) = G (e) ◂ .

Proof. As explained above, we prove a stronger result, namely Tr (A (e)) = G(e) (up to graph isomorphisms). This allows us to conclude thanks to Corollary 15.

Remark 18. If e is an expression without intersection, it can be shown that the transitions in A (e) are all of the form ({p} , {(x, q)}), with only one input and one output. In consequence, the accessible configurations are singletons, and the resulting Petri automaton has the structure of a Nondeterministic Finite-state Automaton (NFA). Actually, in that case, the construction we described above is just a variation on Thompson's construction [START_REF] Thompson | Regular expression search algorithm[END_REF], with inlined epsilon transition elimination.

Combined with Theorem 6 from Section 1, the above theorem allows us to reduce the problem of deciding whether Rel ⊧ e = f to the problem of checking whether L (A (e 1 )) = L (A (e 2 )). By symmetry, it then suffices to decide inclusion of Petri automata languages.

Comparing automata

We want to compare automata by testing if any graph accepted by A 1 is also accepted by A 2 . Let us go back to standard non-deterministic finite-state automata (NFA), to find intuitions. In that setting an automaton over some alphabet Σ is defined by A = ⟨Q, ι, F, ∆⟩ where Q is a finite set of states, ι is an initial state, F is a set of finite states F and ∆ is a set of transitions of the form (p, a, q) where p and q are states and a is a letter. Consider two automata

A 1 = ⟨Q 1 , ι 1 , F 1 , ∆ 1 ⟩ and A 2 = ⟨Q 2 , ι 2 , F 2 , ∆ 2 ⟩. L(A 1 ) ⊆ L(A 2 )
means that for any word w = a 1 ⋯a n accepted by A 1 , w is also accepted by A 2 . Thus if there is an execution in A 1 recognising w then there is an execution in A 2 recognising w. One can then put them together side by side like so:

ι 1 a1 → A1 p 1 a2 → A1 ⋯ an → A1 p n ∈ F 1 ι 2 a1 → A2 q 1 a2 → A2 ⋯ an → A2 q n ∈ F 2
Thus trying to prove that L(A 1 ) ⊆ L(A 2 ) amounts to finding a method to build from any run in A 1 a corresponding run in A 2 . This can be done by computing a simulation between the automaton A 1 and the determinised automaton of A 2 . A simulation between these automata is then a relation

≼ ⊆ Q 1 × P (Q 2 ) such that • ι 1 ≼ {ι 2 }, and if p ≼ P and p ∈ F 1 , then P ∩ F 2 ≠ ∅; • if p ≼ P and (p, a, p ′ ) ∈ ∆ 1 then p ′ ≼ P ′ , where P ′ ∶= {p ′ (p, a, p ′ ) ∈ ∆ 2 , p ∈ P }. p a / / p ′ P ≼ a / / P ′ ≼
If such a relation can be found, then for any accepting execution in A 1 , we can use the relation to extract a corresponding execution in A 2 . It is also possible to prove that if the language of A 1 is indeed included in the language of A 2 , then such a relation exists. This gives us an algorithm to decide the inclusion of languages, because the set of states of both automata being finite, there is only a finite number of candidates for ≼. More realistically, one can define a coinductive algorithm that computes a simulation relation on-the-fly.

We follow a similar approach for Petri automata, but we need to make several important adjustments. Consider two automata

A 1 = ⟨P 1 , T 1 , ι 1 , F 1 ⟩ and A 2 = ⟨P 2 , T 2 , ι 2 , F 2 ⟩,
we try to show that for any graph G accepted by A 1 , G is recognised by A 2 . By Lemma 14, this amounts to proving that for any accepting run ξ in A 1 , Tr (ξ) is recognised by some accepting run ξ ′ in A 2 . Leaving nondeterminism apart, the first idea that comes to mind is to find a relation between the configurations in A 1 and the configurations in A 2 , that satisfy some conditions on the initial and final configurations, and such that if

ξ k ≼ ξ ′ k and ξ k τ → A1 ξ k+1 , then there is a configuration ξ ′ k+1 in A 2 such that ξ k+1 ≼ ξ ′ k+1 , ξ ′ k τ ′ → A2 ξ ′ k+1
, and these transition steps are compatible in some sense. However, such a definition will not give us the result we are looking for. Consider the two runs on the left-hand side:

A B B C D 1 2 a b c W Y Y X Z 1 ′ 2 ′ b a c {A} 1 / / {B, C} 2 / / {B, D} {W } ≼ 1' / / {X, Y } ≼ 2' / / {Y, Z} ≼
The trace of the first run corresponds to the ground term a ∧ (b ⋅ c), and the trace of the second one corresponds to (a ⋅ c) ∧ b. These two terms are incomparable, but the relation ≼ depicted on the right-hand side satisfies the previously stated conditions.

The problem here is that in Petri automata, runs are token firing games. To adequately compare two runs, we need to closely track the tokens. For this reason, we will relate a configuration ξ k in A 1 not only to a configuration ξ ′ k in A 2 , but to a map η k from ξ ′ k to ξ k . This will enable us to associate with each token situated on some place in P 2 another token placed on A 1 .

We want to find a reading of Tr (ξ) in A 2 , i.e. a run in A 2 together with a sequence of maps associating places in A 2 to positions in Tr (ξ). Consider the picture below. Since we already have a reading of Tr (ξ) along ξ (by defining ρ k (p) = ν(k, p), as in the proof of Lemma 14), it suffices to find maps from the places in A 2 to the places in A 1 (the maps η k ): the reading of Tr (ξ) in A 2 will be obtained by composing η k with ρ k .

Tr (ξ)

ξ 0 τ0 / / ξ 1 τ1 / / ⋯ τn-1 / / ξ n τn / / ξ n+1 ξ ′ 0 η0 O O τ ′ 0 / / ξ ′ 1 τ ′ 1 / / η1 O O ⋯ τ ′ n-1 / / ξ ′ n ηn O O τ ′ n / / ξ ′ n+1 ηn+1 O O ρ0 7 7 ρ1 < < ρn [ [ ρn+1 e e
We need to impose some constraints on the maps (η k ) to ensure that (ρ k ○ η k ) 0⩽k⩽n is indeed a correct reading in A 2 . First, we need to ascertain that a transition τ ′ k in A 2 may be fired from the reading state ρ k ○ η k to reach the reading state ρ k+1 ○ η k+1 . Furthermore, as for NFA, we want transitions τ k and τ ′ k to be related: specifically, we require τ ′ k to be included (via the morphisms η k and η k+1 ) in the transition τ k . This is meaningful because transition τ k contains a lot of information about the vertex k of Tr (ξ) and about ρ: the labels of the outgoing edges from k are the labels on the output of τ k , and the only places that will ever be mapped to k in the reading ρ are exactly the places in the input of τ k . Definition 19 (Simulation) A relation ≼ ⊆ P (P 1 ) × P (P 2 ⇢ P 1 ) between the configurations of A 1 and the partial maps from the places of A 2 to the places of A 1 is called a simulation between A 1 and A 2 if:

• {ι 1 } ≼ {[ι 2 ↦ ι 1 ]}; • if ξ ≼ E and ξ (s,t)
→ A1 ξ ′ , then ξ ′ ≼ E ′ where E ′ is the set of all η ′ such that there is some η ∈ E and a compatible set of transitions T ⊆ T 2 such that:

dom (η) T → A2 dom (η ′ ); -∀(s ′ , t ′ ) ∈ T, η(s ′ ) ⊆ s and ∀(x, q) ∈ t ′ , (x, η ′ (q)) ∈ t;

-∀p ∈ dom (η) , (∀(s ′ , t ′ ) ∈ T, p ∉ s ′ ) ⇒ η(p) = η ′ (p).
• if ξ ≼ E and ξ ∈ F 1 , then there must be some η ∈ E such that dom (η) ∈ F 2 . *

We will now prove that the language of A 1 is contained in the language of A 2 if and only if there exists such a simulation. We first introduce the following notion of embedding.

Definition 20 (Embedding) Let ξ = ⟨(ξ k ) 0⩽k⩽n , (τ k ) 0⩽i<n ⟩ be a run in A 1 , and Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T i ) 0⩽i<n ⟩ a parallel run in A 2 . An embedding of Ξ into ξ is a sequence (η i ) 0⩽i⩽n of maps such that for any i < n, we have:

• η i is a map from Ξ i to ξ i ;

• the image of T i by η i is included in τ i , meaning that for any (s, t) ∈ T i , for any p ∈ s and (x, q) ∈ t, η i (p) is contained in the input of τ i and (x, η i+1 (q)) is in the output of τ i ;

• the image of the tokens in Ξ i that do not appear in the input of T i are preserved (η i (p) = η i+1 (p)) and their image is not in the input of τ i . 6. Notice that is it necessary to have a parallel run instead of a simple one: to find something that matches transition 1 , we need to fire two transitions in parallel.

ξ i τi / / ξ i+1 Ξ i ηi O O Ti / / Ξ i+1 ηi+1 O O *
There is a close relationship between simulations and embeddings: Lemma 21. Let A 1 and A 2 be two Petri automata, the following are equivalent:

1. there exists a simulation ≼ between A 1 and A 2 ;

2. for any accepting run ξ in A 1 , there is an accepting parallel run Ξ in A 2 that can be embedded into ξ.

Proof. If we have a simulation ≼, let ξ = ⟨(ξ k ) 0⩽k⩽n , (τ k ) 0⩽k<n ⟩ be an accepting run in A 1 . By the definition of simulation, we can find a sequence of sets of maps

(E k ) 0⩽k⩽n such that E 0 = {[ι 2 ↦ ι 1 ]} and ∀k, ξ k ≼ E k .
Furthermore, we can extract from this a sequence of maps (η k ) 0⩽k⩽n and a sequence of parallel transitions (T k ) 0⩽k<n such that (η k ) is an embedding of ⟨(dom (η k )) 0⩽k⩽n , (T k ) 0⩽k<n ⟩ (which is accepting) into ξ. This follows directly from the definitions of embedding and simulation. On the other hand, if we have property 2., then we can define a relation ≼ by saying that ξ ≼ E if there is an accepting run ξ ′ = ⟨(ξ ′ k ) 0⩽k⩽n , (τ k ) 0⩽k<n ⟩ in A 1 such that there is an index k 0 : ξ = ξ ′ k0 ; and the following holds: η ∈ E if there is an accepting parallel run Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T k ) 0⩽k<n ⟩ and (η ′ k ) 0⩽k⩽n an embedding of Ξ into ξ such that η = η ′ k0 . It is then immediate to check that ≼ is indeed a simulation.

If η is an embedding of Ξ into ξ, we can easily check that (ρ i ○ η i ) 0⩽i⩽n is a parallel reading of Tr (ξ) along Ξ in A 2 , as illustrated by this diagram:

Tr (ξ) ξ 0 τ0 / / ξ 1 τ1 / / ⋯ τn-1 / / ξ n τn / / ξ n+1 Ξ 0 η0 O O T0 / / Ξ 1 T1 / / η1 O O ⋯ Tn-1 / / Ξ n ηn O O Tn / / Ξ n+1 ηn+1 O O ρ0 7 7 ρ1 < < ρn [ [ ρn+1 f f
Thus, it is clear that once we have such a run Ξ with the sequence of maps η, we have that Tr (ξ) is indeed in the language of A 2 . The more difficult question is the completeness of this approach: if Tr (ξ) is recognised by A 2 , is it always the case that we can find a run Ξ that may be embedded into ξ? The answer is affirmative, thanks to Lemma 23 below. If (ρ j ) 0⩽j⩽n is a reading of G along ξ = ⟨(ξ k ) 0⩽k⩽n , (s k , t k ) 0⩽k<n ⟩, we write active(j) for the only position in ρ j (s j )1 .

Definition 22 (Consistent ordering)

⩿ is a consistent ordering on G = ⟨V, E, ι, o⟩ if ⟨V, ⩿⟩ is a linear order and (p, x, q) ∈ E entails p ⩿ q. * Lemma 23. Let G ∈ L (A 2 ) and ⩿ be any consistent ordering on G. Then there exists a run ξ and a reading (ρ j ) 0⩽j⩽n of G along ξ such that ∀k, active(k) ⩿ active(k + 1).

Proof. The proof of this result is achieved by taking any run ξ accepting G, and then exchanging transitions in ξ according to ⩿, while preserving the existence of a reading. The details of this proof being a bit technical, we omit them here.

Notice that if G contains cycles, this lemma cannot apply because of the lack of consistent ordering. This enables us to build an embedding from any reading of Tr (ξ) in A 2 .

Lemma 24. Let ξ a accepting run of A 1 . Then Tr (ξ) is in L (A 2 ) if and only if there is an accepting parallel run in A 2 that can be embedded into ξ.

Proof. We do not include the details of this proof here for length reasons.

For the if direction, we build a parallel reading from the embedding, as explained above. For the other direction, we consider a reading of Tr (ξ) in A 2 along some run ξ ′ . Notice that the natural ordering on ◆ is consistent for Tr (ξ); we may thus change the order of the transitions in ξ ′ (using Lemma 23) and group them adequately to obtain a parallel reading Ξ that embeds in ξ.

So we know that the existence of embeddings is equivalent to the inclusion of languages, and we previously established that it is also equivalent to the existence of a simulation relation. Hence, the following characterisation holds: Theorem 25. Let A 1 and A 2 be two Petri automata. L (A 1 ) ⊆ L (A 2 ) if and only if there exists a simulation relation ≼ between A 1 and A 2 .

Proof. By Lemmas 14, 21 and 24.

As Petri automata are finite, there are finitely many relations in P (P (P 1 ) × P (P 2 ⇢ P 1 )). The existence of a simulation thus is decidable, allowing us to prove the main result: Theorem 26. Given two expressions e, f ∈ Reg ∧- X , testing whether Rel ⊧ e = f is decidable.

Proof. By Theorems 6, 17 and 25, and reasoning by double inclusion.

In practice, we may build the simulation on-the-fly, starting from the pair ({ι 1 } , {[ι 2 ↦ ι 1 ]}) and progressing from there. We have implemented this algorithm in OCaml: even though its theoretical worst case time complexity is huge2 , we get a result almost instantaneously on simple one-line examples.

Conclusions and directions for future work

By introducing Petri automata, we proved the decidability of the equivalence of identity-free regular expressions with intersection, with respect to their relational interpretations. Actually, this also holds for their language interpretations, because Andréka et al. showed in [START_REF] Andréka | The equational theory of Kleene lattices[END_REF] that the classes of identityfree relational Kleene lattices and identity-free language Kleene lattices coincide. They differ however when we include the identity constant, or the converse operation.

Figure 1 :Figure 2 :

 12 Figure 1: Graphs associated to some ground terms

Figure 3 :

 3 Figure 3: The automaton corresponding to the term (a ⋅ b) ∧ (a ⋅ c).

Figure 4 :

 4 Figure 4: Graphs corresponding to ground terms.

Figure 5 :

 5 Figure 5: A Petri automaton. The initial state is A, and the final configurations are {I} and {F, G}.

Definition 9 (

 9 Run, accepting run, parallel run) A run is a sequence ξ = ⟨(ξ k ) 0⩽k⩽n , (τ k ) 0⩽k<n ⟩ of configurations and transitions, such that ξ k ⊆ P , τ k ∈ T and ∀k < n, ξ k τ k → ξ k+1 . When ξ 0 = {ι} and ξ n ∈ F , we call ξ an accepting run. A parallel run is defined similarly, as a sequence Ξ = ⟨(Ξ k ) 0⩽k⩽n , (T k ) 0⩽k<n ⟩, where the T k ⊆ T are compatible sets of transitions such that Ξ k T k → Ξ k+1 . *

Figure 6 :Figure 7 :

 67 Figure 6: An accepting run in the automaton from Figure 5.

ac

  This already shows an important difference between the simulations for NFA and Petri automata. For NFA, we relate a transition p a → p ′ to a transition q a → q ′ with the same label a. Here the transitions ξ k τ k → A1 ξ k+1 may have different labels. Consider the step represented on the right, corresponding to a square in the above diagram. The output of 0 has a label b that does not appear in 0' , and 0' has two outputs labelled by a. Nevertheless this satisfies the conditions informally stated above, indeed, a ∧ b ⩽ a ∧ a holds.However this definition is not yet satisfactory. Consider the two runs below:Their traces correspond respectively to the ground terms a ⋅ (b ∧ c) and(a ⋅ b) ∧ (a ⋅ c). The problem is that a ⋅ (b ∧ c) ⩽ (a ⋅ b) ∧ (a ⋅ c), but with the previous definition, we cannot relate these runs: they do not have the same length. The solution here consists in grouping the transitions 1' and 2' together, and consider these two steps as a single step in a parallel run. This last modification gives us a notion of simulation we can really work with.

Figure 8

 8 Figure 8 illustrates the embedding of some parallel run, with trace((b ⋅ c ⋅ a ⋅ b) ∧ (b ⋅ b ⋅ c ⋅ a)) ⋅ d, intothe run presented in Figure6. Notice that is it necessary to have a parallel run instead of a simple one: to find something that matches transition 1 , we need to fire two transitions in parallel.There is a close relationship between simulations and embeddings:

Figure 8 :

 8 Figure 8: Embedding of a parallel run into the run from Figure 6.

  To present examples in a simple way, we use the standard graphical representation of Petri nets: they are represented as graphs, with round nodes for places and rectangular nodes for transitions. The flow relation is simply represented by arrows; the places appearing in the initial marking have an additional incoming arrow.

a marking M in a net N , a transition τ ∈ T is enabled if for any place p such that (p, τ ) is in the flow relation F , we have W (p, τ ) ⩽ M (p). In that case, τ can fire, and it results in a new marking M ′ such that M ′ (p) = M (p) -W (p, τ ) + W (τ, p). A marking is called accessible if it can be obtained by successively firing transitions starting from M 0 . *

Recall that if (ρ j ) 0⩽j⩽n is a reading along ξ then ∀p, q ∈ s j , ρ j (p) = ρ j (q).

A quick analysis gives a O 2 n+n m complexity bound, where n and m are the numbers of places of the automata.

The construction and algorithm presented here were implemented in OCaml as an exercise. The resulting program is available online as an interactive applet [5].

By adding ǫ-transitions to Petri automata, we could partly cope with the identity, in the sense that we can build automata to recognise the graph languages of expressions over the signature ⟨∨, ∧, ⋅, ⋅ ⋆ , 1, 0⟩. However, we did not find a way of comparing ǫ-Petri automata: the notion of simulation we described here is not equivalent to the inclusion of languages for these automata.

Similarly, we could define a variant of Petri automata for recognising the graph languages associated to expressions with converse: it suffice to consider a duplicated alphabet. However, we did not find a proper way of extending our notion of simulation to capture language inclusion of such automata.