Thomas Geffroy

Jérôme Leroux

Grégoire Sutre

Backward Coverability with Pruning for Lossy Channel Systems

Keywords: Invariants, Program verification, Model-Checking, Well-Structured Transition Systems, Lossy Channel Systems, Coverability Problem

Driven by the concurrency revolution, the study of the coverability problem for Petri nets has regained a lot of interest in the recent years. A promising approach, which was presented in two papers last year, leverages a downward-closed forward invariant to accelerate the classical backward coverability analysis for Petri nets. In this paper, we propose a generalization of this approach to the class of well-structured transition systems (WSTSs), which contains Petri nets. We then apply this generalized approach to lossy channel systems (LCSs), a well-known subclass of WSTSs. We propose three downward-closed forward invariants for LCSs. One of them counts the number of messages in each channel, and the other two keep track of the order of messages. An experimental evaluation demonstrates the benefits of our approach.

CCS CONCEPTS

• Theory of computation → Verification by model checking; Logic and verification

perfect channels. If a safety property is satisfied by a system with unreliable communications, then the property is also satisfied by the same system with perfect communications. The verification of a safety property on a given LCS can often be reduced to a coverability question on a (potentially larger) LCS. Coverability for LCSs is essentially the same as control-state reachability.

Related work. The coverability problem for LCSs was shown to be decidable in [START_REF] Abdulla | Verifying Programs with Unreliable Channels[END_REF]. The precise computational complexity of the problem remained open for fifteen year. It was shown to be hyper-Ackermann-complete in [START_REF] Chambart | The Ordinal Recursive Complexity of Lossy Channel Systems[END_REF]. This complexity could leave us hopeless for practical implementations. However, even though the coverability problem for Petri nets is ExpSpace-complete, tools were recently implemented with great success in practice [START_REF] Blondin | Approaching the Coverability Problem Continuously[END_REF][START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF][START_REF] Geffroy | Occam's Razor Applied to the Petri Net Coverability Problem[END_REF][START_REF] Kaiser | A Widening Approach to Multithreaded Program Verification[END_REF]. We can hope to repeat this success for LCSs since they are somewhat close to Petri nets (both are well-structured transition systems [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]).

Some tools already exist to solve the coverability problem for LCSs. The most prominent one is TReX [START_REF] Annichini | TReX: A Tool for Reachability Analysis of Complex Systems[END_REF]. The tools LASH [START_REF] Boigelot | Symbolic Verification of Communication Protocols with Infinite State Spaces using QDDs[END_REF] and McScM [START_REF] Heußner | McScM: A General Framework for the Verification of Communicating Machines[END_REF] are primarily designed to verify systems with perfect channels, but they can also be used for LCSs by explicitly permitting message losses. TReX and LASH iteratively compute the forward reachability set using (1) a symbolic representation of channel contents and (2) so-called acceleration techniques to speedup the computation. McScM is based on counterexample-guided abstraction refinement [START_REF] Clarke | Counterexampleguided abstraction refinement for symbolic model checking[END_REF] and abstract regular model-checking [START_REF] Bouajjani | Abstract Regular Model Checking[END_REF]. Our approach can be seen as an explicit backward search combined with a symbolic forward abstraction.

Our contribution. We present a generic backward coverability algorithm that relies on downward-closed forward invariants to prune the exploration of the state space. This algorithm works not only for LCSs but for the larger class of well-structured transition systems. We present three invariants for LCSs that can be used by this algorithm. The one we call state inequation ignores the order of messages but counts the number of occurrences of each message in each channel. The other two invariants ignore how many messages are in the channels, but focus on their order. One is based on simple regular expressions [START_REF] Abdulla | On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels[END_REF] and the other is based on quasi-orderings over messages. The second one is as an abstraction of the first one that provides an interesting trade-off between precision and efficiency. We have implemented the algorithm and the three invariants. Our experimental evaluation demonstrates the benefits of our approach.

Outline. Section 2 recalls the coverability problem for well-structured transition systems. Sections 3 and 4 present our generalized backward coverability algorithm with pruning based on downwardclosed invariants. Section 5 recalls lossy channel systems and simple regular expressions. Sections 6 and 7 present two invariants that keep track of the order of messages in the channels. Section 8 presents an invariant that counts the messages in the channels. Section 9 provides our experimental evaluation. Section 10 concludes the paper.

COVERABILITY FOR WELL-STRUCTURED TRANSITION SYSTEMS

The class of well-structured transition systems (WSTS) is a large class of systems with many decidable properties [START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. In fact many classical problems (some termination and safety properties), can be decided with generic algorithms. The coverability problem is such a problem. It is motivated by the formal verification of some safety properties. In this section, we recall in three sub-sections [START_REF] Abdulla | The Benefits of Duality in Verifying Concurrent Programs under TSO[END_REF] classical results about well quasi-orders, (2) the definition of WSTS, and (3) the coverability problem.

Well Quasi-Ordering

We first recall some properties about well quasi-orders (see [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] for additional properties and definitions).

A quasi-ordering over a set S is a binary relation ≤ over S that is transitive and reflexive. Given a subset X ⊆ S, we let ↑X and ↓X denote its upward closure and downward closure, respectively. These sets are defined as follows.

↑X = {s ∈ S | ∃x ∈ X : x ≤ s} ↓X = {s ∈ S | ∃x ∈ X : s ≤ x } A subset U ⊆ S is called an upward-closed set when U = ↑U , and a subset D ⊆ S is called a downward-closed set when D = ↓D. A basis of an upward-closed set U is a set B ⊆ U such that ↑B = U .
Upward closed sets can be denoted by finite bases when ≤ is a well quasi-order. A well quasi-ordering (wqo) over S is a quasi-ordering ≤ over S such that, for every infinite sequence x 0 , x 1 , . . . ⊆ S, there exist i and j with i < j and x i ≤ x j . This implies that any wqo is wellfounded: it admits no strictly decreasing infinite sequence. Proposition 2.1 ( [START_REF] Finkel | Well-structured transition systems everywhere![END_REF][START_REF] Higman | Ordering by Divisibility in Abstract Algebras[END_REF]). For a quasi-ordering ≤ over a set S, the following propositions are equivalent

• ≤ is wqo.

• Every upward-closed set has a finite basis.

• Every infinite non-decreasing sequence

U 0 ⊆ U 1 ⊆ • • • of upward-closed sets eventually stabilizes: there exists k ∈ N such that U k = U k+1 = U k +2 = • • • Notation:
For the remainder of the paper, we will simply write x in place of {x } for singletons, when it causes no confusion. In particular ↑x denotes {s ∈ S | x ≤ s}.

WSTS

We recall the definition of Well-Structured Transition Systems.

Definition 2.2 (Transition System

). A transition system is a tuple S = (S, s init , →) where S is a set of states, s init is the initial state and → ⊆ S × S is the transition relation.

We note * -→ the reflexive and transitive closure of →. [START_REF] Abdulla | Algorithmic Analysis of Programs with Well Quasi-ordered Domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]). A Well-Structured Transition System (WSTS) is a transition system S = (S, s init , →) equipped with a wqo ≤ over S that is compatible with →: for all states s 1 , s 2 , t 1 with s 1 → s 2 and s 1 ≤ t 1 , there exists t 2 ∈ S such that t 1 * -→ t 2 and s 2 ≤ t 2 .

Definition 2.3 (Well-Structured Transition System

Coverability Problem

The coverability problem is a natural problem of safety verification. Formally, a state s f inal of a WSTS S = (S, s init , →, ≤) is said to be coverable if there exists a state s such that s init * -→ s and s ≥ s f inal . The coverability problem consist in deciding if a state is coverable. The set of coverable configurations is denoted by Cov S and it is called the coverability set.

Notice that Cov S is a downward closed set and in particular its complement is an upward closed set that admits a finite basis as any upward closed set. It follows that if B is a finite basis of that set, the coverability problem for a state s f inal reduces to check that s f inal is not in ↑B, i.e. check if b ∈B b ≰ s f inal . Unfortunately, for some natural classes of WSTSs (like the lossy channel systems introduced in the sequel), such a finite basis B is not computable [START_REF] Mayr | Undecidable problems in unreliable computations[END_REF].

Anyway, the coverability problem can be decided thanks to a generic algorithm. This algorithm is based on the following definitions of predecessor sets. Formally, the one-step predecessors function pre S and the many-step predecessors function pre S are functions from P(S) to P(S), defined for any X ⊆ S by:

pre S (X ) = {s ∈ S | ∃x ∈ X : s → x } pre * S (X ) = {s ∈ S | ∃x ∈ X : s * - → x }
We recall from [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] that pre * S (U ) is an upward closed set for any upward closed set U , and a state s f inal is coverable if, and only if, s init is in pre * S (↑s f inal ). The coverability problem is shown to be decidable for WSTSs, thanks to an algorithm computing inductively a basis of the upward closed set pre * S (↑s f inal ). In the next section we introduce a new generic algorithm for deciding the coverability problem that takes benefit of an over-approximation of the coverability sets.

BACKWARD COVERABILITY ANALYSIS WITH PRUNING

The coverability problem is a fundamental question for formal verification and there have been a lot of different methods proposed to solve this problem efficiently. For Petri Nets, a class of WSTS, in recent years, methods were proposed using structural analysis mixed with SMT solving [START_REF] Blondin | Approaching the Coverability Problem Continuously[END_REF][START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF], and the use of continuous coverability in Petri Nets to accelerate the backward coverability decision [START_REF] Blondin | Approaching the Coverability Problem Continuously[END_REF].

Inspired by those new methods, we proposed in [START_REF] Geffroy | Occam's Razor Applied to the Petri Net Coverability Problem[END_REF] one of the top most efficient algorithm for deciding the coverability problem for Petri nets. In that paper, the correctness of our approach relies on the following two properties satisfied by Petri nets:

• strong compatibility: for all states s 1 ≤ t 1 such that s 1 → s 2 , there exists t 2 ∈ S such that t 1 → t 2 and s 2 ≤ t 2 . • upward closed predecessors : for any state s the set of predecessors pre S (↑s) is upward-closed.

In this section we propose to generalize our approach to the full class of WSTS. The generalization is obtained by adapting proofs in such a way we do not rely anymore on those two previously given properties.

The classical backward coverability algorithm [START_REF] Abdulla | Algorithmic Analysis of Programs with Well Quasi-ordered Domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF] for WSTS computes a growing (meaning non-decreasing in the sequel) sequence U 0 ⊆ U 1 ⊆ • • • of upward-closed subsets of S that converges to pre * S (↑s f inal ). In [START_REF] Geffroy | Occam's Razor Applied to the Petri Net Coverability Problem[END_REF] we proposed a way to improve the convergence with the help of a known over-approximation of the coverability set. The idea is to prune U i with the help of that over-approximation.

