Paolo Baldan
email: baldan@math.unipd.it

Thomas Chatain
email: thomas.chatain@lsv.ens-cachan.fr

Stefan Haar
email: haar@lsv.ens-cachan.fr

Barbara König
email: barbara_koenig@uni-due.de

Unfolding-based Diagnosis of Systems with an Evolving Topology 6

Keywords: Model-based diagnosis, distributed and concurrent systems, partial order methods, graph rewriting 2010 MSC: 68Q60, 68Q85, 68Q42, 68M15

We propose a framework for model-based diagnosis of systems with mobility and variable topologies, modelled as graph transformation systems. Generally speaking, model-based diagnosis is aimed at constructing explanations of observed faulty behaviours on the basis of a given model of the system. Since the number of possible explanations may be huge, we exploit the unfolding as a compact data structure to store them, along the lines of previous work dealing with Petri net models. Given a model of a system and an observation, the explanations can be constructed by unfolding the model constrained by the observation, and then removing incomplete explanations in a pruning phase. The theory is formalised in a general categorical setting: constraining the system by the observation corresponds to taking a product in the chosen category of graph grammars, so that the correctness of the procedure can be proved by using the fact that the unfolding is a right adjoint and thus it preserves products. The theory should hence be easily applicable to a wide class of system models, including graph grammars and Petri nets.

Introduction

The event-oriented model-based diagnosis problem is a classical topic in discrete event systems [START_REF] Cassandras | Introduction to Discrete Event Systems[END_REF][START_REF] Sampath | Failure diagnosis using discrete event models[END_REF]. Given an observed alarm stream, the aim is to provide explanations in terms of actual system behaviours. Some events of the system are observable (alarms) while others are not. In particular, fault events are usually unobservable; therefore, fault diagnosis is the main motivation of the diagnosis problem. Given a sequence (or partially ordered set) of observable events, the diagnoser has to find all possible behaviours of the model explaining the observation, thus allowing the deduction of invisible causes (faults) of visible events (alarms). The paper [3] provides a survey on fault diagnosis in this direction.

