Keywords: Systèmes asynchrones, Interprétation abstraite, Vérification de systèmes infinis, canaux FIFO, Automates de treillis, Analyse interprocédurale

Analyse des automates communicants étendus en utilisant des automates de treillis Résumé : Les protocoles de communication utilisés actuellement peuvent être formellement décrits en terme d'automates communicants. Ce modèle, très expressif, n'est cependant pas suffisant pour modéliser facilement des protocoles complexes qui font intervenir des messages structurés encapsulant des entiers ou des listes d'entiers. C'est pourquoi nous proposons, dans ce document, une extension de ce modèle : les automates communicants symboliques. Nous proposons également une méthode d'analyse d'accessibilité approchée, basées sur des automates de treillis. Les automates de treillis sont des automates finis dont les transitions sont étiquetées par des éléments d'un treillis atomique. Nous aborderons le problème de la déterminisation de ces automates, ainsi que la définition d'un opérateur d'élargissement approprié. Nous montrerons aussi que ces automates sont utiles pour l'analyse interprocédurale.

I R I S A I N S T I T U T D E R E C H E R C H E E N I N F O R M A T I Q U E E T S Y S T È M E S A L É A T O I R E S

Introduction

Communication protocols play a very important role in the context of distributed computing and computer networks. These protocols, which aim at ensuring the data transmission and/or detect communication failures, may be wrong due to logical errors of the protocol designer. Such errors may be difficult to detect and to understand, due to the complexity and the non-determinism of the behavior of asynchronous systems. Moreover, even if the protocol is free of logical error, some properties remains of interest, like the maximum size that the buffers may have during the execution of the system. For these reasons, the verification of communication protocols is both an important issue from the point of view of the protocol design, and a challenging problem for analysis techniques.

Communicating Finite-State Machines. Two fundamental approaches have been followed for the analysis of communicating systems in general. One consists in eliminating the need for analyzing FIFO queues contents by adopting a partial order semantics or a so-called true concurrency model: when one process sends a message to another process, one just records the information that the output precedes the input. The seminal work about event structures [START_REF] Nielsen | Petri nets, event structures and domains, part 1[END_REF] leads later to scenario-based models like (High-level) Message Sequence Charts [START_REF]Message Sequence Chart (MSC)[END_REF][START_REF] Reniers | High-level message sequence charts[END_REF] incorporated in UML.

The second approach, on which this paper focuses, consists in considering a model with explicit FIFO queues, and in analyzing their possible contents. A well-studied model is the model of Communicating Finite-State Machines (CFSM), in which finite-state machines communicate by sending messages belonging to a finite alphabet to unbounded FIFO queues. Although it is simple, this model is already quite expressive, since reachability is undecidable for this class of systems [START_REF] Brand | On communicating finite-state machines[END_REF].

In [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF], we proposed a method for the approximated analysis of Communicating Finite-State Machines (CFSM) based on Abstract Interpretation. The principles of our method were to represent the queue contents by regular languages and to define a widening operator that ensures the termination of the computation, but introduces some approximations.

Beyond CFSMs. In this paper, we extend this approach to more expressive communicating systems, where processes manipulate variables of unbounded types and where FIFO queues also transmit values belonging to infinite domains, like integers. The CFSM model is indeed not expressive enough for protocols that explicitly use variables, counters and infinite alphabets of messages. Typical examples of such protocols are sliding window protocols like the Service Specific Connection Oriented Protocol (SSCOP) [START_REF] Bozga | Verification and test generation for the SSCOP protocol[END_REF].

We will sketch our approach with the following example :

Example. Fig. 1 depicts a very simplified version of a sliding window protocol. The sender process tries to send data (identified by an integer) to the receiver process. The receiver process sends an acknowledgment message identifying the data received. The sender has two variables : s is the index of the next data to send, and a is the index of the last acknowledgment message received. The protocol ensures that the sender waits for acknowledgment if s = a + 10. If the sender gets a message ack(p) with p > a + 1, it means that at least one message has been lost and the protocol terminates with an error. There are two queues: one from the sender to the receiver containing data messages, the other containing acknowledgment messages. Notice that we do not model here possible loss of messages.

As in [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF], we want to abstract the contents of the queues by regular languages, represented by finite automata. However, the messages contained in FIFO queues do not belong any more to a finite alphabet, as shown by the example. Contributions. The first contribution of this paper is to define with lattice automata an effective and canonical representation of languages on infinite alphabet, equipped with well-defined operations (union, intersection, concatenation, . . . ). Although the normal form we propose induces in general some approximations, it is a robust notion in the sense that the normalization operator is an upper closure operator which returns the best upper-approximation of a language in the set of normalized languages. The resulting abstract domain allows to lift any atomic abstract domain A for ℘(S) to an abstract domain Reg(A) for ℘(S * ), the set of finite words defined on the alphabet S.