Formally, an invariant for a WSTS S = (S, s init , →, ≤) is a downward-closed set of S that contains the coverability set. In Sections 6 to 8 we present efficient algorithms for computing useful invariants.

For the remainder of this section, we consider a WSTS S = (S, s init , →, ≤) with a target state s f inal and we assume that we are given an invariant I for S = (S, s init , →, ≤). We introduce the sequence U 0 , U 1 , . . . subsets of S defined as follows:

U 0 = ↑(s f inal ∩ I ) U k +1 = ↑(pre S (U k ) ∩ I ) ∪ U k Observe that each U k is upward-closed and that U 0 ⊆ U 1 ⊆ • • • .
On the contrary to the classical backward coverability approach [START_REF] Abdulla | Algorithmic Analysis of Programs with Well Quasi-ordered Domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF], U k +1 does not consider all one-step predecessors of U k , but discards those that are not in I . Note that by taking I = S, which is trivially an invariant, we obtain the same growing sequence as in the classical backward coverability approach [START_REF] Abdulla | Algorithmic Analysis of Programs with Well Quasi-ordered Domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

The two following lemmas are adapted from [START_REF] Geffroy | Occam's Razor Applied to the Petri Net Coverability Problem[END_REF]. They show how to use this new sequence to solve the coverability problem. • • → s 0 and s 0 ≥ s f inal . First observe that s i ∈ I for every i ∈ {0, . . . , n} because I is an invariant for S. Moreover, as s f inal ∈ I we get U 0 = ↑s f inal . We prove, by induction on i, that s i ∈ U i for all i ∈ {0, . . . , n}. The basis s 0 ∈ U 0 follows from the facts that s 0 ≥ s f inal and U 0 = ↑s f inal . For the induction step, let i ∈ {0, . . . , n -1} and assume that s i ∈ U i . Recall that s i+1 ∈ I and s i+1 → s i . It follows that s i+1 ∈ (pre S (U i ) ∩ I ) ⊆ U i+1 . We have shown that s n ∈ U n , hence, s init = s n belongs to k U k . Now, let us assume that s init ∈ k U k and let us prove that s f inal ∈ Cov S . We first prove, by induction on k, that U k ⊆ pre * S (↑s f inal ). The basis follows from the observation that U 0 ⊆ ↑s f inal ⊆ pre * S (↑s f inal ). For the induction step, let k ∈ N and assume that U k ⊆ pre * S (↑s f inal ). Recall that

U k +1 = ↑(pre S (U k ) ∩ I ) ∪ U k , hence, U k +1 ⊆ ↑pre S (U k ) ∪ U k . As U k ⊆ pre * S (↑s f inal ), it follows that pre S (U k ) ⊆ pre * S (↑s f inal ). As pre * S (↑s f inal ) is upward closed, it follows that ↑pre S (U k ) ⊆ pre * S (↑s f inal ). Hence U k +1 ⊆ pre * S (↑s f inal ). We have thus shown that U k ⊆ pre * S (↑s f inal ) for every k ∈ N. We obtain that s init is in pre * S (↑s f inal ), therefore s f inal ∈ Cov S . □
We have presented in this section a growing sequence of upwardclosed sets whose limit contains enough information to decide the coverability problem. Our next step is to transform this sequence into an algorithm.

THE ALGORITHM

Now we want to design an algorithm computing with some finite bases the sequence U 0 ⊆ U 1 ⊆ • • • of upward closed sets introduced in the previous section. The classical sequence without the invariant (or with invariant I = S) can be computed [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] for a WSTS S = (S, s init , →, ≤) when the relation ≤ is computable, and when there exists an effective pre-basis for this WSTS, i.e. an algorithm that can compute for every state s, a finite basis cpre S (s) of the upward closure of pre S (↑s). It follows that the following equality holds:

↑cpre S (s) = ↑pre S (↑s)
We present the backward coverability algorithm with pruning for solving the coverability problem for any WSTS S = (S, s init , →, ≤) with a computable ≤ and a computable function cpre.

Given a finite set X of S, we denote by cpre S (X ) the union x ∈X cpre S (x). We have proved the other inclusion. Now, just let Y = cpre S (X ), and observe that pre S (↑X ) = ↑cpre S (X ).

□

We now have everything to propose the pruned backward coverability algorithm for WSTS. Remark 4.2. Line 10 of the algorithm can be implemented just as the assignment B ← B ∪ P. However, in order to improve the efficiency of the algorithm, we remove non minimal elements as follows. An element x in a set X of states is said to be redundant if there exists y ∈ X with y x such that y ≤ x. Notice that in that case ↑X = ↑Y where Y = X \{x }. Line 10 of the algorithm can be implemented just by inductively removing redundant states one by one. When ≤ is a partial order, this computation returns the set of minimal elements. □ Let ℓ B , ℓ P ∈ N∪ {∞} denote the numbers of executions of lines 5 and 8, respectively. It is understood that l P ≤ l B ≤ l P + 1, with the convention that ∞ + 1 = ∞. Let (B k ) k <ℓ B and (P k ) k <ℓ P denote the successive values at lines 5 and 8 of the variables B and P, respectively. Input: A WSTS S = (S , s ini t , →, ≤) with ≤ computable and an effective pre-basis, a target state s f inal ∈ S and a downward-closed invariant I for S Output: Whether there exists a state s ∈ S such that s ini t * -→ s and s ≥ s f inal .

1 if s f inal ∈ I then 2 B ← {s f inal } 3 else 4 B ← ∅
≤ k < ℓ B , the set B k is a finite basis of U k . For every k with 0 ≤ k < ℓ P , the set P k is a finite basis of ↑(U k +1 \ U k ).
Proof. It is readily seen that B k and P k are finite subsets of states for every k. We first observe that, for every k with 0 ≤ k < ℓ P ,

↑P k = ↑((cpre S (B k ) \ ↑B k ) ∩ I ) [Lines 6-7] = ↑(cpre S (B k ) ∩ (I \ ↑B k )) = ↑(pre S (↑B k ) ∩ (I \ ↑B k )) [Lemma 4.1] = ↑((pre S (↑B k ) ∩ I ) \ ↑B k )
Let us now prove, by induction on k, that U k = ↑B k for every k with 0 ≤ k < ℓ B . The basis U 0 = ↑B 0 follows from lines 1-5 of BCwP and from the definition of U 0 . For the induction step, let k ∈ N with k + 1 < ℓ B , and assume that U k = ↑B k . Line 10 entails that

↑B k +1 = ↑B k ∪ ↑P k . It follows that ↑B k+1 = ↑B k ∪ ↑P k = ↑B k ∪ ↑((pre S (↑B k ) ∩ I ) \ ↑B k ) = U k ∪ ↑((pre S (U k ) ∩ I ) \ U k ) [U k = ↑B k ] = U k ∪ ↑(pre S (U k ) ∩ I ) = U k +1 This concludes the proof that U k = ↑B k for every k with 0 ≤ k < ℓ B .
Moreover, coming back to the characterization of ↑P k , we get that

↑P k = ↑((pre S (↑B k ) ∩ I ) \ ↑B k ) = ↑((pre S (U k ) ∩ I ) \ U k ) = ↑(U k+1 \ U k )
for every k with 0 ≤ k < ℓ P . □ Theorem 4.4. The procedure BCwP terminates on every input and is correct.

Proof. Let us first prove termination. We need to show that any maximal execution of BCwP(S, s f inal , I ) is finite. By contradiction, assume that ℓ B = ∞. According to Lemma 3.1, there exists an index h ∈ N such that U h = U h+1 . We derive from Lemma 4.3 that P h = ∅. Therefore, the execution should terminate at line 9 during the (h + 1) th iteration of the while loop. This contradicts our assumption that ℓ B = ∞.

We now turn our attention to the correctness of BCwP. As it is finite, any maximal execution of BCwP(S, s f inal , I ) either returns False at line 9 or returns True at line 11.

• If it returns False then P ℓ P -1 = ∅ and it follows from Lemma 4.3 that

U ℓ P ⊆ U ℓ P -1 . It follows that U ℓ P -1 = k U k .
Moreover, s init ↑B ℓ P -1 because the condition of the while loop had to hold. It follows hat s init k U k . We derive from Lemma 3.2 that s f inal Cov S .

• If it returns True then s init ∈ ↑B ℓ B -1 and it follows from Lemma 4.3 that

s init ∈ U ℓ B -1 ⊆ k U k . We derive from Lemma 3.2 that s f inal ∈ Cov S .
This concludes the proof of the theorem. □

In the next section we focus our algorithm on lossy channel systems.

LOSSY CHANNEL SYSTEMS

Lossy channel systems (LCSs) have been introduced by Abdulla and Jonsson to verify protocols that are designed to operate correctly even in presence of messages losses [START_REF] Abdulla | Verifying Programs with Unreliable Channels[END_REF]. Informally, an LCS is a finite-state automaton equipped with finitely many first-in first-out channels that are unreliable in the sense that messages can be lost at any time. This section recalls the definition of LCS and shows how to verify them using the BCwP algorithm of the previous section.

Syntax and Semantics of LCSs

A lossy channel system is a tuple S = (Q, q init , M, d, ∆) where Q is the finite set of locations, q init ∈ Q is the initial location, M is the finite alphabet of messages that can be exchanged over the channels, d is the number of channels, and ∆ ⊆ Q × Op × Q is the set of transition rules, where Op = {1, . . . , d} × {!, ?} × M is the set of operations over the channels. An operation is

• either a transmission i!m of a message m into a channel i,

• or a reception i?m of a message m from a channel i.

Example 5.1. Figure 1 represents the LCS with locations Q = {q 1 , q 2 , q 3 , q bad }, initial location q init = q 1 , messages M = {a, b}, a single channel, and rules

∆ = {q 1 1!a ---→ q 2 , q 2 1!b ---→ q 1 , q 2 1?a ---→ q 3 , q 3 1?a ---→ q bad }. □
The operational semantics of an LCS S = (Q, q init , M, d, ∆) is given by an infinite-state transition system S = (S, s init , →) defined as follows. The set of states is S = Q × (M * ) d . So a state s = (q, w 1 , . . . , w d ) is composed of a location q and of words w i describing the contents of the channel i. All channels are empty initially, so the initial state is s init = (q init , ε, . . . , ε).

For each rule δ = (q, op, q ′ ) in ∆, we define the binary relation δ -→ over S as follows: s δ -→ s ′ with s = (q, w 1 , . . . , w d ) and s ′ = (q ′ , w ′ 1 , . . . , w ′ d ) if and only if • either op is a transmission i!m, in which case w ′ i = w i • m and w ′ j = w j for all j i, • or op is a reception i?m, in which case m • w ′ i = w i and w ′ j = w j for all j i. q 1 q 2 q 3 q bad 1!b 1!a 1?a 1?a Figure 1: Simple example of a lossy channel system.

