G Michele Pinna
email: gmpinna@unica.it

Eric Fabre

Spreading nets: a uniform approach to unfoldings

Keywords: Multi-clock nets, unfolding of nets, spreading of nets

This paper is devoted to the study of the notion of spread net. A spread net is a (safe) Petri nets where each place is annotated with some information, taken from a suitable information domain, about how such place can get marked. Spread nets generalize various kinds of nets used to represent the non sequential behaviours of a safe net, like unfoldings, merged processes or trellis processes. The spreading of a net may allow to produce more compact (partially unfolded) nets representing the non sequential behaviour of a net, depending on the chosen information domain. In particular in a spread net it is possible to merge not only conflicting runs, but also to partially refold time, as spread nets allow loops in time.

Introduction

One of the most popular motto in Petri nets is that "the semantics of a net is a net" [START_REF] Smith | The semantics of a net is a net[END_REF]: the executions of a net N are represented with the aid of another net and a suitable mapping relating the semantic net to N . Along this line of thought non-sequential processes have been proposed ( [START_REF] Goltz | The non-sequential behavior of Petri nets[END_REF]), where the causal dependencies among the transitions of a net are faithfully represented. Non-sequential processes are able not only to represent causality, but also the concurrency present in a single computation. They cannot however represent conflicts. To model all the possible non sequential executions of a net, the notion of unfolding has been proposed in [START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part 1[END_REF] and further investigated in [START_REF] Winskel | Event Structures[END_REF] and [START_REF] Engelfriet | Branching processes of Petri nets[END_REF]. The idea is to represent conflicts as branching alternatives (whence the name of Branching Processes, that are essentially unfoldings [START_REF] Engelfriet | Branching processes of Petri nets[END_REF]).

Though unfoldings were introduced to represent the non sequential behaviors of (safe) Petri nets, their main application originated in the fact that they offered new techniques for the verification of concurrent systems: the use of partial orders allows one to have more compact representations of a nets behaviors with a gain in how the verification can be performed. Still, the data structure obtained by unfolding is in general infinite or too large. One of the first attempts to overcome this problem was to turn non sequential processes into an algebra, with a parallel composition and a suitable notion of concatenation ( [START_REF] Degano | Axiomatizing net computations and processes[END_REF] and further investigated in [START_REF] Degano | Axiomatizing the algebra of net computations and processes[END_REF]). An orthogonal approach has been the one pursued in [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits[END_REF] where the unfolding is restricted to a finite complete prefix in a way that still allows one to infer all information needed to represent all possible computations of a safe net. Another way to address this problem is to define an equivalence on some behaviors of (safe) Petri nets, which implies that the data structure adopted cannot be any longer the one devised for unfoldings or prefixes. The notion of unravel net introduced in [START_REF] Casu | Petri nets and dynamic causality for service-oriented computations[END_REF] and [START_REF] Casu | Merging relations: A way to compact Petri Nets' behaviors uniformly[END_REF] goes in this direction requiring that each execution is a partial order, but the overall structure gathering all executions does not need to be a partial order. Focussing on the dependencies to obtain a more compact data structure implies that the net representing more concisely the non sequential behaviours has to fulfill some properties that are posed on the net as a whole, e.g. some subnets should have certain characteristics like the unravel nets, or the net should be acyclic. Overcoming the request that (at least locally) the behavior should be represented using a partial order has led to the introduction of a reveal relation playing the role of causality [START_REF] Balaguer | Building occurrence nets from reveals relations[END_REF][START_REF] Haar | Computing the reveals relation in occurrence nets[END_REF]. There it is shown how to relate occurrence nets and reveal relations. Still the more compact data structure has its origin in the partial ordering representing the dependencies in the net, hence it is based on the unfolding construction.

The approaches limiting the size of the data structure having origin in the work regarding prefixes ( [START_REF] Mcmillan | Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits[END_REF] and further investigated in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] and [START_REF] Khomenko | Canonical prefixes of Petri net unfoldings[END_REF]) focus mainly on the time dimension. Still the resulting data structure may be unnecessarily big, and in the last decade, merged processes [START_REF] Khomenko | Merged Processes: a new condensed representation of Petri net behaviour[END_REF] and the closely related trellis processes [START_REF] Fabre | Trellis processes: A compact representation for runs of concurrent systems[END_REF] were introduced to limit the expansion of the structure due to conflicts. The idea consists in merging runs that result from different choices but produce identical resources, where identical may mean that the same resource is produced by several alternative activities at the same time (trellis processes) or the i-th occurrence of the same resource is produced by again alternative activities (merged processes). These two approaches are quite successful to represent in a compact manner a sufficient set of runs of a concurrent system. However, they rely on distinct treatments for time and for conflicts.

The problem of representing the non sequential executions of a net, possibly in a more compact way, can be faced from another point of view. Rather than requiring that the semantic net representing the non sequential executions of a net obeys to some structural requirements, we define a net where the places are annotated with pieces of information. The properties that the data structure representing the behaviours has to fulfill are conveyed through these pieces of information. One of the advantages of this shift in perspective is that it may relay or derive from local update rules, so we do not necessarily have to count on requirements like the existence of a partial order among places and transitions or similar ones.

Spread nets ( [START_REF] Fabre | Toward a uniform approach to the unfolding of nets[END_REF]) are nets where each place is annotated, and the annotation depends on the transitions putting a token in that place and on the annotations of the places feeding these transitions. In this way it is possible to keep track of the way that place is reached (obtained) in the executions represented by that net. Based on this notion, we continue the line of research initiated in [START_REF] Fabre | Toward a uniform approach to the unfolding of nets[END_REF] for multi-clock nets, and we show how the notion of spreading of nets can be seen as a unified approach to Petri net unfolding, also for nets that are not multi-clock nets. While trellises and merged processes had abandoned the requirement that nodes should not be in self-conflict in the unfolding, the main move here is to abandon also the requirement that the unfolding should be a (directed) acyclic graph. In other words, we consider structures that partially unfold time, and then loop back to previously met resources. This parametric approach is flexible enough to partially or totally expand both conflicts and time, thus capturing previous constructions in a unified setting. It also assigns an equal treatment to time and conflicts. Places are annotated by values from an information domain. The notion of information domain associated to a spread net plays a major role. Indeed, the mechanism guiding the spreading of a net is encoded in the information domain. We illustrate the intuition with a very simple example, which will allow us to stress how the pieces of information are gathered.

N N

Consider the net N above (left), with a single place p and two transitions a and b. The net N on the left, which the initial part of an unravel net, can be considered the representation of the non sequential behaviour of the net on the left where the various computations are made equivalent provided that each firing of a has to be considered equivalent to each firing of b. This equivalence allows to merge the transitions corresponding to the i-th firing of a or b in the net on the left. The main difference with respect to other approaches is that now the places in the net on the right are annotated with a piece of information (in this case it is an equivalence class). As it emerges from this example, the properties one is interested in are coded in the information domains, and in this simple example the property one might be interested in could be that the same number of transitions is executed, regardless if it was a or b. Thus, for instance, in N the place p 2 is annotated with the equivalence class [a] ∼ which contains a and b, or the place p 3 is annotated with the equivalence class [aa] ∼ which contains aa, ab, ba and bb. This approach extends to more complex ways of representing behaviours thanks to the greater freedom for defining equivalences on the computations. This may allow one to ignore some conflicts but also to refold time (possibly local one), or to abstract only parts of a computation that are considered not relevant. The structure obtained by spreading a net with respect to an information domain can be used to check properties of the system more efficiently, as the spreading may give a more compact structure with respect to previous approaches to represent the executions of a net, and to focus only on events of interest. The annotated places of a reachable marking of a spread net represent the state of the system, and they fully describe all the possible computations leading to that state. All these computations are to be considered equivalent with respect to their common future. The information domain depends mainly on what one would like to consider equivalent in the various activities of the system, i.e. indistinguishable from the observations, and this may involve not only conflicts of abstraction but also the folding of executions, which account to say that we can fold time. The semantics of the spread net is reflected in the information domain. The spread net is dependent on it, and in this paper we specify how the domains can be constructed.

We focus mainly on multi-clock nets that are composed of simpler subsystems: basically finite state automata. These automata synchronize on common transitions (labels). The resulting net gives us the basic ingredients we want to elaborate on: causality, that coincides with local time in each component, and conflicts, which are local to a component as well. Each synchronization among finite state automata determines the expansion of conflicts and causalities to all the components of the system. The information domains for these kind of nets (multi-clock nets) are called ticking domains and have a particular structure which depends on the structure of a multi-clock net, and that will be also investigated in this paper.

However the notion of spread net generalizes beyond to multi-clock nets. We introduce it for any kind of net and then we will study how this notion specializes when considering multi-clock nets. The purpose of doing so is to stress that in many case the nets we are interested in may be somehow decomposed in simpler parts, and many times the pieces of information associated to the places in the spreadings may be somehow composed.

This paper is a revised and extended version of [START_REF] Fabre | Toward a uniform approach to the unfolding of nets[END_REF]. Whereas in [START_REF] Fabre | Toward a uniform approach to the unfolding of nets[END_REF] only multi-clock nets were considered, here we generalize the notion of spread net to any kind of net. More importantly we show that classical unfoldings can be seen as spread nets, by constructing adequate information domains. This points out the precise relationship among certain information domains and the structure of the resulting spread net. For instance a place of an occurrence net is naturally annotated with the local configuration corresponding to the transition which is in the preset of that place, or in the case of an unravel net, the set of the local configurations. The close relationship among the structure of the spread net is even more evident in the case the unfoldings are originated by a multi-clock net, and we give here a more detailed account on how the information domains are obtained in this case. Furthermore we give more precise criteria on how to construct the ticking domains in the case of multi-clock nets and we discuss various cases of spreading.

Structure of the paper:

The paper is organized as follows. In Section 2 we review Petri nets, and in Section 3 we introduce the notion of information domain that will be used to annotate nets, obtaining spread nets, which are introduced in Section 4. In the Section 4 we also show how various kinds of nets, like 1-occurrence, occurrence and unravel nets can be considered as spread nets over suitable domains, assessing that the notion of spread net is the appropriate one to capture and generalize some of the various unfolding notions presented in literature. In Section 5 we review the notion of multi-clock nets (5.1) and, in sub-section 5.2, the notion of ticking domain, i.e. the domains tailored for multi-clock nets, is introduced and discussed. Section 6 shows that previous unfolding related constructions for multi-clock nets can be seen as spread nets, focussing on the proper ticking domain characterizing them. In Section 7 we generalize and specialize the notion of ticking domain for a multi-clock net and then we present an algorithm to spread it. We also show that the spreading of a multi-clock net determined by this algorithm is, under some reasonable assumptions, the best construction, in the sense that any other spread net with the same ticking domain is part of the spread net produced by the algorithm. Section 8 illustrates how some useful ticking domains can effectively be constructed. Some conclusions and directions for future research end the paper.

Nets

Notation. Given a set A, by 2 A we denote the set of all subsets of A and by 2 A fin the set of finite subsets of A. With A n we denote the product of A n times. With N we denote the set of natural numbers.

Let A be a set, a multiset of A is a function f : A → N. The set of multisets of A is denoted by µA. The usual operations and relations on multisets, like multiset union or multiset inclusions, are defined in the standard way. A multiset f ∈ µA is a set whenever, ∀a ∈ A, f(a) ≤ 1, and in the case a multiset f is a set, we often write a ∈ f instead of f(a) = 1. Obviously any subset of A can be seen as a multiset of A.

Given a multiset f ∈ µA, [[f]] indicates the set {a ∈ A | f(a) = 0} (thus, with abuse of notation, a multiset f is a set when [[f]] = f).
The cardinality of a (multi)set f is denoted by |f|, and it is defined as a∈A f(a). When no confusion arises we denote the multiset f ∈ µA as a∈A f(a) • a.

Given a finite alphabet A (a finite set of symbols), A * denotes as usual the set of words on A, and ε denotes the empty word. The length of a word w ∈ A * is defined as usual and, with abuse of notation, it is denoted by |w|. Given a word w ∈ A * and a subset X of the alphabet, proj (w, X) is the word obtained by deleting all occurrences of symbols not belonging to X. More formally, for a fixed X, proj (ε,

X) = ε, proj (a • w, X) = a • proj (w, X) if a ∈ X and proj (a • w, X) = proj (w, X) otherwise.
Given a word w ∈ A * , {|w|} denotes the set of all symbols of the alphabet A appearing in w, which is defined inductively as {|ε|} = ∅ and {|a • w|} = {a} ∪ {|w|}.

Nets. We review the notion of Petri net and of token game and then we recall some further notions we will use in the following. Definition 2.1. A Petri net is a tuple N = P, T, F, m 0 , where P is a set of places and T is a set of transitions (with P ∩ T = ∅), F ⊆ (P × T ) ∪ (T × P ) is the flow relation and m 0 : P → N is called the initial marking.

A net P, T, F, m is as usual graphically represented as a bipartite directed graph where the nodes are the places and the transitions, and where an arc connects a place p to a transition t iff (p, t) ∈ F and an arc connects a transition t to a place p iff (t, p) ∈ F .

Given x ∈ T ∪ P , with • x we denote the set {y | (y, x) ∈ F } and with x • the one {y | (x, y) ∈ F }. • x and x • are called the preset and postset respectively of x. Observe that • x and x • may be considered as multisets (over places or transitions, depending on x) and this will be handy in the following.

A transition t is enabled at a marking m if m contains the preset of t, thus if • t ≤ m. If a transition t is enabled at a marking m it may fire yielding a new marking defined by m = m + • t -t • . The firing of t at m giving m is denoted with m [t m . We will always consider nets where ∀t ∈ T . • t and t • are not empty. This implies that no transition t can be executed spontaneously ( • t = ∅) and that the execution of a transition has an effect (t • = ∅), though not necessarily observable (e.g. • t = t • , the firing of t at a given marking cannot be observed only looking at the markings).

Given a marking m, the firing sequence (fs) starting at m of the net N = P, T, F, m 0 , is defined as usually:

1. m is a firing sequence (the empty one, where no transition is fired), and

2. if m [t 1 m 1 • • • m n-1 [t n m n is a firing sequence and m n [t m then also m [t 1 m 1 • • • m n-1 [t n m n [t m
is a firing sequence.

The set of firing sequences of a net N starting at a marking m is denoted by FS N m and it is ranged over by σ. We may omit mentioning the superscript denoting the net when it is clear from the context, and the initial marking m when it coincides with the initial marking of the net.

Given

fs σ = m [t 1 • • • [t n m n , start(σ)
denotes the initial marking m and lead (σ) denotes the marking m n , finally run(σ) denotes the word t 1 . . . t n . Given a net N = P, T, F, m 0 , a marking m is reachable iff there exists a fs σ ∈ FS N m0 such that lead (σ) = m. The set of reachable markings of

N is M N = {lead (σ) | σ ∈ FS N m0 }.
Together with the notion of reachable marking we introduce also the one of state of a net which focuses, for each firing sequence, on the executed transitions rather than on the reached marking. Let σ ∈ FS N m be a firing sequence, we define the multiset st(σ) of transitions as

st(σ) = ∅ if σ = m and st(σ) = t + st(σ ) if σ = m [t σ
, and we call it state of N . The set of states of the net N is the set

St(N ) = {st(σ) | σ ∈ FS N m0 }. A net N = P, T, F,
m 0 is acyclic whenever the transitive and reflexive closure of F is a partial order over P ∪ T . A net N = P, T, F, m 0 is live iff for each transition t and each marking m ∈ M N there exists a firing sequence σ ∈ FS N m such that σ [t . We now recall the notion of safe net. Definition 2.2. A Petri net N = P, T, F, m 0 is said to be safe iff each marking m ∈ M N is a set.

Though safeness is a semantics notion as it is connected with the reachable markings of a net, it can be enforced structurally by adding suitable places (the so called complementary places). In this paper we consider safe nets only, and thus we will often identify a marking m with the set [[m]] and write p ∈ m when m(p) = 1 and m will be considered as a set.

Nets morphisms. Let N = P, T, F, m 0 and N = P , T , F , m 0 be two safe nets, a morphism of safe nets ( [START_REF] Winskel | Event Structures[END_REF]) is a pair (f P , f T ) where f P is a relation between P and P , and f T is a partial mapping from T to T such that 1. f P (m 0 ) = m 0 and for each p ∈ m 0 there exists a unique p ∈ m 0 such that p f P p, 2. if f T (t) = t then the restrictions f op P : • t → • t and f op P : t • → t • are total mappings, and 3. if (p, p ) ∈ f P then the restrictions f T : • p → • p and f T : p • → p • are total mappings. where f op P denotes the opposite relation of f P . A morphism f : N → N preserves the initial marking and reachable markings as well, as it maps a firing sequence of N to a firing sequence of N . When it is clear from the context we may omit the subscript of (f P , f T ) using f instead.

Labeled nets. Let us fix an alphabet Lab of labels. Definition 2.3. A labeled net over a set of label Lab is a tuple N = P, T, F, m 0 , where • P, T, F, m 0 is a net, and

• : T → Lab is a total mapping.
Given a firing sequence σ ∈ FS N m0 of the labeled net N , with tr(σ) we denote the word (run(σ)), often called trace. The set of traces of a labeled net N is denoted with Tr(N ). Observe that this set is never empty, as at least the empty word ε belongs to it, which corresponds to the firing sequence m 0 . The traces here are not the so called Mazurkievich-traces ( [START_REF] Mazurkiewicz | Trace theory[END_REF]), as each of them represents the sequence of labels of a single sequential execution of the net.

The notion of net morphism is adapted to labeled nets in the obvious way: let (N, ) be a labeled safe net over Lab and (N , ) be a labeled safe net over Lab , a morphism is the pair (f, l) where f : N → N is a net morphism and l : Lab → Lab is a partial labeling morphisms such that l is defined on (T ) and (f T (t)) = l( (t)).

As each safe net N = P, T, F, m 0 can be seen as a labeled net on the set of labels T by taking as the identity mapping, we will add such labeling mapping when needed.

Information domains

We introduce now the notion of information domain over a set A. This notion is different from the classical notion of Scott domain as defined in the literature (for instance as in [START_REF] Abramsky | Domain theory[END_REF] and references therein, or [START_REF] Gierz | Encyclopedia of Mathemtics and its Applications[END_REF]), but we prefer to use the term domain as it conveys a similar idea, namely the one that information domains contain pieces of information about a system. An information domain will be a non empty set of elements defined from A (e.g. subsets of A, or languages in A * ), and we will use the elements of a domain to annotate the places of a net. Each element of the information domain will deliver some information about how the place can be marked, and this piece of information will depend on what one whishes to characterize and observe. We support this idea with some simple examples, which will be formalized later.

Example 3.1. Let us fix a set A.

• An information domain can be composed by just one element, say the empty set. This information domain conveys the idea that it is irrelevant to observe or characterize how a given place is marked.

• An information domain can be the set of words A * . The annotation of a place with a word w in A * may characterize the fact that some transitions have been executed to mark that place. w ∈ A * may stress that some transitions are executed more than once top produce that place and that the ordering in the execution is relevant.

• An information domain can be the set of finite subsets of A, namely 2 A fin . In this case we could consider the annotation of a place as the set of transitions executed, regardless the multiplicity or the ordering.

The elements of an information domain are in any case related to a predefined set A, and we indicate this fact by saying that the elements are built over A.

The elements of an information domain can be combined. To combine the elements we define some partial operations. The partial operations take pieces of informations (a multiset of elements of the information domain) and return (a multiset of) new pieces of information. The operations are partial as we have have to state when some pieces of information are coherent, and in general it is not the case that all the pieces of information can be combined together. We define also an updating mapping which takes an element of the information domain and adds to it the piece of information delivered by an element in A. The updating mapping is used to calculate new elements starting from an element of the information domain and an element of the set A. Summing up, we equip information domains with two kind of internal operations: one kind to combine elements and the other to update. They are partial operations: they applies to coherent elements.

Formally: Definition 3.2. Let A be a set, an information domain D (over A) is the 4-tuple (A, Op, τ, A) where 1. A is a non empty set of elements with a distinguished element denoted with 0, that will be ranged over by A, which we call the support,

2.

Op is a non-empty set of partial operations op i : µA

2 A such that, for each X ∈ µA such that |X| = i, if op i (X) is defined then op i (X) = ∅, and 3. τ : A × A → A is an updating mapping.
Given A, an information domain D is basically a partial algebra where A plays the role of the generators of the elements of the algebra. Given op i ∈ Op, i denotes the cardinality of the multiset on A that the partial operation op i receives as argument. The partial operation, when defined, combines the i elements and produce a non empty set of elements of A. The operations op i will be detailed when we introduce the specific information domains, the purpose of each operation is to combine i elements in A, that are assumed to be coherent, and produce elements that can be used by the update mapping. Hence the minimal requirement that when it is defined then the result is a non empty subset of elements of A. The set Op is required to be non empty. The final ingredient of an information domain is the updating mapping that, given an element of A and one of A, produces a new piece of information possibly using the elements in A. We often refer to the support of an information domain as the information domain itself.

We illustrate these operations with some simple examples.

Example 3.3. Given a set A, an information domain over A could be composed by setting A = 2 A fin where each element is a finite subset of A, with ∅ as the distinguished element 0. Each operation op i ∈ Op takes a multiset X ∈ µ2 A fin of size i and returns the union of the elements in A ∈ 2 A fin for which X(A) = 0, i.e. op i (X) = {A | X(A) = 0}. The updating mapping just adds one a ∈ A to an element A ∈ 2 A fin , i.e. the updating mapping returns the union of the set in A ∈ 2 A fin with the singleton {a} ∈ 2 A fin .

Example 3.4. Given a finite set A, let A = {L | L ⊆ A * } be the information domain where each element is a language L ⊆ A * . The 0 could be the language {ε} (it is not the unique choice, for instance the 0 could also be A * ). Each operation op i ∈ Op takes a multiset of languages X of size i and returns a new set of languages, where each of them is obtained combining the various languages in X by some language operations. For instance, a partial operation op i can take a set of languages {L 1 , . . . , L i } and return the set of languages {L k ∩ L l | k = l}, or a set of languages {L 1 , . . . , L i } such that ∀k, l ∈ {1, . . . , i} either L k ⊆ L l or L l ⊆ L k , and return the maximal one. For the updating mapping, we can consider the mapping that takes L ∈ A and a ∈ A and returns the language L • a.

As it is, the notion of information domain is rather abstract. We will show how to construct suitable information domains that should convey the idea that places of a net representing the behaviour of a system can be enriched with information that characterizes precisely that behaviour. In some cases the elements of (the support of) an information domain will turn out to be a partial order, but the unique requirement that we make is that it is non empty, as it should contain the 0, representing the minimal amount of information available.

We are especially interested in information domains where each operation in Op satisfies some further constraint. Definition 3.5. Let D = (A, Op, τ, A) be an information domain over A. We say that D is regular whenever for each op i ∈ Op and for each X ∈ µA, if op i (X) is defined then op i (X) is a singleton.

An information domain is regular iff each partial operation op i can be seen as partial mapping op i : µA A. The information domain in Example 3.3 is regular as each operation returns just one element. This is not necessarily true in Example 3.4.

Example 3.6. Given A, let A = {0}. A contains just one element, the 0. Then D ⊥ = (A, Op, τ, Lab) where A = {0}, Op = {op i : µA A} such that op i (X) = 0 for X(0) = i, and τ (0, a) = 0 for each a ∈ A is an information domain over A. The D ⊥ is regular.

Example 3.7. Let A = {0, α, β} and let op 1 (0) = {α}, op 1 (α) = {α, β} and op 1 (β) = {α}. This information domain, regardless of the updating mapping, is not regular, as op 1 (α) returns a set which is not a singleton.

Regularity is not the unique interesting property of an information domain, we would have also information domains that are revealing, where revealing means that the update mapping produces a new element, and the pieces of information are updated. Definition 3.8. Let D = (A, Op, τ, A) be an information domain over A. We say that D is revealing whenever A = {0} and there exists an element A ∈ A and an element a ∈ A such that τ (A, a) = A.

A revealing domain must have a support containing also elements which are not 0 and these elements can be somehow obtained as the result of the update mapping. The information domain D ⊥ is not revealing, whereas the one in Example 3.3 is a revealing one, as we will see in the next section when discussing occurrence nets as spread nets.

Spread nets

In this section we review the notion of spread net and we show that it may be used to describe the true concurrency semantics of a net, as we pointed out in the introduction. The semantics of a Petri net N has been often given in term of another suitable net (following the "motto" the semantics of a net is a net, [START_REF] Smith | The semantics of a net is a net[END_REF]). Each of the various semantics has relied on an appropriate subclass of nets (e.g [START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part 1[END_REF][START_REF] Boudol | Flow Event Structures and Flow Nets[END_REF][START_REF] Goltz | The non-sequential behavior of Petri nets[END_REF][START_REF] Baldan | Contextual Petri nets, asymmetric event structures and processes[END_REF] and [START_REF] Corradini | Domain and event structure semantics for Petri nets with read and inhibitor arcs[END_REF] among many others), and these semantics nets usually defined by some structural characterizations, e.g. they have to be acyclic, or each transition has to fire just once.

The idea behind the notion of spread net is rather simple: the places of the net are annotated with information from a suitable information domain D, and the annotation of each place in the postset of some transition t is related to the annotations of the places in the preset of t using the partial operations op i and the mapping τ . These annotations fully characterize the spread net, as we will see later. Given a multiset f ∈ µA and a mapping g : A → B, with g(f) we denote the multiset in µB defined as a∈A f(a) • g(a). Definition 4.1. Let N = P, T, F, m 0 , be a labeled safe net over Lab, let D = (A, Op, τ, Lab) be an information domain over Lab with 0 ∈ A as distinguished element, and let h : P → A be a total mapping, called the information mapping, such that

1. for each p ∈ m 0 h(p) = 0, 2. for each t ∈ T , op i (h( • t)) is defined, with i = | • t|, 3. for each p ∈ t • , there exists A ∈ op i (h( • t)) such that h(p) = τ (A, (t)), and 4. ∀p ∈ P , ∀t, t ∈ • p. τ (op i (h( • t)), (t)) = τ (op i (h( • t )), (t )).
Assume that for each t ∈ T there exists a σ ∈ FS N such that σ [t . Then N is a spread net with respect to the information domain D over Lab with the information mapping h, and it will be denoted by N D,h .

The new ingredient of a spread net, which is a safe net where each transition can be fired, is the information mapping h. The requirements we put on this mapping are justified as follows:

• condition 1 assures that the piece of information h(p) associated to the initial places is minimal (0), as initial places represent the beginning of a computation and then no information is available,

• conditions 2 and 3 state that the annotation of a place p in the postset of a transition t is obtained by the annotations in the preset t, combined using a partial operation that should be defined on these inputs, using the label (t) of the transition t, conveying the idea that this execution of the transition t adds some information that is gathered in the places in t • , and

• condition 4 ensures that the annotation associated to the place p does not depend on a specific transition in its preset but it is uniform over the various transitions in • p,

For the time being we do not specify the choice of a specific element from op i (h( • t)) in condition 3. Observe that if the information domain is a regular one then the problem of selecting a specific element does not apply. As a consequence of condition 2, op i is assumed to be defined for the set of annotations related to the places in the preset of each transition of the net. We illustrate the idea with a small example, whose purpose is to show how a net can be annotated over an information domain. Each net can be seen as a spread net over the information domain ({0}, Op, τ, Lab) where τ is the mapping returning just 0 and each mapping in Op returns the set containing the unique element of A. Proposition 4.3. Let N = P, T, F, m 0 , be a labeled safe net over the set of labels Lab, let D ⊥ be the information domain over Lab where A = {0}, Op and τ are defined as mappings returning always 0, and let h : P → A be the information mapping defined as h(p) = 0 for each p ∈ P . Then N D ⊥ ,h is a spread net over D ⊥ .

Proof. D ⊥ is a regular domain (see Example 3.6) as for each i we have that op i (X) = 0 with X(0) = i and τ (0, a) = 0 for each a ∈ Lab. The conditions of Definition 4.1 are easily verified: to each place in the initial marking the 0 information is associated, ∀p ∈ P such that • p = ∅ (i.e. p ∈ • t for some t ∈ T ), we have that ∀t ∈ • p, op i (h( • t)) is defined and the result is 0, and finally τ (0, (t)) = 0. This proposition does not contrast the intuition that a spread net should somehow represent a kind of a net semantics, as it simply states that also a trivial semantics is always available, namely the one where no information is provided about the past of a place, hence the net representing the possible behaviours of another one is just the same net.

Definition 4.4. The spread net N D,h over the information domain D is said to be properly spread whenever for some transition t ∈ T there exists a place p ∈ • t and a place p ∈ t • such that h(p) = h(p ).

A spread net is properly spread whenever the annotations of some places in the preset and postset of some transition are different. The intuition behind this notion is again obvious: when the annotations do not change, the spreading itself (the annotations on the places of the net) is not revealing. Definition 4.5. The spread net N D,h is said to be uniformly spread whenever D is a regular domain.

1-Occurrence, occurrence and unravel nets seen as spread nets

To give ground to the notion of spread net, we review briefly some subclasses of nets (among many possible) that have been proposed as the semantics of nets and we see them as suitable spread nets. For each of them we introduce the information domain that establish this connection. The first one captures the idea that in the execution keeping track of dependencies or alternatives is not relevant, thus many computations may be seen as equivalent with respect to dependencies and conflicts; the second captures the opposite idea: dependencies and alternative are to be preserved faithfully, while the third one allows to equate some computations.

The elements of the information domain represent the pieces of information that can be associated to a place p of the net N , namely the piece of information associated to a computation of the net marking the place p. In the remaining of this section, we concentrate on the semantics nets of N .

1-Occurrence nets. A 1-occurrence net, as introduced in [START_REF] Van Glabbeek | Configuration structures, event structures and Petri nets[END_REF], is a (safe) net where each transition t may fire just once. Definition 4.6. A safe Petri net N = P, T, F, m 0 is said an 1-occurrence net if each state in St(N ) is a set.

In an 1-occurrence net all the different ways a place p receives a token have to be considered as equivalent. A suitable information domain is the one where A has just one element, namely the 0. A labeled 1-occurrence net N = P, T, F, m 0 , where is the identity may be seen as a spread net over the information domain D ⊥ over Lab = T stating that the piece of information attached to each place is 0. Proposition 4.7. Let N = P, T, F, m 0 , be an 1-occurrence net where is the identity mapping, and let D T ⊥ = (A, Op, τ, T ) be the information domain where

• A = {0}, with 0 = ∅,
• Op is such that each op i ∈ Op returns always 0 for all X ∈ µA with |X| = i = | • t| for some t ∈ T , and

• h : P → A associates to each place p ∈ P the element 0 ∈ A, i.e. ∀p ∈ P . h(p) = 0.

Then

N D T ⊥ ,h is a spread net over D T ⊥ .
Proof. See Proposition 4.3.

Observe that the 1-occurrence net is not properly spread, and indeed the presence of the information domain does not add any particular value to the main characteristic of the net, namely the fact that each transition is executed just once. The information domain is regular but it is not revealing. We stress here that being an 1-occurrence net does not depend on the chosen information domain, but this information domain is in general the one tailored for this kind of net, where all the computations are considered as equivalent.

Occurrence nets. An occurrence net [START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part 1[END_REF][START_REF] Winskel | Event Structures[END_REF] is a safe net where dependencies and conflicts among transition occurences, called events, can be inferred from the structure of the net itself. The places of an occurrence net are called conditions and its set is denoted as B, whereas the transitions are called events and its set is denoted as E.

Definition 4.9. An occurrence net C = B, E, W, c 0 is an acyclic safe net such that satisfying the following restrictions:

1. ∀b ∈ c 0 , • b = ∅, 2. ∀b ∈ B. ∃b ∈ c 0 such that b W * b, 3. ∀b ∈ B. | • b| ≤ 1 and • b = ∅ implies that b ∈ c 0 , 4. ∀e ∈ E the set {e | e W * e}
• x # C x iff ∃y, y ∈ E such that y # i y , y W * x and y W * x ,
is an irreflexive relation.

In an occurrence net each condition (place) not in the initial marking is produced by just one event (transition), whereas the ones in the initial marking are produced by none (∀b ∈ c 0 , • b = ∅). Being C an acyclic net, the relation ≤ C defined as W * is a partial order on B ∪ E, and it is often called the causality relation. Furthermore each event has a finite number of predecessors, and the conflict relation induced by the forward conflicts among events and inherited along the causality relation. The two relations of causality ≤ C and conflict # C , are able to characterize the computations of an occurrence net, as each state of the occurrence net is a subset causally closed (to the left) subset of events X ⊆ E which is conflict free, i.e. ∀e, e ∈ X. ¬(e# C e ) and if an event e belongs to X then also the events preceding this one in the partial order are in X as well. Finally we notice that ≤ C is a well founded partial order, and ∀e ∈ E, the finite set {e ∈ E | e ≤ C e} is denoted with e .

An occurrence net can be seen as a spread net. The piece of information associated to each condition (place) of the net is basically the set of events (transitions) that have been executed in order to produce this condition. Indeed in an occurrence net each condition b has a unique history which is easily obtainable taking all the events {e | e ≤ b}.

Summing up, the occurrence net C = B, E, W, c 0 , with being the identity, can be seen as a spread net over the regular domain D = (A, Op, τ, E) with A = 2 E fin , the operations op i ∈ Op returning just the union of i places labels, and τ (A, e) just adding the event in e ∈ E to the subset of events A. Proof. First of all we observe that D is an information domain. Each condition b in the initial marking is annotated with the empty set which is the 0 of 2 E fin , as • b = ∅, being C an occurrence net. Consider now a condition b not in the initial marking, then • b = {e} for some e ∈ E. Consider the conditions in the preset of e. To each condition b ∈ • e is associated a subset of events, on these subsets the union is defined and h

(b) = {e} ∪ ( b ∈ • e h(b )) and b ∈ • e h(b ) is precisely op i (X)
where X is the multiset obtained by h( • e). τ (X, t) just add the event e to X. The last condition of Definition 4.1 is trivially satisfied as for each condition b we have that • b is at most a singleton. Thus C D,h is a spread net over D.

Observe that C D,h is properly spread as each place is labeled by its unique history and that D is regular, furthermore the devised domain is a revealing one.

Example 4.11. Consider the occurrence net in Figure 3. The annotations of conditions are rather obvious, namely they reflect the set of events that come before (in the partial order) each condition. The 0 of the information domain is obviously the empty set and annotates the conditions in the initial marking. For what concerns the operations on the information domain op

i (X 1 , . . . X i ) is 1≤k≤i X k and τ b (X, e) = X ∪ {e}.
It is a well known result that to each occurrence net C it is possible to associate a prime event structure ( [START_REF] Winskel | Event Structures[END_REF]). A prime event structure is the triple (E, ≤, #) where E is a set of events, ≤ is a well founded partial order on E (the causality relation) and # is a symmetric and irreflexive relation on events (the conflict A configuration of a prime event structure is a subset X ⊆ E of events which is conflict free, i.e. ∀e, e ∈ X. ¬(e # e ), and such that ∀e ∈ X. e ⊆ X, where e is, as before, the subset of events {e ∈ E | e ≤ e}. e is a configuration itself and it is the local configuration. Now, given an occurrence net C = B, E, W, c 0 , the triple (E, ≤ C , # C ) is a prime event structure and the information mapping of the spread net of Proposition 4.10 associates to each condition the local configuration of the unique event producing this condition, if such an event exists, otherwise it is the empty set.

∅ b 1 {e 2 } b 2 {e 1 } b 3 {e 1 , e 3 }
The clear relation between prime event structures and occurrence nets is exploited on spread nets as follows: for each event e in the event structure, e and e \ {e} are among the elements of the support, and the operations op i are defined for those (multi)sets of elements such that their union gives an element, namely either a local configuration or a local configuration e without the event e. Observe that this implies that the operations are not defined for the (multi)sets of elements such that their union would contain conflicting events. The updating mapping just add an event e to a subset of events provided that this is not contained in the subset itself.

Unravel nets. Unravel nets [START_REF] Casu | Petri nets and dynamic causality for service-oriented computations[END_REF] are nets in which each computation gives rise to an acyclic subnet where each place has at most one incoming arc (hence an occurrence net). Given a net N = P, T, F, m 0 be a net and let T ⊆ T be a subset of transitions, then N T = P , T , F , m 0 where

P = P ∩ ( • T ∪ T • ) ∪ m 0 , F = F ∩ ((P × T ) ∪ (T × P )) and m 0 is m 0 . Definition 4.12. A safe Petri net U = P, T, F, m 0 is an unravel net if it is an 1-occurrence net and for each state X ∈ St(N ) the subnet U X = • X ∪ X • ∪ m 0 , X, F ∩ (( • X ∪ X • × X) ∪ (X × • X ∪ X • )), m 0 is a an acyclic net where for each p ∈ • X ∪ X • . | • p| ≤ 1 and |p • | ≤ 1.
The requirement that the restriction of the net to the transitions in a state of the net is an acyclic net where each place has at most one incoming and one outgoing arc implies that the places in the initial marking do not have any incoming arc (as otherwise there would exists a state such that the associated net is cyclic). As an unravel net is required to be an 1-occurrence net as well, we have that each transition can be fired at some marking, and then belong at least to a state.

An unravel net as a whole may be cyclic, hence it is not possible to extract a partial order out of it but, as seen above, any run (state) gives a partial order. Places may have more than one incoming arc as well as more than one outgoing arc, thus conflicts among transitions still exist. A syntactic conflict relation is not definable, but a semantic one is available: two transitions are in conflict whenever there is no state of the net containing both. Observe that a place can be produced in several alternative ways.

Viewing an unravel net as a spread net is more complex than for occurrence nets or 1-occurrence nets. We can however use the fact that to each unravel net it is possible to associate a suitable event structure, the so called bundle event structure [START_REF] Langerak | Bundle Event Structures: A Non-Interleaving Semantics for Lotos[END_REF], along the observation we made on the information domain associated to an occurrence net. A bundle event structure is a triple B = (E, , #) where # ⊆ E × E is an irreflexive and symmetric relation and

⊆ CF (E) × E where CF (E) = {X ∈ 2 E fin \ {∅} | ∀e, e ∈ X.
¬(e # e )}. A configuration X ⊆ E is a subset of events such that X is conflict free and there exists a linearization of e 0 e 1 e 2 . . . of the events in X such that for each i and for each A i e i it holds that {e 0 , . . . , e i-1 } ∩ A i = ∅.

The set of the configurations of the bundle event structure B is denoted with Conf(B). Given an unravel net U = P, T, F, m 0 , the triple

B U = (T, { • t t | t ∈ T }, #), where t # t iff ∀X ∈ St(U ) {t, t } ⊆ X,
is a bundle event structure. Furthermore the configurations of B U are related to the states of U , namely

X ∈ St(U ) iff X ∈ Conf(B U
). Thus, similarly to what we have observed for occurrence nets, we can use the bundle event structure to define the annotation of the places of an unravel net. Given a bundle event structure B = (E, , #), we can still associate a kind of causality relation to it. We stipulate that e ≺ e whenever there exists an A e such that e ∈ X. It is then clear that, given a configuration X of this bundle event structure, ≺ * ∩(X × X) is a well founded partial order. Furthermore if e ≺ e but e ∈ X then there exists an e ∈ X such that e # e , e ≺ e and e ∈ X. With the aid of this observation we can define the set of local histories of an event. e is the set of subsets of events Consider the unravel net U = P, T, F, m 0 , and the associated B U = (T, U , # U ) then A, the support of the information domain, is composed by the subsets of finite configurations of the associated bundle event structure and the 0 is {∅}. The operation op i ∈ Op takes all multisets X ∈ µA where X(A) > 0 whenever there exists a place p ∈ P such that for each t ∈ • p we have that A = ∅ and A ⊆ t t , and it returns t ∈ • p t t . Thus, given a transition t, the operation op i takes all the possible local histories to which t can be added, and not only returns the local histories where t is added but also the local histories of the transitions t (those local histories not containing t ) where t is in direct conflict with t as both put a token in the same place p. Finally τ (A, t) takes each Y ∈ A and it either add the transition t to Y if Y ∪ {t} ∈ Conf(B U ) or it add a t such that there exists a place p ∈ P with {t, t } ⊆ • p and Y ∪ {t } ∈ Conf(B U ). We denote this information domain with D B U .

{X | e ∈ X, X ⊆ {e | e ≺ e} ∧ X ∈ Conf(B)},
We are now ready to show that also an unravel net can be considered a spread net over this information domain.

Proposition 4.13. Let U = P, T, F, m 0 , be a label unravel net where is the identity. Let B U = (T, U , # U ) the associated bundle event structure. Let D B U = (A, Op, τ, E) be the information domain illustrated above, and let the information mapping h :

P → A defined as h(p) = {X ⊆ T | X ∈ t for t ∈ • p}. Then U D B U ,h is a spread net over D B U .
Proof. D is clearly an information domain. Each place in the initial marking is annotated with the set containing just the empty set which is the 0 of A as, being U an unravel net, the places in the initial marking have no incoming arcs. Now consider a transition t ∈ • p. op i (h( • t)) is defined and it is equal to the set containing the subsets of all the local histories concerning the transitions t ∈ • (t • ). Now consider a place p ∈ t • , clearly by definition of τ , we have that for all t ∈

• p, τ (A, t) = τ (A , t ) for some A, A ∈ op i (h( • t)). Thus U D B U ,h is a spread net over D B U .
Example 4.14. Consider the unravel net U in Figure 4. The elements of the information domain are found taking the associated bundle event structure, with events {e 1 , e 2 , e 3 , e 4 , e 5 , e 6 }, the conflicting events are e 1 # U e 2 , e 2 # U e 4 and e 5 # U e 6 , which has the following bundles: {e 1 , e 2 } e 3 , {e 3 } e 5 , {e 4 } e 5 and {e 3 } e 6 . The operations op 1 and op 2 are defined as follows: op 1 ({∅}) is equal to {∅}, op 1 ({{e 1 }, {e 2 }}) is equal to {{e 1 }, {e 2 }} and op 1 ({{e 1 , e 3 }, {e 2 , e 3 }}) is equal to {{e 1 , e 3 }, {e 2 , e 3 }}, whereas op 2 ({∅}, {∅}) is equal to {{∅}, {∅}} and finally op 2 ({{e 4 }}, {{e 1 , e 3 }, {e 2 , e 3 }}) is equal to {{e 1 , e 3 , e 4 }}. For all the other inputs they are undefined. Finally the annotations of each place p is t∈ • p t . Remark 4.15. It should be stressed that annotating an unravel net is tricky as the annotation related to a place should contain all the local histories of the transitions in the preset, and then the operations op i and τ are abstractly defined on the whole net. On the contrary the annotation and the operations for the occurrence and the 1-occurrence nets are much less tricky and they have a local nature rather than a global one.

Spread nets and domains

We discuss briefly how information domains and spread nets are intertwined. Proposition 4.3 shows that each labeled safe net can be seen as a spread net over the information domain D ⊥ , namely the domain where the same information is conveyed in each place, and also the 1-occurrence net is a spread net over the same domain (Proposition 4.7). This domain is trivially regular but it is not revealing. Thus 1-occurrence nets are uniformly but not properly spread.

More appealing and challenging is the cases of occurrence nets. The relationship between the structure of the net and prime event structures can be exploited either to define suitable information domains or to enforce suitable structures on the net itself. We have seen how to construct an information domain tailored to an occurrence net, now we show the vice versa, namely how to construct an occurrence net starting from a suitable domain. E,≤,#) is a prime event structure it follows that e = e . The fact that W * is a partial order follows from the fact that ⊆ is a partial order, and this implies also that for each e ∈ E, the set {e | e W * e} is finite. Finally consider e and e which are in conflict. As the configurations of a prime event structures are such that their intersection is a configuration, also e ∩ e is a configuration. Take e such that (a) e ⊆ e ∩ e and (b) for all ê that are greater than e we have that ê ⊆ e ∩ e , then we have that • e ∩ • e = ∅, with e ⊂ e and e ⊂ e . The fact that the conflict relation of the net is inherited along the causality relation is straightforward.

We proceed along the same line also when considering bundle event structure. Given a bundle event structure B = (E, , #) and a subset X ⊆ E of events, with CF(X) we stipulate that either |X| = 1 or ∀e, e ∈ X. e# e . Proposition 4.17. Let B = (E, , #) be a bundle event structure, and let D B be the domain associated to B. Let U D B ,h be a spread net where U is the tuple P, E, F, m 0 , with

P = {({∅}, X) | X ⊆ E ∧ CF(X)}∪ {(X, X) | CF (X) ∧ X = e∈X e } and h((X, X)) = X, F = {(e, p) | ∃X ∈ h(p). e ∈ X}∪{(p, e) | ∃X ∈ h(p). ∃Y ∈ Conf(B). X ∪ {e} ⊆ Y ∧ ∀Z ⊆ Y \ (X ∪ {e}). X ∪ {e} ∪ Z ∈ Conf(B) ⇒ X ∪ {e} ∪ Z = Y }, m 0 = {p ∈ P | h(p) = {∅}},
and being the identity. Then U is an unravel net.

Proof. To prove that U is an unravel net we have to show that each execution of the net gives an acyclic net where each place has at most one incoming arc and one outgoing arc. The places in the initial marking do not have any incoming arc by construction. Consider an event e ∈ E and one of the local histories for it, namely X ∈ e . X can be totally ordered, i.e. X = {e 1 , . . . , e n } with e n = e, with the order induced by the relation. The subnet identified by the places where the information associated to them contains the proper X i = {e 1 , . . . , e i } ⊆ X is a clearly acyclic and the preset and postset of each of these places contains at most one transition. This suffices to ensure that U is an unravel net. Proposition 4.16 and Proposition 4.17, together with Proposition 4.10 and Proposition 4.13 show that each net with certain characteristic can be turned into a spread net on a suitable domain, and also that a suitable domain induces a spread net with certain characteristic.

Multi-clock nets and ticking domains

In the previous section we have discussed the notion of spread net and we have shown that some of the usual nets that are used to describe a true concurrent semantics of some net N can be seen as special cases of a spread net. In this section we recall the notion of multi-clock net (see [START_REF] Fabre | Trellis processes: A compact representation for runs of concurrent systems[END_REF]) and devise a notion of information domain tailored for multi-clock nets, that we will call ticking domain.

Multi-clock nets

The intuition behind the notion of multi-clock net is the following: a net is composed by a number of sequential components, thus the execution time in each component of a transition of the net can be somehow inferred. Each component has a local clock and, as a net has various components, the net has a multi-clock.

A safe net N = P, T, F, m 0 is said to be a net automaton whenever each m ∈ M N is a singleton, and each transition t ∈ T is such that

| • t| = |t • | = 1.
In a net automaton only the choices between the execution of two transitions may be represented, as each reachable marking is obviously a singleton.

A multi-clock net is a safe net which can be seen as a product of net automata which synchronize on common transitions, and the effect of a synchronization are observable in all net automata participating to it (see transition b in Figure 5). The synchronization transitions have a preset which is not a singleton (the components to be syncronized), and we require that the cardinality of the preset of each transition is the same as the one of the postset (the effect of a synchronization, observable or not, has to take place in each of the involved components). Formally: Definition 5.1. A multi-clock net (mcn-net) N is the pair (N, ν) where N = P, T, F, m 0 is a safe net and ν : P → m 0 is a total mapping such that

• for all p, p ∈ m 0 , it holds that p = p implies ν -1 (p) ∩ ν -1 (p ) = ∅,
• ν is the identity when restricted to m 0 , and • for all t ∈ T . ν is injective on • t and on t • , and ν(

• t) = ν(t • ).
The cardinality of a mcn-net N, denoted with υ(N), is the cardinality of m 0 , and represents the number of components.

As ν(m 0 ) = m 0 , ν is injective on the preset (postset) of each transition and that ν( • t) = ν(t • ), for each p ∈ m 0 , the net N p = P p , T p , F p , m p 0 , where P p = ν -1 (ν(p)), T p = T ∩ ( • P p ∪ P p • ), F p is the restriction of F to P p and T p and m p 0 : p → N is such that m p 0 (p ) = 1 iff p = p, is a net automaton. We sometimes denote with p the subset of places P p .

Example 5.2. We illustrate the notion with a simple multi-clock net with just two components, depicted in Figure 5. On the left there is a multi-clock net N where the two components, depicted on the right, N p1 and N p2 synchronize on transition b. The two components are clearly net automata, and the ν mapping is ν(p 1 ) = ν(p 3 ) = p 1 and ν(p 2 ) = ν(p 4 ) = p 2 . The notion of morphism introduced for safe nets can be tailored to multi-clock nets by requiring that partitions are preserved. (f P , f T ) : (N, ν) → (N , ν ) is a multi-clock net morphism if (f P , f T ) is a net morphism from N to N and for each p ∈ P and for each p ∈ P , if p f P p then ν(p) f P ν (p ).

Ticking domains

As we have already said, a multi-clock net can be seen as the composition of net-automata synchronizing on common actions (transitions), and each component of the multi-clock net is identified via an index which is the unique initially marked place of the component. In other words a multi-clock net can be seen as the product of its (sequential) components. In this perspective the annotations of a spread net can be seen as the knowledge that each component has on its behaviour and possibly on the behaviour of the other components which may synchronize with it.

The behaviour of each single component can be easily represented as a language, as a component is a net automaton. We define the information domain associated to each component of the multi-clock net as words over transitions (labeled) of that component.

We first formalize the annotation for a single component (A is related to the (labeled) transitions of that component). Definition 5.3. Let A be an alphabet. A ticking language over A is a language L ⊆ A * . The set of ticking languages over A will be denoted L A .

Given a ticking language L over A, alph(L) denotes its alphabet A. When clear from the context, we will omit the superscript A in L A . L 0 denotes the language reduced to the empty word ε: L 0 = {ε}. A ticking language will often be obtained as the equivalence class of an equivalence relation defined on the words in A * , and often we will use just a word to denote each element of the class.

Example 5.4. Consider the alphabet A = {a, b}, a language can be the set of all words of length 2, hence L = {aa, ab, ba, bb} or the set of all words of length less than or equal to 3 where all the words are equivalent to aab via the equivalence relation induced by the equation a = b, hence {aaa, aab, abb, bbb, bab, baa, bba, aba}.

Once we have introduced the notion of ticking language, we have to say when a tuple of ticking languages can be seen as the annotation of the places of a multi-clock net. We assume the existence of a property P defined on tuples of languages over an alphabet A, hence P ⊆ A * × • • • × A * . A property P may be the one stating that all the words of each language have a common prefix, or that a language has all the words with the same length and each of the others languages contains just the empty word. The property will be used to sort out the tuples of languages we are interested in.

We introduce the notion of information domain tailored for multi-clock nets which we call ticking domain. The notion has to take into account the existence of the several components of a multi-clock net. We assume the existence of a finite set of indexes I = {1, . . . , n}. Definition 5.5. Let I = {1, . . . , n} be a finite set of indices and let, for each i ∈ I, L Ai i be a set of ticking languages over the alphabet A i . Let A be i∈I A i and let P be a property on the tuples with n components belonging to (A * ) n . Let L A = i∈I L Ai i . A ticking domain D of arity |I| over A is the quadruple (A, Op, τ, A), where 1), . . . , v(n))}, the elements of A are called vector-clock and are ranged over by v, and 0 is the vector-clock v such that v(i) = L 0 for each i ∈ I,

• A = {v : I → L A | v(i) ∈ L Ai i ∧ P(v(
• Op is a set of partial operations op i : A i 2 A such that

-i ≤ |I|, and
-if op i (v 1 , . . . , v i ) is defined then op i (v 1 , . . . , v i ) = ∅, and
• τ : I × A × A → A
is the ticking mapping that takes an index i ∈ I, a vector clock and an element in A and returns a vector clock.

The notion of ticking domain is an obvious adaptation of Definition 3.2 to the annotation of multi-clock nets. The elements of a ticking domain are vectors of languages (or words) where the components of the vector all together satisfy a property P, we will see its use in the next sections. Each operation op i ∈ Op acts on a multiset of vector-clocks containing i elements, that cannot be more than the cardinality of the ticking domain. The unique relevant difference from Definition 3.2 is the updating mapping, which is called here ticking mapping. It acts on each component separately, and the effects may differ from a component to another. We again say that a ticking domain is regular is the operations in Op return a singleton. In this case we write op i : A i A. As before, given the set of vector-clocks, the set of operations and the ticking mapping (i.e. the updating mapping) will be defined when constructing the proper domains for the spread net we are interested in. Given a ticking domain D of arity |I|, with A i,j we denote the alphabet A i ∩A j , with i, j ∈ I (obviously A i,j = A j,i ). We will sometime omit the word ticking when it is clear from the context that we are referring to a ticking domain.

We already said that the languages of a vector-clock v may be induced by a suitable equivalence relation ∼. In the case that the equivalence relation is well understood, rather than writing v(i) = {w | w ∼ w} = L w ∼ we simply write v(i) = w and also (w 1 , . . . , w n ) to denote the vector-clock where v(i) = L wi ∼ for 1 ≤ i ≤ n.

Example 5.6. We first set a generic domain. Take any finite index set I and consider the set of alphabets A i , with i ∈ I, then a ticking-domain could be (A, Op, τ, i∈I A i ) with A being the set of vectors v where each component v(j) is the language with just one word and the property P could be that ∀j, k ∈ I, ∀w ∈ v(j), ∀u ∈ v(k), proj (w, A j,k ) = proj (u, A j,k ) (the elements of the vector-clock agree on the common symbols).

The operations can be defined as follows. Take a tuple (v 1 , . . . , v i ) of vector-clocks. The operations are defined only if for each pair of vector-clock v n and v k , the elements are such that for each m ∈ I either the word of the language v n (m) is a prefix of the word of the language v k (m) or vice versa. The result is obtained by taking the maximum of all these words. The operation devised in this way is well defined, as it returns a vector-clock satisfying P. Finally the ticking mapping, for each index, just concatenate the to each word in each language the element of the alphabet i∈I A i , provided that it belongs to the alphabet of the language. Concretely consider two alphabets A 2 = {a, b} and A 1 = {b, c}, the elements of the domain are the pairs of words (w, u) having the same number of b (we identify the language with the unique word it contains), and the operations either take a vector-clock and it returns the vector-clock itself or it take two vectorclocks v = (w, u) and v = (w , u ). In these two vector-clocks it should be that either w is a prefix of w or vice versa, and that either u is a prefix of u or vice versa, and the operation returns a vector-clock composed by the two longest words. We show that this operation is well defined and the resulting vectorclock satisfies the property. Assume that w is a prefix of w and that u is a prefix of u, and assume that proj (u, {b}) = proj (w , {b}). Then, as P(v ) holds, we have that proj (w , {b}) = proj (u , {b}), thus necessarily w contains fewer b than w , but also proj (w, {b}) = proj (u, {b}) as P(v) holds, hence it cannot be that u is a prefix of u as proj (u, {b}) ≥ proj (u , {b}). It holds then that proj (u, {b}) = proj (w , {b}) and P((w , u)) holds. Finally τ , for each index, just concatenate the element to the words if the element belongs to the alphabet.

We stress the fact that, as multi-clock nets can be seen as the composition of more elementary components, also a ticking domain can be seen as the composition of simpler components. The main difference is that we have to establish when the pieces of information coming from other components are coherent and this is the purpose of the predicate P.

Unfoldings of Multi-clock nets as spread nets

When illustrating the notion of spread net (Section 4) we have shown that various subclasses of nets, each of them modeling a semantics for (safe) nets, could be viewed as spread nets for suitable information domains, which we have constructed having in mind how we wanted to annotate these nets. In this section we explore various notions of unfoldings in the same manner. We focus in particular on unfoldings of multiclock nets. For various notions of unfoldings proposed in the literature, we adapt them to multi-clock nets and show how they can be seen as spread nets over suitable domains that are always revealing ones. The element of the ticking domain associated to each place (condition) of the unfolding will carry information about the knowledge that each component has on the executions leading to that place (condition), which is inferred from the way the net is unfolded.

For each kind of unfolding we characterize the associated ticking domain, and each element of a ticking domain will be a vector-clock where each entry is a language (possibly induced by an equivalence class) of words on the alphabet defined by the transitions of the corresponding component of the multi-clock net to be unfolded.

We recall when we consider a net an unfolding. We say that a net N is the unfolding of another net N if some conditions are fulfilled:

• each transition of the unfolding is executed at most once in a computation,

• each computation of the unfolding can be mapped to a computation in the original net via a folding morphism, and

• to each computation of the original net it is possible to find a corresponding computation in the unfolding (where corresponding means that the former computation is mapped to the latter one).

Thus an unfolding is a net N (possibly enjoying some specific characteristics like, for instance, being an unravel net or an occurrence net) and a suitable labeling mapping that turns to be a folding morphism.

Let N = P, T, F, m 0 and N = P , T , F , m 0 be two safe nets, a folding morphism f : N → N is a net morphism where the following further conditions hold:

1. f : P → P and f : T → T are total mappings, 2. ∀t ∈ T it holds that f is bijective on • t and on t • as well, and

3. ∀t, t ∈ T if • t = • t and f (t) = f (t ) then t = t .
The first condition ensures that each place (condition) and transition (event) of the unfolding have a counterpart, i.e. they correspond to a place or a transition of the net to be unfolded, the second states bijectivity on the presets or postsets of transitions and the last requirement is a parsimony requirement: the net representing an unfolding does not contain two transitions which are indistinguishable (bearing the same label and using the same conditions, thus producing the same conditions). In the case of multi-clock nets the morphisms (and henceforth the folding morphisms as well) preserve the partitions.

In this section with alph(N p ) we will denote the set T p ⊆ T of the subnet N p of the multi-clock net N = (N, ν), with N = P, T, F, m 0 , and p ∈ m 0 .

1-unfolding of a multi-clock net

The notion of 1-unfolding has been formalized by van Glabbek and Plotkin in [START_REF] Van Glabbeek | Configuration structures[END_REF] and [START_REF] Van Glabbeek | Configuration structures, event structures and Petri nets[END_REF] and it is meant to capture the so called collective token philosophy.

We briefly illustrate the idea behind this construction. In the collective-token philosophy it is irrelevant to keep track of the transitions that have produced the tokens needed to execute a transition, all the different histories are equated. The only requirement is that each occurrence of a transition in a computation of the original net is uniquely represented in the 1-unfolding. It is then enough to create, for each transition, an occurrence of it connected to the places as the original transition and enforce that this occurrence is executed just once. In the construction this is achieved by creating a place in the preset of each transition and guaranteeing that this place gets marked just once. Occurrences of the same transition are numbered and we implement their ordered execution. The construction is rather syntactic and, to assure that each transition of the 1-unfolding can be executed, we assume that each transition of the multi-clock net N to be unfolded can be executed an arbitrary number of times. Henceforth we assume the multi-clock net N = (N, ν) is live.

The only information that the 1-unfolding has to convey regards the ordering in the execution of a single transition. To achieve this we enrich the multi-clock net by adding some components that have this numbering purpose. Furthermore this enrichment will allow us to define a proper folding morphism.

Enriching multi-clock nets. The enrichment is done by adding a new component for each transition of the original net, and the added component has just a numbering purpose: it should guarantee that the executions of each transition in the net can be numbered just by looking at this added component. We will call the added components numbering-automata.

Consider a multi-clock net N = (N, ν), where N = P, T, F, m 0 , for each t ∈ T we add a place p t which is initially marked and connected with t with an incoming and an outgoing arc. Definition 6.1. Let N = (N, ν) be a multi-clock net, where N is P, T, F, m 0 . Then the enrichment of N, denoted with N, is the pair ( N , ν) where

• N = P , T, F , m 0 is a safe net where

-P = P ∪ {p t | t ∈ T }, -F = F ∪ {(p t , t) | t ∈ T } ∪ {(t, p t ) | t ∈ T }. and
m 0 (p) = m 0 (p) when p ∈ P and m 0 (p) = 1 when p ∈ {p t | t ∈ T }, and

• ν extends ν stipulating that ν(p t ) = p t .
If the original multi-clock net was formed by n synchronizing net automata and it has m transitions, the enriched multi-clock net is formed by m + n synchronizing net automata and the added automata N pt = ({p t }, {t}, {(p t , t), (t, p t )}, {p t }) (we confuse the initial marking with the set) simply counts the occurrence of the transition t. Proposition 6.2. Let N = (N, ν) be a multi-clock net and N = ( N , ν) its enrichment. Then N is a multiclock net.

It is a trivial observation that there is a one to one correspondence between the reachable markings of N and those of N , and between the firing sequences as well. Proof. Obvious.

The enrichment does not influence the behaviour of a multi-clock net.

1-unfolding construction. As we have done for occurrence and unravel nets, we call places conditions and transitions events, thus we use B and E for condition and events, respectively. Definition 6.4. Let N = (N, ν), with N = P, T, F, m 0 , be a multi-clock net and let N be its enrichment. The 1-unfolding O is the (labeled) multi-clock net (O, f ), with O = (O, ν O ), where O = B, E, W, c 0 , f T , ν O and f are defined as follows: • c 0 ((p, * )) = m 0 (p), c 0 ((p t , 0)) = 1 and c 0 ((p t , i)) = 0 for i = 0,

• B = (P × { * }) ∪ ({p t | t ∈ T } × N), • E = T × (N \ {0}), • W = {((p,
• ν O ((p, * )) = ν(p) and ν O ((p t , i)) = (p t , 0), and

• f P ((p, * )) = p, f P ((p t , i)) = p t , and f T (t, i) = t.
The 1-unfolding O is related to the multi-clock net N , and then to N itself. Each condition (p, * ) is related to the place p and the condition (p t , i) to the place p t and the event (t, i) to the transition t. It is routine to check that f is a morphism (which implies that each computation of the 1-unfolding O is mapped to a computation of the multi-clock net N and of N as well). The requirement that each computation of N has a correspondence in a computation of O is trivial. We have turned the construction into a labeled net as the f T can be seen as a labeling of event: to each event (t i , k) it associates the label t.

The liveness assumption on the multi-clock net N allows us to create as many copies of t as we need without being forced to count them beforehands, as the net can stutter. Would we avoid the requirement that each transition of N can be executed an arbitrary number of times we would have to calculate, for each transition t, its maximal number of occurrences resorting to the states of the multi-clock net N. Assume, for instance, that the transition T is executed at most n times in each state, i.e. n = max({X(t) | X ∈ St(N )}) = ξ(t), then we have to introduce the places {(p t , i) | i ≤ ξ(t)}, the transitions associated to t would be {(t, i) | 1 ≤ i ≤ ξ(t)} and so forth. The way places and transitions are connected would not change, as well as the other ingredients of the construction. O = (O, ν O ) is indeed a multi-clock net and O is as well an occurrence net, i.e. each event (transition) is executed just once. Proposition 6.5. Let N = (N, ν) be a multi-clock net and N its enrichment. Let O = ((O, ν O ), f ) be its 1-unfolding. Then (O, ν O ) is a multi-clock net and f is a folding morphism.

Proof. The fact that f is a morphism trivial (it is the identity relation on the places in P and all the numbering places are related to the proper numbering one), and it is also a folding morphism: f is clearly total on places and transitions, and the other two conditions are trivial. Clearly each component of the 1-unfolding is a net-automata: the one deriving by the ones non numbering one are net-automata as they are net automata in N, and the numbering ones are net-automata as well.

Given an 1-unfolding O = (O, f ), we now discuss on how to turn O into a spread net. The ticking domain tailored for this construction is the one where each vector-clock either consists of just the empty word for each entry of the vector-clock, or it has just one entry which is not the empty word and this entry is associated to a numbering component of the enrichment. The operations and the ticking mapping are defined according to this intuition. Example 6.6. The multi-clock net N = (N, ν) on the left in Figure 6 has just one component with two transitions. Its enrichment N is shown below N and has three components, where two of them are numbering ones. On the right of these two multi-clock nets we depict the initial part of the 1-unfolding. Observe that the piece of information associated to the conditions of the unfolding carry, for each numbering component, the number of timess the associated transition has occurred.

(ε, ε, ε) (p, * ) (p a , 0) (ε, ε, ε) (p b , 0) (ε, ε, ε) (p a , 1) (ε, a, ε) (p b , 1) (ε, b, ε) (p a , 2) (ε, aa, ε) (p b , 2) (ε, bb, ε) . . . . . . (a, 1) (b, 1) (a, 2) (b, 2)
Figure 6: A multi-clock net with three components and its 1-unfolding

The following definition details the discussion on how to define the domain. is the quadruple (A, Op, τ, T ) where

• A = {(w 1 , . . . , w n , u pt 1 , . . . , u pt n ) | ∃! p t k . u pt k = ε ∧ ∀i = p t k . w i = ε} ∪ {(ε, .
. . , ε)}, with the 0 being the vector-clock (ε, . . . , ε),

• Op = {op k | 2 ≤ k ≤ n + 1} where op k (v 1 , . . . , v k
) is defined when all the k vector-clock are 0 or just one of them is not, and

op k (v 1 , . . . , v k ) = 0 if ∀i ≤ k. v i = 0 v j if ∃! j.v j = 0
i.e. the result is 0 in the case all the vector-clocks are 0 and the only one not being 0 otherwise, and

• τ is defined as follows:

τ (i, (w 1 , . . . , w n+m ), t k ) = 0 if i = p t k (ε, . . . , w pt k • t k , . . . , ε)
otherwise .

We stress that ∃! p t k . u pt k = ε ∧ ∀i = p t k . w i = ε is the property the elements of the ticking domain have to fulfill, and it says what we have stressed before, namely that at most one component of the vector-clock is different from L 0 , and this component is one of the numbering components.

• h : B → A is defined as h(b) = 0 if b ∈ P (ε, . . . , t i , . . . , ε) if b = (p t , i) is a spread net over D 1unf N .
Proof. By construction it is easy to see that the conditions of Definition 4.1 are fulfilled.

We observe that the ε in the vector-clock corresponding to a non numbering component can be considered as the representative of the equivalence defined equating all the local computation to the empty one (thus forgetting everything). The words in the numbering components are those used to guarantee the order in the execution of the same transition (each word is equivalent to itself).

Branching processes

The 1-unfolding realizes the idea that, in each component which is not a numbering one, the whole past of each place is forgotten. This is represented by the 0 annotation of each condition beside the ones belonging to numbering components. On the contrary we can imagine that the whole past is kept. This gives rise to branching process ( [START_REF] Winskel | Event Structures[END_REF] and [START_REF] Engelfriet | Branching processes of Petri nets[END_REF]). The notion is based on the one of occurrence net where, as we have already mentioned, the computations are definable without resorting to the firing sequence. We recall that in aa occurrence net C = B, E, W, c 0 a subset of conditions X ⊆ B is said to be concurrent whenever

∀b, b ∈ X. b = b ⇒ (¬(b ≤ C b ) ∧ ¬(b ≤ C b) ∧ ¬(b # C b ))
, and it is denoted with co(X). We define at the same time the occurrence net and the folding morphism Definition 6.9. Let N = (N, ν), with N = P, T, F, m 0 , be a multi-clock net. The unfolding C is the labeled multi-clock net (C, f ), with C = (C, ν C ), where C = B, E, W, c 0 , f T , ν C and f are defined as follows: -, p)) = ν(p), and

• B = {(m 0 , p) | p ∈ m 0 } ∪ {({e}, p) | e ∈ E ∧ p ∈ f T (e) • }, • E = {(X, t) | X ⊆ B ∧ co(X) ∧ • t = f P (X)}, • W = {(b, e) | e = (X, t) ∧ b ∈ X} ∪ {(e, b) | b = ({e}, p)}, • c 0 (b) = 1 if b = (m 0 , p) and c 0 (b) = 0 otherwise, • ν C ((
• f P ((-, p)) = p and f T ((-, t)) = t.
The morphism f : C → N is clearly a folding morphism, and the resulting net is obviously an occurrence net which is a multi-clock net as well. The unique difference with respect to the classical notion is that we add the labeling to the occurrence net itself. Proposition 6.10. Let N = (N, ν) be a multi-clock net. Let C = ((C, ν C ), f ) be its unfolding. Then (C, ν C ) is a multi-clock net and f is a folding morphism.

Proof. See [START_REF] Winskel | Event Structures[END_REF] and [START_REF] Fabre | Trellis processes: A compact representation for runs of concurrent systems[END_REF].

We now discuss on how to turn the multi-clock net (C, ν C ) which is the one defined in Definition 6.9 into a spread net, using the fact that C is an occurrence net. Take the labeled occurrence multi-clock net C = (C, ν C ) where C = B, E, W, c 0 , and the labels are the set T , and consider the condition b ∈ B. Assume that • b = ∅, hence it is caused by a unique event, say e, as • b is a singleton. Consider now the set of events X e = {e | e ≤ C e}, and let x e ∈ E * any linearization of the events in X e compatible with ≤ C (meaning that if e ≤ C e then e precedes e in x e ) and f T (w e ) ∈ T * . We observe that, for each p ∈ m 0 :

1. w p = proj (f T (x e ), T p ) is a word over alph(N p ) and there exist σ ∈ FS Np m0 , such that tr(σ) = w p , i.e. projecting the word f T (x e ) on alph(N p ) we obtain a trace of the component N p , and does not depend on a linearization of X e , i.e. for any two different linearization x and x of X e compatible with the partial order induced by the occurrence net, it holds that proj (f T (x), T p ) = proj (f T (x ), T p ). The property P that each vector-clock (w 1 , . . . , w n ) has to satisfy can be written as follows: ∀i, j ∈ {1, . . . , n}.

proj (w i , A j ) = proj (w j , A i ). Thus A = {(w 1 , . . . , w n ) | w i ∈ A i * ∧ ∀i, j. proj (w i , A j ) = proj (w j , A i )}
Consider now a set of vector-clock {v 1 , . . . , v k }. We say that {v 1 , . . . , v k } is bp-homogeneous if for all i, k and for all j it holds that either v i (j) is a prefix of v k (j) or v k (j) is a prefix of v i (j). In this case it is possible to define a maximum among these words, which we denote by max({v 1 (j), . . . , v k (j)}). The operation op i ({v 1 , . . . , v i }) is defined for bp-homogeneous tuples of vector-clocks and it returns the vectorclock (max({v 1 (i), . . . , v i (1)}), . . . , max({v 1 (n), . . . , v i (n)})). The result satisfies the property P. Assume it does not, then there exist two indexes of the resulting vector-clock, say k and j, such that such that proj (w k , A j ) = proj (w j , A k ). Now w k is the max({v 1 (k), . . . , v i (k)}) and w j is the max({v 1 (j), . . . , v i (j)}), and, arguing like we did in Example 5.6, we arrive at a contradiction. Hence the operations are well defined. Finally τ (i, v, t) just concatenates the symbol t to each word on an alphabet containing t. Definition 6.11. Let N = (N, ν) be a multi-clock net, where N = P, T, F, m 0 . The ticking domain for the branching process of N is the quadruple (A, Op, τ, T ) where

• A = {(w 1 , . . . , w n ) | w i ∈ A i * ∧ ∀i, j. proj (w i , A j ) = proj (w j , A i )} with 0 = (ε, . . . , ε), • Op = {op i : A i → A | 1 ≤ i ≤ υ(N)} where op k (v 1 , . . . , v k ) is defined when {v 1 , . . . , v i } is bb- homogeneous and op k (v 1 , . . . , v k ) = (max(V 1 ), . . . , max(V n )) where V k is the set {v i (k) | v i ∈ V }, and
• τ : I × A × T → A
, where I = m 0 , takes and index, a vector-clock v and an element t ∈ T and returns the vector-clock (w 1 , . . . , w n ) where

w i = v(i) • t if t ∈ T i and w i = v(i) otherwise,
and it is denoted with D bp N ,

We are now ready to show that the unfolding of a multi-clock net is indeed a spread net. Proof. Again by construction it is easy to see that all the conditions of Definition 4.1 are fulfilled. In particular take a subset X ⊆ B such that co(X) and there exists an event e such that • e = X, then it is easy to observe that the set {h(b) | b ∈ X} is a bp-homogeneous set of vector-clocks, and this guarantees that the vector-clocks associated to the conditions in the postset of e are the correct ones.

Example 6.13. Consider the multi-clock net in the Example 5.2. In Figure 7 we show the initial part of its branching process, and the annotations making it a spread net.

Trellis processes

Looking from the point of view of how much information on executions is preserved, the 1-unfolding conveys the idea that the whole past is forgotten, hence also dependencies and conflicts are identified (the only information conveyed is that the i-th occurrence of a transition is preceded by the i -1-th occurrence of the same transition). Somehow we can say that 1-unfoldings are minimally spread. Instead the notion of branching process captures the intuition that all the dependencies and conflicts are properly presented. We can say that branching process are maximally spread.

In a multi-clock net two transitions belonging to the same automaton are never concurrent, they may be in conflict in the case they have a common place in their preset or postset. These conflicts are somehow local to the component involved. The idea of a trellis process is that local conflicts may be identified provided that the conflicting transitions happen at the same time and determine the same local state, i.e. the conflicting transitions mark the same place. Thus trellis processes equate some of the computations of the underlying multi-clock net. Here we give a direct construction in the style of 1-unfolding of branching processes seen before.

We introduce a number of auxiliary notions. Given an unravel net N = P, T, F, m 0 , we say that P ⊆ P are concurrent places whenever there exists a firing sequence σ ∈ FS N m0 such that P ⊆ lead (σ). We denote a set of concurrent place P with ĉo(P ). With respect to the analogous notion in occurrence nets, this is semantic notion and clearly if N = P, T, F, m 0 is an occurrence net, then it holds that co(X) iff ĉo(X) for any subset of places X of P . The second one will be used to construct the conditions of the trellis. Consider the multi-clock net N = (N, ν), with N = P, T, F, m 0 . With T i p we denote the set

{w ∈ T * p | |w| = i ∧ ∃σ ∈ FS Np m p 0
. tr(σ) = w}, i.e. all the traces of length i in the net automaton N p .

Finally with P i p we denote the set of places of N p which are marked with a firing sequence of length i,

namely {p ∈ P p | ∃σ ∈ FS Np m p 0 . |tr(σ)| = i ∧ p ∈ lead (σ)}.
With the aids of these notion we can introduce the notion of trellis process Definition 6.14. Let N = (N, ν), with N = P, T, F, m 0 , be a multi-clock net. The trellis process U is the (labeled) multi-clock net (U, f ), with U = (U, ν U ), where U = B, E, W, c 0 , f T , ν U and f are defined as follows:

• B = {(p , {ε}) | p ∈ m 0 } ∪ i>0 {(p , T i p ) | p ∈ P i p } , • E = {(X, t) | X ⊆ B ∧ ĉo(X) ∧ • t = f P (X)}, • W = {(b, e) | e = (X, t) ∧ b ∈ X} ∪ {(e, b) | e = (X, t), b = (p , T i p ) ∧ ∃ b ∈ X. (b = (p , T i+1 p ) ∧ p ∈ t • )}, • c 0 (b) = 1 if b = (p, {ε}) and c 0 (b) = 0 otherwise,
• ν C ((-, p)) = ν(p), and

• f P ((p, -)) = p and f T ((-, t)) = t.
The morphism f : U → N is clearly a folding morphism, and the resulting net is an unravel net which is a multi-clock net as well.

This construction mimics the one of branching process seen previously, following the intuition given in [START_REF] Fabre | Trellis processes: A compact representation for runs of concurrent systems[END_REF]. Thus an event has in its preset a set of concurrent conditions that are mapped onto the preset of the image of the event. The conditions in the postset of the event are calculated using the set of traces associated to the conditions in the preset. Proposition 6.15. Let N = (N, ν) be a multi-clock net. Let U = ((U, ν U ), f ) be its trellis process. Then (U, ν U ) is a multi-clock net and f is a folding morphism.

Proof. The fact that (U, ν U ) where U = B, E, W, c 0 , f T is a multi-clock net follows at once by the construction. We show that f is a morphism. Clearly f P (c 0 ) = m 0 , consider then (X, t) ∈ E, then f T ((X, t)) = t, and we have to prove that f op P : • t → • (X, t) is a total mapping, which is the case as X ⊆ B, ĉo(X) and • t = f P (X). With a similar argument we have that also f op P : t • → (X, t) • is a total mapping, furthermore it is easy to see that f P on • (X, t) and (X, t) • is a bijection. Consider now p = f P ((p, T i p )). Then also f T : • (p, T i p ) → • p is trivially a total mapping, and the same for f T : (p, T i p ) • → p • . The parsimony requirement for f to be a folding morphism is trivially verified.

A trellis-process is not only a multi-clock net, it is also an unravel net. Proposition 6.16. Let N = (N, ν) be a multi-clock net. Let U = (U, f ), with U = (U, ν U ), be its trellis process. Then U = B, E, W, c 0 is an unravel net.

Proof. It follows from the fact that it is a trellis process. In fact in [START_REF] Fabre | Trellis processes: A compact representation for runs of concurrent systems[END_REF] it is shown that each state X ∈ St(N ) is such that N X is acyclic and each place in this subnet has at most one incoming and one outgoing arc.

A trellis process can be viewed as a spread net over a suitable ticking domain. Consider a multi-clock net N = (N, ν) of cardinality υ(N) = n, where N = P, T, F, m 0 , we can define the languages L

Tp i k = {w ∈ T *
pi | |w| = k}, namely the one where all the words have the same length (namely k). Set A i = T pi for some p i ∈ m 0 . The set of elements A we are looking for is composed by vector-clocks v such that for each index 1 ≤ i ≤ n there exists a number k ∈ N such that v(i) = L Ai k . The 0 is the vector-clock where all entries are the language with just the empty word L 0 . Consider now a set of elements of A. We say that the set V of elements of A is t-homogeneous if the following conditions are satisfied:

• for each v ∈ V there exists at most one index 1 ≤ i ≤ n such that v(i) = L 0 , and

• for each v, v ∈ V , if v(i) = L 0 = v (i) then v = v ,
and

• let v = ( i∈I v(i)) \ L 0 if i∈I v(i) = L 0 and v = L 0 otherwise, for each v k ∈ V , there exists w k ∈ v k such that for each i, j, proj (w i , A j ) = proj (w j , A i ).
The first condition states that each vector-clock of a t-homogeneous set has at most a language which is different from the one containing just the empty word, the second one assures that the significant entries of vector-clock are associated to different indexes. The final one assure each significant language contains at least a word which is compatible with a word of the others. Summing up, a t-homogeneous set of vectorclock is composed by vector-clock where the possible entry different from L 0 appears at different indexes, and each vector-clock has at most one entry which is not L 0 . Each operation op i ∈ Op is defined as follows: it takes the vector-clocks v 1 , . . . , v k such that {v 1 , . . . , v k } is t-homogeneous and it returns a vector-clock v such that for each i ∈ I it holds that v(i

) = v j (i) if for some 1 ≤ j ≤ k v j (i) = L 0 and v(i) = L 0 if for all index 1 ≤ j ≤ k it holds v j (i) = L 0 .
The τ in this case acts as follows: it takes an index i, a vector-clock v and a label a, and returns the vector-clock v where all entries but the i-th one are set to L 0 and the i-th one is set to v(i) • {a}.

We can introduce the notion of ticking domain for a trellis process of a multi-clock net N = (N, ν). Recall that with T i we indicate the transition of the subnet N i , with i ∈ ν(m 0 ). Definition 6.17. Let N = (N, ν) be a multi-clock net of cardinality υ(N) = n, where N = P, T, F, m 0 . The ticking domain for the trellis process of N is the quadruple (A, Op, τ, T ) where

• A = {v | ∀i ≤ n. ∃k ∈ N. v(i) = L Ti k }, with 0 = (L 0 , . . . , L 0 ), • Op = {op i : A i → A | 1 ≤ i ≤ n} where op i (v 1 , . . . , v i ) is defined when V = {v 1 , . . . , v i } is t- homogeneous and op k (v 1 , . . . , v i ) = v such that, for each 1 ≤ k ≤ υ(N) v (k) = L 0 if for all 1 ≤ j ≤ i. v i (k) = L 0 and v (k) = v j (k)
for the unique v j such that v j (k) = L 0 , and

• τ : I × A × T → A,
takes and index i ∈ I, a vector-clock v ∈ A and an element t ∈ T , and returns the vector-clock v where

∀j = i. v (j) = L 0 and v (i) = v(i) • {t},
and it is denoted with D tr N .

We need a further notion. As U = (U, f ), with U = (U, ν U ), is a trellis process, then U = B, E, W, c 0 is an unravel net, and in particular, for each b ∈ c 0 , the subnet U b is acyclic and each condition b in U b has a precise distance from b. This distance is the number of conditions preceding b , which is the same in all paths from b to b . We denote this distance with dist(b ). Consider now all the paths from the condition b ∈ c 0 to the condition b belonging to the same partition. These are indeed firing sequences of the subnet U b , and hence can define the language {w | ∃σ ∈ FS U b {b} . lead (σ) = {b } and run(σ) = w} of all the words associated to the paths from b to b which we denote L U b b Proposition 6.18. Let N = (N, ν) be a multi-clock net, where N = P, T, F, m 0 . Let U = (U, f ) be its trellis-process, where U = (U, ν U ). Then U D tr N ,h where • U = (U, ν U ) is a multi-clock net where U = B, E, W, c 0 , f T and ν U are as in Definition 6.14,

• h : B → A is defined as h(b) = v where v(i) = L U ν U (b) b when i = ν U (b) and v(i) = L 0 otherwise, is a spread net over D tr N .
Proof. The annotations of the conditions in the initial marking are clearly 0. The other requirements are easily proved once that one shows that, given an event e in U , {h(b

) | b ∈ • e} is t-homogeneous and that if e ∈ E i , then for the unique condition b ∈ e • such that ν U (b ) = b i ∈ c 0 , h(b ) = v where v(i) = L 0 and dist(b ) = dist(b) + 1. Assume that {h(b) | b ∈ • e} is not t-homogeneous, hence for some b and b in • e we have that, considering v = h(b ) and v = h(b ), v (ν U (b )
) is a language which does not contain any word which is compatible with a word in the language v (ν U (b )). But • e is a ĉo set of conditions, and each condition is annotated with all the local computation of a fixed length marking the conditions in • e, which contradict the assumption, hence {h

(b) | b ∈ • e} is t-homogeneous.
Clearly the op i with i = |{h(b) | b ∈ • e}| is well defined and applied to (h(b 1 ), . . . , h(b j )) returns the vector-clock v, and τ (i, v, f T (e)) concatenates the symbol f T (e) to v(i), hence for the condition in b ∈ e

• such that ν U (b ) = ν U (b i ) with b i ∈ • e it holds that dist(b ) = dist(b i ) + 1.
Example 6.19. Consider the multi-clock net in the Example 5.2. In Figure 8 we show the initial part of its trellis process, with the annotations on the conditions of the net that make it a spread net. The condition b 3 is (p 4 , {t 2 }) and it has as incoming arcs all the arcs coming from all the events labeled with t 2 caused by p 1 , as the language of the component identified by the place p 2 of all the word of length 1 contains just {t 2 }. Remark 6.20. The Proposition 4.16 and Proposition 4.17 show that, given an information domain, one can construct a spread net annotated with the elements of this domain. This can be done also in the case of ticking domain, along the same lines. Indeed this is implied by the trivial observations that the net of a branching process is an occurrence net, and the net of a trellis process is an unravel one. Furthermore the ticking domains considered are regular and revealing and the multi-clock obtained are properly spread.

(ε, ε) b 1 (ε, ε) b 2 (ε, b) b 3 (b, ε) b 4 (a, ε) b 5 (ε, bd) b 6 (bc, ε) b 7 (ab, ε) b 8 (ε, bdb) b 9 (bcb,

Spreading Multi-clock nets

In this section we develop an algorithm to spread a multi-clock net once that a ticking domain D has been selected. Clearly the ticking domain is induced by the net to be spread, and it drives the spreading.

This section is organized as follows: we make precise what the spreading of net is, in analogy to what an unfolding of a net is, then we show how to construct an adequate ticking domain D (Section 7.1) and how to spread a multi-clock net (Section 7.2) with respect to D. Finally, in Section 7.3, we show that indeed the spreading algorithm produces the best spread net.

We start by formalizing what is the spreading S of a multi-clock net N with respect to a domain D.

Definition 7.1. Let N = (N, ν) be a multi-clock net, with N = P, T, F, m 0 , and let D be a ticking domain over T , and let S = (S, ν S ) D,h be a spread net over D, where S = P S , T S , F S , m 0,S . and : T S → T is the labeling mapping. We say that S is a spreading of N if

• there exists a folding morphism f : S → N , and

• for each C = {p 1 , . . . , p i } ⊆ P S subset of places, such that there exists a transition t ∈ T with • t = {f P (p 1 ), . . . , f P (p i )}, and

-op i (h(p 1 ), . . . , h(p i )) is defined,
then there exists a firing sequence σ ∈ FS S m 0,S such that C ⊆ lead (σ).

The spreading of a multi-clock net N is a spread net on a domain which is constructed starting from the components of the multi-clock net N itself and that is folded onto N. The requirements that a spread net has to satisfy, with respect to the net N, ensure that there is a correspondence between the tuples of annotations for which the operations on the vector-clocks elements are defined and the transitions in the net to be spread. Indeed requiring that whenever the annotations of a subset of places in the spread net, mapped to the preset of a transition t, are a tuple for which the operation in the domain is defined, then these places can be reached via a firing sequence, implies that this firing sequence can be extended to another containing a transition of the spread net which will be mapped to t. We recall that in each kind unfolding, if a subset of conditions in the unfolding is mapped to the preset of a transition t in the net, then an event can be added to the unfolding and this event is related to t.

Defining the ticking domain

Given a multi-clock net N = (N, ν), where N = P, T, F, m 0 , we argue on how a domain for the spreading is constructed. As N is a multi-clock net, it easy to define an equivalence relation on the words associated to the firing sequences of each component. This determines the entry associated to this component of a generic vector-clock, and this entry will be the equivalence class of a word on the alphabet determined by the transition of the component (and we can use a word in the equivalence class as the representative). Let A be a finite alphabet, let ∼ be an equivalence relation defined on A * , then with [w] ∼ we denote the equivalence class of w with respect to ∼, i.e. the set {w ∈ A * | w ∼ w }. Definition 7.2. Let N = (N, ν) be a multi-clock net where N = P, T, F, m 0 and let : T → T be the identity labeling mapping. Let I = m 0 be a set of indexes and, for each i ∈ I, let ∼ i be an equivalence relation over Tr(N i ) such that if w ∼ i w then w • u ∼ i w • u. Let P be a property defined on languages over T . Then A is the set of vector-clocks v such that for each i ∈ I. v(i) = [w] ∼i for some w ∈ Tr(N i ), and

P({v(i) | i ∈ I}) holds.
The elements of each vector-clock are equivalence classes, and when no confusion arise, we just write v = (w 1 , . . . , w n ) instead of v = ([w 1 ] ∼1 , . . . , [w n ] ∼n ). The predicate P ensures that the various elements have the proper shape (there exists an execution in the component with this shape) and it mixes the visions of each component on the behaviours of the other components. Furthermore P reflects the fact that it must represent a feasible computation of the whole net. In general we assume that, given a vector-clock v, for each i, j ∈ I (with I the set of indexes of the multi-clock), the words w i ∈ v(i) and w j ∈ v(j) represent compatible local computations, and the word w in T * obtained mixing all these words in such a way that proj (w, T i ) = w i , is an execution of the net.

The second ingredient we have to devise concerns the operations in Op. When discussing branching processes and trellis processes we have assumed the existence of a suitable predicate, e.g. the bp-homogeneity in the case of branching processes. We push this idea a bit further. We need to define when a set of vectorclocks are homogeneous, and to this aim we introduce a predicate, which is defined on sets of vector-clocks. Definition 7.3. Let N = (N, ν) be a multi-clock net. Let A be a set of vector-clocks satisfying P as in Definition 7.2. Let H be a predicate defined on subsets of vector-clocks. We say that the set

V = {v 1 , . . . , v k } is homogeneous if H(V ).
The predicate H is usually inferred by the firing sequences of each component. For instance one can say that H(V ) holds for the set of vector-clocks such that for each word in v i (j) there exists a word w ∈ v k (m) and proj (w, T m ) = proj (w , T j ). This predicate captures the minimal idea that for each local computation σ i in a component there exists a local computation σ j in another component that is coherent with σ i . We stress the fact that this is indeed what it is done usually when constructing the branching or the trellis process of a multi-clock net, but it is also what is basically done when constructing the merged process of a multi-clock net (see [START_REF] Khomenko | Direct construction of complete merged processes[END_REF]).

The operations are defined for homogeneous sets of vector-clocks, and what they do is to return a set of vector-clocks obtained by suitably combining the words of various languages. To this aim we assume the existence of a partial function g that takes as input a tuple of words and return an homogeneous vector-clock. Definition 7.4. Let N = (N, ν) be a multi-clock net. Let A be a set of vector-clock values as in Definition 7.2 and let I be the index set associated to N. Let g :

T * 1 × • • • × T * n
A be a partial function. For each 1 ≤ i ≤ |I| define op i : A i 2 A as the mapping taking a i-tuple of vector-clocks (v 1 , . . . , v i ) such that {v 1 , . . . , v i } is homogeneous, and returning the set vector-clock values defined as {v | ∀i, j.

∃w i ∈ v j (i) ∧ g(w 1 , . . . , w n ) = v}.
The intuition here that op i takes a tuple of local computations (that are compatible as the associated vectorclock is homogeneous) and returns a set of vector-clocks, where each vector-clock is induced by a specific tuple of words using the mapping g. A regular domain is a domain where, given a set if vector-clocks that are homogeneous, the g mapping returns always just one value.

The final ingredient of a ticking domain is the τ which implements the updating of the piece of information. A vector-clock v contains for each component an equivalence class of words, and then the ticking mapping just concatenates the symbol to the words in the equivalence class, when the concatenation is defined, i.e. the symbol belongs to the alphabet. Definition 7.5. Let N = (N, ν) be a multi-clock net, where N = P, T, F, m 0 , and let ∼ p be a an equivalence relations over words in T p for each p ∈ m 0 Let P be a predicate over tuple of languages, and H be a predicate on vector-clocks in A induced by ∼ p and P. Let g be a partial mapping from T * 1 × • • • × T * n to A. Then D P,H N induced by P, H and g is the quadruple (A, Op, τ, T ) where A is defined according to Definition 7.2, Op is defined according to Definition 7.4 and τ implement the chosen updating mapping, is a ticking domain for N.

To illustrate how domains are obtained we review briefly some of examples of the previous section and we provide a new one.

Example 7.6. For the 1-unfolding the property is the one devised in the previous section, namely that just one entry of the vector-clock is not the empty word, and furthermore the only significant entries can be just the counting one. The equivalence relations are trivial: for each component every word is equivalent to the empty word, and for the counting one each word is equivalent to itself. The other ingredients can be easily retrieved. Also the H predicate is obvious, as well as the g mapping.

In the case of the branching process of a multi-clock net, the property is the one stating that a vector-clock (w 1 , . . . , w n ) is such that ∀i, j ∈ {1, . . . , n}. proj (w i , A j ) = proj (w j , A i ). The operations are defined if the tuple of vector-clocks are bp-homogeneous (thus for each component there is a maximum) and the result is given by the maximum applied component-wise. The ticking function just concatenate a label to the proper entry of the vector-clock.

Example 7.7. Consider the multi-clock net (N, ν) in Figure 9. The net has three components, one defined

v 0 = (ε, ε, ε) = 0, v 1 = (ε, t 1 , ε), v 2 = (ε, t 2 , ε
) and v 3 = (ε, t 1 t 1 , ε), thus the domain is finite. The H is defined for all of them and the operations op i are as follows op

2 (v 0 , v 0 ) = op 2 (v 1 , v 0 ) = op 2 (v 0 , v 2 ) = {v 0 }, op 2 (v 1 , v 2 ) = op 2 (v 2 , v 1 ) = {v 1 , v 2 } which implies that the domain is not regular, finally τ (v 0 , t 1 ) = v 1 , τ (v 0 , t 2 ) = v 2 τ (v 1 , t 2 ) = v 2 and τ (v 2 , t 1 ) = v 1 .
The fact that, for instance, op 2 (v 2 , v 1 ) gives {v 1 , v 2 } depends from the fact that the piece of information conveyed by this domain is that the annotations depend on the order on which transitions t 1 and t 2 are performed. Now the choice of which of the possible results in the set {v 1 , v 2 } has to be taken depend by the g mapping which is defined as g(t 1 , t 1 t 2 , t 2 ) = v 2 and g(t 1 , t 2 t 1 , t 2 ) = v 1 .

Spreading Algorithm

We now present an algorithm to spread a multi-clock net. We recall briefly how an unfolding algorithm works. In the initialization phase a set of conditions corresponding to the initial marking is created and it is related to the initial marking via a folding morphism. Then, for each subset of conditions reachable via a firing sequence that is mapped (via the folding morphism) to the preset of a transition t, a new event labeled t is added to the unfolding, if not present, together with conditions produced by this event and related to the postset of the transition t. This step is iterated and this procedure either terminates when no new event can be added or, if it does not terminate, produces at each step a part of the unfolding, the limit of which is the unfolding itself.

To adapt this procedure to the spreading, we need a notion that is the semantic counterpart of the more classical notion of concurrent places used in unfoldings. Definition 7.8. Given a multi-clock net N = (N, ν) where N = P, T, F, m 0 , we say that C ⊆ P is free of conflict if there exists a firing sequence σ ∈ FS N such that C ⊆ lead (σ).

We are now ready to present the algorithm to spread a net with respect to a specific ticking domain, constructed as we have previously devised, which is shown in Figure 10. In the algorithm we use (w 1 , . . . , w n ), where each w i is a word on an alphabet A i , to denote the set of words on n i=1 A i obtained shuffling the words w i , namely proj (w, A i ) = w i for each i and w ∈ (w 1 , . . . , w n ). We make just few comments on this algorithm, as it is the adaptation to this setting of the general algorithm to unfold a net. Indeed the main differences are that we do not only check whether a subset of conditions are reached using a firing sequence, but also that the operation op i of the domain is defined. The outcome of the algorithm is a finite net only in the case where the domain contains a finite number of vector-clock values, otherwise it produce a spread net and a folding morphism at each iteration. Theorem 7.9. Let N = (N, ν), where N = P, T, F, m 0 , be a multi-clock net and let D be a domain over T . Let S = (S D,h , f ) be the result of the spreading algorithm in Figure 10. Then S is a spread net and f : S → N is a folding morphism.

Proof. Clearly S D,h is a spread net by construction. The annotation of the condition in the initial marking is the 0 of the domain, and for each set of conditions C ⊆ B which is free of conflict, namely a reachable subset in the net S, we have that if there is an event e such that • e = C then op i (h(C)) is defined, and the annotation of the conditions in the postset is obtained by the τ applied to f T (e) and a vector-clock in op i (h(C)). The requirement that the annotation is uniform on the various events in the preset of a condition is guaranteed by construction, as we add a new condition mapped on the same place only if the annotation calculated for the condition is not present. Thus all the requirements of Definition 4.1 are fulfilled. Also f is a folding morphism, as indeed f P and f T are total mappings and fulfill the conditions posed on folding morphisms, as by construction, for each event e in E, f T define a bijection on • e and e • . The parsimony requirement is again satisfied by construction. This result has as a consequence that the spreading algorithm applied to a multi-clock net N with respect to a domain D gives a net which is the spreading in the sense of Definition 7.1. • set fT (e) = t, • set νO(p ) = φ -1 P (νO(p)) Let B be the set of the new added conditions, E be the set of added events and W be the added arcs, ν S be the extension of νS to the new added places, then S = ( B ∪ B , E ∪ E , W ∪ W , C0 , ν S , )Dh is the resulting spread net and f the folding morphism. classes are identified with their representative. Finally the property P they have to satisfy is that they are compatible, namely that for each element in the first component there must be an element in the second component and such that both agree on common symbols.

• for each index 1 ≤ i ≤ |C| check if there is a condition b i ∈ B such that h(b i ) = τ (i, v, t)
The predicate H stipulate that v and v are homogeneous whenever ∃w ∈ v(1) and w ∈ v(2) such that proj (w, A 1,2 ) = proj (w , A 1,2 ). The operation op 1 just return the same vector-clock, the operation op 2 (v, v ) returns the vector-clock (v(1), v (2)). Finally the τ concatenates the symbol to the proper entry of the vectorclock.

In the figure places are annotated with the pair (a, v) where a is the place in the net N and v is a vector-clock. The result of the spreading is in Figure 12. The domains considered so far have been always regular domains. The next example discuss the construction in the case the domain is not a regular one.

Example 7.12. In Figure 13 we show the spreading of the multi-clock net in Example 7.7. The domain and the operation are those devised in the Example 7.7. Each condition is decorated with the annotation (v i ), its internal name b k and to which place in the multi-clock net is mapped to, and the same for the events, where the label is inside the event itself. Observe that b 3 and b 8 are annotated like b 6 and b 9 , but the execution of e 5 and e 6 gives different annotations, as e 5 depends on the fact that in the net N the transition b is executed first and e 6 depends on the fact that in the net N the transition a is executed first. With the aid of this notion we can show the following result, which basically state that the spreading algorithm gives us the best result possible, as all the other spreadings are related to this one, when the domain is regular. Theorem 7.14. Let N = (N, ν) be a multi-clock net and let D N be the associated domain (with respect to P, H and g). Assume that D N is regular. Let S = (S D N ,h , f ) be the spreading of N with respect to D N , and let S D N ,h be another spread net with respect to D N such that there exists a morphism g : S → N . Then there exists a unique morphism h : S → S which is annotations preserving.

v 0 b 2 p 2 v 0 b 1 p 3 v 0 b 0 p 1 v 2 b 3 p 2 v 2 b 4 p 3 v 1 b 5 p 3 v 1 b 6 p 1 v 1 b 7 p 3 v 1 b 8 p 1 v 2 b 9 p 2 v 2 b 10 p 3 v 2 b 11 p 1 v 2 b 12 p 2 v 1 b 13 p 1 v 1 b 14
Proof. Consider a spread net S D N ,h where S = (S , ν S ) and S = B , E , W , C 0 , being the labeling induced by the folding morphism, and assume that there exists a folding morphism g : S → N . As each event in a spread net can be executed, we can associate to each event e a depth which is the length of the shortest firing sequence leading to it. Formally depth(e) = min({|run(σ)| | σ ∈ FS S . σ [e }), and this is well defined. We can define the subnets S i of S as follows: the events E i are the set of events {e ∈ E | depth(e) ≤ i}, the conditions are

B i is C 0 ∪ • E i ∪ E i
• , the initial marking is C 0 and the flow relation W i is the restriction of W to the conditions and events in B i and E i respectively. The information mapping h i is the restriction of h to the places in B i .

We now construct the unique mapping k from S to S as follows. First, for each b ∈ C 0 , we set k P (b ) = b such that b ∈ C 0 and f P (b) = g P (b ). This define the morphism k 0 . The morphism is obviously annotation preserving as S D N ,h is a spread net with respect to D N . Now consider the events in E which have depth equal to 0. These are events that are enabled at the initial marking C 0 . Consider the event e such that • e ⊆ C 0 . In the spreading of N we have that the event e corresponds to the transition g T (e ), and then we set h 1

T (e ) = e and to each condition in the postset of e we associate the condition in the postset of e belonging to the same component, and we do this for all the events in E with depth equal to 0. In this way we define k 1 . Iterating the procedure we construct, for each > 0i, a morphism k i from S i-1 to S. Each of the morphism is, by construction, annotation preserving. The limit of this construction gives the desired morphism.

We have to show that this is unique. Assume there is another one, say l. Being a different morphism, and being S a spread net, there should be an event, say e at depth n, which is mapped by k to e 1 and by l at another e 2 . But this is possible only if the domain is non regular, as in this case there could be a choice of the possible events associated in the spreading to the transition g T (e ). Hence the thesis.

Discussion

On constructing domains. The results in the previous section show that spreading a net can give a more compact representation of the behaviour of net with respect to many approaches. Using the notion of domain is possible to introduce much more different criteria with respect to the one introduced in literature to compress these structures. The key ingredient for the spreading of a multi-clock net is clearly the notion of ticking domain. We have seen abstractly how to construct a ticking domain for a multi-clock net. We discuss on how to do this in a more concrete and uniform way, by providing some examples and foreseeing some techniques.

Consider the multi-clock net N = (N, ν) where N = P, T, F, m 0 , and consider the automaton N p with p ∈ m 0 . The equivalence relation on which each element of the ticking domain is defined is clearly an equivalence relation defined on the language L Np = {run(σ) | σ ∈ FS Np {p} }, and we can look at a uniform way to define this equivalence relation when this equivalence relation is of finite index. We do not see this as a limitation as we are introducing spread nets to have a finite and compact representation of the behaviours of a net. To this aim we can imagine that the equivalence relation we are interested in may quite well be represented as equivalence relation induced by a finite state automaton. Consider then a finite state automaton D p = (Q, T p , δ, q 0 , F ), the equivalence on two words w, w ∈ L Np is then defined as δ(q 0 , w) = δ(q 0 , w ) where δ is the extension on words of the transition function δ : Q × T p → Q which is defined classically.

The Figure 14 illustrates some possibilities. For simplicity we identify the domain with the finite state automaton which define the desired equivalence relation. Consider the net automaton N 1 with just two transitions a and b in Figure 14. For this net automaton we can put forward some finite state automata defining equivalences on the words on the alphabet {a.b}. The automaton D 1 conveys the idea that all the computations containing at leas one symbol of the net automaton N are to be considered as equivalent, the D 2 that all the computations have to be considered equivalent, the D 3 has three equivalence classes, depending on the number of a (zero, one or two), the third has four equivalence classes, one contains just the empty word, the second the words where a and b alternates, the starting symbol is a and the final one is b, the D 3 the words where a and b alternates, the starting symbol is b and the final one is a, and the D 4 equates all the words where there are at least two adjacent equal symbols. The figure shows their spreading (in the spreading we omit to indicate to which place the conditions are mapped as it is obvious). For the net automaton N 2 we consider the finite state automaton D 5 in . The spreading is the spread net S 5 in the same figure. The previous example suggests that many of the interesting equivalences where also time is folded are easily represented as a finite automata.

An issue is now on how to introduce a domain that is able to characterize the fact that each transition is observably executed. We can then imagine that, given a component N p of a multi-clock net, it is possible to associate a finite state automaton representing this. Given a net automaton N = P, T, F, {p} , the automaton can be constructed as follows: states are triple (p , i, t) where p ∈ P , i is the distance of p from p, and t ∈ T is a transition putting a token in p or ⊥ if p is p. The distance is the shortest path from p to p . Consider again the finite state automaton D 5 in Figure 14. This is obtained by the net automaton N 2 as follows: q 0 is (p 0 , 0, ⊥), q 1 is (p 0 , 0, a), q 2 is (p 1 , 1, b) and q 3 is (p 0 , 0, c). Clearly the distances in this net automaton are 0 and 1. The transitions with an incoming arc in the place p 0 are a and c, whereas the only one with an incoming arc in the place p 1 is b. Thus the only possible obtainable states are q 0 , q 1 , q 2 and q 3 . The δ is defined almost accordingly to the firing mapping ' [• ' of the net automaton. We stipulate that δ((p, i, t), t ) is either equal to (p , i + 1, t ) if there exists a state (p , i + 1, t ) and {p} [t {p } or the state (p, j, x) for j < i, with x equal to t or ⊥ and there exists a path in the automaton from (p, j, x) to (p, i, t). In the spreading S 5 the events folding the time are e 4 , e 5 and e 6 .

Consider again the multi-clock net in Figure 9, but now consider the domains induced by the finite state automata in Figure 15. The elements of the ticking domain are constructed using the same predicate we defined previously. The vector-clocks are v 0 = (ε, ε, ε), v 1 = (a, a, ε), v 2 = (ε, b, b), v 3 = (a, ε, b) and v 4 = (ac, ε, bc). The operations on the domain are defined as follows:

op 2 (v 0 , v 0 ) = v 0 , op 2 (v 0 , v 1 ) = v 1 , op 2 (v 0 , v 2 ) = v 2 and op 2 (v 1 , v 3 ) = v 3 = op 2 (v 2 , v 3 ). τ (v 0 , a) = v 1 , τ (v 0 , b) = v 2 , τ (v 1 , b) = v 3 , τ (v 2 , a) = v 3 p1 p 1 p 1 a c p3 a b p2 p 2 p 2 b c N p1 N p3 N p2 start (p1, 0, ⊥) (p 1 , 1, a) (p 1 , 2, c) a c start (p0, 0, ⊥) (p0, 0, a) (p0, 0, b) a b a, b a, b start (p2, 0, ⊥) (p 2 , 1, b) (p 2 , 2, c) b c D p1 D p3 D p2
Figure 15: The three components of the multi-clock net in Figure 9 and the finite state automata associated to each of them.

and τ (v 3 , c) = v 4 . The spreading with respect to this domain is the one depicted in Figure 16. Observe that there is no any longer a confusion, as the domain is now regular. Merged processes. In Section 6 we have presented various kinds of unfolding and discussed how they can be seen as spread nets on suitable domains. The common characteristic of these unfolding is that there exists a direct representation. The notion of merged process has been left out, but also merged processes can be seen as spread nets.

v 0 b 2 p 2 v 0 b 1 p 1 v 0 b 0 p 3 v 2 b 3 p 2 v 2 b 4 p 3 v 1 b 5 p 3 v 1 b 6 p 1 v 3 b 7 p 3 v 3 b 8 p 1 v 3 b 9 p 2 v 4
We recall how a merged process is defined. Starting from a branching process, the conflicting conditions that satisfy the requirements • are equally labeled (i.e. mapped to the same place of the net to be unfolded), and

• in the past of each of them the number of conditions bearing the same label of the final one is the same can be merged, that means that they are identified. Consider the multi-clock net in Figure 5 and the part of its branching process depicted in Figure 7. There the conditions b 4 , b 9 and b 17 can be identified as they are mapped on the place p 3 and in their past there is no condition with the same label. If we look at the annotations of these conditions, it is easy to see that just one occurrence of the transition b has been executed and being this transition the only one putting a token in the place p 3 , all the local execution in the left component where the transition b has fired just once have to be considered equivalent. The elements of the ticking domain are then vectors of languages where, for each place in each component, the language contains all the traces associated to the firing sequences of the component putting in the place the i-th token. The property of the vectors-clock is the usual one, each of the language must contain an execution which is compatible with one of the other components.

The following figure show the initial part of the merged process obtained by the initial part of the branching process. The annotations are the vectors of languages, that here are represented as regular expressions. 0 is (ε, ε), v 1 is (a * b, b), v 2 is (a + bc, b + ε), v 3 is (a * b, bd), v 4 is ((a + bc)(a + bc), bd + b + ε), v 5 is ((a * + bc)b, bdb) and v 6 is ((a + bc)(a + bc)(a + bc), bdbd + bd + b + ε) are those annotating the conditions shown in the Figure 17. For a discussion on how to obtain these annotations we refer to [START_REF] Casu | Flow unfolding of multi-clock nets[END_REF].

Composing spread nets and information domains. Multi-clock nets come equipped with a clear operation on how these can be composed: the multi-clock net N = (N, ν) resulting from the composition of two multi-clock nets N 1 = (N 1 , ν 1 ) and N 2 = (N 2 , ν) has as places the union of the places (that are disjoint), as transitions the union of the transitions (that may be not disjoint) and the other components are defined accordingly in such a way that restricting to the places and transitions of a N i ones get exactly N i . Similarly one may imagine a way of composing ticking domains provided that the property the vector-clock of the compound ticking domain is known, which is normally the case. The new elements of the ticking domain are just vectors that are obtained by those of the two ticking domains and that satisfy the property, and the other operations are easily definable. It is then clear that the composition of the two spread nets that are the spreading of N 1 and N 2 (spreading with respect the proper ticking domains) will give the spread net which is the spreading of N with respect to the compound ticking domain.

On a categorical setting. Beside the notion of spread net we have formalized the algorithm for spreading a net, which is basically the same algorithm which is used to unfold a net and we have shown that under the assumption that the domain is regular, the spreading construction can be considered the best one. The above consideration suggests that a categorical treatment is possible.

One should start stating what is a multi-clock net over a domain hence not necessarily a spread one. Let N = (N, ν) be a multi-clock net where N = P, T, F, m 0 , and D = (A, Op, τ, Lab) be a domain. Then N = N D,h , where h : P → A, is a multi-clock net over a domain D. With respect to the notion of spread net, the annotations on places are not subjected to any constraints, hence a net over a domain is simply a net where places are annotated with elements belonging to the set A.

The notion of mapping relating domains can be the following one. Let D = (A, Op, τ, Lab) and D = (A , Op , τ , Lab ). Then a domain mapping is the triple φ = (φ lab , φ dom , φ op ) where φ lab : Lab → Lab , φ dom : A → A and φ op : Op → Op are (partial) mappings such that

• φ dom (0 A ) = 0 A ,
• for all V ⊆ A and for all op i ∈ Op, if op i (V ) is defined and equal to V ⊆ A, then also φ op (op i )(φ dom (V ))

is defined and φ of (op i )(φ dom (V )) = φ dom (V ), and

• φ dom (τ (i, v, a)) = τ (i, φ dom (v), φ lab (a)).

The requirements we put on the mappings between domains is that the 0 of the first domain is mapped onto the 0 of the second domain, and that the operations are preserved. Clearly domain mappings compose.

We have to specialize the notion of morphism on multi-clock nets in order to take into account domains. Recall that, given two multi-clock nets N = (N, ν) and N = (N , ν ), a morphism f : N → N is net morphism such that the partitions are preserved. Let N = N D,h and N = N D ,h be two nets over a domain. Then the pair f = (f, φ) is a morphism whenever f is a net morphism, φ is a domain mapping and φ dom (h(p)) = h (p ) for all p such that (p, p ) ∈ f P .

It is then easy to see that nets over a domain and morphisms between them form a category, called DomNet. It is enough to show that nets morphisms compose, as well as domains mappings. Let f = (f, φ) : N → N and f = (f , φ ) : N → N be two morphisms. Then f • f = (f • f , φ • φ ) : N → N is a well defined morphism and φ dom • φ dom (h(p)) is φ dom (φ dom (h(p)) and, as f is a morphism, for each p such that (p, p ) ∈ f P we have that φ dom (h(p)) = h (p ). Now also f is a morphism, hence for each p such that (p , p ) ∈ f P we have φ dom (h (p )) = h (p ), but then also for each (p, p ) ∈ f P • f P we have that φ dom (φ dom (h(p)) = h (p ). The subcategory of spread net over a domain is the category where objects are spread nets and it is called Spread. With this treatment, we have that the Theorem 7.14 account to say that the spreading define a universal arrow.

Conclusions and future works

In this paper we have proposed the notion of spread net as the net capable of representing the different net based semantics presented in literature. The various unfoldings can be seen as spreadings with respect to specific information domains. We have then applied the notion to multi-clock nets, where the behaviour of the whole net can be obtained by the behaviours of the components. A spread net is a net where each place has an annotation representing the amount of information that has been collected to produce that place, and the piece of information depends on two elements. One element is the piece of information inferred from the annotations of the places in the preset of the transitions in the preset of that place, and the second element is the transition itself.

Spread nets may easily fold conflicts which account to consider as equivalent computations representing conflicting alternatives, as it is done in trellises processes or in merged processes, but, differently from these approaches, they may fold as well time, thus qualifying for a finite representation of possible infinite behaviours. The capability of folding time resembles the notion of concatenation introduced on non-sequential behaviors of nets, whereas the capability of folding conflicts can be considered similar to the so called collective tokens interpretations in Petri nets. According to this interpretation, the way a token is produced does not influence the subsequent use of it (see [START_REF] Pinna | How much is worth to remember? a taxonomy based on Petri Nets Unfoldings[END_REF] for the various approaches presented to unfold a net with respect a token interpretation [START_REF] Van Glabbeek | The individual and collective token interpretation of Petri nets[END_REF]).

The spreading of multi-clock nets has the advantage of being able to unfold each component according to a criterion, and this criterion is not necessarily the same one for all the components, as it is in the existing approaches. Thus we allow that certain components of the net are executed according the individual token philosophy (meaning the the whole history is preserved) or the collective token philosophy (meaning that all the histories are equated) or other different interpretations, where some computations are equated depending on suitable criteria. Clearly what is developed for multi-clock nets may as well be applied to any kind of net where a clear understanding of what the components are and how they do interact.

In this paper we have considered either information domains tuned to express the various kinds of unfolding, or very simple ones, without making any real consideration on the kind of properties one would like to express on the system whose behaviours is described by the spread net. In a sense the target of the paper has been the setting of a framework to express the semantics of nets, based on spread nets and the spreading of a net, hence we have not focussed on the properties an information domain can or should express. Indeed the main advantage of the framework proposed is the fact that it that the act of spreading a net is somehow independent on the chosen information domain, which is a parameter of the algorithm, and then it can be used in quite different contexts. The choice of the information domains influences the properties one would like to characterize. We can then imagine to find information domains which characterize prefixes of a net, or information domains enforcing some other property. We can also imagine to have a way to synthesize information domains starting form the properties one would like to observe, and some suggestions are indeed present in Section 7 and Section 8, but these are just a basis for a theory of information domains. We stress again that the kind of semantics represented in particular spreading depends on the information domain chosen and hence on the properties one would like to focus on.

We have not yet investigated an interesting issue, namely what is the brand of event structure related to spread net, like it is done in [START_REF] Van Glabbeek | Configuration structures, event structures and Petri nets[END_REF]. However we believe that configuration structures can be easily related with spread nets, hence part of the results presented there should be applicable also in our setting. Clearly the kind of event structure related to spread nets will be somehow parametric on the kind of annotations of the spread net.

The categorical treatment of spread nets has to be further investigated. In the previous section we have put forward some ideas. We are confident that this is the correct direction, and the gain of setting the approach in a categorical framework will give us constructions like products for free. Certainly once fixed the kind of information domain, the categorical treatment follows the usual lines, with some advantages, for instance the pieces of information can be used to sort out which transitions have to be synchronized in two spread nets.

Example 4 . 2 .

 42 Consider the information domain D = (A, Op, τ, Lab), with Lab = {a, b, c, d, e}, where A = {0, α, β, γ}, (with the elements defined over Lab, for instance 0 = ∅, α = {a}, β = {b}, γ = {c} and δ = {d}), Op contains op 1 defined as op 1 (0) = {0, α} and op 1 (γ) = {0}, and op 2 defined as op 2 (2β) = {β} and op 2 (0+α) = {0}, and τ is defined as τ (0, a) = 0, τ (α, a) = α, τ (0, b) = β = τ (α, b), τ (α, c) = τ (β, d) = γ and τ (0, e) = 0. The net in Figure 1 is a spread net with respect this information domain with the following information mapping h(p 0 ) = 0, h(p 1 ) = 0, h(p 2 ) = α, h(p 3 ) = h(p 4 ) = β and h(p 5 ) = γ.

Figure 1 :

 1 Figure 1: A spread net

Example 4 . 8 . 3 Figure 2 :

 4832 Figure 2: An 1-occurrence net annotated with an information mapping on D ⊥

  is a finite set, and 5. the relation # C ⊆ E × E defined as • e # i e iff e = e and • e ∩ • e = ∅, and

Proposition 4 . 10 .

 410 Let C = B, E, W, c 0 , be a labeled occurrence net where is the identity, let D = (A, Op, τ, E) be the domain where A = 2 E fin , with 0 = ∅, each op i ∈ Op is defined as op i (X) = {A | X(A) = 0} and τ (A, e) = A ∪ {e}, and let the information mapping h : B → A defined as h(b) = {e ∈ E | e ≤ C b}. Then C D,h is a spread net over D.

b 5 {e 2 , e 4 } b 4 {e 2 , e 4 , e 6 } b 6 {e 1 , e 3 , e 5 } b 7 {e 2 , e 4 , e 8 } b 8 {e 1 , e 3 , e 7 8 Figure 3 :

 5224613724813783 Figure 3: an occurrence net annotated on the information domain formed by subsets of events

  and it is the set of local histories of the event e. With e e we denote {X | X ∪ {e} ∈ e }, i.e. each subset in e without e.

{∅} b 1 {∅} b 2 {{e 1 3 {{e 1 5 {{e 4 }} b 4 {{e 1 6 {{e 1 6 Figure 4 :

 1213154416164 Figure 4: An unravel net

Proposition 4 . 16 .

 416 Let (E, ≤, #) be a prime event structure, let D = (A, Op, τ, E) be the domain whereA = {X ⊆ E | X = e \ {e}} ∪ {X ⊆ E | X = e }, each op i ∈ Op is defined as op i (X) = {A | X(A) = 0}and τ (A, e) = A ∪ {e}, and let C D,h be a spread net where C is the tuple B, E, W, c 0 , with B = {( e , e) | e ∈ E} ∪ {(∅, e) | e ∈ E} and h((X, e)) = X, W = {(e, b) | h(b) = e } ∪ {(b, e) | h(b) ⊂ e ∧ ∀e ∈ e \ h(b). h(b) ⊆ e }, c 0 = {b ∈ B | h(b) = ∅}, and is the identity. Then C is an occurrence net. Proof. Consider C = B, E, W, c 0 , and the information mapping h : B → A. As ∅ ∈ A and C D,h is a spread net we have that all the conditions b such that h(b) = ∅ are such that • b = ∅. For each b ∈ B we have that | • b| ≤ 1. Assume it not the case, this means that there are at least two events e, e in • b and (e, b), (e , b) ∈ W , but then e = h(b) = e and as (

Figure 5 :

 5 Figure 5: A multi clock net and its two components

Proposition 6 . 3 .

 63 Let N = (N, ν) be a multi-clock net and N = ( N , ν) its enrichment. Let m defined as as m(p) = m(p) if p ∈ P and m(p t ) = 1, and let its extension to firing sequences defined as m [t σ = m [t σ. Then FS N m0 = FS N m0 and M N = M N .

Definition 6 . 7 .

 67 Let N = (N, ν) be a multi-clock net, where N = P, T, F, m 0 and n = |T |, and let N its enrichment. The ticking domain for the 1-unfolding of N, denoted with D 1unf N

Proposition 6 . 8 .

 68 Let N = (N, ν) be a multi-clock net, where N = P, T, F, m 0 , and let N its enrichment. Let O = (O, f ) be its 1-unfolding. Then O D 1unf N ,h where • O = (O, ν O ) is the labeled multi-clock net where O = B, E, W, c 0 , f T is obtained by the multi-clock (O, ν O ) constructed in Definition 6.4, and

2 .

 2 let e , e ∈ {|x e |} such that f T (e ), f T (e ) ∈ alph(N p ), then either e ≤ C e or e ≤ C e , i.e. two events belonging to the same component are ordered. 3. let B e = {b | b ≤ C e}, clearly there exists a b 0 ∈ c 0 and b 0 ∈ B e . Consider all the conditions belonging to the same component, and call them B p for p ∈ m 0 . Then B e ∩ B p is a totally ordered set and provided that f P (b 0 ) = p ∈ m 0 , we have that {|proj (f T (w e ), T p )|} = (B e ∩ B p ) • . It is then clear what could be the annotation associated to each condition b of this occurrence net: it is a tuple (w p1 , . . . , w p1 ) where each w pi = proj (f T (x e ), T p ) with e ∈ • b and {p 1 , . . . , p n } = m 0 . The w pi

Proposition 6 . 12 .

 612 Let N = (N, ν) be a multi-clock net, where N = P, T, F, m 0 . Let C = (C, f ) be its unfolding, where C = (C, ν C ). Then C D bp N ,h where • C = (C, ν C ) is the labeled multi-clock occurrence net where C = B, E, W, c 0 , f T and ν C are as in Definition 6.9, and • h : B → A is defined as h(b) = (w p1 , . . . , w pp ) where w p1 = proj (f T (x e ), T p1 ) and X e is any linearization of {e | e ≤ C e} compatible with ≤ C }, is a spread net over D bp N .

Figure 7 :

 7 Figure 7: The spread net obtained by the initial part of the branching process of Figure 5

Figure 8 :

 8 Figure 8: The spread net obtained by the initial part of the trellis process of Figure 5

Figure 9 :

 9 Figure 9: A multi-clock net with three components where the order of execution may play a rôle

  Input: A multi-clock net N = (N, ν) where N = P, T, F, m0 and a ticking domain D = (A, Op τ, T ) based on P, H and g.Output:At each step a spread net S = (S, νS) D,h , where S = B, E, W, C0, , and a folding mapping f from S to N . Initialization step: Create |m0| conditions for S, called C0 and define a bijection fP : C0 → m0. Set νS(b) = b Define, for each b ∈ C0, h(b) = 0, and set S = C0, ∅, ∅, C0, where : ∅ → T is the obvious function. Finally set f as (fP , fT ) where again fT : ∅ → T is the obvious mapping. Recursion: Consider the spread net constructed so far S D,h , where S = (S, νS), with S = B, E, W, C0, , and the mapping f : S → N . Let C = {b1, . . . , bn} ⊆ B be a non empty subset of conditions such that • ∀b, b ∈ C. νS(b) = νS(b ) implies b = b , • op |C| ({h(b) | b ∈ C}) is defined, • C is free of conflict, and • there exists a transition t ∈ T such that • t = fP (C). Check if E contains an event e such that • e = C and fT (e) = t. If yes consider another subset C of B. If not then, consider the element v ∈ op |C| ({h(b) | b ∈ C}) and it is such that g(w1, . . . , w |C 0 | ) = v, w ∈ (w1, . . . , w |C 0 | ) and there exists a firing sequence σ ∈ FS S such that b ∈ lead (σ) and tr(σ) = w = fT (run(σ)), introduce an event e ∈ E and • add e to E and set (e) = T , • for each bi ∈ C add to W the pair (b i , e),

  and fP (b i ) = pi with pi ∈ t • , and if yes then add (e, b i ) to W , if not then add a new condition b i to B, add (e, b i ) to W , set h(b i ) = τ (i, v, t), νS(b i ) = νS(bi) and fP (b i ) = pi

Figure 10 : 2 Figure 11 :

 10211 Figure 10: The spreading algorithm

Figure 12 :

 12 Figure 12: The spreading of the net in Figure11

6 Figure 13 : 7 7. 3 .

 61373 Figure13: The spreading on the net in Figure9with the respect to the domain inExample 7.7

5 Figure 14 :

 514 Figure 14: Two net automata N 1 and N 2 , five finite state automata for equivalence relations on words over {a, b} (D 1 , D 2 , D 3 and D 4 ), a finite state automaton for an equivalence relation on words in {a, b, c} (D 5 ), the spreading S i of N 1 with respect to the domains D i , 1 ≤ i ≤ 4 and the spreading S 5 of N 2 with respect to the domain D 5

6 Figure 16 :

 616 Figure 16: The spreading of the net in Figure 9 with respect to the domain induced by the automata for the local prefixes

9 Figure 17 :

 917 Figure17: The initial part of the merged process of the net in Figure5

  3 } (the one of the first component), {t 2 , t 3 } (the one of the second component) and {t 1 , t 2 } (the one of the third component) are the following: in the first component and the second component every word is equivalent to ε, in the third the equivalence is defined as follows: t 1 ∼ t 2 t 1 , t 2 ∼ t 1 t 2 , t 1 t 1 ∼ t 2 t 2 and for each w ∈ {t 1 , t 2 } * we have that t 1 t 1 w ∼ t 1 t 1 and t 2 t 2 w ∼ t 2 t 2 . The predicate P over the vector-clocks induced by this domain is the trivial one: every vector-clock satisfy the property. Observe that there are just four vector-clocks:

Acknowledgment. We would like to thank the anonymous reviewers for their useful criticisms and suggestions that have helped us to greatly improve the paper.