The second contribution of the paper is to demonstrate the use of this representation for the analysis of symbolic communicating machines (SCM). It appears indeed that this representation needs to be exploited in a clever way in order to be able to prove even simple properties, like in the example that messages in the queue 1 are always indexed by numbers smaller than the variable s. Our analysis shows that a ≤ s ≤ a + 10 (complete results are in Sect. [START_REF] Bojanczyk | Twovariable logic on words with data[END_REF].

A third contribution is to show that lattice automata are also adapted to the abstraction of callstacks in imperative programs, and allows to design potentially very precise interprocedural analysis.

Outline Sect. 3 reminds some definitions about abstract interpretation and finite automata. In Sect. 4, we recall the method of [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF] for analyzing CFSMs using regular languages, which is our departure point. The core contribution of the paper is Sect. 5 where we define lattice automata and their operations, which allows to manipulate languages on infinite alphabet. In Sect. 6 we exploit this representation for the abstract interpretation of Symbolic Communicating Machines. Sect. 7 discuss the use of lattice automata for interprocedural analysis, where they allows to abstract call-stacks of imperative programs.

Irisa 2 Related work

The initial motivation of this work was the analysis of communicating machines. Many techniques have been devoted to the analysis of Communicating Finite-State Machines (CFSM), where both the machines and the alphabet of messages are finite. Reachability of CFSM is undecidable [START_REF] Brand | On communicating finite-state machines[END_REF]. Most approaches for the verification of CFSM are based on exact but semi-decidable acceleration techniques [START_REF] Boigelot | The power of QDDs (extended abstract)[END_REF][START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using QDDs[END_REF][START_REF] Bouajjani | Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations[END_REF][START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF][START_REF] Finkel | Well-abstracted transition systems: application to FIFO automata[END_REF]. A few attack the problem with abstract interpretation techniques [START_REF] Peng | Data flow analysis of communicating finite state machines[END_REF][START_REF] Jeannet | Abstracting call-stacks for interprocedural verification of imperative programs[END_REF]. None of these works deals with a potentially infinite alphabet of messages.

More generally, there are several lines of work aiming at extending classical finite automata (resp. tree automata) representations for regular sets of words (resp. trees) for verification purposes. Mauborgne has proposed efficient representations for a class of sets of trees which strictly includes regular trees [START_REF] Mauborgne | Tree schemata and fair termination[END_REF][START_REF] Mauborgne | Representation of sets of trees for abstract interpretation[END_REF]. Another approach is to focus on the decidability of some logic like the first order logic or the monadic second order logic when the model is a word with data or a tree with data (model of a XML document) [START_REF] Neven | Towards regular languages over infinite alphabets[END_REF]. New kind of automata were introduced, like register automata [START_REF] Kaminski | Finite-memory automata[END_REF], pebble automata [START_REF] Milo | Typechecking for XML transformers[END_REF] or data automata [START_REF] Bojanczyk | Twovariable logic on words with data[END_REF], with the idea that a word with data satisfies the logical formula if it is recognized by the corresponding automata. This approach cannot be applied as is to our problem, as such a logical approach does not take into account any specific logical interpretation for data (in other word, the data domain is unspecified) and there is no notion of approximation.

They have been recently a lot of works devoted to shape analysis which can be relevant to the analysis of queues or stacks. A FIFO queue or a stack can indeed be represented by a list, which is most often the easiest data type to abstract in shape analysis techniques. However, most shape analysis focus on the structure ("the shape") of the memory and ignores data values held by the memory cells [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF][START_REF] Yavuz | Automated verification of concurrent linked lists with counters[END_REF][START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Bouajjani | Abstract tree regular model checking of complex dynamic data structures[END_REF]. It is sometimes possible to handle finite data values, but mainly by brute force enumeration, which is algorithmically expensive in such a context, certainly more than the above-cited approaches based on finite automata. [START_REF] Gopan | Numeric domains with summarized dimensions[END_REF] is a pioneering work for taking into account data values in memory cells. It uses a global polyhedron to relate the numeric contents of each abstract memory cell in an abstract shape graph. The resulting abstraction is not comparable to our proposal, as it is based on very different principles. In particular, the information used for abstraction in shape graphs is mostly attached to nodes instead of edges as in automata. The involved algorithms are also probably more expensive than in our solution.

Conversely, it should be noted that our abstract domain could be applied to shape analysis, although this deserves yet a full study.

Work related to the application of lattice automata to stack abstraction and interprocedural analysis is delayed to Sect. 7.

Preliminaries

Finite automata. A finite automaton is a quintuple

A = (Q, Σ, Q 0 , Q f , δ) where Q is a finite set of states, Σ a finite alphabet of letters, Q 0 ⊆ Q (resp. Q f ⊆ Q) the subset of initial (resp. final) states, and δ ⊆ Q × Σ × Q the transition relation. A word σ = σ 0 . . . σ n ∈ Σ * is recognized by A if
there exists a sequence q 0 . . . q n+1 ∈ Q * such that q 0 ∈ Q 0 , ∀i ≤ n : (q i , σ i , q i+1 ) ∈ δ, and q n+1 ∈ Q f . The set of words recognized by A is a regular language denoted by L(A).

Let ≈ be an equivalence relation on the set of states Q. The equivalence class of a state q ∈ Q w.r.t. ≈ is denoted by q. The quotient automaton A/ ≈= Q, Σ, Q 0 , Q f , δ is defined by

• Q = Q/ ≈, the set of equivalence classes; • Q 0 = { q|q ∈ Q 0 } and Q f = { q|q ∈ Q f };
• ( q, a, q ) ∈ δ ⇐⇒ ∃q 0 ∈ q, ∃q 0 ∈ q : (q 0 , a, q 0 ) ∈ δ

PI n˚1839

For any equivalence relation ≈, we have L(A) ⊆ L(A/ ≈).

Given an equivalence relation on Q, and k ≥ 0, the k-depth bisimulation equivalence relation ≈ k based on is defined inductively by • ≈ 0 = ;

• q ≈ k+1 q ⇐⇒ ∀(σ, q 1 ) ∈ Σ × Q : δ(q, σ, q 1 ) ⇒ ∃q 1 : δ(q , σ, q 1 ) ∧ q 1 ≈ k q 1 ∀(σ, q 1 ) ∈ Σ × Q : δ(q , σ, q 1 ) ⇒ ∃q 1 : δ(q, σ, q 1 ) ∧ q 1 ≈ k q 1

The largest bisimulation relation contained in is defined as ≈= k≥0 ≈ k . The equivalence bisimulation relation is defined as the largest bisimulation relation contained in the relation separating final states from other states:

q q (q ∈ Q f ∧ q ∈ Q f ) ∨ (q ∈ Q f ∧ q ∈ Q f ).
Two states are equivalent if they are related by the equivalence bisimulation relation.

A is deterministic if there is a unique initial state and if δ(q, σ, q ) ∧ δ(q, σ, q ) =⇒ q = q . Any finite automaton can be transformed into a deterministic automaton recognizing the same language, using the subset construction. A is a minimal deterministic automaton (MDA) if it is deterministic and if there exists no deterministic automaton with fewer states recognizing the same language. Given a regular language L, there exists a unique (up to isomorphism) MDA A(L) recognizing it. Any deterministic automaton A can be minimized by removing unreachable states and quotienting it w.r.t. the largest bisimulation relation separating final states from non final states.

Lattices. A partially ordered set (Λ, ) is a lattice if it admits a smallest element ⊥, a greatest element , and if any finite set of elements X ⊆ Λ admits a greatest lower bound (glb) X and a least upper bound (lub) X. A lattice is complete if the glb and lub operators are defined for any (possibly infinite) subset of Λ. An element x ∈ L of a lattice Λ is an atom if it is minimal i.e. ⊥

x ∧ ∀y ∈ A : ⊥ y x =⇒ y = x. The set of atoms of L is denoted by At(Λ). A lattice is atomic if any element x ∈ L is the least upper bound of atoms smaller than itself : x = {a | a ∈ At(Λ) ∧ a x}. For instance, the set of convex polyhedra in R n ordered by inclusion is an atomic lattice but is not a complete lattice. However, the set of convex sets in R n is an atomic and complete lattice. A finite partition of a lattice is a finite set (λ i ) 0≤i<n of elements such that ∀i = j : λ i λ j = ⊥ and ∀λ ∈ Λ : λ = n-1 i=0 (λ λ i ). If the lattice is atomic, there is an isomorphism between an element λ ∈ Λ and its projection λ λ 0 , . . . , λ λ n-1 on the partition. A (finite) partitioning function π : Σ → Λ is a function such that (π(σ)) σ∈Σ is a (finite) partition of Λ.

Abstract Interpretation. Most program analysis problems come down to solving a fix-point equation x = F (x) where x belongs to an ordered domain C (typically, the powerset ℘(S) of the state space of a program). Abstract interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is a general method to find approximate solutions of such fix-point equations. Its principles are to perform successively two kind of approximations:

1. The static approximation consists in substituting to the concrete domain C, a simpler abstract domain A. The abstract lattice A is linked to the concrete lattice C by a concretization function γ : A → C which is monotone. The concrete fix-point equation is transposed into the abstract domain A, so that to solve a new equation

y = F (y), y ∈ A with γ • F F • γ
This ensures the soundness of the method, in the sense that γ(lfp(F )) lfp(F ).

2. The iterative resolution of the new fix-point equation can still involve infinite iterations. Although one can choose abstract lattices A that satisfy the ascending chain condition, better results can be obtained by removing this restriction [START_REF] Cousot | Comparing the Galois connection and widening/narrowing approaches to abstract interpretation[END_REF] and resorting to an additional dynamic approximation. It consists in using a widening operator ∇ as follows: the original sequence

Irisa y 0 = ⊥, y n+1 = F (y n ) is replaced by z 0 = ⊥, z n+1 = z n ∇F (z n ).
Under technical assumptions on ∇, the iterative computation of the sequence (z n ) n≥0 is guaranteed to converge after a finite number of steps to some upper-approximation z ∈ A of the least fix-point of F (more precisely, a post-fix-point of F ).

This principles can be applied for instance to define an interval analysis of a program with integer variables, in which the concrete domain C = ℘(Z n ) of possible valuations of variables is abstracted by a product (I(Z)) n of intervals on integers. An abstract value thus associates to each variable its possible range of values. This is an upper-approximation in the sense that what is guaranteed is that the values outside the interval cannot be taken by the variable. Given two abstractions γ i : A i → C, i = 1, 2 for the same concrete domain C, A 2 refines A 1 if there exists a (concretization) function γ 12 : A 1 → A 2 such that γ 1 = γ 2 • γ 12 . This means that any concrete property c ∈ C representable by A 1 (ie.,

∃a 1 ∈ A 1 : c = γ 1 (a 1 )) is representable by A 2 (ie., ∃a 2 ∈ A 2 : c = γ 2 (a 2 ) by taking a 2 = γ 12 (a 1 )).

Analysis of CFSM using abstract interpretation

Our method for the analysis of Symbolic Communicating Machine (SCM) reuse most of the principles we have developed in [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF] for the analysis of the simpler model of Communicating Finite-State Machines. As a consequence, we first describe this method in this section, which serves as an introduction to the next sections.

The CFSM Model

A Communicating Finite-State Machine (CFSM) models a system of finite-state machines sending or receiving messages via n unbounded FIFO queues, modeling communication channels.

Definition 1 (CFSM) A communicating finite-state machine is given by a tuple (C, Σ, c 0 , ∆) where:

• C is a finite set of locations (control states)

• Σ = Σ 1 ∪ Σ 2 ∪ • • • ∪ Σ n is
a finite alphabet of messages, where Σ i denotes the alphabet of messages that can be stored in queue i;

• c 0 ∈ C is the initial location;

• ∆ ⊆ C × A × C is a finite set of transitions, where A = i {i} × {!, ?} × Σ i is the set of actions. An action can be -either an output i!m: "the message m is sent through the queue i";

-or an input i?m: "the message m is received from the queue i".

In the examples, we define CFSMs in terms of an asynchronous product of finite state machines (FSMs) reading and writing on queues.

Example. The connexion/disconnection protocol between two machines is the following (Fig. The operational semantics of a CFSM (C, Σ, c 0 , ∆) is given as an infinite transition system Q, Q 0 , → where

• Q = C × Σ * 1 × • • • × Σ * n is the set of states; • Q 0 = { c 0 , ε, . . . , ε } is the set of initial states;
• → is defined by the two rules:

(c 1 , i!m, c 2 ) ∈ ∆ w i = w i • m c 1 , w 1 , . . . , w i , . . . , w n -→ c 2 , w 1 , . . . , w i , . . . , w n (c 1 , i?m, c 2 ) ∈ ∆ w i = m.w i c 1 ,
∈ C × Σ * 1 × • • • × Σ * n
where c is the current location and w i is a finite word on Σ i representing the content of queue i. At the beginning, all queues are empty, so the initial state is c 0 , ε, . . . , ε .

Reachability analysis of a CFSM

The forward collecting semantics defines the semantics of a CFSM in terms of its set of reachable states. A set of states

X ∈ ℘(Q) = ℘(C × Σ * 1 × • • • × Σ * n ) can be viewed as a map X : C → ℘(Σ * 1 × • • • × Σ * n
) associating a control state c with a language X(c) representing all possible contents of the queues when being in the control state c. The forward semantics of actions a :

℘(Σ * 1 ו • •×Σ * n ) → ℘(Σ * 1 ו • •×Σ * n ) is defined as: i!m (L) = { w 1 , . . . , w i • m, . . . , w n | w 1 , . . . , w i , . . . , w n ∈ L} (1) i?m (L) = { w 1 , . . . , w i , . . . , w n | w 1 , . . . , m • w i , . . . , w n ∈ L} (2)
i!m (resp. i?m ) associates to a set of queues contents the possible queues contents after the output (resp. the input) of the message m on the queue i, according to the operational semantics of CFSM.

Using the inductive definition of reachability -a state is reachable either because it is initial, or because it is the immediate successor of a reachable state -, the reachability set RS is defined as the least solution of the fix-point equation

∀c ∈ C, X(c) = X 0 (c) ∪ (c ,a,c)∈∆ a (X(c )) (3)
Irisa where Q 0 is the initial set of states.

As there is no general algorithm that can compute exactly such a reachability set [START_REF] Brand | On communicating finite-state machines[END_REF], we propose in [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF] an approximate analysis method based on abstract interpretation. The problem here is that we need to abstract the concrete domain of queues ℘(Σ * 1 × • • • × Σ * n ) which does not enjoy a finite representation.

Regular languages as an abstract domain for queues

Abstracting a single queue. For the sake of simplicity, we first consider the case of a single queue. Observe that the set ℘(Σ * ) is actually the set of languages L(Σ) defined on the alphabet Σ. The solution we propose in [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF] is to abstract the set of languages L(Σ) by the set of regular languages R(Σ). This simple solution presents two nice properties:

• R(Σ) is closed under union, intersection, negation and semantic transformers !m (corresp. to concatenation) and ?m (corresp. to the derivative operator of [START_REF] Janusz | Derivatives of regular expressions[END_REF]). Moreover, Q 0 = { c 0 , } is regular, so that all operators involved in Eq. ( 3) can be transposed to R(Σ) without loss of information.

• From a computational point of view, regular languages have as a standard canonical representation the minimal deterministic automaton (MDA) recognizing them.

As a consequence, we only have to define a suitable widening operator to ensure convergence of iterative resolutions of fix-point equations on R(Σ). Indeed, the lattice R(Σ) does not satisfy the ascending chain condition and is even not complete. [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF] adapts a widening operator for regular languages first mentioned in [START_REF] Feret | Abstract interpretation-based static analysis of mobile ambients[END_REF]. This widening operator is based on an extensive and idempotent operator

ρ k : R(Σ) → R(Σ) (i.e. ρ k (X) ⊇ X and ρ k • ρ k = ρ k ), where k ∈ N is a parameter. ρ k will induce a widening operator defined by X 1 ∇ k X 2 = ρ k (X 1 ∪ X 2 )
. Thus, the proposed widening does not work by extrapolating a difference as usual in abstract interpretation, but by simplifying the regular languages generated during the iterative resolution. Now ρ k (X) is defined by quotienting the MDA A(X) recognizing X by the k-depth bisimulation relation based on the partition of the states 3 illustrates the effect of this operator. As the number of states of the MDA of ρ k (X) is bounded by 4 |Σ| k+1 × 2 |Σ| k , the co-domain of ρ k is finite for a k and Σ fixed. Hence the defined operator ∇ k satisfies the technical definition of a widening operator.

Q of A(X) into Q 0 ∩Q f , Q 0 \Q f , Q f \Q 0 , and Q\(Q 0 ∪Q f ). Fig.
An upper-approximation of the least solution of Eq. 3 can now be computed by computing the sequence

∀c ∈ C X (0) (c) = X 0 (c) ∀c ∈ C X (n+1) (c) = X (n) (c) ∇ k (c ,a,c)∈∆ a (X (n) (c )) (4)
Abstracting several queues. When the system involves several queues, the simplest solution is to abstract each queue independently, leading thus to a non-relational or attribute-independent analysis.

It consists in taking

A nr = R(Σ 1 ) × • • • × R(Σ n ) as an abstract lattice, ordered component-wise. The meaning function γ nr : A nr → ℘(Σ * 1 × • • • × Σ * n ) is defined by γ nr ( L 1 , . . . , L n ) = γ(L 1 ) × • • • × γ(L n )
We can however view a configuration of the queues, which is a vector of words (w 1 , . . . ,

w n ) ∈ Σ * 1 × • • • × Σ * n
, as a single word w 1 . . . w n obtained by concatenation and the addition of a separation

PI n˚1839 L = aax + bay ρ 1 (L) = (a + b)a(x + y) a a x b a y a a x b a y L = ax 3 bx 3 c ρ 1 (L) = ax + (bx + ) * c a x x x b x x x c a x x b x c
Figure 3: The extensive and idempotent operator ρ k on regular languages letter . One can then apply the abstraction for a single queue on such concatenated word. This leads to the relational abstraction

A r = R(Σ ∪ { }) γ r (X) = { w 1 , . . . , w n ∈ Σ * 1 × . . . × Σ * n | w 1 . . . w n ∈ X}
where a single automaton is used to represent the possible contents of all queues. One just has to adapt to concatenated words the output and input operations, as well as the widening (by modifying the initial partition on which ρ k is based). This abstraction is strictly more precise, as A r can represent exactly all the elements of A nr , plus many more.

Example. The connexion/disconnection protocol depicted in Fig. 2 illustrates both kind of abstractions and illustrates the usefulness of a more precise relational analysis:

Relational Analysis Non-Relational Analysis Client/ Queue 1 # Queue 2 Server 0/0 (co) * (oc) * #ε + c(oc) * #d 1/0 (co) * (oc) * o#ε + (co) * #d 0/1 c(oc) * #ε 1/1 (co) * #ε Client/ Queue 1 Q.2 Server 0/0 o * + (o * c) + (ε + o + + o + c) d * 1/0 (o * c) * o + d * 0/1 o * + (o * c) + (ε + o + + o + c) d * 1/1 o + + o * (co + ) + d *
The result given by the relational analysis happens to be the exact reachability set, unlike the non-relational one. The non-relational analysis misses the fact that there is at most one d in the second queue, which induces many approximations.

However, this operator ensures the convergence if and only if the alphabet Σ is finite. Thus this work cannot be applied for communicating systems with an infinite alphabet of messages, e.g. a protocol that can send integer values as messages, like the example of Sect. 1.

If we want to deal with such protocols, we must find a way to combine the previous work (on regular languages) with more classical abstractions of infinite domains (intervals, polyhedra, etc...).

Lattice automata

In this section we define with lattice automata an abstract representation for languages on infinite alphabets. The principle of lattice automata is to use elements of an atomic lattice for labeling the transitions of a finite automaton, and to use a partition of this lattice in order to define a projected finite automaton which acts as a guide for defining extensions of the classical finite automata operations.

Irisa

We motivate our choices and show that they lead to a robust notion of approximation, in the sense that normalization is an upper-closure operation and can be seen as a best upper-approximation in the lattice of normalized lattice automata. Lattice automata are finite automata, the transitions of which are labeled by elements of an atomic lattice (Λ, ) instead of elements of a finite and unstructured alphabet. They recognize languages on atomic elements of this lattice. For instance, the interval automaton of Fig. 4 recognizes all sequences of rational numbers x 0 . . . x n-1 where n is odd, x 2i ∈ [0, 1] and x 2i+1 ∈ [START_REF]The APRON numerical abstract domain library[END_REF][START_REF] Bardin | FAST: Fast Acceleration of Symbolic Transition systems[END_REF]. Such an automaton can be used to represent possible contents of a queue containing rational numbers.

[0, 1] [1, 2]
However, the classical operations on finite automata cannot be extended as is on lattice automata. It is in particular the case of the determinization and minimization operations, because some lattice automata cannot be determinized in the usual way (this would require the ability to complement elements). We need these two operations which provide a normal form in the finite case, and which allows to define in a simple way other operations such as union and intersection. Consequently, we propose another notion of determinization which is in some sense an optimal approximation of the classical operation. We first formally define lattice automata, and we advocate the idea of using a partition of the lattice in order to define a projected finite automaton which acts as a guide for defining determinization, minimization operations. We then define the other classical operations such as union and intersection, before defining a suitable widening operator which allows to consider lattice automata as a fully equipped abstract domain.

Basic definition and discussion

Definition 2 (Lattice automaton) A lattice automaton is a tuple Λ, Q, Q 0 , Q f , δ where :

• Λ is an atomic lattice, the order of which is denoted by ;

• Q is a finite set of states;

• Q 0 ⊆ Q and Q f ⊆ Q are the
sets of initial and final states;

• δ ⊆ Q × (Λ \ {⊥}) × Q is a finite transition relation. 1
A finite word w = a 0 . . . a n ∈ At(Λ) * is accepted by the lattice automaton if there exists a sequence q 0 , q 1 , . . . , q n+1 such that q 0 ∈ Q 0 , q n+1 ∈ Q f , and ∀i ≤ n, ∃(q i , λ i , q i+1 ) ∈ δ : a i λ i .

The set of words recognized by a lattice automaton A is denoted by L A . The inclusion relation between languages induces a partial order on lattice automata : Definition 3 (Partial order on lattice automata) The partial order between lattice automata is defined as

A A iff L A ⊆ L A .
Remark 1 (Downward closure of transitions.) With the Definition 2, if there exists a transition (q, λ, q ) in δ, then any (q, λ , q ) with λ λ may be added without modifying the recognized language. Hence, such transitions are redundant.

From now on, we assume that all transitions of a lattice automaton are maximal in the following sense : (q, λ, q ) ∈ δ ∧ (q, λ , q ) ∈ δ implies that λ and λ are not comparable. 1 No transition is labeled with the bottom element ⊥.

PI n˚1839 [0, 0] [2, 2] [2k, 2k]
Figure 5: A family of interval automata A k with unbounded branching degree

1 2 y = 0 x = 0 1 1,2 2 "y = 0 ∧ x = 0" "x = 0 ∧ y = 0" x = 0 ∧ y = 0 "x = 0 ∧ y = 0" x = 0 ∧ y = 0 (a) non-deterministic (b) deterministic automaton automaton ?
Figure 6: Attempt to determinize a lattice automaton on the lattice of affine equalities Remark 2 (Words on atoms) We restrict the recognized words of a lattice automaton to be composed of atoms because we want the two automata of Fig. 8 to be equivalent in terms of their recognized languages. If words were composed of any elements of the lattice, the word composed of the single element {0 ≤ x ≤ 3, 0 ≤ y ≤ 1} would be recognized by the first automaton but not the second one. In the same spirit, we require that the lattice Λ is atomic, so that any element λ ∈ Λ labeling a transition is isomorphic to the set of atoms it dominates.

Remark 3 (Status of ⊥) ⊥ cannot label a transition, not only as a consequence of the previous remark, but also because this corresponds to the intuition that ⊥ does not represent any element and denotes a notion of emptiness.

Definition 4 A lattice-based regular language is a language recognized by a lattice automaton A. We denote by Reg(Λ) the set of lattice-based regular languages.

Definition 2 raises however a number of problems. We expose them before introducing our solution to them. The first problem is related to the bounded branching degree property: in a deterministic finite automaton, there are at most |Σ| transitions outgoing from a state. However, with definition 2, the branching degree of lattice automata is not bounded, as shown in Fig. 5.

The second problem is related to the notion of determinism. The classical notion of determinism can be extended in a straightforward way as follows:

Definition 5 (Deterministic lattice automaton) A lattice automaton Λ, Q, Q 0 , Q f , δ is deter- ministic if it has a unique initial state and if (q, λ 1 , q 1 ) ∈ δ ∧ (q, λ 2 , q 2 ) ∈ δ =⇒ λ 1 λ 2 = ⊥.
Can now any lattice automaton be made deterministic while still recognizing the same language ? The answer is negative, as illustrated by the example of Fig. 6, which uses the lattice of affine equalities [START_REF] Karr | Affine relationships among variables of a program[END_REF] 2 . The problem here is that elements of an atomic lattice cannot be complemented in general. With some lattices, like the lattice of intervals where an element can be complemented by a finite union of intervals, this problem can be overcome by splitting transitions, cf. Fig. 7, but we are back then to the branching degree problem. Fig. 7 illustrates a third annoying aspect: we have given to the alphabet a lattice structure (instead of a weaker partial ordered structure) with the idea of exploiting the lattice operations offered by abstract domains. But in Fig. 7(c) we cheat by using several transitions instead of using the least upper bound operator. Moreover, using such explicit unions may be problematic to define minimization and canonical form. For instance, how to choose between the two minimal automata of Fig. 8 ? The problem here is that there is no canonical representation for unions of convex polyhedra.

-1 0 1 2 3 4 -1 0 1 2 3 1 2 {0 ≤ x ≤ 3, 0 ≤ y ≤ 1 } {0 ≤ x ≤ 1, 1 < y ≤ 2 } 1 2 {1 < x ≤ 3, 0 ≤ y ≤ 1 } {0 ≤ x ≤ 1, 0 ≤ y ≤ 2 } -1 0 1 2 3 4 -1 0 1 2 3
Figure 8: Two deterministic convex polyhedra automata that are equivalent 1 2 The solution we propose to fix these problems is to use a finite partition of the lattice Λ, which allows to decide when two transitions should be merged using the least upper bound operator. The fusion of transitions will induce in general an over-approximation, controlled by the fineness of the partition. The gain is that the projection of labels onto their equivalence classes produces a finite automaton on which we can reuse classical notions.

{0 < x ≤ 3, 0 ≤ y ≤ 2, x + 2y ≤ 5} -1 0 1 2 3 4
Definition 6 (Partitioned lattice automaton (PLA)) A partitioned lattice automaton (PLA) A is a lattice automaton A = Λ, π, Q, Q 0 , Q f , δ equipped with a partitioning function π : Σ → Λ such that Σ is a finite alphabet and the transition relation δ satisfies:

∀(q, λ, q ) ∈ δ, ∃σ ∈ Σ : λ π(σ) A PLA is merged 3 if: (q, λ 1 , q ) ∈ δ ∧ (q, λ 2 , q ) ∈ δ =⇒ π -1 (λ 1 ) ∩ π -1 (λ 2 ) = ∅ Definition 7 (Shape automaton and Shape equivalence) Given a PLA A = Λ, π, Q, Q 0 , Q f , δ , its shape automaton shape(A) is a finite automaton (Σ, Q, Q 0 , Q f , →)
obtained by projecting the transition relation δ onto the equivalence classes: (q, λ, q ) ∈ δ =⇒ q π -1 (λ) -→ q . Two PLA are shape-equivalent if their two shapes recognize the same language.

Two transitions of a PLA labeled by elements belonging to different equivalence classes cannot be merged and are always kept separate, whereas they might be merged in the opposite case. Determin-istic merged PLA have the finite branching degree property: its states can have at most |Σ| outgoing transitions.

From an expressiveness point of view, PLA are as expressive as lattice automata.

Proposition 1 (Equivalence between lattice automata and PLA) Given a lattice automaton A = Λ, Q, Q 0 , Q f , δ and a partitioning function π : Σ → Λ, there exists a partitioned lattice automaton A = Λ, π, Q, Q 0 , Q f , δ recognizing the same language (this relies on the atomic lattice assumption).

Proof: A is obtained from A by replacing each transition (q, λ, q ) of A by at most |Σ| transitions (q, λ i , q ), where

λ i = λ π(σ i ) if λ i = ⊥.
However, for a given partition, merged PLA are strictly less expressive, as shown on Fig. 8 and9 with the trivial partition of size 1. Moreover, if one considers the lattice of affine equalities, which can be partitioned only with the trivial partition of size 1, the automaton of Fig. 6(a) shows that in general merged PLA are strictly less expressive than PLA.

Proposition 2 Let A be a PLA. If shape(A) is deterministic, then A is deterministic.

Proof: Let (q, λ 1 , q 1 ) and (q, λ 2 , q 2 ) be two transitions of A, and (q, σ 1 , q 1 ) and (q, σ 2 , q 2 ) be the two corresponding transitions of shape(A). Since shape(A) is deterministic, π -1 (λ 1 ) ∩ π -1 (λ 2 ) = ∅. Since π is a partitioning function, we have :

1. λ i π(σ i ) 2. π(σ 1 ) π(σ 2 ) = ⊥ So λ 1 λ 2 = ⊥. And then A is deterministic.
The converse is false in general. This property leads us to define a stronger notion of determinism :

Definition 8 (Strong determinism) A PLA A is strongly deterministic if shape(A) is determin- istic.
This notion of determinism is useful since it is defined on the well-known finite automata, and is a guideline for the definition of a determinization algorithm. Therefore, in the sequel, "deterministic" means "strongly deterministic". With all those definitions, we will be able to define a normalized form for lattice-based regular language L. This normalization will exploit the following lemma :

Lemma 1 (Testing language inclusion) Let A = Λ, π, Q, Q 0 , Q f , δ and A = Λ, π, Q , Q 0 , Q f , δ be two PLAs with the same partitioning function. Then A A iff there is a simulation relation R ⊆ ℘(Q) × ℘(Q ) verifying : 1. Q 0 RQ 0 2. ∀X ⊆ Q, ∀Y ⊆ Q : XRY =⇒ (X ∩ Q f = ∅) =⇒ Y ∩ Q f = ∅ 3. Let X ⊆ Q and Y ⊆ Q such that XRY .
For any atom a ∈ At(Λ), there are two sets X a ⊆ Q and Y a ⊆ Q such that X a RY a and:

∃(q x , λ x , q x ) ∈ δ : q x ∈ X ∧ a λ x =⇒ ∃(q y , λ y , q y ) ∈ δ : q y ∈ Y ∧ a λ y ∧ q x ∈ X a ∧ q y ∈ Y a

Irisa

Algorithm: Inclusion test for two PLAs

Input: two PLAs A = Λ, π : Σ → Λ, Q, Q 0 , Q f , δ and A = Λ, π : Σ → Λ, Q , Q 0 , Q f , δ Output: a boolean is included begin is included := true ; R := {(Q 0 , Q 0 )}; ToDo := {(Q 0 , Q 0 )}; while ToDo = ∅ ∧ is included do (X, Y ) := pickAndRemoveElement(ToDo);
for all a ∈ At(Λ) do 1 X a := ∅; Y a := ∅; for all (q x , λ x , q x ) ∈ δ such that q x ∈ X and a λ x do X a := X a {q x }; endfor for all (q y , λ y , q y ) ∈ δ such that q y ∈ y and a λ y do

Y a := Y a ∪ {q y }; endfor if (Y a = ∅ =⇒ X a = ∅) then is included := is included ∧ X a ∩ Q f = ∅ =⇒ Y a ∩ Q f = ∅ ; if (X a , Y a ) / ∈ R then R := R ∪ (X a , Y a ) ; ToDo := ToDo ∪ (X a , Y a ) ; endif endif endfor endwhile return is included ; end 1
The number of atoms may be infinite. So an implementation would manipulate elements λx λy for all outgoing transitions (qx, λx, q x ) ∈ δ, qx ∈ X and (qy, λy, q y ) ∈ δ, qy ∈ Y . Proof: On one hand, if there is a simulation like this one, it is obvious that L A ⊆ L A , because of the definition of a language recognized by a lattice automaton.

On the other hand, if L A ⊆ L A , we can build R starting from Q 0 RQ 0 and using the same algorithm as the "inclusion test algorithm" (Fig. 10). And the condition :

∀X ⊆ Q, Y ⊆ Q , XRY =⇒ (X ∩ Q f = ∅) =⇒ Y ∩ Q f = ∅ is always true, because L A ⊆ L A .
This algorithm works if all states of the two automata are reachable from an initial state and coreachable from a final state. Note that this is an implicit hypothesis for all propositions and algorithms of the present paper.

Note that the algorithm for inclusion test does not need any determinization step. This determinization is implicitly performed on the fly during the algorithm.

Normalization of PLAs

Normalization of partitioned lattice automata will be obtained by merging, determinizing and minimizing PLA. These operations provide a canonical form for PLA. Although this normalization induces an upper-approximation of the recognized language, this is a robust notion in the sense that the approximation is optimal.

Any PLA A = Λ, π, Q, Q 0 , Q f , δ recognizing a language L can be transformed into a merged PLA A m = Λ, π, Q, Q 0 , Q f , δ m
A recognizing a language L m ⊇ L by merging transitions as follows:

q, q ∈ Q σ ∈ Σ λ m = { λ π(σ) | (q, λ, q ) ∈ δ} (q, λ m , q ) ∈ δ m
The upper-approximation on the recognized language comes from the use of the lub operator. For instance, with a single equivalence class on R 2 , the merged PLA associated to any automata depicted on Fig. 8 is depicted on Fig. 9.

Determinization

The determinization of a PLA mimics the determinization of its shape automaton using the subset construction on states and is illustrated on Fig. 11. The difference is that the transitions are merged in the course of the algorithm when they are labeled with values belonging to the same equivalence class. The resulting algorithm is given in Fig. 12.

Proposition 3 (Determinising PLA is a best upper-approximation) Let A be a PLA and A the PLA obtained with the algorithm of Fig. 12. Then A is the best upper-approximation of A as a merged and deterministic4 PLA: 1. A A ;

For any merged and deterministic PLA A based on the same partition as A, A

A =⇒ A A .

Proof: The result is a merged and deterministic PLA because the algorithm determinizes the shape and performs merging of new transitions. It is also clear that the resulting automaton recognizes a greater language than the original one. We must prove the third point of the proposition.

Let A = Λ, π, Q, Q 0 , Q f , δ be the initial PLA, A = Λ, π, X , X 0 , X f , ∆ the result of our algorithm and A = Λ, π, Q , Q 0 = {q 0 }, Q f , δ a merged and deterministic PLA such that L A ⊆ L A .
As usual, we suppose that, in these automata, all states are reachable from the initial states and coreachable form the final states.

We can build two simulation relations R on ℘(Q) × Q and R on ℘(Q) × Q defined as :

• At the beginning, (Q 0 , q 0 ) ∈ R and (Q 0 , q 0 ) ∈ R ,

Algorithm: Determinization of a PLA Input: a PLA A = Λ, π : Σ → Λ, Q, Q 0 , Q f , δ whose states are co-reachable Output: a merged deterministic PLA A = Λ, π, X, X 0 , X f , ∆ begin X := {Q 0 }; X 0 := {Q 0 }; X f := ∅; ∆ := ∅;
ToDo := {Q 0 }; while ToDo = ∅ do x := pickAndRemoveElement(ToDo); for all σ ∈ Σ do λ u := ⊥; x := ∅; for all (q, λ, q ) ∈ δ such that q ∈ x and λ π(σ) = ⊥ do • if we have (Q x , q x ) ∈ R then for all σ ∈ Σ, we consider Q y = {q ∈ Q|∃(q, λ, q ) ∈ δ ∧ q ∈ Q x ∧ λ π(σ)}. Since L A ⊆ L A and A is deterministic, there is a unique q y ∈ Q verifying (q x , λ , q y ) ∈ δ ∧ λ π(σ), thus we add (Q y , q y ) ∈ R . Note that we have λ = {λ|∃(q, λ, q ) ∈ δ ∧ q ∈ Q x ∧ λ π(σ)} λ }. Since L A ⊆ L A and A is deterministic, there is a unique q y ∈ Q verifying (q x , λ , q y ) ∈ δ ∧ λ π(σ), so we can also add (Q y , q y ) ∈ R .

λ u := λ u (λ π(σ)); x := x ∪ {q }; endfor if λ u = ⊥ then ∆ := ∆ ∪ {(x, λ u , x )}; if x ∈ X then X := X ∪ {x }; if x ∩ Q f = ∅ then X f := X f ∪ {x }; ToDo := ToDo ∪ {x }; endif endif endfor endwhile end
By construction, the two simulation relations define a simulation relation

R ⊆ Q × Q : (q , q ) ∈ R = ∃X ∈ ℘(Q), (X, q ) ∈ R ∧ (X, q ) ∈ R so L A ⊆ L A .
Corollary 1 (The determinisation operation is an upper-closure operation) The operation det : PLA → PLA is an upper-closure operation: it is (i) extensive: det (A) A; (ii) monotone: for any A, A defined on the same partition, A A ⇒ det(A) det (A ); and (iii) idempotent: det(det (A)) = det(A).

Proof: The extensivity has already been shown. We have A A det(A ). det(A) being the best approximation of A as a deterministic merged PLA, det(A) det(A ), which proves the monotonicity. The idempotence is a trivial consequence of Prop. 3.

[30] also studies the determinization of extended automata, but their extended automata represent programs and have a different semantics. Transitions are labeled not only by guards (which could be identified to our labels) but also assignments. In this context, the proposed determinization algorithm is exact but may not terminate (it is only a semi-algorithm).

PI n˚1839

Minimization

We use for PLA a notion of minimization based on its shape automaton, in the same spirit as for the notion of determinism.

Definition 9 A PLA is minimal or normalized if it is merged and if its shape automaton is minimal and deterministic. A normalized PLA will be also called a NLA (normalized lattice automaton).

The algorithm to minimize a PLA consists in removing its unconnected states, determinizing it according to the previous algorithm and quotienting it according to the equivalence bisimulation relation as defined on the states of its shape automaton (cf. Sect. 3). However, when quotienting the states of a PLA, transitions labeled with elements belonging to the same equivalence class are merged, which may induce an over-approximation of the recognized language, as shown on Fig. 11.

Definition 10 (Quotient PLA) Given a merged PLA Λ, π : Σ → Λ, Q, Q 0 , Q f , δ and an equiva- lence relation ≈ on the set of states Q, the quotient automaton A/ ≈ = Λ, π, Q, Q 0 , Q f , δ is defined by • Q = Q/ ≈, the set of equivalence classes; • Q 0 = { q|q ∈ Q 0 } and Q f = { q|q ∈ Q f };
• δ is defined by the rule σ ∈ Σ λ u = {λ π(σ) | ∃q 0 ∈ q, ∃q 0 ∈ q : (q 0 , λ, q 0 ) ∈ δ} ( q, λ u , q ) ∈ δ

Note that the quotient automaton is a merged PLA.

Theorem 1 (Minimizing PLA is a best upper-approximation) For any PLA A, there is a unique (up to isomorphism) NLA A based on the same partition π such that 1. A A

for any NLA A based on the partition π, A A =⇒ A A .

Proof: The minimization algorithm consists first in determinizing the automaton, and then, in quotienting the result by the largest bisimulation relation on its states induced by its shape automaton. The result is merged and deterministic and the quotient operation ensures that its shape is minimal and deterministic. Thus it is minimal according to Def. 9.

Then we show that if two automata A 1 and A 2 recognize the same language L then minimize(A 1 ) is isomorph to minimize(A 2 ). We have L ⊆ L det(A2) and det(A 2 ) is merged and deterministic. According to the properties of det(A 1 ), we have L det(A1) ⊆ L det(A2) . The same thing holds when switching A 1 and A 2 , so det(A 1 ) and det(A 2 ) are two deterministic automata recognizing the same language. Thus the two automata are bisimilar according to a variant of Lemma 1 and we can conclude that L minimize(A1) = L minimize(A2) . Moreover shape(minimize(A 1 )) and shape(minimize(A 2 )) are isomorphic, and we can extend this isomorphism to minimize(A 1 ) and minimize(A 2 ) thanks to the previous language equality.

Definition 11 Let fix a partitioning function π : Σ → Λ. For any language L ∈ Reg(Λ) recognized by a lattice automaton A, L will denote the language recognized by the unique NLA A verifying the properties of Thm. 1.

Corollary 2 (The normalisation operation is an upper-closure operation) The function Corollary 3 For any languages L 1 and L 2 ,

L 1 ∪ L 2 ⊆ L 1 ∪ L 2 (5)
L 1 ∩ L 2 ⊆ L 1 ∩ L 2 (6)
The inclusion is strict, because of the use of least upper bound during normalization. To see this, consider the lattice of intervals on rationals, partitioned with the trivial partition of size 1. Take

L 1 = 0, L 2 = 2. One has L 1 = L 1 , L 2 = L 2 , L 1 ∪ L 2 = 0 + 2, but L 1 ∪ L 2 = x∈[0,2]
x. Take now

L 1 = 0 + 2 and L 2 = 1 + 3. One has L 1 = x∈[0,2] x, L 2 = x∈[1,3] x, L 1 ∩ L 2 = x∈[1,2] x, but L 1 ∩ L 2 = ∅.
Complexity. Let A be a lattice automaton with n states, m transitions and a partition of size p (i.e. |Σ| = p). The complexity of the previous algorithms is given on Tab. 1, where the operations on Λ are considered as atomic.

Thm. 1 defines a normalization for languages recognized by PLA. For any language L ∈ Reg(Λ) recognized by a PLA A, L will denote the language recognized by the unique NLA verifying the properties of Thm. 1. The set of NLA defined on Λ with the partition π will be denoted by Reg(Λ, π), which denotes also the corresponding set of recognized languages.

Having defined a normal form for PLA, we can now specify classical operations on languages recognized by NLA by defining them on their automata.

Refinement of the partitioning function

In the previous paragraphs, the partitioning function π : Σ → Λ was fixed. The precision of the approximations made during the merging, determinization and minimization operations depends on the fineness of the partitioning function. For example, all outgoing transitions from a given state would be merged during the determinization algorithm employed with the trivial partition of size 1.

Definition 12 A partitioning function π 2 : Σ 2 → Λ refines a partitioning function π 1 : Σ 1 → Λ if : ∀σ 2 ∈ Σ 2 , ∃σ 1 ∈ Σ 1 : π 2 (σ 2 ) π 1 (σ 1 ) Let A 1 = Λ, π 1 : Σ 1 → Λ, Q, Q 0 , Q f , δ 1 be a PLA. The automaton A 2 = Λ, π 2 : Σ 2 → Λ, Q, Q 0 , Q f , δ 2 refines A 1 if π 2
refines π 1 and the transitions of δ 2 are obtained by :

(q, λ 1 , q ) ∈ δ 1 σ 2 ∈ Σ 2 λ 2 = λ 1 π(σ 2 ) (q, λ 2 , q ) ∈ δ 2

PI n˚1839

Refining an automaton does not modify immediately the recognized language, but leads to a more precise upper-approximation in merging, determinization and minimization operations.

Proposition 4 Let A 1 be a PLA and A 2 a PLA refining A 1 . Then L A 1 = L A 2 , merge(A 1 ) merge(A 2 ), det(A 1 ) det(A 2 ) and A 1 A 2 .
Proof:

1. Obvious 2. For two states q, q ∈ Q and for any σ 1 ∈ Σ 1 , σ 2 ∈ Σ 2 such that π 2 (σ 2 ) π 1 (σ 1 ), we have :

λ m2 = { λ π 2 (σ 2 ) | (q, λ, q ) ∈ δ 1 } λ m1 = { λ π 1 (σ 1 ) | (q, λ, q ) ∈ δ 1 }
where λ mi labels the transition obtained by merging the transitions between q 1 , q 2 labeled with elements in π i (σ i ).

3. Idea of the proof : during each iteration of the while loop, the determinization of the automaton A 2 merges less states and less transitions than the determinization of the automaton A 1 .

4. Idea of the proof : the equivalence class of the bisimulation relation (for the quotienting algorithms) are also more precise with π 2 , so both determinization and quotienting merge less states and transitions of the original automaton.

Refining the partition π makes he class of normalized languages Reg(Λ, π) more expressive.

Proposition 5 Let π 1 and π 2 two partitioning functions for Λ, with π 2 refining π 1 . Then Reg(Λ, π 1 ) ⊆ Reg(Λ, π 2 ).

Proof: Let A 1 ∈ Reg(Λ, π 1 ) be a NLA. Its refinement A 2 according to π 2 (cf. Def. 12) is normalized, and thus A 2 ∈ Reg(Λ, π 2 ).

Choosing an adequate partitioning function is thus important. For the analysis of SCM, where data messages are usually composed of a message type and some parameters, the type of the message defines a natural partition. When this standard partition is not sufficient for the analysis, it can be refined to a more adequate partition. In this sense, the abstraction refinement techniques based on partitioning (see for instance [START_REF] Jeannet | Dynamic partitioning in linear relation analysis. application to the verification of reactive systems[END_REF][START_REF] Mauborgne | Trace partitioning in abstract interpretation based static analyzers[END_REF]) are applicable to lattice automata.

Operations on PLA and their recognized languages

After the definition of a robust normalization concept, we can now define the classical operations on languages (union, intersection, . . . ) by defining them on lattice automata.

Set operations

Inclusion test. Two PLAs that are not normalized can be compared for language inclusion using a simulation relation taking into account the partial order of the lattice, cf. lemma 1. If they are normalized, one can first compare for inclusion their shape automata, and in case of inclusion, one can compare the labels of matching transitions.

Irisa Λ = ({a, b, c, d}×I(Q) ordered by (x 1 , I 1 ) (x 2 , I 2 ) ⇔ x 1 = x 2 ∧ I 1 ⊆ I 2 and partitioned with π : x ∈ {a, b, c, d} → (x, [-∞, +∞]) (a, [0, 0]) (b, [0, 0]) (d, [0, 0]) (d, [2, 2]) (c, [0, 0]) (a, [0, 0]) (b, [0, 0]) (d, [0, 0]) (d, [2, 2]) (c, [0, 0]) (Deterministic but not minimal) (a, [0, 0]) (b, [0, 0]) (d, [0, 0]) (d, [2, 2]) (Deterministic and minimal) (a, [0, 0]) (b, [0, 0]) (d, [0, 2]) (a) Lattice (b)
The two minimized automata (c) Intersection to be intersected and its approximation

A i = Λ, π, Q i , Q i 0 , Q i f
, δ i can be computed very simply as the disjoint union of the two PLA; this produces the PLA

A = Λ, π, Q 1 ∪ Q 2 , Q 1 0 ∪ Q 2 0 , Q 1 f ∪ Q 2 f , δ 1 ∪ δ 2 which is not deterministic.
Normalizing A transforms the exact union operation in an upper bound operator defined as follows:

A 1 A 2 = A 1 ∪ A 2 .
As a corollary of Theorem 1, this upper bound operator is actually a least upper bound operator on the set of NLA ordered by language inclusion.

Intersection and its normalized upper-approximation. The exact intersection of two PLAs

A i = Λ, π, Q i , Q i 0 , Q i f
, δ i can be computed as a product of the two PLA; this produces a PLA

A = Λ, π, Q 1 × Q 2 , Q 1 0 × Q 2 0 , Q 1 f × Q 2 f , δ where δ is defined by (q 1 , λ 1 , q 1 ) ∈ δ 1 (q 2 , λ 2 , q 2 ) ∈ δ 2 λ 1 λ 2 = ⊥ ((q 1 , q 2 ), λ 1 λ 2 , (q 1 , q 2 )) ∈ δ
We implicitly remove unconnected states in A. If the input automata are normalized, A is merged and deterministic, but not necessarily minimal. Minimizing it may induce an upper-approximation, as shown by Fig. 13. Thus, NLA are not closed under (exact) intersection.

These operations allow to equip the set of NLA with a join semilattice structure.

Proposition 6 (NLA as a join semilattice) The set of NLA defined on an atomic lattice Λ with a fixed partition π, ordered by language inclusion, is a join semilattice: it has bottom and top elements, and a least upper bound operator.

If the standard lattice operations on Λ are computable, so are the corresponding operations on the join semilattice of NLA.

Proof: It is clear that the bottom and top elements of this semilattice are respectively the empty automaton Λ, π, Q = ∅, Q 0 = ∅, Q f = ∅, δ = ∅ recognizing no words, and the universal automaton

Λ, π, Q = {q}, Q 0 = Q, Q f = Q, δ = σ∈Σ (q, π(σ), q
) recognizing any word on the alphabet At(Λ). The least upper bound operator is the operator on NLA defined in Sect. 5.3. Last, we have also given in Sect. 5.3 algorithms for testing inclusion and for computing the least upper bound.

PI n˚1839

Remark 4 (Deterministic merged PLA as a full lattice) If we consider the set of deterministic and merged (but not necessarily minimal) PLA, then this set partially ordered by language inclusion has a true lattice structure, instead of just the join semilattice structure of NLA. Indeed, Proposition 3 may be used to prove that the determinization of the exact union is a least upper bound operation, and as the exact intersection of 2 deterministic merged PLA is a deterministic merged PLA, this intersection is trivially a greatest lower bound.

One could manipulate deterministic merged PLA instead of NLA. But there may be several deterministic merged PLA recognizing the same language, hence the isomorphism between languages and automata is lost. The other drawbacks of such a choice is that testing inclusion is more expensive (one needs to use simulation) and that one cannot extend the widening operation on finite automata defined in Sect. 4.3.

Other language operations

Language concatenation. Language concatenation on deterministic PLA is performed exactly as for finite automata, by substituting to the final states of the first automaton a copy of the initial state of the second automaton. The obtained automaton is non-deterministic in general and requires normalization. Language concatenation can also be computed on non deterministic PLA, by using transitions and -closure to remove them.

Left derivation. In the finite case, the left derivation [START_REF] Janusz | Derivatives of regular expressions[END_REF] of a finite automaton is performed w.r.t. a letter. The corresponding operation would consists in deriving a PLA according to an equivalence class. However, the partition is a way to control the precision of the approximations performed by the various operations on PLA, and it does not have a semantic meaning.

As a consequence, we define a more general left derivation L/λ operator as follows:

•/• : Reg(Λ) × Λ → Reg(Λ) (L, λ) → {ω ∈ At(Λ) * | ∃a λ : a • ω ∈ L}
We have clearly the identity L/λ = a∈At (λ) L/a, from which we can deduce the following proposition:

Proposition 7 Let λ ∈ Λ and (λ σ ) σ∈Σ be the projection of λ on the partition defined by π : Σ → Λ.

Then L/λ = σ∈Σ L/λ σ .

The left derivation can be implemented exactly on a deterministic PLA

A = Λ, π, Q, Q 0 = {q 0 }, Q f , δ as follows: •/• : PLA × Λ → (Σ → PLA) (L, λ) → ( σ → A/(λ π(σ)) )
where A/(λ π(σ)) is the empty automaton if λ π(σ) = ⊥, and the deterministic PLA Λ, π, Q, Q 0 = {δ(q 0 , σ)}, Q f , δ otherwise. One obtains a finite set of deterministic automata instead of a single one. This set can be of course upper-approximated by the least upper bound deterministic PLA, denoted by A/λ = σ∈Σ (A/λ)(σ).

"First" and "Pop" operations. In addition to the left derivation, it may also be useful to extract the letters beginning the words of a language as follows:

first : Reg(Λ) → ℘(At(Λ)) L → {a ∈ At(Λ) | a • ω ∈ L} Irisa NLA
O(2 n ) normalized no normalized intersection ( ) O(n 2 log n) normalized no normalized pop O(p • 2 n ) normalized no
Table 2: Complexity of various operations on NLA. We assume NLA with n states, m transitions and a partition of size p (i.e. |Σ| = p)

The equivalent (algorithmic) definition on a deterministic PLA

A = Λ, π, Q, Q 0 = {q 0 }, Q f , δ is : first : PLA → (Σ → Λ) A → (σ → first (A)(σ))
where for each σ ∈ Σ, first(A)(σ) is the label of the unique transition (q 0 , λ, q) ∈ δ with λ π(σ), if it exists, and ⊥ otherwise. It is clear that the set of atoms covered by first (A) is exactly first(L A ) :

σ∈Σ {a ∈ At(Λ) | a first (A)(σ)} = first(L A )
The first operation can be combined with the left derivation in order to implement the pop operation, which extracts the first letters and derives the corresponding "residue" automaton :

pop : PLA × Λ → (Σ → Λ × PLA) (A, λ) → σ → λ first(A)(σ) , A/(λ π(σ))
The complexity of the previous operations is summarized on Tab. 2.

Widening on NLA

The widening on NLA we define here combines the widening on finite automata of [START_REF] Gall | Verification of communication protocols using abstract interpretation of FIFO queues[END_REF] reminded in Sect. 4.3 with the standard widening operator ∇ Λ : Λ × Λ → Λ that we assume for the atomic lattice Λ. If a widening operator is not strictly required for Λ (because Λ satisfies the ascending chain condition), then ∇ Λ can be defined as the least upper bound . We first extend the ρ k operator defined on finite automata in Sect 4.3.

Definition 13 (Operator

ρ k on NLA) Let A = (Λ, π, Q, Q 0 , Q f , ∆) be a NLA, shape(A) = (Σ, Q, Q 0 , Q f , δ) its shape automaton. Let k ≥ 0 be an integer and ≈ k the k-depth bisimulation relation on Q induced by the partition of Q into Q 0 ∩ Q f , Q 0 \ Q f , Q f \ Q 0 and Q \ (Q 0 ∪ Q f ) and the transition relation δ ⊆ Q × Σ × Q. We define ρ k (A) as the quotient PLA A/ ≈ k .
The widening operator we suggest consists in applying the operator ρ k when the two argument automata have a different shape automaton, and to apply the widening operator of the lattice Λ on their matching transitions when the two argument automata have the same shape automaton, as illustrated by Fig. 14.

PI n˚1839 [-7, -5] ∇ 0 [-9, -2] [6, 9] = [-9, -2] [6, 9]
[-9, -5] Definition 14 (Widening on NLA) Let A 1 and A 2 be two NLA defined on the same partition π with A 1 A 2 . The widening operator ∇ k is defined as :

A 1 ∇ k A 2 = ρ k (A 2 ) if shape(A 1 ) = shape(ρ k (A 2 )) A 1 A 2 otherwise (which implies shape(A 1 ) = shape(A 2 ))
where A 1 A 2 is the NLA A which has the same set of states as A 1 and A 2 and the set of transitions δ defined by the rule:

σ ∈ Σ (q, λ 1 , q ) ∈ δ 1 (q, λ 2 , q ) ∈ δ 2 λ 1 , λ 2 π(σ) (q, (λ 1 ∇ Λ λ 2 ) π(σ), q ) ∈ δ If A 1 A 2 , then A 1 ∇ k A 2 A 1 ∇ k (A 1 A 2 ).
Notice that with the other hypothesis, the condition shape(A 1 ) = shape(ρ k (A 2 )) is equivalent to shape(A 1 ) shape(ρ k (A 2 )), and its negation shape

(A 1 ) = shape(ρ k (A 2 )) ⊇ shape(A 2 ) implies shape(A 1 ) = shape(A 2 ).
Theorem 2 ∇ k is a proper widening operator:

1. for any NLA A1, A 2 defined on the same partition such that

A 1 A 2 , A 2 A 1 ∇ k A 2 ;
2. If there is an increasing chain of NLA A 0 A 1 . . . A n . . ., the chain A 0 A 1 . . . A n . . . defined as A 0 = A 0 and

A i+1 = A i ∇ k (A i A i+1
) is not strictly increasing.

Proof:

1. We have A 1 A 2 by hypothesis. If shape(A 1 ) = ρ k (shape(A 2 )) = shape(ρ k (A 2 )), A 1 ∇ k A 2 = ρ k (A 2 ) A 2 . If shape(A 1 ) = shape(A 2 ) = ρ k (shape(A 2 )), A 2 A 1
A 2 because for each pair of matching transitions (q, λ 1 , q ) and (q, λ 2 , q ) with λ 1 , λ 2 π(σ), we have λ 2 (λ 1 ∇ Λ λ 2 ) π(σ) (as ∇ Λ is a widening operator on Λ).

2. (A i ) i≥0 is an increasing chain of NLA because of the first property. Thus, (S i = shape(A i )) i≥0 is an increasing chain of finite automata. Moreover, by definition of

∇ k on NLA, S i+1 = S i ∇ k (S i S i+1 ) = ρ k (S i S i+1
). As ∇ k as defined on finite automata is a widening operator, the chain (S i ) i≥0 becomes stationary at some rank N . The chain (A i ) i≥N is thus an increasing sequence of NLA with identical shape automaton S. For each transition (q, σ, q ) ∈ δ S , one can extract the corresponding transition sequence (q, λ i , q ) ∈ δ A i with λ i π(σ). The sequence (λ i ) i≥N converges after a finite number of steps, because ∇ Λ is a widening operator. As there is only a finite number of transitions in the shape automaton S, the sequence (A i ) i≥N also converges after a finite number of steps. Irisa 5.5 NLA as an abstract domain for languages, stacks and queues.

Normalized lattice automata allows to define an abstract domain functor which lifts abstract domains for some set to abstract domains for languages on this set. More precisely, given an atomic abstract lattice A γ A --→ ℘(S) for some set S with the concretization function γ A , and a partitioning function π for A, Reg(A, π) can be viewed as an abstract domain for L(S) = ℘(S * ), the languages on elements of S, with the concretization function

γ : Reg(A, π) → ℘(S * ) A → {s 0 . . . s n ∈ S * | a 0 . . . a n ∈ L A ∧ ∀i : s i ∈ γ A (a i )}
and the widening operator of Def. 14. Reg(A, π) is a non-complete join semilattice of infinite height.

We have in addition the following monotonicity result for Reg(A, π) seen as a functor.

Theorem 3 Let γ i : A i → ℘(S), i = 1,
: Reg(A 1 , π 1 ) → Reg(A 2 , π 2 ) such that Γ 1 = Γ 2 • Γ 12 .
Most languages operations can be efficiently abstracted in Reg(A, π). This is in particular the case of languages operations corresponding to the operations offered by the FIFO queue or stack abstract datatypes. Hence, Reg(A, π) is a suitable abstract domain for FIFO queues or stacks on elements of S.

Application to the abstract interpretation of SCM

We illustrate in this section the application of the abstract domain Reg(A, π) defined in the previous section to the analysis of symbolic (or extended) Communicating Machines. This application is actually the initial motivation for the study of lattice automata.

Symbolic Communicating Machines

Symbolic Communicating Machines (SCM) are Communicating Finite-State Machine extended with a finite set of variables V , the values of which can be sent into FIFO queues, cf. Fig. 1. A transition is triggered when a condition on the value of the variables is satisfied. In such a case, the transition can first emit or receive values from a FIFO queue, then modify the values of variables, and last make the control jump to the destination location. This model is similar to other models like Extended Communicating Finite-State Machines [START_REF] Higuchi | A verification procedure via invariant for extended communicating finite-state machines[END_REF] or Parametrized Communicating Extended Finite-State Machines [START_REF] Lee | Protocol specification using parameterized communicating extended finite stte machines -a case study of the atm abr rate control scheme[END_REF].

Definition 15 A SCM with N queues is defined by a tuple C, V, c 0 , Θ 0 , P, ∆ where :

PI n˚1839
• C is a nonempty finite set of locations (control states).

• V = {v 1 , . . . , v n } is a nonempty, finite set of variables. The domain of values of a variable v is denoted by D v , and the set of valuations of all variables in V by D V .

• c 0 ∈ C is the initial control state, and Θ 0 ⊆ D V , a predicate on V , is the initial condition.

• P = {p 1 , . . . , p n } is a nonempty, finite set of formal parameters that are used to send/receive values to/from FIFO queues. We assume that all queues use the same set of parameters D P .

• ∆ is a finite set of transitions. A transition δ is either an input c 1 , G, i? p, A, c 2 or an output c 1 , G, i! p, A, c 2 where :

1. c 1 and c 2 are resp. the origin and destination locations;

2. i ∈ [1.
.N ] is a queue number 3. p is the vector of formal parameters, which holds the values sent or received to/from the queue i;

4. G( v, p) ⊆ D V × D P is a predicate on the variables and the formal parameters (also called guard).

5.

A is an assignment of the form v := A( v, p), where A : D V × D P → D V , which defines the values of the variables after the transition.

Compared to the definition of Extended Communicating Finite-State Machines [START_REF] Higuchi | A verification procedure via invariant for extended communicating finite-state machines[END_REF], the values sent to queues may be of any type. Indeed, our model is closer to the Parametrized Communicating Extended Finite-State Machines model [START_REF] Lee | Protocol specification using parameterized communicating extended finite stte machines -a case study of the atm abr rate control scheme[END_REF] (although there is no major difference between the three models). As a consequence, the alphabet of the queue contents is D P . This alphabet is not finite if D P is not finite.

The operational semantics of a SCM C, V, c 0 , Θ 0 , P, ∆ is given as an infinite transition system Q, Q 0 , → where

• Q = C × D V × (D P ) * N is the set of states; • Q 0 = { c 0 , v, ε, . . . , ε | v ∈ Θ 0 } is the set of initial states;
• → is defined by the two rules:

(c 1 , G, i! p, A, c 2 ) ∈ ∆ w i = w i • p G( v, p) v = A( v, p) c 1 , v, w 1 , . . . , w i , . . . , w N → c 2 , v , w 1 , . . . , w i , . . . , w N (c 1 , G, i? p, A, c 2 ) ∈ ∆ w i = p.w i G( v, p) v = A( v, p) c 1 , v, w 1 , . . . , w i , . . . , w N → c 2 , v , w 1 , . . . , w i , . . . , w N A global state of a SCM is thus a tuple c, v, w 1 , . . . , w N ∈ C × D V × (D P ) * × • • • × (D P ) *
where c is a control state, v is the current value of the variables and w i is a finite word on D P representing the content of queue i.

The concrete collecting semantics of a SCM depicted on Tab. 4 is deduced from the operational semantics as it was done in Sect. 4.2. It is a bit more complex because the model involves symbolic operations. Irisa 6.2 SCM with a single queue: a simple approach There are classical solution for the abstraction of scalar variables. Consequently, the main issue of applying abstract interpretation techniques on this model is the abstraction of the queue contents. Whereas the queue contents in the CFSM model were abstracted by regular languages, queue contents in the SCM model will be abstracted using the abstract domain of lattice automata.

If there is a single queue, the concrete set of states associated to each control point c ∈ C has the structure ℘(D V × (D P ) * ): one associates to each control point the set of possible configurations for the variables of the communicating machine and its FIFO queue

The concrete lattice ℘(D V × (D P ) * ) can be abstracted with ℘(D V ) × L(D P ) by projecting the two components. This allows to abstract ℘(D V ) using classical abstractions for variables of the environment, and to use lattice automata for abstracting the domain of queue contents L(D P ).

For the sake of simplicity, and as an example, we will assume in the sequel that all variables and parameters are of rational type, and that sets of valuations are abstracted using the lattice of convex polyhedra V (k) = Pol(Q k ). We have the abstraction

℘(Q n × (Q p ) * ) --→ ← --℘(Q n ) × L(Q p ) ←-V (n) × Reg(V (p) )
As the atoms of the lattice V (p) = Pol(Q p ) are precisely the elements of Q p , the concretization function of Reg(V (p) ) is just the identity. The induced abstract semantics is given on Tab. 5.

Example. We consider the protocol presented in the introduction (Fig. 1). For the purpose of the analysis, we make the asynchronous product of the two automata. The result is a control structure with four states, labeled 00, 01, 10 and 11, with the following convention : the SCM is in the "xy" state if the sender is in the "x" state and the receiver is in the "y" one.

The example was modeled by a system of equation and we solved the reachability analysis using a generic fix-point calculator. We used the polyhedra abstract lattice as implemented in the APRON library [START_REF]The APRON numerical abstract domain library[END_REF]. No partitioning of the alphabet lattice was employed in this example. We obtained the result of Tab. 6.

The result of this analysis is disappointing: one is not able to prove that the messages contained in the queues are indexed by integers that are lower than the variable s. This is not due to the queue abstraction, nor due to the variables abstraction, but to the coupling of the two abstractions. The following section proposes a solution to this problem..

SCM with a single queue: linking message and state variables

The idea to improve on the previous abstraction is to use an augmented semantics to link the message variables contained in queues with the state variables of the machines. The proposal of this section is to put into queues not only the queue content itself, but also (a subset of) the environment. This allows not only to establish relations between messages in queues and the current environment, but also to indirectly establish relations between the messages contained in different letters. For instance, the abstract value s ∈ [START_REF] Bouajjani | Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations[END_REF][START_REF] Bouajjani | Abstract tree regular model checking of complex dynamic data structures[END_REF], data({sp = 3}) • data({sp = 2}) • data({sp = 1}) will represent the 2 concrete states (s = 8, data(5) • data(6) • data(7)) and (s = 9, data(6) • data [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF] • data( 8)). This is to be compared with the standard abstraction of these 2 states:

s ∈ [8, 9], data(p ∈ [5, 6])) • data(p ∈ [6, 7]) • data(p ∈ [7, 8])
which represents 2 4 = 16 concrete states.

PI n˚1839

Example. We performed a new analysis based on these non-standard semantics on the same example as before. A 'widening up to" operator was used instead of the standard widening on polyhedra [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]. We obtained the better result of Tab. 7.

This analysis is quite accurate, since it shows that :

• 0 ≤ a ≤ s ≤ a + 10 • 0 ≤ p ≤ s -1 • 0 ≤ v ≤ s -1
Remark 5 (Efficiency of the approach.) It should be noted that the abstraction of this section is much more expensive than the abstraction of Sect. 6.2, because guards and assignments do not apply only on the abstract value representing state variables, but also the abstract values labeling the transitions of the automata. This suggests the use of a small partition π of the lattice Λ and the use of a small parameter k in the widening, in order to keep the lattice automata reasonably small. However, the gain in precision brought by this approach worth it, although experimental results on a significative set of examples is still lacking.

Remark 6 (The particular case of a partition of size 1) In our analysis examples, we did not exploit a partition of the alphabet lattice. In such a case, normalized lattice automata have a very simple, linear structure of the form:

q 0 q 1 q 2 . . . . . . q n
If such an automaton is the normalized image of the widening operator with parameter k, then n ≤ k + 2.

λ 0 λ 1 λ n-1 λ n
In general, the most natural choice for the analysis of SCM is to partition the alphabet according to the different kinds of messages exchanged (transmission, retransmission, acknowledgment, . . . ).

SCM with several queues

As in Sect. 4.3, there are mainly two ways to analyze systems with several queues. One can follow :

• a non-relational, attribute-independent method, in which an abstract configuration is defined by a polyhedron representing the value of the state variables and N lattice automata, each representing a queue content,

• or a relational, attribute-dependent method, in which a single lattice automaton recognizes concatenated words w = w 1 w 2 . . . w N , where each subword w i represents the content of the queue i and is a special separating character [START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using QDDs[END_REF].

The extension to lattice automata of these two variants discussed in Sect. 4.3 for finite automata is straightforward. In the previous subsections, the analyzed example, which has two FIFO queues, was implicitly analyzed with a non-relational approach.

Irisa

Prog = (P i ) 0≤i<n : A program is defined by a set of procedures LVar i , l i : Set of local variables of procedure P i fp i : Tuple of formal call parameters of procedure P i fp i ⊆ LVar i fr i : Tuple of formal return parameters of procedure P i fr i ⊆ LVar i G i = K i , I i : Flow graph of the procedure P i K i : Control points of the procedure P i s i , e i ∈ K i : start and exit points of procedure P i

Application to interprocedural analysis

The analysis of communicating machines was the initial motivation for the study of lattice automata in Sect. 5. However there is an interesting application in precise interprocedural analysis, where one can use lattice automata for abstracting call-stacks. This would allow both to simplify and to improve the abstraction proposed in [START_REF] Jeannet | Abstracting call-stacks for interprocedural verification of imperative programs[END_REF]. One can also see this application as an extension to infinite state programs of [START_REF] Esparza | A BDD-based model checker for recursive programs[END_REF] which uses pushdown automata to model finite-state recursive programs and finite automata for representing (co)reachable sets of configurations.

Program model. Tab. 8 sums up our notations and assumptions on recursive programs. Notice that we assume no global variables, and parameter passing by value. We use a symmetrical notion of effective and formal call parameters for return parameters in an instruction (y 1 , y 2 ) = P (x 1 , x 2 ) where y 1 , y 2 are effective return parameters assigned from formal return parameters fr in P . To integrate the call-string and functional approach, we make an important assumption, which is that formal parameters are not modified in a procedure. This is not restrictive, as one can always copy such variables into local variables. Tab. 9 defines the semantic domains used for these programs. We assume that the top of a stack Γ ∈ Act + is on the left side of the word Γ, but the other convention is also possible. 5We do not detail more the program model, as we will focus on the abstraction of call-stacks and we will not detail the induced abstraction of the instructions and procedure calls and returns.

Well-formed call-stacks. Reachable call-stacks should reflect the equality of effective parameters in a caller procedure and formal callee parameters in the callee procedure. Thus well-formed callstacks Γ = c n , n . . . c 1 , 1 . . . c 0 , 0 satisfy : ∀i < n : i+1 ( fp) = i ( x) where x denotes the effective parameters at the call point c i and fp the formal call parameters in the corresponding callee procedure. We will implicitly focus on such well-formed stacks.

Using lattice automata for interprocedural analysis. In the concrete semantics of programs, it is standard to partition the state-space according to the current control point. Thus, we use the identity Act + = K → LEnv × Act * . Now, given an abstraction ℘(LEnv ) --→ ← --Λ for environments, we can use the following abstraction:

℘(Act + ) ---→ ← --- α γ K → Λ × Reg(K × Λ)
The most natural partitioning for the lattice K × Λ is of course the finite partitioning function π(k) = {k} × Λ .

In the forward abstract (operational) semantics induced by this abstraction, an intraprocedural instruction modifies only Y in an abstract configuration (Y, Γ) ∈ Λ × Reg(K × Λ). A procedure call from an abstract configuration (Y, F ) at point c results in a configuration of the form (Y , ({c}, Y ) • F ) at start point s of the callee. A procedure return from an abstract configuration (Y, F ) at exit point e to the return point c consists in computing Y = first(F )(c) and in modifying it using the return value in Y . This is where it is useful to exploit the well-formedness of call-stacks, by unifying Y with Y using the equality Y ( fp) = Y ( x) before assigning the formal return parameters in Y to the effective return parameters in Y .

One can define similarly a backward abstract semantics, and one can also intersect the resulting backward analysis with the result of a forward analysis, as described in [START_REF] Jeannet | Abstracting call-stacks for interprocedural verification of imperative programs[END_REF] Interprocedural analysis by explicit representation of the call-stacks. The call-string approach of [START_REF] Sharir | Semantic foundations of program analysis[END_REF], generalized by tokens in [START_REF] Jones | A flexible approach to interprocedural data flow analysis and programs with recursive data structures[END_REF] corresponds to a very strong abstraction of the call-stacks in which the value of variables is largely ignored. It is more suitable to compilation-oriented dataflow analysis than to program verification. A different line of work consists in modeling recursive programs using pushdown automata, and exploiting the property that the set of (co)reachable stacks of pushdown automata is regular [START_REF] Caucal | On the regular structure of prefix rewriting[END_REF] and its computation has a polynomial complexity [START_REF] Esparza | An automata-theoretic approach to interprocedural data-flow analysis[END_REF][START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model checking[END_REF][START_REF] Finkel | A direct symbolic approach to model checking pushdown systems[END_REF]. The application of this approach to verification is mainly restricted either to programs manipulating finite-state variables, or to programs first abstracted to such programs [START_REF] Esparza | A BDD-based model checker for recursive programs[END_REF], although [START_REF] Reps | Weighted pushdown systems and their application to interprocedural dataflow analysis[END_REF] removes some restrictions using weights on transitions. The approach sketched in this section can be seen as an extension of this line of work to more expressive programs, where undecidability is overcome by resorting to approximations.

The lattice automata abstraction may be seen as both an improvement and a simplification of [START_REF] Jeannet | Abstracting call-stacks for interprocedural verification of imperative programs[END_REF], which derives and unifies two classical techniques for interprocedural analysis (namely the call-string and functional approaches identified by [START_REF] Sharir | Semantic foundations of program analysis[END_REF]) by abstract interpretation of the operational semantics of imperative programs. Compared to the lattice automata abstraction, the abstract domain is roughly a set of environments labeled with call-strings: K * → Λ (instead of Reg(K × Λ)). The concretization function uses again the well-formedness property to rebuild stacks from such abstract values. In the context of interprocedural shape analysis, [START_REF] Rinetzky | Interprocedural shape analysis for recursive programs[END_REF] represents explicitly the call-stack using the same abstract representation than for the memory configurations.

There are some advantages in having an explicit representation of call-stacks in interprocedural analysis. As long as data variables are not abstracted, the more classical functional approach is as precise, but as soon as they are, such an explicit representation allows to recover some loss of information. Moreover, the stack abstraction approach allows to describe naturally transformations such as procedures inlining in the course of an analysis. This is discussed in more details in [START_REF] Jeannet | Abstracting call-stacks for interprocedural verification of imperative programs[END_REF]. Last, some applications require information on the stack. This is the case for instance of analysis related to stack inspection mechanisms for ensuring security properties in Java and .NET architecture [START_REF] Besson | Model checking security properties of control flow graphs[END_REF]. Another example is the test selection technique proposed in [START_REF] Constant | Automatic test generation from interprocedural specifications[END_REF], in the context of conformance testing of reactive systems w.r.t. an interprocedural specification.

Conclusion

We defined in this paper an abstract domain for languages on infinite alphabets, which are represented by lattice automata. Our main motivation was the analysis of symbolic (or extended) communicating Irisa machines which exchange infinite data through FIFO queues, but this abstract domain may also be used for abstracting call-stacks in the analysis of recursive programs.

The principle of lattice automata is to use elements of an atomic lattice for labeling the transitions of a finite automaton, and to use a partition of this lattice in order to define a projected finite automaton which acts as a guide for defining determinization, minimization and widening operations. We motivate our choices and show that they lead to a robust notion of approximation, in the sense that normalization is an upper-closure operation and can be seen as a best upper-approximation in the join semilattice of normalized lattice automata.

The resulting abstract domain allows to lift any atomic abstract domain A for ℘(S) to an abstract domain Reg(A) for ℘(S * ). It is also parametric: it is parametrized first by the underlying alphabet lattice, then by a partition of the alphabet lattice, and last by the parameter of the widening operator. Its precision may be improved by adjusting these parameters.

We illustrate the use of lattice automata for the verification of symbolic communicating machines, and we show the need for a non-standard semantics to couple the abstraction of the state variables of the machines with the contents of the FIFO queues. To our knowledge, this is the first technique able to prove the specified properties on our example without manual transformation of the model, despite its relative simplicity. We also explore the applicability of lattice automata to interprocedural analysis and compare this solution to related work.

As a result, this work extends both analysis techniques dedicated to communicating machines, and interprocedural analysis based on an explicit representation of the call-stacks.

Future work includes first a deeper study of the experimental relevance of lattice automata to the analysis of SCM. The challenge we would like to take up is the verification of the SSCOP communication protocol, which is a sliding window protocol from which our running example is extracted. Previous verification attempts that we are aware of are either based on enumerated state-space exploration techniques [START_REF] Bozga | Verification and test generation for the SSCOP protocol[END_REF], or on the partial use of theorem proving [START_REF] Rusu | Combining formal verification and conformance testing for validating reactive systems[END_REF]. It would be interesting to study the application of lattice automata to shape analysis, in the spirit of [START_REF] Bouajjani | Abstract tree regular model checking of complex dynamic data structures[END_REF]. A last direction which could be explored is the generalization of lattice automata recognizing languages on infinite alphabets to tree automata recognizing trees on infinite sets of symbols.

Figure 1 :

 1 Figure 1: A simplistic protocol

Figure 2 :

 2 Figure 2: The connexion/disconnection protocol

Figure 4 :

 4 Figure 4: an interval automaton

b c a 0 a 1 a 2 a 3 a 4 ⊥Figure 7 :

 47 Figure 7: Attempt to determinize a lattice automaton

Figure 9 :

 9 Figure 9: A merged PLA with the one-element partition

Figure 10 :

 10 Figure 10: Inclusion test algorithm for a merged PLA

Figure 11 :

 11 Figure 11: Determinization and minimization of an interval automaton with the partition ] -∞, 0] [0, +∞[

Figure 12 :

 12 Figure 12: Determinization algorithm for a merged PLA

Figure 13 :

 13 Figure 13: Intersection of normalized PLA and its upper-approximation

Figure 14 :

 14 Figure 14: Widening on interval PLA, with a partition [-∞, 0[ [0, +∞] and k = 0

  w 1 , . . . , w i , . . . , w n -→ c 2 , w 1 , . . . , w i , . . . , w n A global state of a CFSM is thus a tuple c, w 1 , . . . , w n

Table 1 :

 1 Complexity of the basis operations on PLAs

	Irisa

• : PLA → NLA ⊆ PLA is an upper-closure operator: it is extensive, monotone (given a fixed partition), and idempotent.

Proof: Based on the same principle as Corollary 1.

  2 two abstract domains for ℘(S) such that A 2 refines A 1 , withγ 12 : A 1 → A 2 such that γ 1 = γ 2 • γ 12 (cf. Sect. 3). Let π 1 a partitioning function for A 1 , and π 2 a partitioning function for A 2 refining γ 12 • π 1 . The abstract domain Reg(A 2 , π 2 ) refines Reg(A 1 , π 1 ). Let Γ i : Reg(A i , π i ) → ℘(S * ) the two concretization functions. Let A 1 ∈ Reg(A 1 , π 1 ) be a NLA. We can build a NLA A 2 ∈ Reg(A 2 , π 2 ) such that γ 2 (A 2 ) = γ 1 (A 1 ).One first replace in A 1 transitions labeled by λ 1 ∈ π 1 (σ 1 ) by transitions labeled by λ 2 = γ 12 (λ 1 ) ∈ γ 12 • π 1 (σ 1 ). The set of elements in S "covered" by the two labels is clearly the same. The resulting automaton A 2 thus satisfies Γ 2 (A 2 ) = Γ 1 (A 1 ). Moreover, A 2 is a NLA belonging to Reg(A 2 , γ 12 • π 2 ). One now define A 2 as the refinement of A 2 w.r.t. the refined partition π 2 , which recognizes the same language according to Prop. 4.This transformation from A 1 to A 2 defines a function Γ 12

Proof:

Table 8 :

 8 Syntactic domains for imperative programs LEnv i = LVar i → Value : local environments for procedure/function P i ∈ LEnv = i LEnv i

	v ∈ Value	: values of expressions and variables
		: local environments for any procedure/function
	c, ∈ Act = K × LEnv	: activation record
	Γ ∈ Act *	: stacks (sequences) of activation records = program states

i ∈

Table 9 :

 9 Semantic domains for imperative programs

The lattice of affine equalities, which could also be called the lattice of affine subspaces, is the lattice formed by the conjunctions of affine equalities on the space R n . Irisa

The term "merged" comes from the merging operation needed to build a merged PLA from a given PLA.PI n˚1839

Remember that "deterministic" means strongly deterministic.Irisa

This choice is important insofar as the lattice automata abstraction does not commute with the reverse operation on words.PI n˚1839

Parameterized Domains with k ≥ 0 Concrete domain

The semantics of a transition is defined as follows: first the queue variables p are introduced, and then constrained by the guard (semantics of guards). A push or pop operation is possibly performed. Last, the assignment updates the value of state variables. For push and pop, the value p is defined by a kind of unification between the guard and the queue content.

Table 5: Standard abstract semantics Non-standard abstract semantics. The formalization of this technique requires slightly heavier notations. We assume that we put all the environment in the queue. The abstract lattice is then

with the concretization function

Table 7: Analysis of the example with the non-standard approach

The partitioning function π : Σ → V (p) used in PLA is implicitly extended to π : Σ → V (n+p) . A (n) may be seen as a reduced product of the two interacting components V (n) and Reg(V (n+p) ).

Abstract operations. The abstract semantics of guards now involves both the abstract environment and the queue:

The abstract semantics of assignments is more complex:

where Y = A (Y ) and δ = {(q 1 , λ , q 2 ) | (q 1 , λ, q 2 ) ∈ δ ∧ λ defined as below }. λ ( v, p 0 ) is obtained from λ( v, p 0 ) by the following operations:

We build φ( v, p, v , p 0 ) = λ( v, p 0 ) ∧ v = A( v, p) ∧ Y ( v, p), where v is the value of the state variables after the assignment, v and p the current value of state and message variables, and p 0 the value of the message variable in the transition of the lattice automaton.

We then build φ ( v , p 0 ) = ∃ v∃ p : φ by eliminating variables in the current environment; Last we perform a renaming:

The application of the assignment to a NLA produces a NLA; in particular, as the partitioning function involves only the message parameters, and A modifies only the state variables, the lattice automaton remains well-partitioned.

The semantics of message outputs and inputs are in some way simpler than with the previous abstract semantics: The semantics of transitions remains similar to that of Tab. 5.

PI n˚1839


E Budyn
email: ebudyn@uic.edu

J Jonvaux

T Hoc

Physical Imaging of fracturing Human Cortical Bone

Keywords: fracture, toughness, contact, bone, XFEM, imaging

In the present study, we present a procedure associating either the eXtended Finite Element Method (XFEM) or the standard Finite Element Method (FEM) to a Digital Imaging Correlation technique (DIC) called microextensometry (CorrelmanuV) in order to investigate the local fracture toughness of micro cracks in human Haversian cortical bone at the scale of the osteons. The micro cracks are tested in tension and in compression.

Introduction

Microcracks are usually involved in the bone remodelling process and fracture risk assessment [START_REF] Nalla | Mechanistic fracture criteria for the failure of human cortical bone[END_REF][START_REF] Fratzl | When the cracks begin to show[END_REF]. Better knowledge of fracture occurrence at the micro scale is then an essential step to increase diagnostic reliability. During most daily exercise such as walking, bones undergo cyclic fatigue loading that alternates between tension and compression. Therefore the present models address the determination of the stress intensity factors of the microcracks under tension and compression in posterior femur mid-diaphysis of female human cortical bone.

Methodology

Tension

In tension, a three point bending device for millimetric samples was built to fit under a light microscope. We considered a beam specimen of an average length of 5 mm and a square cross-section of an average 2 mm width as shown in Figure 1. The specimen were precracked by 600 µm depth calibrated incisions. The cortical bone morphology was surveyed using a digital imaging processing technique [START_REF] Smith | User's Manual. Plot Digitizer[END_REF] in BSEM (Back Scattered Electron Microscopy) and the grey scale was correlated to the local mineralisation levels as shown in Figure 2. The local elastic moduli were measured by nanoindentation correlated to the mineralisation levels. The local Poisson ratios were extrapolated from the osteonal strain fields. A small window of observation was studied in the vicinity of the initial crack. To reconstruct the physical stress field, the following constitutive elements were included in an XFEM model: the osteons' transversal profiles, the cement lines around them, In order efficiently to incorporate evolving micro cracks, we designed a procedure associating the eXtended Finite Element Method (XFEM) [START_REF] Belytschko | Elastic crack growth in finite elements with minimal remeshing[END_REF][START_REF] Moës | A finite element method for crack growth without remeshing[END_REF] to the Digital Imaging Correlation technique (DIC) to investigate the local stress intensity factors at the scale of the osteons in human Haversian bone. The method can be related to the approach that has been applied to polycrystalline microstructures [START_REF] Héripré | Coupling between experimental measurements and polycrystal finite element calculations for micromechanical study of metallic materials[END_REF]. This method is able to incorporate fracture [START_REF] Budyn | Multiple scale modeling of cortical bone fracture in tension using x-fem[END_REF][START_REF] Budyn | Fracture strength assessment and aging signs detection in human cortical bone using an x-fem multiple scale approach[END_REF] in explicit cortical bone microstructure as shown in Figure 3(c). Due to the small size of the observation window, the experimental displacement was applied along the edges of the explicit model. Cortical bone was considered brittle due to its high content of hydroxyapatite and under plane stress condition as the surface of the sample is observed. The stress intensity factors were calculated using the interaction integral. The L 2 norm of the difference between the experimental and numerical fields was less than 1.3% in all cases, therefore the model adequately replicates the experiments in human Haversian cortical bone and provides valuable information on three scales.

(1a) (1b) (1c) (2a) (2b) (2c) (3a) (3b) (3c) (4a) (4b) (4c)

Compression

In compression, the samples of the same size were loaded in a micro compression device without precracking. As FEM model of the cortical bone microstructure was also constructed but the cracks were explicitly discretised as shown in Figure 4(c). As the window of observation was wider, the experimental displacement field was imposed at all imaging points inside the polyphase medium. The imaging points were incorporated into the mesh using an optimised adaptivity algorithm.

The contact solution was iteratively calculated by Newton-Raphson method [START_REF] Mijar | An augmented lagrangian optimization method for contact analysis problems, 1: formulation and algorithm[END_REF] until convergence of the displacement field. The frictional contact condition was checked at the mid-point of each element [START_REF] Dorogoy | Shear loaded interface crack under the influence of friction: a finite difference solution[END_REF] and was enforced by nodal penalties along the crack edges [START_REF] Belytschko | Nonlinear Finite Elements for Continua and Structures[END_REF].

Results

The model provides the fracture strength and the global response at the macroscopic scale (mm), the stress-strain fields at the microarchitectural level (10-100 µm) and the crack profiles at the

Figure 1 :

 1 Figure 1: (a) procedure of sample cut, (b) sample dimension, (c) testing setting, (d) osteonal loading.

Figure 2 :

 2 Figure 2: (a) BSEM (Back Scattered Electron Microscopy) of w06005, (b) Young's modulus map in MPa in ModNum of w06005.

Figure 3 :

 3 Figure 3: 1,2,3,4 (a) Light microscopy observation window of microcracks in human cortical bone specimen of 300 by 1100 µm under tension, 1,2,3,4 (b) Digital Correlation Imaging of the kinematic strain field ε 22 where the displacement field is prescribed at all mesh points, 1,2,3,4 (c) Physical strain field ε 22 obtained by an XFEM model of the micro cracks that reconstructs the explicit microstructure and where the experimental displacements are only prescribed along the edges. The color scale is [-0.0035; 0.0049] in pictures (b) and (c).

Figure 4 :

 4 Figure 4: (a) Light microscopy observation window of microcracks in human cortical bone specimen of 1400 by 1900 µm under compression, (b) Digital Correlation the kinematic strain field ε 11 where the displacement field is prescribed at all mesh points, (c) Physical strain field ε 11 obtained by an FEM model of the micro cracks that reconstructs the microstructure and the displacements are prescribed at all imaging points. The color scale is [-0.0158; 0.0170] in pictures (b) and (c).

Table 1 :

 1 Stress intensity factors in sample w06005 versus the micro cracks' lengths -10 µm) and fracture parameters such as the stress intensity factors. The results obtained in this work emphasise the influence of the microstructure on bone failure. The model incorporates the explicit bone microstructure with its specific microarchitecture and heterogeneous mechanical behaviour of the tissue. The model confirms the local toughening mechanism[START_REF] Kj Koester | The toughness of human cortical bone measured with realistically short cracks[END_REF] that is usually observed in bone and indicates some possible explanations. The model also indicates how the fracture properties could be modified in regard to possible alterations of the microstructure integrity which are not detectable by conventional clinical tools, and proposes a new procedure to diagnose pathologies.

		K I	K II	K eq	a i	L 2
		MPa √ m	MPa √ m	MPa √ m	mm	%
	tension
	step 1	0.33	-0.09	0.34	0.774	0.47
	step 2	0.64	0.21	0.67	0.774	0.59
	step 3	1.38	0.44	1.45	0.968	1.04
	step 4	1.27	0.28	1.30	1.236	1.28
	compression
	crack 1	0.01	-0.14	0.14	0.158	0.19
	crack 4 1	-0.58	-0.22	0.62	0.11	0.19
	crack 4 2	-0.36	-0.52	0.63	0.11	0.19
	crack 6	-0.49	-1.17	1.27	0.105	0.19
	crack 7	-0.6	-2.35	2.43	0.065	0.19

Acknowledgments

The authors are grateful for the research support of the University of Illinois at Chicago and the CNRS. The authors are grateful to Sebastien Uzel for his work on samples under tension during his Master Thesis. The authors are grateful to Françoise Garnier for the SEM study. The first author is grateful to Professor Alexander Chudnovsky and Professor Michael Scott.