The relations δ -→ capture the perfect semantics of first-in firstout channels. To capture message losses, we also define the binary relation → λ over S. Formally, s → λ s ′ with s = (q, w 1 , . . . , w d ) and s ′ = (q ′ , w ′ 1 , . . . , w ′ d ) if and only if the locations q and q ′ are the same and there exists a channel i ∈ {1, . . . , d} such that w ′ i is obtained from w i by deleting one message (i.e.,

w i = u • m • v and w ′ i = u • v,
for some m ∈ M and u, v ∈ M * ) and w ′ j = w j for all j i. For example, (q 2 , a • b • a) → λ (q 2 , a • a). We also introduce, for technical reasons, the identity relation {(s, s) | s ∈ S }, written → ε . Now, the binary relation → over S is defined to be the union of the relation → ε , of the relation → λ and of the relations δ -→ where δ ranges over ∆.

Example 5.2. Consider again the LCS depicted in Figure 1. The state (q bad , ε) is reachable from the initial state because (q 1 , ε) → (q 2 , a) →→ (q 2 , aba) → λ (q 2 , aa) →→ (q bad , ε). But a message loss (i.e., a → λ step) is required to do so. □

LCSs Are Well-Structured

As was already observed in [START_REF] Abdulla | Algorithmic Analysis of Programs with Well Quasi-ordered Domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF], lossy channel systems are wellstructured, and so coverability is decidable for them. The wellstructure of LCSs allows us to use the algorithm presented in Section 4. But we need to show that the required effectivity conditions are fulfilled. Let us start by recalling how LCSs can be framed as well-structured transition systems.

For two words u and v in M * , we say that u is a subword of v, written u ⪯ v, if u can be obtained from v by erasing some letters. In other words, u is a (possibly non-contiguous) subsequence of v. The relation ⪯ is obviously a partial ordering1 on M * . Moreover, it is wqo on M * . This last result is due to Higman [START_REF] Higman | Ordering by Divisibility in Abstract Algebras[END_REF].

Given an LCS S = (Q, q init , M, d, ∆), we define the relation ≤ over S = Q × (M * ) d as follows. For two states s = (q, w 1 , . . . , w d ) and s ′ = (q ′ , w ′ 1 , . . . , w ′ d ), let s ≤ s ′ if and only if q = q ′ and w i is a subword of w ′ i for every i ∈ {1, . . . , d}. It is readily seen that this relation is a partial ordering on S. The following lemma is an easy consequence of the definitions of → λ and ≤.

Lemma 5.3. The relations ≥ and (→ λ ) * are equal.

It follows from the previous lemma that coverability and reachability coincide for lossy channel systems (equipped with ≤). Indeed, if there exists a state s ∈ S such that s init * -→ s ≥ s f inal then