Since the number of possible explanations may be huge, especially in the case of highly concurrent systems, it is advisable to employ space-saving methods. In [3,[START_REF] Fabre | Distributed monitoring of concurrent and asynchronous systems[END_REF], the global diagnosis is obtained as the fusion of local decisions: this distributed approach allows one to factor explanations over a set of local observers and diagnoses, rather than centralizing the data storage and handling.

We will build here upon the approach of [START_REF] Benveniste | Diagnosis of asynchronous discrete event systems, a net unfolding approach[END_REF] where diagnoses are stored in the form of unfoldings. The unfolding of a system fully describes its concurrent behaviour in a single branching structure, representing all the possible computation steps and their mutual dependencies, as well as all reachable states; the effectiveness of the approach lies in the use of partially ordered runs, rather than interleavings, to store and handle explanations extracted from the system model. In order to provide some intuition about unfoldings, an example of a Petri net and a fragment of its unfolding are reported in Fig. 1. In the Petri net, for later use, a bold face label is used to denote alarms, i.e., observable transitions. More explicitly, transitions labelled a, b, c, d are observable, while e, f are not. The unfolding is inductively constructed, starting from the initial marking and recording, step after step, any possible firing of a transition, with the tokens it produces. Hence transitions and places in the unfolding can be seen as occurrences of firing of transitions (events) and of tokens in computations of the original net. The causal dependencies and conflicts between items of the unfolding are made explicit by the struture of the unfolding itself. For instance, let us focus on the upper part of the unfolding. The two events labelled a are in conflict, since they consume a common resource, while the leftmost event labelled a is a cause for the event labelled e. Instead, the absence of dependencies between the events e and f , means that such events are concurrent and thus they can interleave in any way.

While [START_REF] Benveniste | Diagnosis of asynchronous discrete event systems, a net unfolding approach[END_REF] and subsequent work in this direction were mainly directed to Petri nets, here we face the diagnosis problem in mobile and variable topologies. This requires the development of a model-based diagnosis approach which applies to other, more expressive, formalisms. Unfoldings of extensions of Petri nets where the topology may change dynamically were studied in [START_REF] Chatain | Models for the supervision of web services orchestration with dynamic changes[END_REF][START_REF] Bruni | Non-sequential behaviour of dynamic nets[END_REF]. Here we focus on the general and well-established formalism of graph transformation systems.

In order to retain only the behaviour of the system that matches the observation, it is not the model itself that is unfolded, but the product of the model with the observations, which intuitively represents the original system constrained by the observation; under suitable observability assumptions, only a finite prefix of the unfolding must be considered. The construction is carried out in a suitably defined category of graph grammars, where such a product can be shown to be the categorical product. A further pruning phase is necessary in order to remove incomplete explanations that are only valid for a prefix of the observations. The steps of the diagnosis procedure can be illustrated, for the Petri net case, by referring to the net in Fig. 1. Assume that the observation is given by the sequence a b c. The idea consists in representing the observation as a special system, in this case a Petri net. This can be easily done, as shown in the left part of Fig. 2. Then, taking the product of the system with the observation, we force events in the system to occur synchronously with those of the observation net. The unfolding of the product intuitively represents all the runs of the system which are consistent with the observation. For the considered example, such an unfolding is represented in the right part of Fig. 2 (for the sake of readability some places which do not influence the overall behaviour are omitted). Some events, although compatible with the observation, cannot be part of a complete explanation of the observation. For instance, in the example, after firing the transition labelled a in the middle, depicted in grey, no other event can be fired. Hence there is no way of explaining the occurrence of b and c in the observation. This transition is removed in the pruning phase, which produces the actual diagnosis. Observe that, even in this simple case, the set of possible sequential executions explaining the observation would have been larger than the diagnosis in the form of an unfolding, as concurrent events can interleave in any way. For instance, indicating an event with the pair (label, number), a possible explanation would be (a, 1) (e, 2) ( f, 3) (b, 5) (c, 7). But since event ( f, 3) is concurrent with (a, 1) and (e, 2), also other interleavings, such as (a, 1) ( f, 3) (e, 2) (b, 5) (c, 7) or ( f, 3) (a, 1) (e, 2) (b, 5) (c, 7) are valid explanations. Additionally, since event (e, 2) is not observable and concurrent with ( f, 3), (b, 5), (c, 7), it can be omitted or inserted in any position after (a, 1), leading to several more valid explanations. The diagnosis technique proposed for graph grammars, which, as explained above, follows analogous steps, is shown to be correct. More precisely, we prove that the runs of the unfolding produced by the diagnosis procedure properly capture all those runs of the model which explain the observation. This non-trivial result relies on the fact that unfolding for graph grammars is a coreflection, hence it preserves limits (and especially products, such as the product of the model and the observation). In order to ensure that the product is really a categorical product, special care has to be taken in the definition of the category.

The rest of the paper is structured as follows. In Section 2 we introduce the category of graph grammars used in the paper, characterise the product in such a category and discuss the unfolding semantics. In Section 3 we introduce interleaving structures, an intermediate semantic model which is instrumental in developing the theory of diagnosis. In Section 4 we formalise the diagnosis problem and show how to construct a diagnosis for a given system and observation. In Section 5 we prove the correctness of the diagnosis procedure and give some experimental results in Section 6. Finally in Section 7 we draw some conclusions and outline directions of future research. An appendix includes some auxiliary material about asymmetric event structures, along with the proof of a technical result needed in the paper. This is an extended version of the conference paper [START_REF] Baldan | Unfolding-based diagnosis of systems with an evolving topology[END_REF], which includes detailed definition of the grammar morphisms needed to get the right notion of product, full proofs of the results and a section with experimental evaluations.

Graph Grammars and Grammar Morphisms

In this section we summarise the basics of graph rewriting in the single-pushout (spo) approach [START_REF] Löwe | Algebraic approach to single-pushout graph transformation[END_REF]. We introduce a category of graph grammars, whose morphisms are a variation of those in [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF] and we provide a characterisation of the induced categorical product, which turns out to be adequate for expressing the notion of composition needed in our diagnosis framework. Then we argue that the unfolding semantics smoothly extends to this setting and, as in [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF], the unfolding construction can be characterised categorically as a universal construction. The existence of a satisfactory unfolding semantics motivates our choice of the spo approach as opposed to the more classical double-pushout (dpo) approach, for graph rewriting.

Graph Grammars and their Morphisms

Given a partial function f : A ⇀ B we write f (a) ↓ whenever f is defined on a ∈ A and f (a) ↑ whenever it is undefined. We denote by dom( f ) the domain of f , i.e., the set {a ∈ A | f (a) ↓}. Let f, g : A ⇀ B be two partial functions. We write f ≤ g when dom( f ) ⊆ dom(g) and f (x) = g(x) for all x ∈ dom( f ).

For a set A, we denote by A * the set of finite sequences over A. Given f : A ⇀ B, the symbol f * : A * → B * denotes its extension to sequences defined by f * (a 1 . . . a n ) = f (a 1 ) . . . f (a n ), where it is intended that the elements on which f is undefined are "forgotten". Specifically, f * (a 1 . . . a n ) = ε whenever f (a i ) ↑ for every i ∈ {1, . . . , n}. Instead, f ⊥ : A * ⇀ B * denotes the strict extension of f to sequences, satisfying f ⊥ (a 1 . . . a n ) ↑ whenever f (a i ) ↑ for some i ∈ {1, . . . , n}.

Definition 1 ((hyper)graph). A (hyper

)graph G is a tuple (N G , E G , c G ), where N G is a set of nodes, E G is a set of edges and c G : E G → N * G is a connection function. Given a graph G we will write x ∈ G to say that x is a node or edge in G, i.e., x ∈ N G ∪ E G .

Definition 2 (partial graph morphism). A partial graph morphism

f : G ⇀ H is a pair of partial functions f = f N : N G ⇀ N H , f E : E G ⇀ E H such that: c H • f E ≤ f ⊥ N • c G (*)
We denote by PGraph the category of hypergraphs and partial graph morphisms. A morphism is called total if both components are total, and the corresponding subcategory of PGraph is denoted by Graph.

Notice that, according to Condition (*), if f is defined on an edge then it must be defined on all its adjacent nodes: this ensures that the domain of f is a well-formed graph. The inequality in Condition (*) ensures that any subgraph of a graph G can be the domain of a partial morphism f : G ⇀ H. Instead, the stronger (apparently natural) condition

c H • f E = f ⊥ N • c G
would have imposed f to be defined over an edge whenever it is defined on all its adjacent nodes. We will work with typed graphs [START_REF] Corradini | Graph processes[END_REF][START_REF] Löwe | An Algebraic Framework for the Transformation of Attributed Graphs[END_REF], which are graphs labelled over a structure that is itself a graph, called the type graph. In Fig. 3 the reader can find an example of a typed graph (top) with the corresponding type graph (bottom). Note that, when depicting a graph, nodes and edges are represented as circles and boxes, respectively. In our examples we have both unary (hyper-)edges (represented by boxes connected to one node only) and binary hyperedges (where the order of nodes is indicated by an arrow, going from the first to the second node.) The typing morphism is implicitly represented by labelling each item of the graph with the item of the type graph it is mapped to.

Definition 3 (typed graph). Given a graph

Definition 4 (graph production, direct derivation).

Fixing a graph T of types, a (T -typed graph) production q is an injective partial typed graph morphism L q r q ⇀ R q . It is called consuming if r q is not total. The typed graphs L q and R q are called left-hand side and right-hand side of the production.

Given a typed graph G and a match, i.e., a total injective morphism g : L q → G, we say that there is a direct derivation from G to H using q (based on g), written G ⇒ q H, if there is a pushout square in T -PGraph as on the right.

L q g r q / R q h G d / H
Roughly speaking, the rewriting step removes from G the image of the items of the left-hand side which are not in the domain of r q , namely g(L qdom(r q )), adding the items of the right-hand side which are not in the image of r q , namely R qr q (dom(r q )). The items in the image of dom(r q ) are "preserved" by the rewriting step (intuitively, they are accessed in a "read-only" manner). Additionally, whenever a node is removed, all the edges incident to such a node are removed as well. For instance, consider production fail at the bottom of Fig. 5. Its left-hand side contains a unary edge and its right-hand side is the empty graph. The application of fail to a graph is illustrated in Fig. 4, where the match of the left-hand side is indicated as shaded.

Definition 5 (typed graph grammar). A (T -typed)

spo graph grammar G is a tuple T, G s , P, π, Λ, λ , where G s is the (typed) start graph, P is a set of production names, π is a function which associates to each name q ∈ P a production π(q), and λ : P → Λ is a labelling over the set Λ. A graph grammar is consuming if all the productions in the range of π are consuming.

As standard in unfolding approaches, in the paper we will consider consuming graph grammars only, where each production deletes some item. Hereafter, when omitted, we will assume that the components of a given graph grammar G are T, G s , P, π, Λ, λ . Subscripts carry over to the component names.

For a graph grammar G we denote by Elem(G) the set N T ∪ E T ∪ P. As a convention, for each production name q the corresponding production π(q) will be L q r q ⇀ R q . Without loss of generality, we will assume that the injective partial morphism r q is a partial inclusion (i.e., that r q (x) = x whenever defined). Moreover we assume that the domain of r q , which is a subgraph of both |L q | and |R q |, is the intersection of these two graphs, i.e., that |L q | ∩ |R q | = dom(r q ), componentwise. Since in this paper we work only with typed notions, we will usually omit the qualification "typed", and, sometimes, we will not indicate explicitly the typing morphisms.

In the sequel we will often refer to the runs of a grammar defined as follows.

Definition 6 (runs of a grammar). Let G be a graph grammar. Then Runs(G) consists of all sequences r 1 r 2 . . . r n where r i ∈ P and G s

r 1 ⇒ G 1 r 2 ⇒ G 2 • • • r n ⇒ G n for some G 1 , . . . , G n .
Example 1. As a first example, let us consider the graph grammar S, whose start and type graph are in Fig. 3, while productions are given in Fig. 5. For productions (and the corresponding partial morphisms) we adopt the following graphical representation: edges that are deleted or created are drawn with solid lines, whereas edges that are preserved are indicated with dashed lines. Nodes which are preserved are indicated with numbers, whereas newly created nodes are not numbered. Productions that should be observable (a notion that will be made formal in Section 4) are indicated by bold face letters. Grammar S models a network with mobility whose nodes are either senders (labelled S ), receivers (R) or intermediary nodes (I). Senders may send messages (production snd) which can then cross connections (production cross) and should finally arrive at a receiver (production rcv). The network is variable and of unbounded size as we allow the creation of new intermediary nodes and connections to such nodes (production cnode). Note that a newly created node is initially inactive (label II) and it will become active only later, by means of production act. Other rules are given to connect a sender to an intermediary node and an intermediary node to a receiver (productions cconn 1 and cconn 2 ). Finally, a node can disappear (and in this case, as commented before, also all its connections are removed) as expressed by production fail. Production idl simply deletes and generates again a connection. It can be interpreted as a transient failure of the connection, which makes it unavailable for a while.

cconn 2 : M 1 R 1 R 1 C 2 1 C 2 M M
An example of run in S is given by the sequence snd cross cconn 2 cross rcv, where a message is generated by a sender, it travels towards a receiver and it is finally received. This is made possible by an extension of the network which, in the second step, is enriched with a new connection. A graphical representation of the run can be found in Fig. 6.

We next define the class of grammars which we will focus on.

Definition 7 (semi-weighted SPO graph grammars).

A grammar G is semi-weighted if (i) the start graph G s is edge-injective, (ii) for each q ∈ P, for any x, y ∈ E |R q | -E |L q | if t R q (x) = t R q (y) then x = y, i.e., the right-hand side graph R q is injective on the "produced edges" and (iii) in the start graph G s and, for any q ∈ P, in L q and in the graph L q ∪ R q , there are no isolated nodes.

Intuitively, Conditions (i) and (ii) ensure that in a semi-weighted grammar each edge generated in a computation has a uniquely determined causal history. Condition (iii) essentially says that only edges carry semantic information, while 6 nodes are just used as attaching points for edges. At a more technical level, it ensures that the correspondence between the type graphs of two graph grammars as established by a grammar morphism, is determined by the correspondence on edges. These facts are essential for the validity of Theorem 1.

X f ′ f ′L f ′R ? ? ? ? ? ? ? ? A X f f L o o f R / / k O O B X f z " " y | | (1) A X f 1 f L 1 o o f R 1 / / B X f 2 f L 2 o o f R 2 / / C (a) (b)
We next introduce a category of graph grammars, which will be used to define products and to characterise the unfolding construction as a coreflection. The choice of arrows of the category is quite subtle: other possible notions of morphisms are conceivable but they do not necessarily provide the right notion of product and the coreflection result. In order to define grammar morphisms we need to introduce the notion of semi-abstract span, which, roughly speaking, provides a categorical generalisation of the notion of multirelation.

Given a category C, a (concrete) span f

: A ↔ B in C is a pair of total graph morphisms f = f L : X f → A, f R : X f → B , where X f is called the support.
A semi-abstract span [ f ] : A ↔ B is an equivalence class of spans obtained by considering the support up to isomorphism, i.e.,

[ f ] = { f ′ : A ↔ B | ∃k : X f → X f ′ .(k isomorphism ∧ f ′L • k = f L ∧ f ′R • k = f R )} (see Fig. 7.(a)).
If C is a category with pullbacks, then semi-abstract spans can be composed as follows: given two semi-abstract spans

[ f 1 ] : A ↔ B and [ f 2 ] : B ↔ C, their composition is the (equivalence class of a) span f constructed as in Fig. 7.(b) (i.e., f L = f L 1 • y and f R = f R 2 • z)
, where the square (1) is a pullback. This allows one to consider a category Span(C) which has the same objects as C and semi-abstract spans in C as arrows.

The following definition generalises the notion of image of a set through a multirelation (see, e.g., [START_REF] Bruni | Some algebraic laws for spans (and their connections with multirelations)[END_REF]).

Definition 8 (pullback-retyping relation). Let [ f T ] :

T 1 ↔ T 2 be a semi-abstract span in Graph, let G 1 be a T 1typed graph, and let G 2 be a T 2 -typed graph. Then G 1 and G 2 are related by pullback-retyping (via

[ f T ]) if there exist total morphisms x : |G 2 | → |G 1 | and y : |G 2 | → X f T such that the square in the following diagram is a pullback: |G 1 | t G 1 |G 2 | t G 2 B B B B B B B B x o o y T 1 X f T f L T o o f R T / / T 2
In this case we will write f T {x, y}(G 1 , G 2 ), or simply f T (G 1 , G 2 ) if we are not interested in morphisms x and y.

Some concrete examples of retypings will be discussed after Definition 10.

We are now ready to introduce grammar morphisms. Except for the treatment of the labels, these morphisms coincide with those in [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF], which are, in turn, a generalisation of Winskel's morphisms for Petri nets (see [START_REF] Winskel | Event Structures[END_REF]). The latter ensure the existence of products, which can be interpreted as asynchronous compositions, and of some coproducts, modelling nondeterministic choice [START_REF] Winskel | Petri nets, algebras, morphisms, and compositionality[END_REF]. Besides the component specifying the (multi)relation between the type graphs, a morphism from G 1 to G 2 includes a (partial) mapping between production names. Furthermore a third component explicitly relates the (untyped) graphs underlying corresponding productions of the two grammars, as well as the graphs underlying the start graphs.

|G s 1 | t Gs 1 |G s 2 | t Gs 2 ; ; ; ; ; ; ; ι s f o o k T 1 X f T f L T o o f R T / / T 2 |R q 1 | t Rq 1 |R q 2 | ι R f (q 1 ) o o k R t Rq 2 ( ( ( ( ( ( ( ( ( ( ( ( ( ( (1)
|L q 1 | ≥ t Lq 1 4 4 4 4 4 r q 1 > } } } } } } } } } } |L q 2 | ≥ r q 2 = { { { { { { { { { { ι L f (q 1 ) o o k L 5 5 5 5 5 5 t Lq 2 O O O O O O O ' ' O O O O O T 1 X f T f L T o o f R T / / T 2 (a) (b)

Definition 9 (grammar morphism). Let

G i (i ∈ {1, 2}) be graph grammars such that Λ 2 ⊆ Λ 1 . A morphism f : G 1 → G 2 is a triple [ f T ], f P , ι f where • [ f T ] : T 1 ↔ T 2 is a semi-abstract span in Graph, called the type-span; • f P : P 1 → P 2 ∪ {∅} is a total function, where ∅ is a new production name (not in P 2 ), with associated production ∅ ⇀ ∅; • ι f is a family {ι f (q 1 ) | q 1 ∈ P 1 } ∪ {ι s f } of morphisms in Graph such that ι s f : |G s 2 | → |G s 1 | and for each q 1 ∈ P 1 , if f P (q 1 ) = q 2 , then ι f (q 1 ) is a pair ι L f (q 1 ) : |L q 2 | → |L q 1 |, ι R f (q 1 ) : |R q 2 | → |R q 1 | .
such that the following conditions are satisfied:

Preservation of the start graph.

There exists a morphism k such that f T {ι s f , k}(G s 1 , G s 2 ), i.e., the diagram in Fig. 8.(a) commutes and the square is a pullback.

Preservation of productions.

For each q 1 ∈ P 1 , with q 2 = f P (q 1 ), there exist morphisms k L and k R such that the square (1) in Fig. 8.(b) commutes, and

f T {ι Y f (q 1 ), k Y }(Y q 1 , Y q 2 ) for Y ∈ {L, R}.

Preservation of labelling.

For each q 1 ∈ P 1 , f P (q 1 ) ∅ iff λ 1 (q 1 ) ∈ Λ 2 and, in this case, λ 2 ( f P (q 1 )) = λ 1 (q 1 ).

For technical convenience, the partial mapping on production names is represented as a total mapping by enriching the target set with a distinguished element ∅, representing "undefinedness". With respect to the morphisms in [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF], note that here for the existence of a morphism from G 1 to G 2 we require that Λ 2 ⊆ Λ 1 and there are some restrictions on the labelling as expressed by Condition 3 above.

Definition 10 (category of graph grammars).

We denote by GG the category where objects are spo graph grammars and arrows are grammar morphisms. By SGG we denote the full subcategory of GG having semi-weighted graph grammars as objects. Example 2. Let us consider a second graph grammar M which will be used as a running example. The start and type graph are given in Fig. 9, while the productions can be found in Fig. 10.

Grammar M still models an evolving network with message passing, but here a connection may spontaneously get corrupted (production crpt), a fact which causes the corruption of any message which crosses it (production cross 2 ). Note that in order to represent corrupted items there are two additional types in the type graph: CC for corrupted connections and CM for corrupted messages. It could also be natural to add another rule cross 4 modelling a corrupted message crossing a corrupted connection, but we omit this rule for keeping the presentation simpler.

The two example grammars S and M are used to illustrate the notion of grammar morphism. We define a morphism f : M → S which intuitively maps M into S by forgetting about the distinction between corrupted and non corrupted items. More formally, the type span is f T : T M ↔ T S , where X f T = T M , the left leg f L T : T M → T M is the identity and the right leg f R T : T M → T S maps the two connection edges in T M (i.e., C and CC) to the only connection edge in T S (i.e., C); the same happens for messages, while any other item in T M is mapped to the corresponding item in T S (see Fig. 11).

The component on productions f P : P M → P S ∪ {∅} maps productions crcv and crpt in M to rcv and idl in S, respectively, while productions cross i (i ∈ {1, 2, 3}) in M are all mapped to production cross in S. The remaining productions snd, rcv, cconn i (i ∈ {1, 2}), cnode, act, fail in M are mapped to the corresponding productions, with the same name, in S. Note that in this case no production in M is mapped to ∅, which intuitively means that the mapping is total on productions. All the morphisms in the ι f family are isomorphisms.

It can be easily seen that the conditions of Definition 9 concerning the preservation of start graph and productions are satisfied. Since, in this case, the left leg of the type span f L T is the identity, the pullback-retyping of a typed graph G will result in a diagram of the kind

|G| t G |G| t G t G ; f R T ! ! B B B B B B B B id o o T M T M id o o f R T / / T S
i.e., it just amounts to a retyping via a post-composition with f R T . We observe that morphisms can be more sophisticated, as spans can represent general (multi-)relations. The pullback retyping construction can, e.g., remove some types and multiply some others. For instance Fig. 12(a) shows a span f ′ T (the left and right leg are implicitly given by the labelling) and Fig. 12(b) the graph which would result by applying the pullback retyping to the left-hand side of cross 2 . Note that the connection CC disappears, while the message M is doubled.

cconn 2 : 1 R 1 R C M 1 R 1 R fail: intermediary node fails I 1 I 1 II 1 act: activate intermediary node C C 1 S CM 1 C 2 1 C 2 M M 1 2 1 2 M CC CM 1 C 2 1 2 CM CM C 1 2

Product in the category of grammars

The choice of grammar morphisms and, in particular, the conditions on the labelling, lead to a categorical product suited for composing two grammars G 1 and G 2 : productions with labels in Λ 1 ∩ Λ 2 are forced to be executed in a synchronous way, while the others are executed independently in the two components. At a more technical level, the type and start graph of the product grammar are obtained by taking the disjoint union of the type and start graphs of G 1 and G 2 . Similarly, productions in the product grammar which arise from the synchronisation of productions of G 1 and G 2 are constructed by taking the disjoint union of the left-and right-hand sides of the original productions.

Proposition 1 (product of graph grammars).

Let G 1 and G 2 be two graph grammars. Their product in GG is defined as G = G 1 × G 2 with the following components:

• T = T 1 ⊎ T 2 ;
• G s = G s1 ⊎ G s2 , with the obvious typing;

• P = {(p 1 , p 2 ) | λ 1 (p 1 ) = λ 2 (p 2 )} ∪ {(p 1 , ∅) | λ 1 (p 1 ) Λ 2 } ∪ {(∅, p 2 ) | λ 2 (p 2 ) Λ 1 }; • π(p 1 , p 2 ) = π 1 (p 1 ) ⊎ π 2 (p 2 ), where π i (∅) is the empty rule ∅ ⇀ ∅; • Λ = Λ 1 ∪ Λ 2 ; • λ(p 1 , p 2 ) = λ i (p i ), for any i ∈ {1, 2} such that p i ∅;
where, p 1 and p 2 range over P 1 and P 2 , respectively, and disjoint unions are taken componentwise. The projections

f i : G → G i (i ∈ {1, 2}) are morphisms f i = f iT , f i P , ι f i , where • f iT : T 1 ⊎ T 2 ↔ T i has support T i , the left leg f i L T : T i → T 1 ⊎ T 2 is the obvious injection, while the right leg f i L T : T i → T i is the identity; • f i P : P → P i ⊎ {∅} is the obvious projection;
• concerning the components of ι f i : for the start graph ι s f i :

G si → G s1 ⊎ G s2 is the obvious inclusion; ι L f i and ι R f i are defined analogously. 11
If G 1 , G 2 are both semi-weighted grammars, then G as defined above is semi-weighted, and it is the product of G 1 and G 2 in SGG.

Proof. Let G ′ be another graph grammar with morphisms f ′ i : G ′ → G i . We have to show that there exists a unique morphism

f ′ : G ′ → G with f i • f ′ = f ′ i . G 1 G 2 G f 1 BB B f 2 > > | | | G ′ f ′ 1 F F f ′ 2 X X f ′ O O
The morphism f ′ will be defined as follows:

• Assume that f ′ i T : T ′ ↔ T i has support X i . Then for f ′ T : T ′ ↔ T 1 ⊎ T 2 take X 1 ⊎ X 2
as support, where the arrows

X 1 ⊎ X 2 → T ′ and X 1 ⊎ X 2 → T 1 ⊎ T 2 are obtained as mediating morphisms (see diagram below). T 1 T 2 T 1 id BB B % % K K K K T 2 id > > | | | y y s s s s X 1 C C > > | | | ) ) S S S S S S S S -- T 1 ⊎ T 2 X 2 [ [ BB B u u k k k k k k k k r r X 1 ⊎ X 2 O O T ′
The category of graphs with total morphisms is an adhesive category with a strict initial object (the empty graph), which is hence extensive [START_REF] Lack | Adhesive and quasiadhesive categories[END_REF]. This implies that the two squares X i , T i , X 1 ⊎ X 2 , T 1 ⊎ T 2 must be pullbacks. It follows that the composition of the spans f ′ T and f iT equals f ′ i T . Furthermore the span f ′ T is unique since, again by extensivity, taking X 1 ⊎ X 2 as support is the only way to obtain two pullbacks; then the arrows of the span are fixed as mediating morphisms.

• Now define f ′ P : P ′ → P ⊎ {∅} as follows:

f ′ P (q ′ ) = ( f ′ 1 P (q ′ ), f ′ 2 P (q ′
)) if at least one of the components of the pair is different from ∅ and f ′ P (q ′ ) = ∅ otherwise. The situation is depicted in the diagram below:

P 1 P 2 P f 1 P a a B B B f 2 P = = | | | P ′ f ′ 1 P F F f ′ 2 P X X f ′ P O O Clearly f i P • f ′ P = f ′ i P
and it is easy to see that f ′ P is unique. In fact, let f ′′ P : P ′ → P ⊎ {∅} another mapping with

f i P • f ′′ P = f ′ i P and let q ′ ∈ P ′ . It holds that λ ′ (q ′ ) ∈ Λ ′ ⊇ Λ = Λ 1 ∪ Λ 2 .
We distinguish two cases λ ′ (q ′ ) ∈ Λ 1 ∪ Λ 2 : in this case at least one of f ′ 1 P (q ′ ) and f ′ 2 P (q ′ ) must be different from ∅. Hence, since the f i P are simply projections, we deduce that

f ′′ P (q ′ ) = ( f ′ 1 P (q ′ ), f ′ 2 P (q ′ )) = f ′ P (q ′ ). -λ ′ (q ′ ) Λ: in this case f ′ i P (q ′ ) = ∅ for i ∈ {1, 2}. Since (∅, ∅) is not in P, we deduce that f ′′ P (q ′ ) = ∅ = f ′ P (q ′ ).
Note that for the argument above, the condition about labels in the definition of grammar morphisms (Condition 3 in Definition 9) is essential.

• Finally, the components of ι f ′ can be defined as follows: in the diagram below take the pullback of

X 1 ⊎X 2 → T ′ and |G s ′ | → T ′ in
|G s1 | * * V V V V V V V V V V V V / / S ι s f ′ % % |G s2 | z z v v v o o |G s ′ | X 1 / / + + V V V V V V V V V V V V V V X 1 ⊎ X 2 & & M M M M M X 2 o o z z u u u u T ′ Analogously one can define morphisms ι L f ′ : |L q | ⇀ |L q ′ |, ι R f ′ : |R q | ⇀ |R q ′ |
for productions q ′ ∈ P ′ , q ∈ P where f ′ P (q ′ ) = q. It remains to show that the square on the left below commutes. Let q i = f 1 P (q) and consider the diagram on the right below. It is known that all triangles and squares-apart from the bottom square-commute and that |L q | is the coproduct of |L q 1 | and |L q 2 |. Since the two coprojections |L q i | ⇀ |L q | are jointly epi (also in the category of partial morphisms), commutativity follows from a simple diagram-chasing argument.

|L q | / |R q | |L q ′ | / |R q ′ | |R q 1 | B B B B B B B B B ! ! |R q 2 | || | | | | | | | o o |L q 1 | B B B B B B B B B 6 n n n n n n ! ! |L q 2 | 6 n n n n n n || | | | | | | | o o |R q | |L q | 6 n n n n n n |R q ′ | |L q ′ | 6 n n n n n n
Note also that whenever G 1 and G 2 are semi-weighted, then G is semi-weighted. And since every arrow in GG between semi-weighted grammars is also an arrow in SGG, the same argument applies. 2

Occurrence Grammars and Unfolding

A grammar G is safe if (i) for all H such that G s ⇒ * H, H is injective, and (ii) for each q ∈ P, the left-and right-hand side graphs L q and R q are injective.

In words, in a safe grammar each graph G reachable from the start graph is injectively typed, and thus we can identify it with the corresponding subgraph t G (|G|) of the type graph. With this identification, a production can only be applied to the subgraph of the type graph which is the image via the typing morphism of its left-hand side. Thus, according to its typing, we can think that a production produces, preserves or consumes items of the type graph, and using a net-like language, we speak of pre-set, context and post-set of a production, correspondingly. Intuitively the type graph T plays the role of the set of places of a net, whereas the productions in P correspond to the transitions. Definition 11 (pre-set, post-set and context of a production). Let G be a graph grammar. For any production q ∈ P we define its pre-set • q, context q and post-set q • as the following subsets of E T ∪ N T :

• q = t Lq (|L q | -|dom(r q )|) q = t Lq (|dom(r q )|) q • = t Rq (|R q | -r q (|dom(r q )|)).
Symmetrically, for each item x ∈ T we define

• x = {q ∈ P | x ∈ q • }, x • = {q ∈ P | x ∈ • q}, x = {q ∈ P | x ∈ q}.
Causal dependencies between productions are captured as follows.

Definition 12 (causality).

The causality relation of a grammar G is the (least) transitive relation < over Elem(G) satisfying, for any node or edge x ∈ T , and for productions q, q ′ ∈ P,

1. if x ∈ • q then x < q; 2. if x ∈ q • then q < x; 3. if q • ∩ q ′ ∅ then q < q ′ .
As usual ≤ is the reflexive closure of <. Moreover, for x ∈ Elem(G) we denote by ⌊x⌋ the set of causes of x in P, namely {q ∈ P | q ≤ x}.

As it happens in Petri nets with read arcs, the fact that a production application not only consumes and produces, but also preserves a part of the state, leads to a form of asymmetric conflict between productions; for a more thorough discussion of asymmetric event structures see Appendix A.1 and [START_REF] Baldan | Contextual Petri nets, asymmetric event structures and processes[END_REF].

Definition 13 (asymmetric conflict).

The asymmetric conflict relation of a grammar G is the binary relation ր over the set of productions, defined by: 1. if q ∩ • q ′ ∅ then q ր q ′ ; 2. if • q ∩ • q ′ ∅ and q q ′ then q ր q ′ ; 3. if q < q ′ then q ր q ′ . Intuitively, whenever q ր q ′ , q can never follow q ′ in a computation. This holds when q preserves something deleted by q ′ (Condition 1), trivially when q and q ′ are in conflict (Condition 2) and also when q < q ′ (Condition 3). Conflicts are represented by cycles of asymmetric conflict: if q 1 ր q 2 ր . . . ր q n ր q 1 then the entire set {q 1 , . . . , q n } will never appear in the same computation.

An occurrence grammar is an acyclic grammar which represents, in a branching structure, several possible computations beginning from its start graph and using each production at most once. Recall that a relation R ⊆ X × X is called finitary if for any x ∈ X, the set {y ∈ X | R(y, x)} is finite.

Definition 14 (occurrence grammar).

An occurrence grammar is a safe grammar O = T, G s , P, π, Λ, λ such that 1. causality < is irreflexive, its reflexive closure ≤ is a partial order, and, for any q ∈ P, the set ⌊q⌋ is finite and asymmetric conflict ր is acyclic on ⌊q⌋; 2. any item x in T is created by at most one production in P, i.e., | • x| ≤ 1; 3. the start graph G s is the set Min(O) of minimal elements of Elem(O), ≤ (with the graphical structure inherited from T and typed by the inclusion);

A finite occurrence grammar is deterministic if relation ր + , the transitive closure of ր, is irreflexive. We denote by OGG the full subcategory of GG with occurrence grammars as objects.

Intuitively, by condition 1 the causes of any event are finite and free of conflicts (cycles of asymmetric conflict), while condition 2 ensures that any item is generated at most once in a computation. By condition 3, the start graph of an occurrence grammar is determined by Min(O). An occurrence grammar is deterministic when it does not contain conflicts so that all its productions can be executed in the same computation. Given two occurrence grammars O 1 and O 2 , we say that O 1 is a sub-grammar of O 2 , if O 1 ⊆ O 2 , componentwise, and the inclusion of O 1 into O 2 is a grammar morphism. In the sequel, the productions of an occurrence grammar will often be called events. The notion of configuration captures the intuitive idea of (deterministic) computation in an occurrence grammar.

Definition 15 (configuration).

Let O be an occurrence grammar. A configuration is a subset C ⊆ P satisfying the following requirements 1. for any q ∈ C it holds that ⌊q⌋ ⊆ C; 2. ր C , the asymmetric conflict restricted to C, is acyclic and finitary.

The set of configurations of O is denoted as Conf (O).

It is shown in [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF] that, indeed, configurations faithfully represent computations in an occurrence grammar: all the productions in a configuration can be applied in a derivation exactly once in any order compatible with ր, and all and only the derivations in O can be obtained in this way. Hence the runs of an occurrence grammar are exactly the linearisations, compatible with the asymmetric conflict relation, of its configurations, i.e., the following holds:

Proposition 2 (configurations as runs).

Let O be an occurrence grammar. Then Runs(O) = {q 1 . . . q n | {q 1 , . . . , q n } ∈ Conf (O) ∧ ∀i < j. ¬(q j ր q i )}.

Since occurrence grammars are particular semi-weighted grammars, there is an inclusion functor I : OGG → SGG. As an easy corollary of [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF]Theorem 45], this functor has a right adjoint. We remark that this theorem would not hold if we considered GG instead of SGG. Theorem 1 (coreflection). The inclusion functor I : OGG → SGG has a right adjoint, the so-called unfolding functor U : SGG → OGG.

As a consequence of the above result U, as a right adjoint, preserves all limits and in particular products, i.e., given two grammars G 1 and G 2 , it holds that

U(G 1 × G 2 ) = U(G 1 ) × U(G 2 ).
The result in [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF] is obtained through the explicit definition of the unfolding U(G). Given a grammar G the unfolding construction produces an occurrence grammar which fully describes its behaviour recording all the possible graph items which are generated and the occurrences of productions. The unfolding of G is constructed inductively by starting from a grammar which only includes the start graph of G (which is also used as a type graph), and then extending such grammar, at any step, by applying productions in any possible way to the type graph, without deleting items but only generating new ones, and recording the corresponding production instances. The result is an occurrence grammar U(G) and a grammar morphism f : U(G) → G, called the folding morphism, which maps each item (instance of production or graph item) of the unfolding to the corresponding item of the original grammar. The construction is not formally defined here, we refer the reader to [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF]. In Section 4 we will show an example of an unfolding.

As an immediate consequence of the fact that the unfolding U(G) completely captures the behaviour of a grammar G, we have the following result.

Proposition 3 (completeness of the unfolding). For any semi-weighted graph grammar G it holds that

λ * (Runs(U(G))) = λ * (Runs(G)).

Interleaving Structures

Interleaving structures [START_REF] Baldan | Distributed unfolding of petri nets[END_REF] are a semantic model which captures the behaviour of a system as the collection of its possible runs. They are used as a simpler intermediate model which helps in stating and proving the correctness of the diagnosis procedure.

An interleaving structure is essentially a collection of runs (sequences of events) satisfying suitable closure properties. Given a set E, we will denote by E ⊙ the set of sequences over E in which each element of E occurs at most once.

Definition 16 (interleaving structures).

A (labelled) interleaving structure is a tuple I = (E, R, Λ, λ) where E is a set of events, λ : E → Λ is a labelling of events and R ⊆ E ⊙ is the set of runs, satisfying: (i) R is prefix-closed, (ii) R contains the empty run ε, and (iii) every event e ∈ E occurs in at least one run.

The components of an interleaving structure I will be denoted by E, R, Λ, λ, possibly with subscripts. The category of interleaving structures, as defined below, is adapted from [START_REF] Baldan | Distributed unfolding of petri nets[END_REF] by changing the notion of morphisms in order to take into account the labels. This is needed to obtain a product which expresses a suitable form of synchronised composition.

Definition 17 (interleaving morphisms).

Let I i with i ∈ {1, 2} be interleaving structures. An interleaving morphism from I 1 to I 2 is a partial function θ : E 1 ⇀ E 2 on events such that 1. Λ 2 ⊆ Λ 1 ; 2. for each e 1 ∈ E 1 , θ(e 1 ) ↓ iff λ 1 (e 1 ) ∈ Λ 2 and, in this case, λ 2 (θ(e 1 )) = λ 1 (e 1 ); 3. for every r ∈ R 1 it holds that θ * (r) ∈ R 2 .

Morphism θ is called a projection if it is surjective on runs, i.e., θ * : R 1 → R 2 is surjective. The category of interleaving structures and morphisms is denoted Ilv.

Observe that an interleaving morphism θ : I 1 → I 2 is necessarily injective on the events occurring in each run, i.e., for any run r 1 = e 1 . . . e k ∈ R 1 , for i j we have θ(e i ) θ(e j ), when both are defined. Otherwise, θ(r) could not be a run in I 2 as it would contain two occurrences of the same event.

An occurrence grammar can be easily mapped to an interleaving structure, by simply taking all the runs of the grammar.

Definition 18 (interleaving structures for occurrence grammars). For an occurrence grammar O we define Ilv(O) = (P, Runs(O), Λ, λ).

We next characterise the categorical product in Ilv, which turns out to be, as in GG, the desired form of synchronised product.

Proposition 4 (product of interleaving structures).

Let I 1 and I 2 be two interleaving structures. Then the product object I 1 × I 2 is the interleaving structure I = (E, R, Λ, λ) defined as follows. Let

E ′ = {(e 1 , e 2 ) | e 1 ∈ E 1 , e 2 ∈ E 2 , λ 1 (e 1 ) = λ 2 (e 2 )} ∪ {(e 1 , * ) | e 1 ∈ E 1 , λ 1 (e 1 ) Λ 2 } ∪ {( * , e 2 ) | e 2 ∈ E 2 , λ 2 (e 2 ) Λ 1 }
and let π i : E ⇀ E i be the obvious partial projections (e.g., π 1 (e 1 , x 2 ) = e 1 and π 1 ( * , x 2 ) ↑ for e 1 ∈ E 1 and

x 2 ∈ E 2 ∪ { * }). Then R = {r ∈ (E ′ ) ⊙ | π * 1 (r) ∈ R 1 , π * 2 (r) ∈ R 2 }, E = {e ′ ∈ E ′ |
e occurs in some run r ∈ R}, Λ = Λ 1 ∪ Λ 2 and λ is defined in the obvious way.

Proof. Let I ′ be any interleaving structure and let θ i : I ′ → I i be morphisms. Let us define θ : I ′ → I as follows:

θ(e ′ ) ↑ if θ 1 (e ′ ) ↑ and θ 2 (e ′ ) ↑ θ(e ′ ) =            (θ 1 (e ′ ), θ 2 (e ′ )) if θ 1 (e ′ ) ↓ and θ 2 (e ′ ) ↓ (θ 1 (e ′ ), * ) if θ 1 (e ′ ) ↓ and θ 2 (e ′ ) ↑ ( * , θ 2 (e ′ ))
if θ 1 (e ′ ) ↑ and θ 2 (e ′ ) ↓

Trivially, the diagram, seen in the category of sets and partial functions, commutes and θ is uniquely determined.

Hence to conclude we just need to show that θ is a well-defined interleaving morphism. In fact, 1. Since there are morphisms θ i :

I ′ → I i , necessarily Λ i ⊆ Λ ′ , for i ∈ {1, 2} and thus Λ = Λ 1 ∪ Λ 2 ⊆ Λ ′ . 2.
For each e ′ ∈ E ′ , θ(e ′ ) ↓ iff λ ′ (e ′ ) ∈ Λ. In more detail:

θ(e ′ ) ↓ ⇐⇒ θ 1 (e ′ ) ↓ or θ 2 (e ′ ) ↓ ⇐⇒ λ ′ (e ′ ) ∈ Λ 1 or λ ′ (e ′ ) ∈ Λ 2 ⇐⇒ λ ′ (e ′ ) ∈ Λ 1 ∪ Λ 2 = Λ.
And clearly, when defined,

λ ′ (e ′ ) = λ(θ(e ′ )) 3. For any r ′ ∈ R ′ , θ * (r ′ ) ∈ R.
In fact, notice that, due to commutativity,

π * i (θ * (r ′ )) = θ * i (r ′ ) ∈ R i . Hence, by construction, θ * (r ′ ) ∈ R. 2

Diagnosis and Pruning

In this section we use the tools introduced so far in order to formalise the diagnosis problem. Then we show how, given a graph grammar model and an observation for such a grammar, the diagnosis can be obtained by first taking the product of the model and the observation, considering its unfolding and finally pruning such unfolding in order to remove incomplete explanations. As already mentioned, typically only a subset of the productions in the system is observable. Hence, for this section, we fix a graph grammar G with Λ as the set of labels, and a subset Λ ′ ⊆ Λ of observable labels; an event or production is called observable if it has an observable label. In order to keep explanations finite, we will only consider systems that satisfy the following observability assumption (compare [START_REF] Sampath | Failure diagnosis using discrete event models[END_REF][START_REF] Haar | Partial order diagnosability of discrete event systems using Petri net unfoldings[END_REF]): any infinite run must contain an infinite number of observable productions.

In the sequel we will need to consider the runs of a system which have a number of observable events coinciding with the number of events in the observation. For this aim the following definition will be useful.

Definition 19 (n-runs of a grammar).

Let G be a graph grammar. For a given n ∈ N we denote by Runs n (G) the set of all runs for which the number of observable productions equals n.

The outcome of the diagnosis procedure is an occurrence grammar which, intuitively, collects all the behaviours of the grammar G modelling the system, which are able to "explain" the observation.

An observation can be a sequence (in the case of a single observer) or a set of sequences (in the case of multiple distributed observers) of alarms (observable events). Here we consider, more generally, partially ordered sets of observations, which can be conveniently modelled as deterministic occurrence grammars.

Definition 20 (observation grammar

). An observation grammar A for a given grammar G, with observable labels Λ ′ , is a (finite) deterministic occurrence grammar labelled over Λ ′ . Given a sequence of observed events, we can easily construct an observation grammar A having that sequence as observable behaviour. It will have a production for each event in the sequence, with the corresponding label. Each such production consumes a resource generated by the previous one in the sequence (or an initial resource in the case of the first production). The same construction applies to general partially ordered sets of observations. Example 3. In the running example grammar M (see Fig. 9 and Fig. 10), assume that we have the following observation: snd cnode cconn 2 crcv, i.e., we observe, in sequence, the sending of a message, the creation of a new intermediary node with the corresponding connection, the creation of a connection to a receiver and the reception of a corrupted message. As explained above, these four observations can be represented by a simple grammar A (see Fig. 13) with four productions, each of which either consumes an initial resource or a resource produced by the previous production. These resources are modeled as 0-ary edges (labelled X, Y, W, Z). The start graph is depicted with bold lines, and the left-and right-hand sides of the productions of the occurrence grammar are indicated by using a Petri-net-like notation: productions are drawn with black rectangles connected to the edges they consume or produce by dashed lines.

When unfolding the product of a grammar G with its observation A, we obtain a grammar U = U(G × A) with a morphism π : U → A, arising as the image through the unfolding functor of the projection G × A → A (since the unfolding of an occurrence grammar is the grammar itself). Now, as grammar morphisms are simulations [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF], given the morphism π : U → A we know that any configuration in U is mapped to a configuration in A. Say that a configuration in U is a full explanation of A if it is mapped to the configuration of A including all its productions. As U can still contain events belonging only to incomplete explanations, the aim of pruning is to remove such events.

Definition 21 (pruning).

Let π : U → A be a grammar morphism from an occurrence grammar U to an observation A. Then, the pruning of π, denoted by Pr(π), is the sub-grammar of U obtained by keeping only the productions in

{q ∈ P U | ∃C ∈ Conf (U) : (q ∈ C ∧ π(C) = P A )}
The next technical lemma shows that applying the pruning operation to a morphism π : U → A no runs in U which provide a full explanation of A are lost.

Lemma 1 (interleavings of a pruned grammar). Let π : U → A be a grammar morphism from an occurrence grammar to an observation A with n productions. Then

Runs n (Pr(π)) = {r ∈ Runs(U) | π * (r) ∈ Runs n (A)}.
Proof. We first show that Runs n (Pr(π)) ⊆ {r ∈ Runs(U) | π * (r) ∈ Runs n (A)}. Take any run r ∈ Runs n (Pr(π)). Then clearly r ∈ Runs(U) since Pr(π) is a subgrammar of U. Furthermore, since π preserves the observable productions, π * (r) must contain exactly n observable productions and thus it belongs to Runs n (A).

For the other direction take any run r ∈ Runs(U) such that π * (r) ∈ Runs n (A). Then, again, r must contain exactly n observable productions. Furthermore take the configuration C consisting of the productions in r. Since π maps C to the set of all productions of A, none of the productions of r is removed during the pruning phase. Hence r ∈ Runs n (Pr(π)).

2

Discussing the efficiency of pruning algorithms is outside the scope of the paper; for sequential observations an on-the-fly algorithm is discussed in [START_REF] Benveniste | Diagnosis of asynchronous discrete event systems, a net unfolding approach[END_REF].

As described above, the diagnosis is constructed by first taking the product of G with the observation (this intuitively represents the system constrained by the observation). This product is then unfolded to get an explicit representation of the possible behaviours explaining the observation. Finally, a pruning phase removes from the resulting occurrence grammar the events belonging (only) to incomplete explanations. This is formalised in the definition below.

Definition 22 (diagnosis grammar).

Let G be the grammar modelling the system of interest and let A be an observation. Take the product G × A, the right projection ϕ : G × A → A and consider π = U(ϕ) : U(G × A) → A.

Then the occurrence grammar Pr(π) is called the diagnosis grammar for the model G and the observation A, and it is denoted by D(G, A).

Since the observability assumption holds, it can be shown that the diagnosis grammar is finite whenever the observation is finite. Roughly, the argument is as follows. Assume that the diagnosis grammar is infinite. Since it is finitely branching it must contain an infinite computation, which, by the observability assumption, would contain infinitely many observable events. However, this cannot be the case since all computations in the diagnosis grammar contain at most as many observable events as the observation.

Example 4. We can compute the product of grammars M and A and unfold it. For the sake of clarity Fig. 14 shows only a prefix of the unfolding (The full unfolding is presented in Section 6.) In order to give a compact representation of such prefix we again use a Petri-net-like notation. Edges that are preserved by a production are indicated by read arcs, i.e., dashed arcs without arrowhead that connect an edge and a black rectangle.

The considered prefix depicts one possible explanation: here the message is sent (event a) and crosses the first connection (b). Possibly concurrently a new intermediate node and a connection to this node is created (c). The new node is initially inactive and it becomes active immediately after (d). The new connection is crossed by the message (e) and, in a possibly concurrent step, a new connection to the receiver is created (f). Such connection is corrupted (g), leading to the corruption of the message (h) and its reception by the receiver (i). Observable events are indicated by bold face letters.

Several events of the unfolding have been left out due to space constraints, for instance:

• Events belonging to alternative explanations: the corruption of the first connection or the corruption of the newly created middle connection (or the corruption of any non-empty subset of these connections). Alternatively it might have been the case that the new connection was created from the original intermediate node directly to the receiver.

• Events that are not directly related to the failure, such as the corruption of the first or second connection after the message has crossed.

Furthermore there are events belonging to prefixes of the unfolding that cannot be extended to a full observation. For instance, the full unfolding would contain an event corresponding to an (uncorrupted) message crossing the rightmost uncorrupted connection C. However, this is a false trail since, after this, it would be impossible to complete the explanation with the reception of a corrupted message (in fact, this would require the sending of a new message, an event which would be visible and inconsistent with the observation). These events belonging only to incomplete explanations are removed from the unfolding in the pruning phase.

We remark that-due to the presence of concurrent events-the unfolding is a much more compact representation of everything that might have happened in the system than the set of all possible interleavings of events. 18

Correctness of the Diagnosis

We now show our main result, stating that the runs of the diagnosis grammar properly capture all those runs of the system model which explain the observation. This is done by exploiting the coreflection result (Theorem 1) and by additionally taking care of the pruning phase (Definition 21).

To lighten the notation, hereafter, given an interleaving structure I we write λ * (I) for λ * (R I ). Recall that, given f :

Λ 1 ⇀ Λ 2 , f * : Λ * 1 → Λ *
2 denotes the (non-strict) extension of f to sequences. Then f -1 : P(Λ * 2 ) → P(Λ * 1 ) is its inverse.

A first lemma shows that the labelled runs of a product of occurrence grammars O 1 × O 2 can be obtained by suitably combining pairs of compatible runs of O 1 and O 2 . By "compatible" we mean that they admit a common extension, obtained by interleaving the run of O 1 with events labelled in (Λ 1 ∪ Λ 2 ) -Λ 2 and, dually, the run of O 2 with events labelled in (Λ 1 ∪ Λ 2 ) -Λ 1 .

Lemma 2.

Let O 1 , O 2 be two occurrence grammars and let f i : Λ 1 ∪ Λ 2 ⇀ Λ i (i ∈ {1, 2}) be the obvious partial inclusions. Then it holds that

λ * (Ilv(O 1 × O 2 )) = f -1 1 (λ * 1 (Ilv(O 1 ))) ∩ f -1 2 (λ * 2 (Ilv(O 2 ))). Proof. Let I 1 = Ilv(O 1 ), I 2 = Ilv(O 2 ) and I = I 1 × I 2 = Ilv(O 1 ) × Ilv(O 2 )
. Furthermore let π i : I → I i , i ∈ {1, 2} be the projections. We first observe that

λ * (I) = λ * (R I ) = {λ * I (r) | r ∈ (E I ) ⊙ ∧ π * 1 (r) ∈ R 1 ∧ π * 2 (r) ∈ R 2 } ( †) = {w ∈ Λ * | f * 1 (w) ∈ λ * 1 (R 1 ), f * 2 (w) ∈ λ * 2 (R 2 )} = f -1 1 (λ * 1 (R 1 )) ∩ f -1 2 (λ * 2 (R 2 )) = f -1 1 (λ * 1 (I 1 )) ∩ f -1 2 (λ * 2 (I 2 ))
The equality marked ( †) above, which is not obvious, can be shown as follows.

⊆: Take r ∈ R I and consider the sequence of labels λ * I (r) associated with r. Since π 1 is defined exactly on the events whose label is in Λ 1 , it holds that λ *

1 (π * 1 (r)) = f * 1 (λ * I (r)), hence f * 1 (λ * I (r)) ∈ λ * 1 (R 1 ). Similarly one can show that f * 2 (λ * I (r)) ∈ λ * 2 (R 2 ). ⊇: Let w ∈ Λ * be such that f * 1 (w) ∈ λ * 1 (R 1 ) and f * 2 (w) ∈ λ * 2 (R 2 ). Assume that w = c 1 . . . c k , f * 1 (w) = c i 1 .
. . c i n and f * 2 (w) = c j 1 . . . c j m . Furthermore let r 1 = f i 1 . . . f i n ∈ R 1 be a run with λ * 1 (r 1 ) = f * 1 (w) and let r 2 = g j 1 . . . g j m ∈ R 2 be a run with λ * 2 (r 2 ) = f * 2 (w). Now construct a run r = e 1 . . . e n with

e i =          ( f i , g i ) if c i ∈ Λ 1 ∩ Λ 2 ( f i , * ) if c i ∈ Λ 1 \Λ 2 ( * , g i ) if c i ∈ Λ 2 \Λ 1
It holds that π * 1 (r) = r 1 , π * 2 (r) = r 2 and obviously λ * I (r) = w. Hence w is contained in the left-hand set. We next show that λ * (I) = λ * (Ilv(O 1 × O 2 )), and thus we conclude. This follows from Lemma 3 in Appendix A.2 which guarantees the existence of a total projection δ : Ilv(O 1 × O 2 ) → I. In fact, since δ respects labellings and is total, whenever it maps two runs of Ilv(O 1 ×O 2 ) to one run of I, they must be associated with the same label sequence. Using, additionally, the fact that δ is surjective on runs, the desired equality immediately follows.

2

The next proposition shows that considering the product of the original grammar G and of the observation A, taking its unfolding and the corresponding labelled runs, we obtain exactly the runs of G compatible with the observation.

Proposition 5. Let G be a grammar and A an observation, where Λ is the set of labels of G and Λ ′ ⊆ Λ the set of labels of A. Furthermore let f : Λ ⇀ Λ ′ be the obvious partial inclusion. Then it holds that:

λ * (Ilv(U(G × A))) = λ * (Runs(G)) ∩ f -1 (λ * (Runs(A))).
Proof. First, recall that, by Proposition 3, λ * (Runs(G)) = λ * (Ilv(U(G))) and λ * (Runs(A)) = λ * (Ilv(U(A))) = λ * (Ilv(A)). Furthermore due to the fact that unfolding is a coreflection (Theorem 1), we have

U(G × A) = U(G) × U(A).
Hence we have to show that

λ * (Ilv((U(G)) × (U(A)))) = λ * (Ilv(U(G))) ∩ f -1 (λ * (Ilv(U(A)))).
This is a corollary of Lemma 2 for

O 1 = U(G), O 2 = U(A) = A, Λ 1 = Λ, Λ 2 = Λ ′ ; furthermore f corresponds to f 2 and f 1 is the identity since Λ ′ ⊆ Λ. 2
We can finally prove that the described diagnosis procedure is complete, i.e., given an observation of size n, the runs of the diagnosis grammar D(G, A) with n observable events are in 1-1-correspondence with those runs of G that provide a full explanation of the observation. As a preliminary result, on the basis of Proposition 5, one could have shown that the same holds replacing the diagnosis grammar with U(G × A), i.e., the unpruned unfolding. The result below additionally shows that no valid explanation is lost during the pruning phase.

Theorem 2 (correctness of the diagnosis). With the notation of Proposition 5 it holds that:

λ * (Runs n (D(G, A))) = λ * (Runs(G)) ∩ f -1 (λ * (Runs n (A))).
That is, the maximal interleavings of the diagnosis grammar (seen as label sequences) are exactly the runs of the model which explain the full observation.

Proof. By definition

λ * (Runs n (D(G, A))) = λ * (Runs n (Pr(π 2 ))), (1)
where, if we let U = U(G × A), then π 2 : U → A is the (image through the unfolding functor of the) second projection of the product. By Lemma 1, the set (1) is the same as

λ * ({r ∈ Runs(U) | π * (r) ∈ Runs n (A)}), (2)
We will now show that set (2) coincides with ⊆: Let w = λ * (r) for some r ∈ Runs(U) and π * (r) ∈ Runs n (A). By Proposition 3, w ∈ λ * (Runs(G)). The fact that w ∈ f -1 (λ * (Runs n (A))) easily follows by observing that λ * (π * 2 (r)) ∈ λ * (Runs n (A)) is a subsequence of w where all unobservable labels are missing and these labels, by definition, can be reinserted by f -1 . This proves the inclusion (2) ⊆ (3).

λ * (Runs(G)) ∩ f -1 (λ * (Runs n (A))). (3)
⊇: Let w ∈ λ * (Runs(G)) ∩ f -1 (λ * (Runs n (A))). Observe that λ * (Runs(G)) ∩ f -1 (λ * (Runs n (A))) ⊆ λ * (Runs(G)) ∩ f -1 (λ * (Runs(A))) = λ * (Ilv(U)) ( Proposition 5)
Hence there exists a run r ∈ Runs(U) such that λ * (r) = w. By definition of a morphism, π * 2 (r) ∈ Runs(A) and λ

* (π * 2 (r)) = f * (λ * (r)) = f * (w) ∈ λ * (Runs n (A)) (by choice of w). Hence also π * 2 (r) ∈ Runs n (A). Summing up r ∈ {r ∈ Runs(U) | π 2 (r) ∈ Runs n (A)} and since λ * (r) = w we conclude w ∈ λ * (π -1 2 (Runs n (A))). 2
Observe that, due to the nondeterministic nature of the diagnosis grammar, events which are kept in the pruning phase as they are part of some full explanation of the observation, can also occur in a different configuration. As a consequence, although all inessential events have been removed, the diagnosis grammar can still contain spurious configurations which cannot be extended to full explanations. As an example, consider the graph grammar G in Fig. 15, given in a Petri-net-like notation. Assume we observe three unordered events a, b, c. Then the unfolding of the product basically corresponds to G itself. In the pruning phase nothing is removed, since each event is part of a chain consisting of a, b, c which fully explains the observation. However, since different explanations can interfere, there is a configuration (indicated by the dashed closed line) that cannot be further extended to an explanation.

Experimental Evaluation

In order to give an idea about the practical applicability of our approach, we use some existing tools in order to compare the size of the unfolding with that of interleaving-based models which could be used for analysing the running example (message passing over a network).

Graph grammars are unfolded by using an extension of the tool Augur [START_REF] König | Augur 2-a new version of a tool for the analysis of graph transformation systems[END_REF], whose original purpose is to compute approximated unfoldings in order to abstract infinite-state graph transformation systems. The extension, under the assumption that rules do not delete nodes, can also be used to produce an ordinary, non-approximated, unfolding of a graph grammar. In our running example this assumption is violated only by rule fail, which is however not involved in the specific observation that we are considering and thus can be safely omitted. We have not yet implemented the computation of the product of two graph grammars (this is done manually) and pruning. We took the running example grammar M (see Figures 9 and10) and computed the product of this grammar and the observation grammar for the sequence snd cnode cconn 2 crcv. The unfolding is shown in Figures 16 and17, visualized by using GraphViz. 1 For reasons of clarity the output of the tool, i.e. the unfolding, is split into two components: the underlying type graph and a Petri net which represents the rules, depicting deletion, preservation and creation of the edges of the type graph.

S _3 0 C _5 0 1 I _6 0 R _8 0 X _9 S _86 0 M _87 0 Y _88 CC _90 0 1 M _92 0 CM _94 0 I _97 0 II _98 0 C _99 0 1 W _100 M _102 0 CM _104 0 CC _106 0 1 I _108 0 C _109 0 1 Z _110 I _112 0 M _114 0 CM _116 0 CM _118 0 CC _120 0 1 I _122 0 C _123 1 0 Z _124 R _126 0 M _128 0 CM _130 0 CM _132 0 CM _134 0 CC _136 1 0 R _138 0 R _140 0 R _142 0 CM _144 0 R _146 0
The unfolding includes 40 edges, 4 nodes and 26 transitions (a prefix of this unfolding was already presented in Figure 14). The unfolding shown here is still unpruned. In the pruned version the transitions labelled cross1 115 and cross1 129 would be removed. They correspond to cases where an uncorrupted message arrives at the receiver, thus making the last observation (crcv) impossible.

The five transitions labelled crcv represent five distinct situations: either the message has passed from the sender to the original intermediate node cirectly to the receiver and the corruption of the message has been caused by the first connection (crcv 127) or by the second connection (crcv 139). Or the message has passed from the sender to the original intermediate node to a new intermediate node to the receiver and its corruption has been caused by the first (crcv 143), second (crcv 141) or third (crcv 147) connection. Note that the last event (crcv 147) corresponds to event i in Figure 14.

In order to get an idea of the cost of a diagnosis algorithm based on interleavings, we can compute the product of the transition system of M with an automaton representing the observation. The size of the resulting transition system is the same as the size of the state space of the product grammar. We determined the corresponding number of states (taken up to isomorphisms) by using Groove2 , a tool for state space exploration and model-checking of graph transformation systems [START_REF] Rensink | The GROOVE simulator: A tool for state space generation[END_REF]. The state space consists of 205 states and it is not straightforward to deduce manually the diagnosis information from the corresponding transition system. Since this example is still fairly small we took the same grammar M and considered a slightly longer observation sequence: snd cnode cconn2 cnode crcv. In this case, the unfolding consists of 83 edges, 8 vertices and 57 transitions, whereas the state space contains 1338 states. In general, for highly concurrent systems, the unfolding tends to be exponentially smaller than the interleaving model; this blow up in the size will decrease for systems where the degree of concurrency is limited.

Conclusion

In this paper we formalised event-based diagnosis for systems with variable topologies, modelled as graph transformation systems. In particular we have shown how to exploit the coreflection result for the unfolding of graph grammars in order to show the correctness of a diagnosis procedure generating partially ordered explanations for a given observation.

We are confident that the approach presented in the paper, although developed for transformation systems over hypergraphs, can be generalised to the more abstract setting of adhesive categories. In particular we have developed a generalization of the unfolding procedure [START_REF] Baldan | Unfolding grammars in adhesive categories[END_REF] that works for spo-rewriting in (suitable variations of) adhesive categories [START_REF] Lack | Adhesive and quasiadhesive categories[END_REF]. This would allow one to have a kind of parametric framework which can be used to instantiate the results of this paper to more general rewriting theories, e.g., rewriting graphs with scopes, graphs with second-order edges, and other kind of graph structures (which for instance occur in the various UML diagrams).

We are also interested in distributed diagnosis where every observer separately computes possible explanations of local observations that however have to be synchronized. In [START_REF] Baldan | Distributed unfolding of petri nets[END_REF] we already considered distributed unfolding of Petri nets; for diagnosis however, the non-trivial interaction of distribution and pruning has to be taken into account. Distribution will require the use of pullbacks of graph morphisms, in addition to products. Pullbacks are needed since we want to describe system composition via a common interface.

Proof. In order to prove that δ is a p¡rojection, consider any run r = e 1 . . . e n in Ilv(O 1 ) × Ilv(O 2 ). We have to prove that there exists a run r ′ of Ilv(O 1 × O 2 ) such that δ * (r ′ ) = r.

By definition of interleaving structure morphisms, r i = δ * i (r) is a run in Ilv(O i ), for i ∈ {1, 2}. Hence, by Proposition 2, the set C i of events which occur in r i is a configuration C i ∈ Conf (O i ) and r i is a linearisation of C i compatible with the asymmetric conflict relation ր i in O i , for i ∈ {1, 2}

Consider the aes E s (O i ) underlying grammar O i for i ∈ {1, 2}. Note that functor E s is a right adjoint by Theorem 3 and thus it preserves limits and, in particular products. Hence

δ * i (δ * (r ′ )) = Ilv(π i ) * (r ′ ) = r i
From this, recalling how the product of interleaving structures is characterised (Proposition 4), we deduce that δ * (r ′ ) = r, as desired.

In order to prove that δ is total it suffices to observe that, for any event e in Ilv(O 1 × O 2 ) (and hence in O 1 × O 2 ), either Ilv(π 1 (e)) or Ilv(π 2 )(e) are defined. This immediately follows by from the fact that, by Proposition 1, either π 1 (e) ∅ or π 2 (e) ∅. Now, this implies that δ(e) must be defined, since otherwise either δ 1 • δ = π 1 or δ 2 • δ = π 2 would not hold.

2

Figure 1 :

 1 Figure 1: A Petri net (left) and a fragment of its unfolding (right).

Figure 2 :

 2 Figure 2: An observation (left) and the corresponding diagnosis net (right).

4

 4

Figure 3 :Figure 4 :

 34 Figure 3: The start graph and type graph of the example graph grammar S.

Figure 5 :

 5 Figure 5: Example grammar S: message passing over an evolving network.

Figure 6 :

 6 Figure 6: A run in the example grammar S.

Figure 7 :

 7 Figure 7: Equivalence and composition of spans.

Figure 8 :

 8 Figure 8: Diagrams for spo grammar morphisms.

Figure 9 :

 9 Figure 9: Start graph and type graph for the running example grammar M.

Figure 10 :Figure 11 :Figure 12 :

 101112 Figure 10: Productions for the running example grammar M.

Figure 13 :

 13 Figure 13: A graph grammar representing an observation A, given in a Petri-net-like notation.

Figure 14 :

 14 Figure 14: Running example: prefix of the unfolding of the product.

Figure 15 :

 15 Figure 15: Spurious runs in a diagnosis grammar.

Figure 16 :

 16 Figure 16: Type graph of the unfolding of the product.

Figure 17 :

 17 Figure 17: Petri net underlying the unfolding of the product.

  Recalling that aes-morphisms map configurations into configurations (see[START_REF] Baldan | Contextual Petri nets, asymmetric event structures and processes[END_REF] Lemma 3.6]), we have thatC ′ = {π ′ (e 1 ), . . . , π ′ (e n )} is a configuration in E s (O 1 × O 2 )and it is immediate to see that r ′ = π ′ * (r) is a linearisation of C ′ compatible with asymmetric conflict. Since for any occurrence grammar O, we haveConf (O) = Conf (E s (O)), we deduce that C ′ ∈ Conf (O 1 × O 2 ) and r ′ ∈ Ilv(O 1 × O 2 ).Additionally, by commutativity of the diagram above, E s (π i ) * (r ′ ) = δ i * |R (r) = δ * i (r) = r i for i ∈ {1, 2} and thus, since both E s and Ilv when applied to a grammar morphism leave the production mapping unchanged, for i ∈ {1, 2} we haveIlv(π i ) * (r ′ ) = r iComing back to the diagram in the statement of the lemma, by commutativity, for i ∈ {1, 2} we have:

  |G 1 | ⇀ |G 2 | consistent with the typing, i.e., such that t G 1 ≥ t G 2 • f . A typed graph G is called injective if the typing morphism t G is injective. It is called edge-injective if the component on edges of t G is injective. The category of T -typed graphs and partial typed graph morphisms is denoted by T -PGraph.

T , a typed graph G over T is a graph |G|, together with a total morphism t G : |G| → T . A partial morphism between T -typed graphs f : G 1 ⇀ G 2 is a partial graph morphism f :

  order to obtain S . The arrows |G si | → S are obtained as mediating morphisms. and thus it is isomorphic to |G s |. This gives morphism ι s f ′ and shows that |G s | can be obtained from |G s ′ | via pullback-retyping. The arrow ι s f ′ must be unique since it is the mediating morphism of a coproduct.

Since the squares |G si |, |G s ′ |, X i , T ′ are pullbacks, the squares |G si |, X i , S , X 1 ⊎ X 2 are also pullbacks, due to pullback splitting. Hence, since we are working in an extensive category, S must be the coproduct of |G s1 |, |G s2 |

  E s (O 1 × O 2 ) = E s (O 1 ) × E s (O 2 ), i.e., E s (O 1 ) E s (O 1 × O 2 )Define an aes corresponding to the run r, i.e.,R = {e 1 , . . . , e n }, ≤ R , ր R , Λ R , λ R ,where < R is defined by e i < R e i+1 for i ∈ {1, . . . , n -1} and≤ R = (< R ) * . Moreover ր R = < R , Λ R = Λ 1 ∪ Λ 2 andλ R is the restriction of the labelling in Ilv(O 1 ) × Ilv(O 2 ). It is not difficult to see that δ i|R : R → E s (O i ), the restriction of δ i to {e 1 , . . . , e n }, is a well-defined aes morphism for i ∈ {1, 2}. Therefore we deduce the existence of a unique mediating morphism π ′ : R → E s (O 1 × O 2 ) as shown in the diagram below E s (O 1 ) E s (O 1 × O 2 )

	o o	E s (π 1 )	E s (π 2 )	/ / E s (O 2 )
	is a product diagram in AES.

E s (π 1 ) o o E s (π 2 ) / / E s (O 2 ) R δ 1 |R

http://www.graphviz.org/

http://groove.cs.utwente.nl/groove-home/

Acknoledgements. We are very grateful to the anonymous referees for their valuable comments on the preliminary version of the paper.

 [START_REF] Chatain | Models for the supervision of web services orchestration with dynamic changes[END_REF]Supported by RNRT project SWAN, INRIA Sabbatical program, the DFG project SANDS and project AVIAMO of the University of Padova.

Appendix A. Auxiliary Material

In this appendix we first briefly recap the functorial event structure semantics for graph transformation systems, as defined in [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF] and adapt them to the labelled setting. The semantics is given in terms of asymmetric event structures (aes's) [START_REF] Baldan | Contextual Petri nets, asymmetric event structures and processes[END_REF], a generalization of prime event structures where the conflict relation is allowed to be non-symmetric. A functor mapping any occurrence grammar into an aes is defined. The event structure semantics of a graph grammar is obtained by taking the aes associated to the unfolding of the grammar.

Then, using the characterisation of the aes's semantics as a right adjoint, we prove a property of the product of interleaving structures which is fundamental for the theory in the paper.

Appendix A.1. From occurrence grammars to asymmetric event structures

For technical reasons we first introduce pre-asymmetric event structures. Then asymmetric event structures will be defined as special pre-asymmetric event structures satisfying a suitable condition of "saturation".

Definition 23 (asymmetric event structure). A pre-asymmetric event structure (pre-aes) is a tuple

, where E is a set of events, ≤, ր are binary relations on E called causality and asymmetric conflict, respectively, and λ : P → Λ is a labelling over the set of labels Λ, such that:

1. causality ≤ is a partial order and ⌊e⌋ = {e ′ ∈ E | e ′ ≤ e} is finite for all e ∈ E; 2. asymmetric conflict ր satisfies, for all e, e ′ ∈ E:

where, as usual, e < e ′ means e ≤ e ′ and e e ′ .

An asymmetric event structure (aes) is a pre-aes which additionally satisfies:

Definition 24 (category of AESs). Let A 0 and A 1 be two aes's such that Λ 1 ⊆ Λ 0 . An aes-morphism f :

for all e 0 ∈ E 0 , f (e 0 ) ↓ iff λ 0 (e 0 ) ∈ Λ 1 and, in this case, λ 1 ( f (e 0 )) = λ 0 (e 0 ); and for all e 0 , e ′ 0 ∈ E 0 , assuming that f (e 0 ) ↓ and f

) ∧ (e 0 e ′ 0 ) ⇒ e 0 ր 0 e ′ 0 . We denote by AES the category having asymmetric event structures as objects and aes-morphisms as arrows.

The notion of configuration for aes's is completely analogous to that of occurrence grammars.

Definition 25 (configurations).

Let A be an aes. A configuration of A is a set of events C ⊆ E such that 1. for any e ∈ C it holds ⌊e⌋ ⊆ C; 2. ր C , the asymmetric conflict restricted to C, is acyclic and finitary.

Given any occurrence grammar, the corresponding asymmetric event structure is readily obtained by taking the production names as events. Causality and asymmetric conflict are the relations defined in Definitions 12 and 13.

Definition 26 (AES for an occurrence grammar).

Let O = T, G s , P, π, Λ, λ be an occurrence grammar. The aes associated to O, denoted E s (O), is the saturation of the pre-aes P, ≤, ր, Λ, λ , with ≤ and ր as in Definitions 12 and 13.

The above construction naturally gives rise to a functor, which is a right adjoint. The following theorem is adapted from a result of [START_REF] Baldan | Unfolding semantics of graph transformation[END_REF] which can straightforwardly be extended to labelled grammar morphisms.

Theorem 3 (coreflection).

For any occurrence grammar morphism h : O 0 → O 1 let E s (h)(q) = h P (q) if h P (q) ∅ and E s (h)(q) ↑, otherwise. Then E s : OGG → AES is a well-defined functor, which is a right adjoint.

As a right adjoint E s preserves limits, specifically it preserves products. Then the mediating morphism δ is a projection which is total on events.

Appendix A.2. A property of the product of interleaving structures

Ilv(O 1 )

Ilv(π 1 )


Brice Beltran

Mohamed Benbouzid

Tarek Ahmed-Ali

Hervé Mangel

DFIG-Based Wind Turbine Robust Control Using High-Order Sliding Modes and a High Gain Observer

Keywords: Wind turbine (WT), Doubly-Fed Induction Generator (DFIG), high gain observer, high-order sliding mode

This paper deals with the power generation control in variable speed wind turbines. In this context, a control strategy is proposed to ensure power extraction optimization of a DFIGbased wind turbine. The proposed control strategy combines an MPPT using a high gain observer and second-order sliding mode for the DFIG control. This strategy presents attractive features such as chattering-free behavior, finite reaching time, robustness and unmodeled dynamics (generator and turbine). The overall strategy has been validated on a 1.5-MW three-blade wind turbine using the NREL wind turbine simulator FAST.

I. Introduction

Variable speed wind turbines are continuously increasing their market share, since it is possible to track the changes in wind speed by adapting shaft speed and thus maintaining optimal power generation. The more variable speed wind turbines are investigated, the more it becomes obvious that their behavior is significantly affected by the used control strategy. Typically, they use aerodynamic controls in combination with power electronics to regulate torque, speed, and power. The aerodynamic control systems, usually variable-pitch blades or trailing-edge devices, are expensive and complex, especially when the turbines are larger. This situation provides a motivation to consider alternative control approaches and to introduce more intelligence [1].

Therefore, this paper deals with power generation control in variable speed wind turbines. A control strategy is proposed to ensure power extraction optimization and reduce mechanical stresses in the drive train of a DFIGbased wind turbine. The proposed control strategy combines an MPPT using a high gain observer and second-order sliding mode for the DFIG control. This strategy presents attractive features such as chattering-free behavior, finite reaching time, robustness and unmodeled dynamics (generator and turbine).

The overall control strategy, illustrated by Fig. 1, has been validated on a 1.5-MW three-blade wind turbine using the NREL wind turbine simulator FAST.

II. Wind Turbine Modeling

The global scheme for a grid-connected wind turbine is given in Fig. 2. The wind turbine modeling is inspired from [START_REF] Beltran | High-order sliding mode control of variable speed wind turbines[END_REF]. In the following, the wind turbine components models are briefly described.

II.1. Turbine Model

In this case, the aerodynamic power P a captured by the wind turbine is given by

  23 1 2 ap P R C v    (1)
where Normally, a variable speed wind turbine follows the C pmax to capture the maximum power up to the rated speed by varying the rotor speed to keep the system at  opt . Then it operates at the rated power with power regulation during high wind periods by active control of the blade pitch angle or passive regulation based on aerodynamic stall.

R v   (2)
The rotor power (aerodynamic power) is also defined by aa PT  [START_REF] Amirat | The state of the art of generators for wind energy conversion systems[END_REF] According to [START_REF] Beltran | High-order sliding mode control of variable speed wind turbines[END_REF], the following simplified model is adopted for the turbine (drive train) for control purposes.

ag J T K T       (4)

II.2. Generator Model

The WT adopted generator is the DFIG. DFIG-based WT will offer several advantages including variable speed operation (±33% around the synchronous speed), and four-quadrant active and reactive power capabilities. Such system also results in lower converter costs (typically 25% of total system power) and lower power losses compared to a system based on a fully fed synchronous generator with full-rated converter. Moreover, the generator is robust and requires little maintenance [START_REF] Amirat | The state of the art of generators for wind energy conversion systems[END_REF][START_REF] Müller | Doubly fed induction generator systems[END_REF].

The control system is usually defined in the synchronous d-q frame fixed to either the stator voltage or the stator flux. For the proposed control strategy, the generator dynamic model written in a synchronously rotating frame d-q is given by ( 5).

 

d V R I dt d V R I dt d V R I dt d V R I dt L I M I L I M I L I M I L I M I T p M I I I I                                                            (5)
For simplification purposes, the q-axis is aligned with the stator voltage and the stator resistance is neglected [START_REF] Müller | Doubly fed induction generator systems[END_REF]. These will lead to (6).

dI d M v R I s L I dt L L dt dI M v R I s L I s dt L L M T p I L                                            (6)

III. The MPPT Strategy

III.1. Problem Formulation

The reference torque of the MPPT block must address two problems: the captured power maximization and be driven according to the three fundamental operating regions illustrated by Fig. 3.

In practice, there are two possible regions of turbine operation, namely the high-and low-speed regions. High speed operation (III) is frequently bounded by the speed limit of the machine. Conversely, regulation in the lowspeed region (II) is usually not restricted by speed constraints. However, the system has nonlinear nonminimum phase dynamics in this region. This adverse behavior is an obstacle to perform the regulation task [START_REF] Senjyu | Output power leveling of wind turbine Generator for all operating regions by pitch angle control[END_REF].

In region II, the control objective is to optimize the capture wind energy by tracking the optimal torque T opt .

The standard strategy neglect the dynamic of the drive train, which means that the aerodynamic torque is supposed to be equal to the generator torque. It is obvious that in many cases, and especially for turbulent winds, this assumption will not be realistic. The proposed control strategy relies then on the aerodynamic torque estimation using a high gain observer [START_REF] Farza | Observer design for a class of MIMO nonlinear systems[END_REF][START_REF] Beltran | A combined high gain observer and high-order sliding mode controller for a DFIG-based wind turbine[END_REF]. This estimate is then used to derive a high-order sliding mode controller that ensures T opt tracking in finite time.

III.2. High Gain Observer

A high gain observer will therefore be used to estimate the aerodynamic torque. A key feature of a high gain observer is that it will reduce the chattering induced by a sliding mode observer [START_REF] Farza | Observer design for a class of MIMO nonlinear systems[END_REF].

From (4), we have

a em TT K J J J       (8)
The following notations are introduced.

1 2 a x T x J        (9)
Thus we have [START_REF] Skander-Mustapha | Comparative analysis of control strategies for DFIG based wind system under small grid faults[END_REF] or in matrix form

1 2 1 2 () em T K x x x x JJ x f t            
( , ) ( ) x A x x u t y C x           where   1 01 00 10 ( , ) 0 0 () () A C K x u xu J t ft                              .
A candidate observer could be [START_REF] Farza | Observer design for a class of MIMO nonlinear systems[END_REF] 11 ˆˆˆ( , ) ( )

T x Ax x u S C C x x          (11)
Let us define

() x x x     then   1 ( ) ( ) ( ) ( ) T x A S C C x x x t               (13) Consider the quadratic function T V x S x  (14) then   2 2 ( ) ( ) 2 ( ) T T T T V xS x V V x C C x x S x x x S t                          Therefore   m ax ( ) ( ) 2 ( ) () xx V V x S t                    (15)
We can assume that (triangular structure and the Lipschitz assumption on φ) A practical estimate of the aerodynamic torque is then obtained as M θ decreases when θ increases. The asymptotic estimation error can be made as small as desired by choosing high enough values of θ. However, very large values of θ are to be avoided in practice since the estimator may become noise sensitive. Now, the control objective can be formulated by the following tracking errors

  ( ) ( ) () x x x ft              with K J  It comes that 2 m ax m ax 2 ( ) 2 ( ) V V x S x S            then 12 V V c V c V         with m ax 1 m in m ax 2 m in () 2 () () 2 () S c S S c S              Now taking     01 m ax m in 1 m ax m in 1 m ax 1, ( )
() 2
() 2 () c S S c S M Sc                          and  >  0 ,
T opt a e T T  (18)
where T a is observed. Then we will have

  2 T opt a t g a e k T K T T         (19)
If we define the following functions

  2 2 opt opt a t a Fk G k T K T             ( 20
)
then

Tg e F T G       (21)
Let us consider the following observer based on the supertwisting algorithm [START_REF] Beltran | High-order sliding mode control of variable speed wind turbines[END_REF], [START_REF] Levant | Integral high-order sliding modes[END_REF].

   

The gains B 1 and B 2 are chosen as

    2 1 2 1 1 2 2 2 11 2 4 0 m M m mM B A B A G F                              (23)
Thus we will guaranty the convergence of e T to 0 in a finite time t c . The aerodynamic torque estimation is then deduced.

T a = T opt , t > t c . ( 24
)
The above proposed high gain observer principal is illustrated by the block diagram in Fig. 4.

IV. Control of the DFIG-Based Wind Turbine

The DFIG-based WT control objective is to optimize the extracted power by tracking the optimal torque T opt [START_REF] Beltran | A combined high gain observer and high-order sliding mode controller for a DFIG-based wind turbine[END_REF]. The control is a compromise between conversion efficiency and torque oscillation smoothing [START_REF] Heidari | Lyapunov based self-tuning control of wind energy conversion system[END_REF][START_REF] Skander-Mustapha | Comparative analysis of control strategies for DFIG based wind system under small grid faults[END_REF][START_REF] De Battista | Sliding mode control of wind energy systems with DOIG-power efficiency and torsional dynamics optimization[END_REF].

The reactive power is expressed as follows.

d M e V R I g L I I L L dt V R I g L i M e p T M g LL L                                                   (29)
If we define the functions G 1 and G 2 as follows.

d M G g L I I L L dt MM G p g L I g T L L L                                  
Thus we have

V G R I LL MM e p V G p R I L L L L                          (30)
Now, lets us consider the following high-order sliding mode controller based on the supertwisting algorithm [START_REF] Beltran | High-order sliding mode control of variable speed wind turbines[END_REF], [START_REF] Skander-Mustapha | Comparative analysis of control strategies for DFIG based wind system under small grid faults[END_REF].

                        (31)
Where the constants B 1 , B 2 , B 3 , B 4 ,  1 , and  2 satisfy (32).

Thus, we can assert that there exist finite times t Tem and t Ird leading to (33). This means that the control objective is achieved.

        11
s sr r r r G B M B p B LL LB G B BB L LB                                    (32) _ , , rd em rd ref rd I ref em T I I t t T T t t            (33)

V. Validation Results with FAST

The proposed SOSM control strategy has been tested for validation using the NREL FAST code [13]. An interface has been developed between FAST and Matlab-Simulink  enabling users to implement advanced turbine controls in Simulink convenient block diagram form.

Numerical validations, using FAST with Matlab-Simulink  have been carried out on the NREL WP 1.5-MW (Fig. 5) wind turbine using turbulent FAST wind data shown by Fig. 6 [START_REF] Hand | Advanced control design and field testing for wind turbines at the National Renewable Energy Laboratory[END_REF]. The wind turbine, the DFIG ratings, and control parameters are given in the Appendix.

The observer validation is clearly illustrated by Fig. 7. Indeed, the aerodynamic torque tracks efficiently the optimal torque. As shown in Figs. 8 and9, very good tracking performances are achieved in terms of DFIG rotor current and WT torque with respect to wind fluctuations. The proposed control strategy does not induce increased mechanical stress as there are no strong torque variations. The proposed control strategy that combines a high gain observer-based MPPT and a second-order sliding mode has been compared to classical techniques used in wind power industry. The first one is that using the active power as reference and leading to the following control reference [START_REF] Poitiers | Advanced control of a doubly-fed induction generator for wind energy conversion[END_REF]. This approach supposes that the active power is equal to the generator power. This approximation drives a difference between the desired torque and the generated one (Fig. 10).

The second classical approach is the one using the following reference [START_REF] Cardenas | Sensorless vector control of induction machines for variable-speed wind energy applications[END_REF]. In this case, bad tracking performances are also achieved (Fig. 11).

VI. Conclusion

This paper dealt with a second-order sliding mode control of a doubly-fed induction-based wind turbine combined with a high gain observer-based MPPT. The proposed control strategy has been tested and validated using the NREL FAST simulator on a 1.5-MW wind turbine.

=

  Leakage coefficient,  = 1 -M 2 /L s L r ; θ r = Rotor position; ω r (ω s )= Angular speed (synchronous speed); s = Slip; p = Pole pair number.

Fig. 1 .Fig. 2 .

 12 Fig. 1. The proposed control structure.

Fig. 3 .

 3 Fig. 3. Steady-state power curves.

  where

  Let S be the unique solution of the algebraic Lyapunov equation0 TT S A S S A C C    

Fig. 4 .

 4 Fig. 4. High gain observer principle.Adapting (25) to our hypotheses, it comes then

Fig. 5 .Fig. 6 .Fig. 7 .

 567 Fig. 5. 1.5-MW wind turbine illustration.

Fig. 8 .

 8 Fig. 8. Torque tracking performance: Reference (blue) and real (green).

Fig. 9 .

 9 Fig. 9. Current Ird tracking performance:Reference (blue) and real (green).

Fig. 10 .

 10 Fig. 10. Torque: Reference (blue) and real (green).

Fig. 11 .

 11 Fig. 11. Torque: Reference (blue) and real (green).

Appendix