s init * - → s * - → s f inal hence s init * - → s f inal .
The converse always holds by reflexivity of ≤. Lemma 5.4 ([3,[START_REF] Finkel | Well-structured transition systems everywhere![END_REF]). The semantics of a lossy channel system, equipped with the partial order ≤, is a WSTS. Proof. Since the set Q of locations is finite, equality is a wqo on Q. Recall that ⪯ is a wqo on M * . It follows that ≤ is a wqo on S. It remains to prove that ≤ is compatible with the relation →. Consider three states s, s ′ and t such that s → s ′ and s ≤ t. By Lemma 5.3, it holds that t * -→ s. Therefore, t * -→ s → s ′ = t ′ , which concludes the proof that ≤ is compatible with →. □

As mentioned previously, we want to solve the coverability problem for lossy channel systems using the BCwP algorithm of Section 4. But several effectivity conditions need to be fulfilled in order to do so, even if we use the trivial invariant I = S.

Firstly, we observe that the partial order ≤ is computable because there are only finitely many channels and ⪯ itself is computable.

Secondly, we need to show LCSs admit an effective pre-basis, meaning that there exists an algorithm that, given a state s, computes a finite basis of ↑pre S (↑s). Toward this end, we introduce two functions cpre ! and cpre ? from M × M * to M * defined as follows:

cpre ! (m, w) = w ′ if w = w ′ • m w otherwise cpre ? (m, w) = m • w
See examples in Figure 2. Now, for a state s = (q, w 1 , . . . , w d ) and a rule δ = (p, i#m, q) ∈ ∆, with # ∈ {!, ?}, we let cpre δ (s) = (p, w 1 , . . . , w i-1 , cpre # (m, w i ), w i+1 , . . . w d ). It is readily seen that cpre δ is computable. The following lemma shows that LCSs admit an effective pre-basis.

Lemma 5.5. For every state s = (q, w 1 , . . . , w d ) in S, the set {s} ∪ {cpre δ (s) | δ = (p, op, q) ∈ ∆} is a finite basis of ↑pre S (↑s).

Thirdly, line 10 of the BCwP algorithm simply amounts to the computation of the minimal elements of B ∪ P.

We now have a way to solve the coverability problem for LCSs. To accelerate the computation we need good invariants. The next sections aim to provide that.

Simple Regular Expressions

The BCwP algorithm of Section 4 makes use of downward-closed invariants in order to accelerate the classical backward coverability analysis. Invariants are potentially infinite sets of states. So before attempting to generate good invariants, we need a finite representation for them. As there are only finitely many locations, the complexity comes from channel contents. These are d-tuples of words over the finite alphabet M of messages. A natural and simple approach consists in using recognizable subsets of (M * ) d to represent (potentially infinite) sets of channel contents. This is a reasonable limitation since the coverability set of an LCS, which is its most precise downward-closed invariant, is recognizable [START_REF] Abdulla | Verifying Programs with Unreliable Channels[END_REF][START_REF] Cécé | Unreliable Channels are Easier to Verify Than Perfect Channels[END_REF]. By Mezei's theorem, recognizable subsets are finite unions of cartesian products of regular languages over the alphabet M. Since we are interested in downward-closed invariants, we focus on downwardclosed regular languages. Such languages can be represented by simple regular expressions [START_REF] Abdulla | On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels[END_REF].

Let us recall the definition of simple regular expressions. An atom is either (ε + m) for a message m in M or (m

1 + • • • + m n ) * where m 1 , . . . , m n are messages in M with n ≥ 1. A product is a finite concatenation a 1 • • • a n of atoms. A simple regular expression (SRE) is a finite sum p 1 + • • • + p n of products.
The language of an SRE r is the regular language associated with it and will be denoted by r . The following lemma gives us a reason to use SREs to represent downward-closed regular languages.

Lemma 5.6 ([2]

). A language L ⊆ M * is downward-closed if and only if it can be represented by an SRE.

In practice, it is desirable for efficiency reasons to manipulate SREs that do not contain redundancies. We say that a product p = e 1 • • • e n is in normal form [START_REF] Abdulla | On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels[END_REF] if and only if for all 1 ≤ i ≤ n, we have e i • e i+1 ⊈ e i+1 and e i .e i+1 ⊈ e i . An SRE p 1 + . . . +p n is in normal form if all products p i are in normal forms and there are no products p i and p j with i j such that p i ⊆ p j .

Lemma 5.7 ([2]

). For every SRE r , there is a unique (up to commutativity of +) SRE in normal form, which is denoted by nf(r ), such that nf(r ) = r . Furthermore, nf(r ) can be computed from r in quadratic time.

We can see that there exist infinite increasing sequences of SREs. This means that we cannot directly use SREs to compute downward-closed invariants via Kleene iteration. Let us illustrate this issue on the LCS of Figure 1. Applying Kleene iteration to the loop q 1 1!a ---→ 1!b ---→ q 1 leads to the sequence ε, (a + ε) • (b + ε), (a +ε)•(b +ε)•(a +ε)•(b +ε), etc. There exist acceleration techniques that can derive the effect of an arbitrary iteration of the loop [START_REF] Abdulla | On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels[END_REF], and come up with (a +b) * . But, in general, the coverability set of an LCS cannot be computed [START_REF] Mayr | Undecidable problems in unreliable computations[END_REF] even though it is downward-closed and, hence, recognizable. Therefore, we settle for over-approximations of the coverability set. In the next section, we will introduce a subclass of SREs, that we call compact simple regular expressions, and show how to use it to compute downward-closed invariants.

INVARIANT USING COMPACT SRES

Despite the assumption that messages may be lost, all messages that remain in a channel are in the same order as the order in which they were sent. If a system sends some messages a and then some messages b in a channel, this channel can't contain a word that contains a message b after a message a. In this section, we propose an abstraction of channel contents that focuses on this kind of properties, and ignores the numbers of occurrences of messages. For instance, this abstraction provides properties of the type: it's not possible to have a message a after a message b.

We present an invariant generation technique that uses a subclass of SREs, that we call compact simple regular expressions. The idea is to abstract the contents of a channel with simple expressions of the form

(a * • b * ) + (a * • (c + d) * ).
Formally, a compact simple regular expression (CSRE) is an SRE p i where every product p i is a compact product. A compact product is of the form a 1 • • • a n with every atom a i of the form (m 1 + • • • +m n ) * and such that every two atoms a i and a j with i j have distinct messages (i.e., a i ∩ a j = {ε}). Some examples of CSREs are given in Figure 3. We see that every compact product is in normal form. However, not all CSREs are in normal forms. We note CSRE nf the set of CSREs in normal form. It is readily seen that this set is finite. The CSREs of Figure 3 are all in normal form. We define the binary relation ⊑ over CSRE by r 1 ⊑ r 2 if and only if r 1 ⊆ r 2 . This relation is reflexive and transitive hence it is a quasi-ordering. The relation ⊑ is also antisymmetric for CSREs in normal form, therefore ⊑ is a partial order over CSRE nf . Note that ⊑ is not antisymmetric over the full class of CSREs (e.g.,

csre 1 = (a * • b * ) + (a * • c * ) csre 3 = ε csre 2 = ((a + b) * ) + ((c + d) * • e * ) csre 4 = ∅
(a + b) * = (a + b) * + a * ).
We will exhibit a Galois connection between (P(M * ), ⊆) and (CSRE nf , ⊑). The two following lemmas are needed to do so. Lemma 6.1. Consider two subsets of messages

A 1 , A 2 ⊆ M. For every languages L 1 ⊆ (M \ A 1 ) * and L 2 ⊆ (M \ A 2 ) * , it holds that (A * 1 • L 1 ) ∩ (A * 2 • L 2 ) = (A * • (L 1 ∩ B * 2 • L 2 )) ∪ (A * • (L 2 ∩ B * 1 • L 1 )) where A = A 1 ∩ A 2 , B 1 = A 1 \A 2 and B 2 = A 2 \A 1 .
Proof. We only prove ⊆ since the converse inclusion is imme-

diate. Let w ∈ (A * 1 • L 1 ) ∩ (A * 2 • L 2 ). There exists u 1 ∈ A * 1 , v 1 ∈ L 1 , u 2 ∈ A * 2 and v 2 ∈ L 2 such that w = u 1 • v 1 = u 2 • v 2 .
Assume that the length of u 1 is smaller than or equal to the length of u 2 . There exists u ′ 2 such that

u 2 = u 1 •u ′ 2 . It follows that u 1 ∈ (A 1 ∩ A 2 ) * = A * . Observe also that v 1 = u ′ 2 • v 2 . Since v 1 ∈ L 1 ⊆ (M \ A 1 ) * , we get that u ′ 2 ∈ (A 2 \A 1 ) * = B * 2 , and so v 1 ∈ (B * 2 • L 2 ). We have shown that w ∈ (A * • (L 1 ∩ B * 2 • L 2 )
). Symmetrically, if the length of u 1 is larger than or equal to the length of u 2 , then w ∈ (A * • (L 2 ∩ B * 1 • L 1 )). □ Lemma 6.2. The set of languages that can be represented by CSREs is closed under intersection.

Proof. We show that the intersection of the languages of two compact products can be represented by a CSRE. The lemma then follows by distributivity of intersection over union and by closure of CSREs under sum. For a compact product p = a 1 • • • a n , we write |p| the number n of atoms composing p. We prove by induction on k ≥ 0, that for all compacts products p 1 and p 2 such that |p 1 | + |p 2 | ≤ k, there exists a CSRE r such that p 1 ∩ p 2 = r . For the basis step, we have p 1 = p 2 = ε and p 1 ∩ p 2 = ε . For the induction step, let p 1 and p 2 two compact products such that

|p 1 | + |p 2 | = k + 1.
If one them is equal to ε then p 1 ∩ p 2 = ε . Otherwise, p 1 and p 2 may be written as the compact products

p 1 = A * 1 • p ′ 1 and p 2 = A * 2 • p ′ 2 where A 1 and A 2 are two subsets of M. Note that p ′ 1 ⊆ (M \ A 1 ) * and p ′ 2 ⊆ (M \ A 2 ) * . We get from Lemma 6.1 that p 1 ∩ p 2 = (A * • ( p ′ 1 ∩ B * 2 •p ′ 2 )) ∪ (A * • ( p ′ 2 ∩ B * 1 •p ′ 1
)) where A, B 1 and B 2 are defined as in the lemma. Observe that

|p ′ 1 | + |B * 2 • p ′ 2 | = |p ′ 2 | + |B * 1 • p ′ 1 | = k.
It follows from the induction hypothesis that there exists two CSREs r 1 and r 2 such that

r 1 = ( p ′ 1 ∩ B * 2 • p ′ 2 ) and r 2 = ( p ′ 2 ∩ B * 1 • p ′ 1 )
. We obtain that

p 1 ∩ p 2 = A * • r 1 + A * • r 2 . It is routinely checked that r 1 a * • b * ∩ b * • a * = a * ∪ b * a * • b * ∩ (a + b) * = a * • b *
(M * ) → CSRE nf is defined by α(L) = nf( {r ∈ CSRE nf | L ⊆ r }).
The function α is well-defined because CSRE nf is closed by intersection and is finite. Note that α(L) is computable when L is a regular language. We observe that (α, γ ) is a Galois connection between (P(M * ), ⊆) and (CSRE nf , ⊑). In order to apply the classical framework of abstract interpretation [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF], it remains to show that we can perform abstractly the operations over the channels, namely transmissions and receptions.

For a language L ⊆ M * , let

m -1 L = {w ⊆ M * | m • w ∈ L}.
Following the classical framework of abstract interpretation, an abstract transmission is defined by (!m) # (r ) = α( r • m) and an abstract reception is defined by (?m) # (r ) = α(m -1 • r ). Let us show how to compute (!m) # (r ) and (?m) # (r ) given a CSRE r in normal form. We only need to consider the case where r is a compact product since

(!m) # (p 1 + • • • + p n ) = nf((!m) # (p 1 ) + • • • + (!m) # (p n )),
and similarly for (?m) # .

For a compact product p = a 1 • • • a n , let merдe(a 1 • • • a n ) denote the atom that contains exactly the messages that appear in a 1 , . . . , a n . Formally, merдe(a

1 • • • a n ) is the atom A * where A = {m ∈ M | m ∈ a 1 ∪ • • • a n }.
We have for a compact product p = a 1 • • • a n and a message m ∈ M:

(!m) # (p) = a 1 • • • a k -1 • merдe(a k • • • a n ) if m ∈ p p • m * otherwise (?m) # (p) = a k • • • a n if m ∈ p ∅ otherwise
where, in both cases, k the unique index such that m ∈ a k . By a standard construction, we can extend the Galois connection (α, γ ) into a Galois connection between (P(S), ⊆) and the abstract domain consisting of the set of maps from Q to CSRE d nf , partially ordered by the component-wise extension of ⊑. So we can apply the classical framework of abstract interpretation [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF] to generate an inductive downward-closed invariant by a standard fixpoint computation in this abstract domain. Since the set CSRE nf is finite, the fixpoint computation is guaranteed to converge. We may then use this downward-closed invariant to accelerate the backward coverability analysis, as is done in the BCwP algorithm of Section 4. However, this acceleration comes at a price: the generation of the invariant itself might be costly. We illustrate this issue in the following example. Example 6.3. Consider an alphabet M containing the distinct messages x 1 , y 1 , z 1 , . . . , x n , y n , z n . Let L ⊆ M * be the language all i ∈ {1, . . . , n}. There are exponentially many such products. Observe that r is in normal form. □

The potential exponential blow-up illustrated in Example 6.3 may limit, in practice, the usefulness of our invariant generation technique based on CSREs. See Section 9 for experimental results. The next section aims at solving this problem.

INVARIANT USING ORDERING FLOWS

In the last section, we saw how to generate downward-closed invariants by an abstraction of channel contents that ignores the numbers of occurrences of messages and only cares about their respective order. This abstraction relies on so-called compact simple regular expressions (CSREs). However, the generation of this invariant might be costly in practice. This comes from the fact that CSREs are, in fact, not compact enough (see Example 6.3).

We now present an invariant generation technique based on quasi-orderings (i.e. transitive and reflexive relations) over messages, that we call message ordering flow (MOFs). The goal is still the same: we want to keep track of which messages can be in which order in each channel. But we want an invariant that is faster to compute than the one based on CSREs.

Let M denote the set of messages of an LCS for which we want to compute a downward-closed invariant. A message ordering flow (MOF) is a pair (A, R) where A ⊆ M and R is quasi-ordering over A. We let MOF denote the set of MOFs. We define the partial ordering ⊑ over MOF by

F 1 ⊑ F 2 with F 1 = (A 1 , R 1 ) and F 2 = (A 2 , R 2 ) if and only if A 1 ⊆ A 2 and R 1 ⊆ R 2 .
The least upper bound of two MOFs

F 1 = (A 1 , R 1 ) and F 2 = (A 2 , R 2 ) is F 1 ⊔ F 2 = (A, R) where A = A 1 ∪ A 2 and R = (R 1 ∪ R 2 ) + , i.e., the transitive closure of R 1 ∪ R 2 .
The greatest lower bound of F 1 and F 2 is

F 1 ⊓ F 2 = (A, R) where A = A 1 ∩ A 2 and R = R 1 ∩ R 2 .
As in Section 6, we want to exhibit a Galois Connection between (P(M * ), ⊆) and (MOF, ⊑). It is readily seen that the concretisation of a MOF is a downwardclosed language. But the set γ (MOF ) of languages that can be represented by a MOF misses an important language, namely the empty language. So we extend the set MOF with a new element, written ⊥, whose concretisation is γ (⊥) = ∅. Conversely, the abstraction of the empty language is α(∅) = ⊥. We also extend ⊑ in the obvious way. For every MOF F , we have ⊥ ⊔ F = F and ⊥ ⊓ F = ⊥.

Observe that, by construction, (α, γ ) is a Galois connection between (P(M * ), ⊆) and (MOF, ⊑). As in Section 6, in order to apply the classical framework of abstract interpretation [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF], it remains to show that we can perform abstractly the operations over the channels, namely transmissions and receptions. • (!m)

# (⊥) = (?m) # (⊥) = ⊥. • (!m) # (A, R) = (A ′ , R ′ ) where A ′ = A ∪ {m} and R ′ = R ∪ (A × {m}) ∪ (B × B) where B = {b ∈ A | (m, b) ∈ R} is the set of all messages that can appear after m. • (?m) # (A, R) = ⊥ if m A, otherwise (?m) # (A, R) = (A ′ , R ′ )
where A ′ = {b ∈ A | (m, b) ∈ R} is the set of all messages that can appear after m and R ′ = R ∩ (A ′ × A ′ ). As with CSREs, we can extend the Galois connection (α, γ ) into a Galois connection between (P(S), ⊆) and the abstract domain consisting of the set of maps from Q to MOF d , partially ordered by the component-wise extension of ⊑. Again, we can generate an inductive downward-closed invariant by a standard fixpoint computation in this abstract domain. Since the set MOF is finite, the fixpoint computation is guaranteed to converge. We may then use this downward-closed invariant in the BCwP algorithm of Section 4.

On the contrary to CSREs that can suffer from an exponential blow-up, each MOF is of size at most quadratic in the cardinal of the alphabet M of messages of the LCS under analysis.

Example 7.1. Let us revisit Example 6.3. Recall that the language L defined there is

L = x 1 * • (y 1 * + z 1 * ) • x 2 * • (y 2 * + z 2 * ) • • • x n * • (y n * + z n * )
This language can be represented by the MOF F = (A, R) where A contains exactly the messages x 1 , y 1 , z 1 , . . . , x n , y n , z n and R respects the quasi-ordering shown in Figure 5, that is, R is the reflexive and transitive closure of the arrows depicted in that figure. On the contrary to the minimal CSRE representing L, which is exponential in n, the size of F is quadratic in n. □

INVARIANT WITH STATE INEQUATION

The last two invariants focused on the order of messages in the channels. Neither invariant takes into account the number of messages. We now present an invariant based on the Petri net state equation. It is a simple invariant that just counts the number of messages that can be in each channel. The state equation was recently used successfully for solving Petri net coverability problems [START_REF] Blondin | Approaching the Coverability Problem Continuously[END_REF][START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF][START_REF] Geffroy | Occam's Razor Applied to the Petri Net Coverability Problem[END_REF].

Inspired by the state equation for Petri nets, we associate to an LCS and a state s f inal = (q f inal , w 1 , . . . , w d ), a system of inequations that must be satisfiable when s f inal is coverable. This system is defined over a vector x of free variables ranging over Z ∆ . Intuitively, x(δ ) denotes the number of times an execution uses the rule δ to cover the state s f inal .

We first build a system of equations over x, called the location constraints that takes into account the number of times an execution enters and leaves a location. To do so, we introduce the vector e i in Z Q defined as zero everywhere except for the index i where it is one. We denote by LC s f inal (x) the following system of equations:

e q ini t + δ =(p,op,q)∈∆ x(δ )(-e p + e q ) = e q f inal (1)
Next, we build a system of inequalities over x, called the channel constraints that counts the number of times each message m is sent and received in each channel i. To do so, we introduce the vector e i,m defined as the matrix in Z d ×|M | where the value is zero everywhere except for the index i, m where it is one. Given a word w of messages, we denote by |w | m the number of occurrences of m in w. We denote by CC s f inal (x) the following system of inequations where the inequality ≥ over the matrices is defined componentwise:

δ =(p,i!m,q)∈∆ x(δ )e i,m - δ =(p,i?m,q)∈∆ x(δ )e i,m ≥ m ∈M i ∈ {1,...,d } |w i | m (2)
Finally, we introduce the system of equations SI s f inal (x) defined as the conjunction LC s f inal (x) ∧ CC s f inal (x). The proof of the following lemma is immediate by observing that if s f inal is coverable there exists an execution from s init to a state s ≥ s f inal . Denoting by x(δ ) the number of times the rule δ is used by this execution, we get a vector x satisfying SI s f inal (x).

Lemma 8.1. The system SI s f inal (x) is satisfiable for every coverable configuration s f inal .

Corollary 8.2. The set I LCS = {s f inal | ∃x SI s f inal (x)} is an invariant.

EXPERIMENTAL EVALUATION

We have presented a coverability checking algorithm, namely BCwP, that is parametrized by a downward-closed invariant. The algorithm uses this invariant in order to accelerate the classical backward coverability analysis. We have also presented three different invariant generation techniques, respectively based on compact simple regular expressions (CSREs), on message ordering flows (MOFs) and on the state inequation (SI). We now present our experimental results.

We want to evaluate two main effects of the invariants: the number of states handled and the time saved or added. On one hand, if the algorithm handles less states (computes less states with cpre, prunes more), this leads to a gain in time. On the other hand, an invariant can also slow down the computation in two ways: firstly for the generation of the invariant itself and secondly for checking membership of a given state in the invariant.

We have implemented the BCwP algorithm in the language OCaml. The prototype consists of a little more than three thousand lines of code. It can be found online [START_REF] Geffroy | coverability checker for LCS[END_REF]. It only works for lossy channel systems but, as it is modular, it can be extended to all well-structured transition systems with decidable order and effective pre-basis. New invariants can also be added easily. The state inequation invariant needs the help of an SMT-solver. We chose Z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF]. Our experiments were run on a machine running Ubuntu Linux 14.04, with an Intel invariants CSRE and MOF and to check if state is in the invariant or not. Table 4 shows for each invariant the time spent before starting the algorithm and the total time spent checking if a state is in the invariant. We see that the state inequation is very fast to precompute. The reason is that it just needs to write the inequation for the SMT-solver Z3. Satisfiability checks are only accounted for in the times to check membership in the invariant. The invariant CSRE can take too much pre-computation time as illustrated with Example 6.3 in Section 6. The MOF invariant was able to do the computation in less time excepted for the Peterson protocols with four peers. Note that, unlike Z3, the least fixpoint module was not carefully coded with performance in mind.

The MOF and CSRE invariants have a similar pruning impact (see Table 3), but we see that MOF was better overall. It pruned less in a few examples but the biggest gap was between 5.3% against 0% for server. And in 6 examples out of 11 where they both finished they pruned exactly the same states. Because the pre-computation times are better for MOF, the invariant MOF is better than CSRE.

Regarding the SI invariant, we observe in Tables 3 and4 that it did not prune states for the models BAwCC and BAwPC but it still cost time. Recall that the state inequation keeps track of the numbers of messages in each channel. This means that it was not helpful to have this information for these models.

Remark 9.1. We did not present results using combinations of invariants, but this is of course possible. Indeed, the intersection of downward-closed invariants is also a downward-closed invariant. In practice, we do not compute the intersection: if we have two invariants I 1 and I 2 , we prune a configuration c if, and only, if c I 1 or c I 2 . Our prototype is capable of using any combination of the invariants SI , CSRE and MOF. It turns out that such combinations are worse than single invariants for our examples. For instance, our hardest examples (Peterson3 and Peterson4) do not benefit from SI +MOF, because the time needed for the pre-processing of MOF is greater than the time to solve the coverability question with SI . This does not mean that combinations of invariants have no interest, they could be useful for other models. □

Overall we see that, for most examples, at least one invariant was able to accelerate the computation.

Lemma 3 . 1 .

 31 The sequence U 0 ⊆ U 1 ⊆ •

Lemma 4 . 1 .

 41 Let D be a downward-closed set of S. For every finite subset X ⊆ S, it holds that ↑pre S ((↑X ) ∩ D) = ↑(cpre S (X ) ∩ D). Proof. We first prove that the equality ↑((↑Y ) ∩ D) = ↑(Y ∩ D) holds for every finite set Y and for every downward closed set D. First of all, notice that Y ∩ D ⊆ (↑Y ) ∩ D ⊆ ↑((↑Y ) ∩ D). It follows that ↑(Y ∩ D) ⊆ ↑((↑Y ) ∩ D). Conversely, let s ∈ ↑((↑Y ) ∩ D). There exists d ∈ (↑Y ) ∩ D such that d ≤ s. As d ∈ ↑Y , there exists y ∈ Y such that y ≤ d. As D is downward closed, we derive from y ≤ d that y ∈ D. Thus y ∈ Y ∩ D. From y ≤ d ≤ s we get s ∈ ↑y ⊆ ↑(Y ∩ D).

ALGORITHM 1 :

 1 BCwP(S, s f inal , I ).

5 while s ini t ↑B do 6 N 7 P 8 if P = ∅ then 9 return False 10 Let

 678910 ← (cpr e S (B)) \ ↑B /* new predecessors */ ← N ∩ I /* prune uncoverable states */ B be a finite basis of ↑(B ∪ P ) 11 return True Lemma 4.3. For every k with 0

Figure 2 :

 2 Figure 2: Example of cpre ! and cpre ? .

Figure 3 :

 3 Figure 3: Examples of compact simple regular expressions.

Figure 4 :

 4 Figure 4: Examples of intersections of compact products.

  Let us start with the abstraction function α : P(M * ) → MOF . For a word w ∈ M * , let α(w) = (A, R) ∈ MOF where A = {m ∈ M | m ⪯ w } is the set of all messages occurring in w and R = {(a, b) ∈ A × A | a = b ∨ ab ⪯ w }. Recall that ⪯ is the sub-word partial order on M * . For a non-empty language L ⊆ M * , we define α(L) to be the least upper bound of {α(w) | w ∈ L}. The concretisation function γ : MOF → P(M * ) is defined by γ (A, R) = {w ∈ A * | ∀ab ⪯ w, (a, b) ∈ R}.

Figure 5 : 3 .

 53 Figure 5: MOF for the language L of Example 6.3.

  • • is ultimately stationary. It holds that s f inal ∈ Cov S if, and only if, s init ∈ k U k . there exists s 0 , . . . , s n ∈ S such that s init = s n , s n → s n-1

	Proof. Every infinite non-decreasing (w.r.t. ⊆) sequence of up-
	ward-closed sets is ultimately stationary since ≤ is a wqo.	□
	Lemma 3.2. Proof. If s f inal ∈ Cov S then s init	* -→ s ≥ s f inal for some
	states s in S. Since s init	* -→ s,

Recall that a partial ordering on a set S is binary relation on S that is reflexive, transitive and antisymmetric.

CONCLUSION

We have presented in this paper a backward coverability algorithm for WSTSs, parametrized by downward-closed forward invariants. We have introduced three new invariants for lossy channel systems. One of these invariants counts messages and the other two keep track of the order of messages. We have implemented a prototype to assess the efficiency of these invariants. Our experimental evaluation shows an acceleration of the classical approach for two of the three invariants. As future work, we intend to apply these techniques to verify safety properties on weak-memory models because they are closely related to LCSs [6].

Our prototype takes as input a system of communicating finitestate automata, each with their own locations and rules, given in the scm file format. We build (on-the-fly) a global LCS by taking the cartesian product of these automata. While the CSRE and MOF invariants are computed on this global LCS, we optimize the state inequation invariant to avoid an exponential blow-up in Equation [START_REF] Abdulla | The Benefits of Duality in Verifying Concurrent Programs under TSO[END_REF]. Instead of applying Equation (1) to the global LCS, we create one equation for each automaton. The two systems are equivalent but the membership problem in the latter is easier.

The different examples come with the tool McScM [START_REF] Heußner | McScM: A General Framework for the Verification of Communicating Machines[END_REF]. We present the results of 13 examples. The examples BAwCC, BAwPC, BAwCC_enh and BAwPC_enh are business protocols and came from [START_REF] Ravn | Modelling and Verification of Web Services Business Activity Protocol[END_REF]. The first two are coverable examples and the last two are their enhanced uncoverable versions. Others examples include two versions of the Peterson protocol, one with three peers, the other with four, a version of the pop3 protocol, a simple server protocol and a tcp protocol with and without an error inserted, and finally a ring protocol. Many examples have tens of target states, and our prototype can handle that. Even though we presented our algorithm to solve the coverability problem for only one target state, it is easy to extend the algorithm for a set of targets, by taking U 0 = ↑(S f inal ∩ I ) where S f inal is the set of all target states.

We were unable to compare our prototype with TReX [5] because the tool is not available anymore. So we compared with McScM [START_REF] Heußner | McScM: A General Framework for the Verification of Communicating Machines[END_REF], which uses the same scm format and can solve the coverability problem for LCS, even though this is not its primary goal. McScM has four verification engines. The best engine suited to our examples was cegar. It was able to solve 10 of 13 examples within three minutes but crashed with Peterson4 and was not finished after two hours for brp and BAwCC_enh. In comparison, our prototype solved all cases with the invariant state inequation. Without invariant and with the invariant MOF it was able to solved all examples except two and with the invariant CSRE all except three.

Table 1 compares the time needed to solve the coverability problem without invariant, noted ∅, and with the invariants SI , CSRE and MOF. The least time is reported in the fifth column. In the last column, we put the time needed by McScM with the best engine for each example. We can see that SI dramatically accelerates the computation in the biggest examples. The same effect is also found for the invariant MOF except for the Peterson4 protocol where MOF did not terminate within 96 hours. Those numbers can be explained by the numbers of operations that the algorithm performed. Table 2 compares the numbers of nodes visited, i.e., the numbers of targets states added each step with all states created by the cpre in line 6 before removing those that are already in ↑B. Sometimes the number of visited states is very low compared to the version without invariant. For example for the invariants CSRE and MOF for the examples BAwCC_enh and BAwPC_enh it is 59 and 44 compared to 38218 and 19193. It is because the invariants were able to prune all targets states. Therefore the algorithm did not even enter the while loop.

To understand more specifically the pruning for each invariant and each example, we provide Table 3. It shows the number of times the algorithm tested if a state was or was not in the invariant, as well as the percentage of times the state was outside the invariant and hence was pruned.

We see that many times the algorithm was able to prune some states and therefore to decrease the number of states handled. This comes at a cost, since we need to compute a least fixpoint for the


Antoine Marot

Benjamin Donnot

Camilo Romero

Luca Veyrin-Forrer

Marvin Lerousseau

Balthazar Donon

Isabelle Guyon

Learning to run a power network challenge for training topology controllers

Keywords: Artificial Intelligence, Control, Power Flow, Reinforcement Learning, Competition

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

I. INTRODUCTION

Grid operators are in charge of ensuring that a reliable supply of electricity is provided everywhere, at all times. However, their task is becoming increasingly difficult under the current steep energy transition. On one hand, we observe the advent of intermittent renewable energies on the production side and of prosumers on the demand side, coupled to the globalization of energy markets over a more and more interconnected European grid. This brings a whole new set of actors to the power system, adding lots of uncertainties to it. On the other hand, recent improvements in terms of energy efficiency have put an end to the total consumption growth, and de facto to the growth in revenues, thus limiting new costly investments. Public acceptance with regards to the installation of new infrastructure is also a growing issue. This shifts the way we traditionally develop the grid, from expanding its capacity by building new power lines, to optimizing the existing one as it is, closer to its limits, with rather digital means and every flexibilities at our disposal.

Currently, operators must analyze massive amounts of data to take complex coordinated decisions over time with higher reactivity, to operate under an ever more constrained environment with greater control. An under-exploited flexibility, which could alleviate in part the problem, is the grid topology, as already pointed out by early work [START_REF] Bacher | Network topology optimization with security constraints[END_REF]. This avenue is explored in the present paper. As of today, it is still beyond the state-of-the-art to control optimally such grid topology "at scale", beyond the level of "branch switching" [START_REF] Fisher | Optimal branch switching[END_REF] (e.g. considering more complex actions such as "bus splitting"), because of the non-linear and combinatorial nature of the problem. Lately, we demonstrated an augmented expert system ability [START_REF] Marot | Expert system for topological remedial action discovery in smart grids[END_REF] to discover steady-state tactical solutions to unsecure grid states by relying on bus splitting. Its acceptable computational time opens new perspectives for a revival of such class of actions. In addition, novel and more flexible actions should also be considered today, intervening not only instantaneously as a tactic rather independently of other decisions, but over a time horizon as a strategy to manage more numerous overlapping and interfering decisions. To exploit such a complex array of actions, optimal control methods [START_REF] Fisher | Optimal branch switching[END_REF] have been explored but are hard to deploy in control rooms because of limited computing budget constraints.

With the latest breakthroughs in Artificial Intelligence (AI) from AlphaGo at Go [START_REF] Silver | Mastering the game of go with deep neural networks and tree search[END_REF] and Libratus at Poker [START_REF] Brown | Safe and nested subgame solving for imperfect-information games[END_REF], Deep Reinforcement Learning (RL) seems a promising avenue to develop a control algorithm, a.k.a. an artificial agent, able to operate a complex power system at scale near real-time and over time, assisted by existing advanced physical grid simulators. Recent work [START_REF] Donnot | Anticipating contingencies in power grids using fast neural net screening[END_REF] has already shown the value of Deep Learning for accelerating power flow computation and risk assessment applications for power systems, demonstrating its ability to model such system behavior, adding more credit to the Deep RL potential. RL formulations have already been applied to specific power system related problems (see [START_REF] Glavic | Reinforcement learning for electric power system decision and control: Past considerations and perspective[END_REF] for a review), but not for continuous power system realtime operations, a problem for which no test cases existed today, probably limiting any subsequent development. Related applications concern the unit commitment problem with an interesting multi-stage formulation [START_REF] Dalal | Hierarchical decision making in electricity grid management[END_REF], but on an infra-day timeframe with rather simplistic assessment of intra-day real time operation. These authors also promote leveraging the capabilities of Deep RL as a catalyst for successful future works. They finally insist on the real-world challenge of Safe-RL to manage for instance a power system for which contingencies, and related overloads, rarely occur but need to be closely managed, to avoid cascading failures and subsequent blackouts. More broadly, Safe-RL is a hot research topic in the whole RL community to eventually address real-world challenges for critical systems [START_REF] Dulac | Challenges for real-world reinforcement learning[END_REF].

In line with those recent development and in order to foster further advances both within the power system and RL communities, we open-sourced a new platform to build and run power system synthetic environments to further develop and benchmark new controllers for continuous near-real time operations. We indeed built and released a first IEEE14 environment test case upon which we organized a competition Learning to run a Power Network (L2RPN) with an emphasis on the challenging use of topological flexibilities and the safety robustness requirement. The L2RPN competition which we will present and analyze here, takes some inspiration from the Learning to run [START_REF]Learning to run challenge: Synthesizing physiologically accurate motion using deep reinforcement learning[END_REF] competition, whose goal was to learn a controller of a human body to walk and run. This was an opportunity for bio mechanical researchers to successfully address their problem together with the RL community.

The following paper is organized as follows: first we present an overview of the objective and results of this first L2RPN competition. We further review the design and modelling of the related test environment. We then propose a conceptual Markov Decision Process framework to analyze the nature of the problem for a given test environment. Finally we describe the results through a comparative analysis of the best submitted agents and other baselines, and give conclusions. [START_REF] Lerousseau | pypownet: A modular python library for reinforcement learning on power systems management[END_REF] opensourced platform1 relying on openGym RL framework. 100 participants signed in, 15 of which were particularly active with many submissions every week. Figure 1a showed the 7 best participants who all achieved interesting and successful scores, with a mix of RL, Machine Learning (ML), expert system and tree search approaches we comment in section V. They all succeeded in beating simple baselines used to design the challenge, and RL approaches achieved the best results. The goal of the competition was to operate the power grid in real-time over several days at a 5 minute time-resolution. More precisely, the aim was to manage the powerflows i (in Amperes) at every time-step t, given injections x, aka production and loads, and grid topology denoted by τ . The score function gave incentives to optimize the margins through all lines, in order to maximize the overall residual grid capacity ∆Cg, given power lines capacities imax l , aka thermal limits:

M argin l (t) = max 0, 1 - i l (t) imax l , ∀l ∈ L (1)
To manage the grid, an agent could only use topological actions in A τ on lines L and substations Sub in that challenge, while meeting further operational constraints on actions and overloads. Some actions could be illegal, violating some operational rules further described in Section III, or result in a diverging powerflow computation, most likely due to some voltage issues. Choosing an illegal action resulted in a null score at that time-step. To assess an agent performance, the following score at time-step t was used as a proxy for ∆Cg :

Score(t) =    0 if illegal action or divergence ∆Cg(t) = n l l=1 f (M argin l (t)) (2)
Every line somehow contribute to the real-time power grid capacity, represented by the sum in the score. But already loaded lines should affect more the residual capacity of the grid as they soon become bottlenecks to transmit more flows. This is why more value should be given on increasing the margins of already loaded lines, while increasing the margin of a line not very loaded does not add up to the overall capacity. We chose f (x) = 1 -(1 -x) 2 shown in Figure 1b in that prospect. Optimizing ∆Cg eventually contributes to minimizing power losses on the grid, smoothing the power line usage to avoid materials aging too quickly, and maximizing the grid flexibility which are all today's challenges for power grids in most developed countries.

Finally, and most importantly, overload Ov l (that happen when i l >= imax l ) had to be solved dynamically to avoid line disconnection and further cascading failures. Any cascading failure resulted in a game over and a null score for a scenario s, putting a strong penalty on not being secure:

Score(s) =    0, if game-over during s T t=0 Score(t), otherwise (3)
Formalizing the score objective as a maximization problem of positive gains allows us to easily define a penalty as a null score if some rules of the environment are violated. b) Evaluation: Along the competition, participants could submit their agent on the Codalab platform 2 to be tested on unseen validation scenarios. A score was computed for each scenario and revealed to the participants, in addition to the time-step of game over if one occurred. At the end of the competition, participants were assessed on new 10 secret test scenarios similarly chosen, as described in Section V, with no other information than their cumulative score. Finally, to reflect one main characteristic of real-time operations for which time is limited, resulting in a trade-off between exploration and exploitation, participants would only get a score if they managed to finish their scenario within an allocated 20-minute time budget as shown on Figure 1a. It was calibrated as being 10 times the running time of the most simple baseline: a do-nothing (DN) agent. Expert Systems and tree-search approaches appeared to be slow, since they relied more extensively on simulations, and had to limit their exploration to meet the time constraint.

c) Benefits of a Challenge: While reproducibility is a hot issue for scientific research and further model deployment, a challenge format looks appealing to avoid some pitfalls. Indeed, a challenge acts as a benchmark whose goal is to decouple the problem modeling from a solver implementation. Compared to the fine tuning of ones own method, a challenge aims at giving equal chance to every field expert to tune its solution in a given time slot and compare against one another. Its success also depends on the clarity of the submitted problem, on the ergonomy and robustness of its platform, on the transparency of its results, with an intrinsic need of reproducibility to faithfully deliver ones score and reliably announce the winners. Finally, winners had to open-source their code to obtain the price, further enforcing reproducibility.

III. CHALLENGE DESIGN

The difficulty of setting up this kind of challenge lies in the fact that one has to design a whole synthetic and interactive environment to test controllers (like a video game), and not just a fixed dataset. We designed it following 3 guiding principles: 1) Realism : the environment should represent real-world power system operational constraints and distributions. 2) Feasibility : solutions should exist to finish scenarios under the available actions given game over conditions. 3) Interest : harder scenarios should be challenging to finish and most scenarios should be complex to optimize.

There is a natural trade-off in making a game interesting and feasible: a most interesting game will more likely be more difficult with potential feasibility issues arising. Now a Grid World, aka an environment for a power grid, is the combination of the following components:

• A power grid (with substations and powerlines of different characteristics) and a grid topology τ • Real-time injections x(t), next time-step forecasts x(t+1) • Lines Capacities imax l and additional operational rules • Events such as maintenance and contingencies The power flows i l (t) are computed by a power-flow simulator.The platform then allows some interactions for an agent with that environment through actions a τ (t). Participants had the option to simulate the effect of their action before choosing one, but using some computation time budget. To assess how feasible and interesting an environment is for agents, we defined the following simple baseline agents :

• a "do nothing" (DN) agent that remains in the reference topology τ ref and which is already robust most of the time, much better actually than taking random, and mostly stupid, actions. • a single topology agent (DN τ ), which is a DN agent running in a constant topology τ distinct from τ ref .

• a greedy (GR) agent that simulate do-nothing and all unitary actions at a given time-step, and take the most immediately beneficial one.

These agents can finish all together most scenarios, while highlighting hard to complete ones. Let's now describe in more details the different steps of the challenge design.

a) Choosing a Power Grid and define topology τ : To be realistic, we first chose a grid among common IEEE power grids. For that first challenge, we chose a minimalist grid to better ensure feasibility and help analysis, but yet a grid for which topological actions could still be useful to manage it. Such a grid needed to be meshed with several electrical paths. We hence chose the IEEE14 grid as it is a meshed grid with 2 West and East corridors between a meshed South Transmission Grid and a meshed North Distribution Grid. Even with only 14 substations, the number of potential overall configurations, hence the combination of actions, is tremendous. For such a size, we however did not consider the occurrence of contingencies and maintenance since it will most often lead to infeasibilities. Overloads were only the result of peak productions or peak loads in certain areas of the grid.

The reference topology τ ref is the base case topology, fully meshed, with every lines in service and single electrical node per substations. However, up to two electrical nodes are possible per substation, modeled as a 2-bus bar.

The topology can be changed by actions a τ (t) ∈ A τ , that can be of two kinds :

• Binary Line switching a l (2 20 possible actions)

• Bus bar switching of elements at a substation a busi (2 20 * 2+16 ) for 20 lines and 16 injections

There are as many actions as there are topology configurations. Eventually, the number of reachable configurations at a given time is limited by considering some operational rules. on Figure 2 to better represents today's energy mix and dynamics to consider managing resulting issues. The total load consumption profile follows the French consumption one and individual loads are computed given a constant key factor from the original IEEE case on Figure 3. Solar and wind power also follow French related distribution with correlations between wind and solar. The nuclear power plant is a baseload, slowly varying and the thermal power plant compensates for the remaining production required for balancing (see Figure 3). For this challenge, we restricted the distribution of injections to be representative of winter months over which we observe peak loads. Next time frame forecast where also provided for injections x with 5% gaussian noise uncertainty. The second part of the game design was about setting up the right thermal limits (no thermal limits are given for the IEEE14 case) so that some overloads appear, not all being easily solvable, but many of them that can be solved by at least a baseline to remain feasible. From the grid structure perspective, only 2 electrical corridors exists as illustrated on Figure 2. We cannot allow both of them being overloaded at the same time, since there will not exist any more path to reroute electricity with topology to relieve all overloads. We hence chose to preferably constrain line capacities on the West Corridor (buses 2 → 5 → 6 → 13), while keeping spatial consistency for thermal limits overall from a grid development perspective. Overloads eventually appear 3% of the time over those lines in the scenarios running DN agent. Other lines had their capacities rated above the max power flow observe in the reference topology.

To make the game more interesting, we also want to have a spread distribution on the time of occurrence of overloads as shown on Figure 4. Running an ensemble of expertly selected DN τ baselines (see Table I) solves 85% of the overloads. This demonstrates that our game is both feasible, and has some difficult interesting situations (following our guiding principles). Also, the GR baseline does not perform well on all scenarios : this agent tends to get stuck in bad local configurations.

Finally, real-world problems get complex because of operational constraints.We choose to model the following ones:

• reaction time -time to react to an overload before the line get disconnected by protections, 2 time-steps here. • activation time -there is a maximum number of actions that a human or a technology can performed in a given time period, one action per substation here. • recovery time (cooldown) -due to physical properties of the assets, there is some time after activation before a flexibility can be reactivated, set to 3 time-steps here. You can look at flexibilities as a kind of budget. When you use one, you consume part of your budget before recovering it some time after. This induces some credit assignment problem. Let's now formalize the whole problem under those settings with the generic framework of Markov Decision Processes.

IV. PROBLEM FORMALIZATION

Markov Decision Processes (MDPs) [?] are useful and general abstractions to solve a number of problems in optimization and control. We decide to further formalize our problem here using this framework, which will help determine the nature of the problem under different settings. An MDP is generally represented by a tuple S, A, P, r, γ with:

• S the state space of observations from the environment.

• A the action space, the potential agent interactions with the environment. • P the stochastic transition function p(s(t + 1)|s(t), a(t)) which computes the system dynamics. It defines a Markovian assumption. • r(t) = r(s(t), a(t)) the immediate reward function. The policy determines the next action a(t + 1) as a function of s(t) and r(t). The policy can adapt itself (by reinforcement learning) to maximize the expectation (over all possible trajectories) of this function:

G(t) = T k=t+1 γ k-t-1 r(k) (4)
where γ ∈ [0, 1] is the discount rate. Our L2RPN problem is actually a two-factor MDP (Figure 5), a special case of MDP in which the state S is a quadruplet:

• : unobserved influences on inputs x. • x: observed inputs of the system, not influenced by the actions of the agent. • τ : other observed inputs of the system, influenced by the actions of the agent. • y: observed outputs of the system, y = F (x, τ ). Function F specifies the system of interest and y is essentially here powerflows i l and overloads Ov l . F is a function of two factors x and τ (injections and topology in our case). The 'observed inputs' x may or may not be organized in a time series. In our case they are. Injections are continuous timeseries. For τ , it is only changing under limited agent actions and some rare events such as contingencies and maintenance.

The agent's actions only influence τ . Although there are many ways in which τ (t); x(t); y(t) could influence (t+1) variables, we only considered the following:

• x → x: injections are timeseries.

• τ → τ : agent's "position" τ (t + 1) is constrained by past positions τ (t) given the limited action rule, de facto limiting the freedom of the agent to influence y. • y → τ : overloaded flows can lead to line disconnections, or cascading failure, hence influencing the topology . • τ → a: recovery time constrains future actions. Without operational constraints and robustness consideration of cascading failures, the problem is mostly an instance of the contextual bandit more specific case on Figure 5 (only x(t) → x(t+1)) under which more specific algorithm than RL can be preferred and perform quite well. Adding τ → τ by limiting instantaneous actions makes it a regular RL problem. Our platform could actually run this latter setting as an easy mode to make an agent's training easier at first. However the problem we proposed in this first challenge, our hard mode, already involved some more complexity as depicted on Figure 5. Successful approaches in the easy mode would not necessarily work in the hard mode, especially since it involves robustness issues in the latter case. These causal diagrams are hence useful for understanding the problem proposed. It helps the designer anticipate if modeling a new constraint will change the nature and complexity of the problem and it helps the participant select the appropriate class of methods to solve it. In particular, ML and RL methods indeed appeared suited for this first challenge as expected.

V. RESULT ANALYSIS

We now review the challenge results, by first describing the properties of the scenarios on which participants were tested, and giving a description of the best agents. Then we analyze the agents behavior on these and eventually present a post-analysis of their performance. Finally we will propose an oracle approach to derive a near upper-bound for the scores, to better assess the optimization gap of the agents.

a) Validation and test scenarios: In order to select interesting scenarios, we tried to combine multiple criteria that were identically set for both validation and test scenarios:

• Difficulty levels: difficulty ranges from easy (no overload at all for the DN agent) to hard (no known solution has been found using our ensemble of DN τ agent baseline).

It reduces the likeliness of having tie contestants. • Diverse tasks: some scenarios focus on handling overloads in the morning, while others test evening peak consumption management. In a scenario, no overload appears, to test agents does not react randomly. In others, overloads vanish naturally, to test agents do not overreact. • Diverse context: we include variability by changing the day of the week of the scenarios, to make sure the powergrid can be handled for all days of the week, and not only at some very restrictive times. • Diverse horizons: we finally have scenarios of different length, varying from 1 day (288 time-steps) to 3 days (864 time-steps), to test agents in different kind of settings: longer scenarios favor stable agents with longer horizon, shorter scenarios favor greedy agents. Those scenarios were mainly selected to test the robustness of agents, that is their ability to finish a given scenario. However, beside being robust, participants still had to continuously optimize the grid margins. Let's now describe the best agents and examine their behavior on the test scenarios.

b) Agent Description: From Figure 1a, we can see that only the groups called "Lebron James" (LB), "LearningRL" (LR) and "Stephan Curry" (2nd team from Geirina, so we only consider LB) managed to finish all test scenarios, with ML + RL approaches. Both codes are open-source and referenced on the challenge website 3 . "Kamikaze" (KM, ML approach) and "Smart Dispatcher" (SD, Expert system + greedy validation) each failed on one, whereas they previously managed all validation scenarios. "Menardpr" (MD, greedy tree search approach) failed on one, on both test and validation scenarios. Winners were less computationally intensive at test time, thanks to Machine Learning, while also being more effcicient, making them relevant in a setting of real-time decision making.

Comparing LB and LR from a code analysis, LR appeared to be the only participant to never query the simulate function to validate or explore additional actions at test time: this is quite an achievement to only rely on what the agent learnt, and trust it. Its model was based on the actor critic (A3C) algorithm [START_REF] Mnih | Asynchronous methods for deep reinforcement learning[END_REF]. This is an architecture with two main components, a policy network (actor) and a value network (critic). A3C aim at learning a policy function directly, through the actor module. The critic module then criticize the actor given the new state value after taking an action, to adjust and improve its behavior. Actor and critic modules are learnt asynchronously by pooling multiple workers that learn independently and improve a global agent.

LB agent on the other hand combined an RL model based on a dueling DQN algorithm [START_REF] Wang | Dueling network architectures for deep reinforcement learning[END_REF], coupled to a set of actions selected through extended prior analysis and imitation learning. Dueling DQN is most similar to DQN [START_REF] Mnih | Human-level control through deep reinforcement learning[END_REF] except that the neural network architecture explicitly try to encode separately at its core a state value function and an action advantage function, later combined to better estimate the Q-value.

In addition, LB uses few expert rules, especially "don't do anything if all your margins are good enough, below a threshold of 80%", and make extensive use of the simulate function when deciding on taking an action, to strongly validate a set of suggested action. This is representative on how operators have been doing until today. Their approach is closer to an assistant: an RL model suggests some actions and an expert model make a cautious choice among them and the ones he knows, validating with a simulator. c) Agents action space: All participants tried with different strategies to reduce the action space to explore at first. SD relied on its operator's expertise to identify relevant substations and lines to test on, still using a diverse set of assets with selected topologies. MD only focused on line switching to meet the time constraint with a tree search approach. However, most participants let aside line switching, sometimes an interesting option when no overloads exist to reroute some flows, but often detrimental when the grid is overloaded.

LR also used some domain knowledge over the symmetries in a substation to reduce the number of true actions. More interestingly, they started their exploration from scratch and learnt robust actions automatically through a curriculum learning. They indeed started to learn in an easy mode (no game over), upsampling the scenarios to quickly see more diverse situations. They somehow already learnt useless actions and potentially useful actions to route the flows. They then switched to the hard mode with the appropriate time resolution to learn managing overloads and being robust to them. They used their own reward function when learning to penalize strongly on overloads when occurring, different from our score in (2). Our score is not a good reward function to learn from in that prospect, as its gradient, and hence the learning signal, is null in the overload regime. They eventually converged to only act on two substations, a bit restrictive. This might be changed by relaxing their reward function. LB team on the other hand did an extensive analysis on influential topologies on a batch of sampled grid states to initialize their learning. At the end, they used quite a diverse set of assets. Figure 6 summarizes the number and diversity of actions agents used on test scenarios.

d) Behavior analysis : Looking at agent actions in realtime from Figure 7 on a test scenario, we can detect different kinds of behavior. SD is indeed doing lots of actions, trying to optimize the score continuously, but somehow going back and forth erratically when the grid is loaded: overloads might be appearing due to its actions. LB is a pretty stable agent, anticipating soon enough potential overloads through its expert rule. However its topology seems to always be drifting from the reference topology which might be detrimental on long scenarios. Finally, LR is also quite stable due to its small action space but has the ability to go back and forth. Extended AI agent behavior analysis will be conducted in future works, as it is an emerging field [START_REF] Rahwan | Machine behaviour[END_REF] with new tools being released [START_REF] Osband | Behaviour suite for reinforcement learning[END_REF].

We eventually ran an additional post analysis experiment on larger batch of monthly scenarios given for training. It showed that all agents are still failing on several scenarios (LB: 5 fails, LR: 11 fails, SD: 9 fails), highlighting some instabilities on the long term. Scenario 37 appeared especially difficult with no agent succeeding. We should hence aposteriori adjust or augment our selection criteria to develop a more comprehensive benchmark of this task. Also, beyond robustness, the challenge was also about continuously optimizing the flows on the grid.

e) Revised scores with oracle baseline: In the short duration of the competition, participants mainly focused on their agent robustness, as a single gameover prevented them from winning. From the behavior analysis, agents do not appear to take many actions over a scenario, except from SD agent, which might indicate that agents did not try to optimize the flows beside avoiding overloads. To assess how good they did on this second task, we need to define an upper-bound baseline to get a better idea of what a good score should be.

While imperfect information is given to the participants along the game as they don't know yet the future, as organizers we can make use of the full scenario information to compute an oracle baseline, our upper-bound. For our method, we rely on the connection there exists between topology configuration I benchmark 3 . This highlights that controlling the topology still remains a hard problem given a huge action space requiring lots of exploration. It also challenges us as organizers to offer more representative scores that will give more incentives to the participants to perform better on a related task.

VI. CONCLUSIONS

The challenge was successful in addressing safety considerations and was necessary to open a new research avenue for a broad community, extended to Machine Learning researchers. It demonstrated that developing topological controllers for real-time decision making is indeed possible, especially when using reinforcement learning. Framing the problem as a twofactor MDP allowed us to also expose the difficulties faced by reinforcement learning solutions to such control problems. The diversity of submissions and behaviors helped us appreciate the pros and cons of each approach. Evaluating the participants' performance pushed us to define new interesting baselines and scoring metrics for future research and challenge designs. Our post-challenge analyses revealed both the feasibility of such approaches and the important gap to optimality, particularly for continuous power flow optimization, giving us an incentive to take the design of a new benchmark to the next level, including scaling up the dimensions of the grid.

  -June 29 -July 3, 2020 arXiv:1912.04211v1 [eess.SP] 5 Dec 2019

  II. THE L2RPN COMPETITION a) Challenge overview: This first L2RPN competition ran over 6 weeks starting on May 2019 over the Codalab challenge platform. It was based on the pypownet

  Score function f(Margin l ) Fig. 1. 1a Final leaderboard of the L2RPN competition with cumulated scores and computation time. 1b Instantaneous line margin score function

Fig. 2 .

 2 Fig. 2. a) IEEE14 Grid and production localization. b) Two existing electrical corridors between Transmission and Distribution Grids.b) Generating Injections x(t) and Forecasts x(t+1):While the IEEE 14 grid only had initially thermal production, we introduce renewable wind and solar plants as depicted

Fig. 3 .Fig. 4 .

 34 Fig. 3. a) Production, thermal and renewable, profiles over a typical month of January. b) Load profiles, all similar modulo a proportional factor. c) Line capacities imax and operational rules: :

Fig. 5 .

 5 Fig. 5. a) Contextual Bandit framework. b) L2RPN MDP formalization.

Fig. 6 .

 6 Fig. 6. Number of actions used at different substations (red) or lines (blue), ordered by indices, for different agents and our oracle over test scenarios.

Fig. 7 .

 7 Fig. 7. Agent behavior over validation scenario 3 showing the depth of agent actions at a given time-step, 0 meaning the agent is in the reference topology

  Normalized scores for SD and LB agents, compared to an oracle with 100 points. There still exists an optimization gap to improve on. TABLE

	Scenario	SD	LB
	1	72,5	61,5
	2	-10,5	90,2
	3	53	82,5
	4	49,5	81,5
	5	47,5	70,0
	6	48	47
	7	19,5	63
	8	39,5	77,5
	9	52,5	93
	10	56,5	56,5
	(b)

21st Power Systems Computation Conference PSCC 2020 Porto, Portugal -June 29 -July 3, 2020

GitHub for pypownet framework: https://github.com/MarvinLer/pypownet

The challenge has been re-enacted and is open for post-challenge submissions at https://competitions.codalab.org/competitions/20767 21st Power Systems Computation Conference PSCC 2020 Porto, Portugal -June 29 -

July 3, 2020

Porto, Portugal -June 29 -July 3, 2020

21st Power Systems Computation Conference PSCC 2020 Porto, Portugal -June 29 -July 3, 2020

Benchmark competition & github of winners at l2rpn.chalearn.org 21st Power Systems Computation Conference PSCC 2020 Porto, Portugal -June 29 -July 3, 2020

Acknowledgements

Many people have contributed to the design and implementation of the L2RPN challenge. We would like to acknowledge the contributions of Marc Mozgawa, Kimang Khun, Joao Arajo, Marc Schoenauer, Patrick Panciatici, Olivier Pietquin, and Gabriel Dulac-Arnold. The challenge is running on the Codalab platform, administered by Universit Paris-Saclay and maintained by CKCollab LLC, with primary developers Eric Carmichael and Tyler Thomas

r(0, 3) r [START_REF] Bacher | Network topology optimization with security constraints[END_REF][START_REF] Donnot | Anticipating contingencies in power grids using fast neural net screening[END_REF] r [START_REF] Brown | Safe and nested subgame solving for imperfect-information games[END_REF][START_REF] Donnot | Anticipating contingencies in power grids using fast neural net screening[END_REF] r [START_REF] Donnot | Anticipating contingencies in power grids using fast neural net screening[END_REF][START_REF] Donnot | Anticipating contingencies in power grids using fast neural net screening[END_REF] r(0, 4) r [START_REF] Bacher | Network topology optimization with security constraints[END_REF][START_REF] Dulac | Challenges for real-world reinforcement learning[END_REF] r [START_REF] Brown | Safe and nested subgame solving for imperfect-information games[END_REF][START_REF] Dulac | Challenges for real-world reinforcement learning[END_REF] r [START_REF] Donnot | Anticipating contingencies in power grids using fast neural net screening[END_REF][START_REF] Dulac | Challenges for real-world reinforcement learning[END_REF] r(0, 5) r [START_REF] Bacher | Network topology optimization with security constraints[END_REF][START_REF] Fisher | Optimal branch switching[END_REF] r [START_REF] Brown | Safe and nested subgame solving for imperfect-information games[END_REF][START_REF] Fisher | Optimal branch switching[END_REF] r [START_REF] Donnot | Anticipating contingencies in power grids using fast neural net screening[END_REF][START_REF] Fisher | Optimal branch switching[END_REF]

Fig. 8. reward graph G for several topology configurations τ and allowed transitions in dashed green. The oracle optimal path (in red) misses a max immediate reward at t 3 as no direct transition is allowed between τ 1 and τ 3 .

and topological action: given one action we can deduce the topology configuration we reach, knowing which configuration to reach to get some reward we can deduce the necessary action. We decided to run test scenarios under thousands of topology configurations in parallel (not all, which is too hard computationally) to later identify what would have been very good topologies at a given time and infer the preferred course of actions. Ultimately, it is framed as a longest path problem as on Figure 8. Our method can be decomposed in 5 steps: 1) Define a dictionary of interesting unitary actions D a from n unitary selected assets as on Table I 2) Identify all combinations of D a actions to create the oracle action space A oracle and related topology configuration space S(τ ) oracle when applied to τ ref .

A topology can be n action away from the reference one. 3) Apply all τ ∈ S(τ ) oracle independently and run them in parallel on scenarios to compute the reward of each configuration τ at each time-step t. This results in directed chains G τ with edges e Gτ (t) = reward(τ, t) 4) From all {G τ }, build the overall connex graph G of possible topology trajectories, given allowed topology transitions from operational rule. Add edges between reachable configurations (τ a ,τ b ): e (τa,τ b ) (t) = reward(τ b , t). 5) Compute the best score through the longest path on the directed acyclic graph G and determine the related course of actions {a(t)} t=0..T ∈ A oracle . Our score is always greater than all agents while respecting the operational rules, effectively defining on upper-bound. To determine how good other agents did, we define a revised score taking DN as a zero-reference score (computed in easy mode considering the optimization task only), oracle as a max:

The revised scores in Table I suggest that there still exists a gap between our oracle upper-bound and the best submitted agents. Figure 6 highlights that our oracle continuously took some actions, every 2 to 3 timesteps on average, as opposed to other agents. This confirms that agents did not do quite well on this optimizing task. Thus we reopened the challenge test case as a Felxibility id Target config. (a) Selected unitary actions at subs and lines for oracle. In bold, the ones used previsously for thermal limit design