Bas Luttik

Unique Parallel Decomposition in Branching and Weak Bisimulation Semantics

We consider the property of unique parallel decomposition modulo branching and weak bisimilarity. First, we show that totally normed behaviours always have parallel decompositions, but that these are not necessarily unique. Then, we establish that finite behaviours have unique parallel decompositions. We derive the latter result from a general theorem about unique decompositions in partial commutative monoids.

Introduction

A recurring question in process theory is to what extent the behaviours definable in a certain process calculus admit a unique decomposition into indecomposable parallel components. Milner and Moller [START_REF] Milner | Unique decomposition of processes[END_REF] were the first to address the question. They proved a unique parallel decomposition theorem for a simple process calculus, which allows the specification of finite behaviour up to strong bisimilarity and includes parallel composition in the form of pure interleaving without interaction between the components. They also presented counterexamples showing that unique parallel decomposition may fail in process calculi in which it is possible to specify infinite behaviour, or in which certain coarser notions of behavioural equivalence are used.

Moller, in [START_REF] Moller | Axioms for Concurrency[END_REF], proved several more unique parallel decomposition results, replacing interleaving parallel composition by CCS parallel composition, and then also considering weak bisimilarity. These results were established with subsequent refinements of an ingenious proof technique attributed to Milner. Christensen, in [START_REF] Christensen | Decidability and Decomposition in Process Algebras[END_REF], further refined the proof technique to make it work for the normed behaviours recursively definable modulo strong bisimilarity, and for all behaviours recursively definable modulo distributed bisimilarity.

With each successive refinement of Milner's proof technique, the technical details became more complicated, but the general idea of the proof remained the same. In [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] we made an attempt to isolate the deep insights from the technical details, by identifying a sufficient condition on partial commutative monoids that facilitates an abstract version of Milner's proof technique. To concisely present the sufficient condition, we have put forward the notion of decomposition order ; it is established in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF], by means of an abstract version of Milner's technique, that if a partial commutative monoid can be endowed with a decomposition order, then it has unique decomposition.

Application of the general result of [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] in commutative monoids of behaviour is often straightforward: a well-founded order naturally induced on behaviour by (a terminating fragment of) the transition relation typically satisfies the properties of a decomposition order. All the aforementioned unique parallel decomposition results can be directly obtained in this way, except Moller's result that finite behaviours modulo weak bisimilarity have unique decomposition. It turns out that a decomposition order cannot straightforwardly be obtained from the transition relation if certain transitions are deemed unobservable by the behavioural equivalence under consideration.

In this paper, we address the question of how to establish unique parallel decomposition in settings with a notion of unobservable behaviour. Our main contribution will be an adaptation of the general result in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] to make it suitable for establishing unique parallel decomposition also in settings with a notion of unobservable behaviour. To illustrate the result, we shall apply it to establish unique parallel decomposition for finite behaviour modulo branching or weak bisimilarity. We shall also show, by means of a counterexample, that unique parallel decomposition fails for infinite behaviours modulo branching and weak bisimilarity, even if only a very limited form of infinite behaviour is considered (totally normed behaviour definable in a process calculus with prefix iteration).

A positive answer to the unique parallel decomposition question seems to be primarily of theoretical interest, as a tool for proving other theoretical properties of interest about process calculi. For instance, Moller's proofs in [START_REF] Moller | The importance of the left merge operator in process algebras[END_REF][START_REF] Moller | The nonexistence of finite axiomatisations for CCS congruences[END_REF] that PA and CCS cannot be finitely axiomatised without auxiliary operations, Hirshfeld and Jerrum's proof in [START_REF] Hirshfeld | Bisimulation equivalence is decidable for normed process algebra[END_REF] that bisimilarity is decidable for normed PA, and the completeness proofs for the equational axiomatisations of PA and CCS with auxiliary operations in [START_REF] Fokkink | An omega-complete equational specification of interleaving[END_REF] and [START_REF] Aceto | A finite equational base for CCS with left merge and communication merge[END_REF], all rely on unique parallel decomposition. There is an intimate relationship between unique parallel decomposition and of cancellation with respect to parallel composition; the properties are in most circumstances equivalent. In [START_REF] Castellani | Distributed bisimulations[END_REF], cancellation with respect parallel composition was first proved and exploited to prove the completeness of an axiomatisation of distributed bisimilarity. Unique parallel decomposition could be of practical interest too, e.g., to devise methods for finding the maximally parallel implementation of a behaviour [START_REF] Corradini | Towards parallelization of concurrent systems[END_REF], or for improving verification methods [START_REF] Groote | Verification of parallel systems via decomposition[END_REF].

This article is organised as follows. In Section 2 we introduce the process calculus that we shall use to illustrate our theory of unique decomposition. There, we also present counterexamples to the effect that infinite behaviours in general may not have a decomposition, and totally normed behaviours may have more than one decomposition. In Section 3 we recap the theory of decomposition put forward in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] and discuss why it is not readily applicable to establish unique parallel decomposition for finite behaviours modulo branching and weak bisimilarity. In Section 4 we adapt the theory of [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] to make it suitable for proving unique parallel decomposition results in process calculi with a notion of unobservability. We end the paper in Section 5 with a short conclusion.

This article is an extended abstract of [START_REF] Luttik | Unique parallel decomposition in branching and weak bisimulation semantics[END_REF], which includes additional examples and detailed explanations, and more elaborate proofs.

We define a simple language of process expressions together with an operational semantics, and notions of branching and weak bisimilarity. We shall then investigate to what extent process expressions modulo branching or weak bisimilarity admit parallel decompositions. We shall present examples of process expressions without a decomposition, and of totally normed process expressions with two distinct decompositions.

Syntax

We fix a set A of actions, and declare a special action τ that we assume is not in A. We denote by A τ the set A ∪ {τ }, and we let a range over A and α over A τ . The set P of process expressions is generated by the following grammar:

P ::= 0 | α.P | P + P | P P | α * P (α ∈ A τ ).
The language above is BCCS (the core of Milner's CCS [START_REF] Milner | Communication and Concurrency[END_REF]) extended with a construction to express interleaving parallelism and the prefix iteration construction α * to specify a restricted form of infinite behaviour. We include only a very basic notion of parallel composition in our calculus, but note that this is just to simplify the presentation. Our unique decomposition theory extends straightforwardly to more intricate notions of parallel composition, e.g., modelling some form of communication between components. To be able to omit some parentheses when writing process expressions, we adopt the conventions that α. and α * bind stronger, and that + binds weaker than all the other operations.

α.P α --→ P P α --→ P P + Q α --→ P Q α --→ Q P + Q α --→ Q P α --→ P P Q α --→ P Q Q α --→ Q P Q α --→ P Q α * P α --→ α * P P α --→ P α * P α --→ P Table 1. The operational semantics.
Operational semantics and branching and weak bisimilarity We define on P binary relations α --→ (α ∈ A τ ) by means of the operational rules in Table 1. We shall henceforth write P --P if there exist P 0 , . . . , P n (n ≥ 0) such that

P = P 0 τ --→ • • • τ
--→ P n = P . Furthermore, we shall write P (α)

--→ P if P α --→ P or α = τ and P = P . Definition 1 (Branching bisimilarity [START_REF] Van Glabbeek | Branching time and abstraction in bisimulation semantics[END_REF]) A symmetric binary relation R on P is a branching bisimulation if for all P, Q ∈ P such that P R Q and for all α ∈ A τ it holds that if P α --→ P for some P ∈ P, then there exist

Q , Q ∈ P such that Q --Q (α)
--→ Q and P R Q and P R Q .

We write P ↔ b Q if there exists a branching bisimulation R such that P R Q.

The relation ↔ b is an equivalence relation on P (this is not as trivial as one might expect; for a proof see [START_REF] Basten | Branching bisimilarity is an equivalence indeed! Information[END_REF]). It is also compatible with the construction of parallel composition in our syntax, which means that, for all P 1 , P 2 , Q 1 , Q 2 ∈ P:

P 1 ↔ b Q 1 and P 2 ↔ b Q 2 implies P 1 P 2 ↔ b Q 1 Q 2 .
(

(The relation ↔ b is also compatible with α., but not with + and α * . In this paper, we shall only rely on compatibility with .)

Definition 2 (Weak bisimilarity [START_REF] Milner | Operational and algebraic semantics of concurrent processes[END_REF]) A symmetric binary relation R on P is a weak bisimulation if for all P, Q ∈ P such that P R Q and for all α ∈ A τ it holds that if P α --→ P for some P ∈ P, then there exist

Q , Q , Q ∈ P such that Q --Q (α) --→ Q --Q and P R Q .
We write P ↔ w Q if there exists a weak bisimulation R such that P R Q.

Like ↔ b , the relation ↔ w is an equivalence relation on P, and compatible with parallel composition. Note that ↔ b ⊆↔ w ; we shall often implicitly use this property below.

A process expression is indecomposable if it is not behaviourally equivalent to 0 or a non-trivial parallel composition (a parallel composition is trivial if one of its components is behaviourally equivalent to 0). We say that a process theory has unique parallel decomposition if every process expression is behaviourally equivalent to a unique (generalised) parallel composition of indecomposable process expressions. Uniqueness means that the indecomposables of any two decompositions of a process expression are pairwise behaviourally equivalent up to a permutation.

Milner and Moller in [START_REF] Milner | Unique decomposition of processes[END_REF] already observed that there exist infinite behaviours without a decomposition modulo strong bisimilarity; their example a * 0 also does not have a decomposition modulo branching and weak bisimilarity. To exclude such examples of infinite behaviours with decompositions, we need to confine our attention to process expressions with terminating behaviour. (A formalisation of aforementioned notions pertaining to unique decomposition is postponed until the next section.)

For a ∈ A and process expressions P and Q we write P a --Q whenever there exist process expressions P and Q such that P --P a --→ Q --Q. We say that P is silent and write P if there do not exist a ∈ A and Q such that P a --Q. Definition 3 A process expression P is totally normed if there exist a natural number k ∈ N, process expressions P 0 , . . . , P k ∈ P and actions a 1 , . . . , a k ∈ A

such that P = P 0 a1 --• • • a k
--P k and P k . The weak norm wn(P) of a totally normed process expression P is defined by wn(P) = min{k : ∃P 0 , . . . , P k ∈ P. ∃a 1 , . . . , a k ∈ A.

P = P 0 a1 --• • • a k --P k } .
It is immediate from their definitions that both branching and weak bisimilarity preserve weak norm: if two process expressions are branchingly or weakly bisimilar, then they have equal weak norms. It is also easy to establish that a parallel composition is weakly normed if, and only if, both parallel components are weakly normed. In fact, weak norm is additive with respect to parallel composition: the weak norm of a parallel composition is the sum of the weak norms of its parallel components. Note that a process expression with weak norm 0 is behaviourally equivalent to 0.

With a straightforward induction on weak norm it can be established that totally normed process expressions have a decomposition. But sometimes even more than one, as is illustrated in the following example.

Example 4 Consider the process expressions P = a * τ.b.0 and Q = b.0. It is clear that P and Q are not branching bisimilar. Both P and Q have weak norm 1, and from this it immediately follows that they are both indecomposable. Note that, according to the operational semantics, P P gives rise to the following three transitions:

1. P P a --→ P P; 2. P P τ --→ P Q; and 3. P P τ --→ Q P.
Further note that P Q a --→P Q and Q P a --→Q P. (The complete transition graph associated with P P by the operational semantics is shown in Figure 1.) Using these facts it is straightforward to verify that the symmetric closure of the binary relation R = {(P P, P Q), (P P, Q P)} ∪ {(P Q, Q P), (P 0, 0 P), (Q 0, 0 Q)} is a branching bisimulation, and hence P P ↔ b P Q. It follows that P P and P Q are distinct decompositions of the same process up to branching bisimilarity.

Incidentally, the processes in the above counterexample also refute claims in [START_REF] Fröschle | Normed processes, unique decomposition, and complexity of bisimulation equivalences[END_REF] to the effect that processes definable with a totally normed BPP specification have a unique decomposition modulo branching bisimilarity and weak bisimilarity.

Apparently, more severe restrictions are needed.

Definition 5 Let k ∈ N; a process expression P is weakly bounded by k if for all ∈ N the existence of P 1 , . . . , P ∈ P and a 1 , . . . , a ∈ A such that

P a1 --• • • a --P implies that ≤ k.
We say that P is weakly bounded if P is bounded by k for some k ∈ N. Lemma 6 Let P and Q be process expressions such that P ↔ w Q. Then P is weakly bounded if, and only if, Q is weakly bounded.

P P P Q P 0 Q P Q Q Q 0 0 P 0 Q 0 0
In the remainder of this paper we shall establish that weakly bounded process expressions have a unique parallel decomposition both modulo branching and weak bisimilarity. We shall derive these results from a more general result about unique decomposition in commutative monoids.

Partial commutative monoids and decomposition

In this section we recall the abstract algebraic notion of partial commutative monoid, and formulate the property of unique decomposition. We shall see that the process theories discussed in the previous section give rise to commutative monoids of processes with parallel composition as binary operation. The notion of unique decomposition associated with these commutative monoids coincides with the notion of unique parallel decomposition as discussed.

Then, we shall recall the notion of decomposition order on partial commutative monoids proposed in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF]. We shall investigate whether the notion of decomposition order can be employed to prove unique parallel decomposition of weakly bounded process expressions modulo branching and weak bisimilarity. Definition 7 A (partial) commutative monoid is a set M with a distinguished element e and a (partial) binary operation on M (for clarity in this definition denoted by •) such that for all x, y, z ∈ M :

x • (y • z) (x • y) • z (associativity); x • y y • x (commutativity);
x • e e • x x (identity).

The symbol • will be omitted if this is unlikely to cause confusion. Also, we shall sometimes use other symbols ( , +, . . . ) to denote the binary operation of a partial commutative monoid.

Remark 8

We adopt the convention that an expression designating an element of a partial commutative monoid M is defined only if all its subexpressions are defined. Furthermore, if t 1 and t 2 are expressions and R is a binary relation on M (e.g., equality or a partial order), then t 1 Rt 2 holds only if both t 1 and t 2 are defined and their values are related in R. For a more succinct formulation we used in Definition 7 the symbol introduced by Kleene [13]: if t 1 and t 2 are expressions designating elements of M , then t 1 t 2 means that either t 1 and t 2 are both defined and have the same value, or t 1 and t 2 are both undefined. We mention a key example of a commutative monoid that will serve to illustrate the theory of decomposition that we present in this paper.

Example 9 Let X be any set. A (finite) multiset over X is a mapping m : X → N such that m(x) > 0 for at most finitely many x ∈ X; the number m(x) is called the multiplicity of x in m. The set of all multisets over X is denoted by M(X). If m and n are multisets, then their sum m n is obtained by coordinatewise addition of multiplicities, i.e., (m n)(x) = m(x) + n(x) for all x ∈ X. The empty multiset is the multiset that satisfies (x) = 0 for all x ∈ X. With these definitions, M(X) is a commutative monoid. If x 1 , . . . , x k is a sequence of elements of X, then x 1 , . . . , x k denotes the multiset m such that m(x) is the number of occurrences of x in x 1 , . . . , x k .

Process expressions modulo branching or weak bisimilarity also give rise to commutative monoids. Recall that ↔ b and ↔ w are equivalence relations on the set of process expressions. We denote the equivalence class of a process expression In this paper, the similarities between the commutative monoids B and W will be more important than the differences. It will often be necessary to define notions for both commutative monoids, in a very similar way. For succinctness of presentation, we allow ourselves a slight abus de language and most of the time deliberately omit the subscripts b and w from our notation for equivalence classes. Thus, we will be able to efficiently define notions and prove facts simultaneously for B and W.

For example, since both ↔ b and ↔ w are compatible with , we can define a binary operation simultaneously on B and W simply by

[P] [Q] = [P Q],
by which we then mean to define a binary operation on B and a binary relation on W, respectively, by

[P] b [Q] b = [P Q] b and [P] w [Q] w = [P Q] w .
Henceforth, we leave it to the reader to specialise notions, and also statements about these notions and their proofs, to B and W (or one of its submonoids to be introduced below).

We agree to write just 0 for [0]. It is straightforward to establish that the binary operation is commutative and associative (both on B and W), and that 0 is the identity element for . Notation 12 Let x 1 , . . . , x k be a (possibly empty) sequence of elements of a monoid M ; we define its generalised product

x 1 • • • x k inductively as follows: (1) if n = 0, then x 1 • • • x k e, and (2) if n > 0, then x 1 • • • x k (x 1 • • • x k-1 )x k . Occasionally, we shall write k i=1 x i instead of x 1 • • • x k . Furthermore, we write x n for the k-fold composition of x, i.e., x k k i=1 x i with x i = x for all 1 ≤ i ≤ k.
An indecomposable element of a commutative monoid is an element that cannot be written as a product of two elements that are both not the identity element of the monoid.

Definition 13 An element p of a commutative monoid M is called indecomposable if p = e and p = xy implies x = e or y = e.

Example 14 1. The indecomposable elements of M(X) are the singleton multisets, i.e., the multisets m for which it holds that x∈X m(x) = 1. 2. The indecomposable elements of B fin , B tn , B, W fin , W tn , and W are the equivalence classes of process expressions that are not behaviourally equivalent to 0 or a non-trivial parallel composition.

We define a decomposition in a partial commutative monoid to be a finite multiset of indecomposable elements. Note that this gives the right notion of equivalence on decompositions, for two finite multisets x 1 , . . . , x k and y 1 , . . . , y are the equal iff the sequence y 1 , . . . , y can be obtained from the sequence x 1 , . . . , x k by a permutation of its elements.

Definition 15 Let M be a partial commutative monoid. A decomposition in M is a finite multiset p 1 , . . . , p k of indecomposable elements of M such that

p 1 • • • p k is defined. The element p 1 • • • p k in M
• • • p k = p 1 • • • p . A decomposition d in M is unique if d ≡ d implies d = d
for all decompositions d in M . We say that an element x of M has a unique decomposition if it has a decomposition and this decomposition is unique. If every element of M has a unique decomposition, then we say that M has unique decomposition.

Example 16 Every finite multiset m over X has a unique decomposition in M(X), which contains for every x ∈ X precisely m(x) copies of the singleton multiset x .

The general notion of unique decomposition for commutative monoids, when instantiated to one of the commutative monoids of processes considered in this paper, indeed coincides with the notion of unique parallel decomposition as discussed in the preceding section. We have already seen that the commutative monoids B tn , B, W tn and W do not have unique decomposition. Our goal in the remainder of this paper is to establish that the commutative monoids B fin and W fin do have unique decomposition.

Preferably, we would like to have a general sufficient condition on partial commutative monoids for unique decomposition that is easily seen to hold for B fin and W fin , and hopefully also for other commutative monoids of processes. We shall now first recall the sufficient criterion put forward in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF], which was specifically designed for commutative monoids of processes. Then, we shall explain that it cannot directly be applied to conclude that B fin and W fin have unique decomposition. In the next section, we shall subsequently modify the condition, so that it becomes applicable to the commutative monoids at hand.

Definition 17

Let M be a partial commutative monoid; a partial order on M is a decomposition order if (i) it is well-founded, i.e., every nonempty subset of M has a -minimal element; (ii) the identity element e of M is the least element of M with respect to , i.e., e x for all x in M ; (iii) it is strictly compatible, i.e., for all x, y, z ∈ M if x ≺ y and yz is defined, then xz ≺ yz;

(iv) it is precompositional, i.e., for all x, y, z ∈ M x yz implies x = y z for some y y and z z; and

(v) it is Archimedean, i.e., for all x, y ∈ M

x n y for all n ∈ N implies that x = e.

In [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] it was proved that the existence of a decomposition order on a partial commutative monoid is a necessary and sufficient condition for unique decomposition. The advantage of establishing unique decomposition via a decomposition order is that it circumvents first establishing cancellation, which in some cases is hard without knowing that the partial commutative monoid has unique decomposition. We refer to [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] for a more in-depth discussion.

In commutative monoids of processes, an obvious candidate decomposition order is the order induced on the commutative monoid by the transition relation. We define a binary relation --→ on B and W by

[P] --→ [P ] if there exist Q ∈ [P], Q ∈ [P ] and α ∈ A τ such that Q α --→ Q .
We shall denote the inverse of the reflexive-transitive closure of --→ (both on B and W) by , i.e., = (--→ * ) -1 .

Lemma 18 If P and Q are process expressions such that

[Q] [P], then there exists Q ∈ [Q] such that P --→ * Q .
The following lemma implies that every set of process expressions has minimal elements with respect to the reflexive-transitive closure of the transition relation. Caution: it holds true of our process calculus only thanks to the very limited facility of defining infinite behaviour, by means of simple loops.

Lemma 19 If P 0 , . . . , P i , . . . (i ∈ N) is an infinite sequence of process expressions, and α 0 , . . . , α i , . . . (i ∈ N) is an infinite sequence of elements in A τ such that P i αi --→ P i+1 for all i ∈ N, then there exists j ∈ N such that P k = P for all k, ≥ j.

Proposition 20

is a well-founded precompositional partial order on each of the commutative monoids B, B tn , B fin , W, W tn , and W fin .

Note that if the iteration prefix in our process calculus is replaced by any of the familiar more general forms of iteration or recursion, then as defined above will not be anti-symmetric, nor well-founded. Nevertheless, it is sometimes possible to define an anti-symmetric and well-founded partial order on processes based on the transition relation in a setting with a more general form of infinite behaviour, at least for totally normed processes. (See, e.g., [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] for an example of an anti-symmetric and well-founded order on normed processes definable in ACP with recursion, which is based on the restriction of the transition relation.)

The ordering defined on B tn , B, W tn and W is not a decomposition order: on B and W it does not satisfy conditions (ii), (iii) and (v) of Definition 17, and on B tn and W tn it does not satisfy condition (iii) of Definition 17. (The latter is illustrated in Example 4.)

Proposition 21

on B tn , B fin , W tn and W fin is Archimedean and 0 is its least element.

We should now still ask ourselves the question whether on B fin and W fin is strictly compatible. An important step towards proving the property for, e.g., B fin would be to establish, for all weakly bounded process expressions P, Q and R, the following implication:

P τ --→ Q & P R ↔ b Q R =⇒ P ↔ b Q. Example 4
illustrates that this implication does not hold for all totally normed processes, suggesting that the implication is perhaps hard to establish from first principles. In fact, all our attempts in this direction so far have failed. Note, however, that establishing the implication would be straightforward if we could use that is cancellative (i.e., P R ↔ b Q R implies P ↔ b Q), and this, in turn, would be easy if we could use that B fin has unique decomposition.

The difficulty of establishing strict compatibility is really with strictness; it is straightforward to establish the following non-strict variant. Let M be a partial commutative monoid; a partial order on M is compatible if for all x, y, z ∈ M : if x y and yz is defined, then xz yz.

Proposition 22

on B tn , B fin , W tn , and W fin is compatible.

A partial order on a partial commutative monoid that has all the properties of a decomposition order except that it is compatible but not strictly compatible, we shall henceforth call a weak decomposition order.

Definition 23 Let M be a partial commutative monoid; a partial order on M is a weak decomposition order if it is well-founded, has the identity element e ∈ M as least element, is compatible, precompositional and Archimedean.

The following corollary summarises Propositions 20, 21 and 22.

Corollary 24

on B tn , B fin , W tn , and W fin is a weak decomposition order.

In [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] it is proved that the existence of a decomposition order is a sufficient condition for a partial commutative monoid to have unique decomposition. Note that since is a weak decomposition order on B tn and W tn , and according to Example 4 these commutative monoids do not have unique decomposition, the existence of a weak decomposition order is not a sufficient condition for having unique decomposition; it should be supplemented with additional requirements to get a sufficient condition.

Strictness of compatibility -which is the only difference between the notion of decomposition order of [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] and the notion of weak decomposition order put forward here-is used both in the proof of existence of decompositions and in the proof that decompositions are unique. We shall now first establish the existence of decompositions in B tn , B fin , W tn , and W fin separately. In the next section, we shall discuss uniqueness of decompositions in B fin and W fin . We shall propose a general subsidiary property that will allow us to establish uniqueness of decompositions in commutative monoids with a weak decomposition order, and establish that it holds in B fin and W fin .

Proposition 25 In the commutative monoids B tn , B fin , W tn , and W fin every element has a decomposition.

Uniqueness

The failure of on B fin and W fin to be strictly compatible prevents us from getting our unique decomposition results as an immediate consequence of the result in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF]. Nevertheless, most of the ideas in the proof of uniqueness of decompositions in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] can be adapted and reused in the context of commutative monoids endowed with a weak decomposition order, albeit with the technical details more involved. There is one special case in the unique decomposition proof that cannot be settled for commutative monoids with a weak decomposition order in general; this special case can be settled with an additional requirement on that is satisfied both in B fin and in W fin .

For the remainder of this paper, let M be a partial commutative monoid in which every element has a decomposition, and let be a weak decomposition order on M .

The decomposition extension of

The uniqueness proof in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] considers a minimal counterexample against unique decomposition, i.e., an element of the commutative monoid with at least two distinct decompositions, say d 1 and d 2 , that is -minimal in the set of all such elements. Then, an important technique in the proof is to select a particular indecomposable in one of the two decompositions and replace it by predecessors with respect to the decomposition order. From minimality together with strict compatibility it is then concluded that the resulting decomposition is unique, which plays a crucial role in subsequent arguments towards a contradiction. To avoid the use of strict compatibility, we need a more sophisticated notion of minimality for the considered counterexample. The idea is to not just pick a -minimal element among the elements with two or more decompositions; we also choose the presupposed pair of distinct decompositions (d 1 , d 2 ) in such a way that it is minimal with respect to a well-founded ordering induced by on pairs of decompositions.

Let X be a set. If m and n are multisets over X, then we write m -n for the multiset difference of m and n. We define the decomposition extension of ≺ by d d if, and only if, there exist, for some k ≥ 1, a sequence of indecomposables p 1 , . . . , p k ∈ M , a sequence x 1 , . . . , x k ∈ M , and a sequence of decompositions d 1 , . . . , d k such that Lemma 26 The partial order on decompositions is well-founded.

(i) x i ≺ p i (1 ≤ i ≤ k); (ii) each d i is a decomposition of x i (1 ≤ i ≤ k); and (iii) d = (d -p 1 , . . . , p k ) (d 1 • • • d k ).
In our uniqueness proof, we shall use the well-foundedness of both and the Cartesian order × induced on pairs of decompositions by . For two pairs of decompositions (d

≡ d 2 , but not d 1 = d 2 . A counterexample (d 1 , d 2 )
against unique decomposition is minimal if it is both minimal with respect to and minimal with respect to × . If unique decomposition would fail then there would exist a minimal counterexample. For the subset of processes with two or more decompositions is nonempty, and therefore, by well-foundedness of , it has a -minimal element, say x. Then, by well-foundedness of × on pairs of decompositions, the nonempty set of pairs of distinct decompositions with x as their composition has a minimal element, say (d 1 , d 2 ).

The general idea of the proof is that we derive a contradiction from the assumption that there exists a minimal counterexample (d 1 , d 2 ) against unique decomposition. The decompositions d 1 and d 2 should be distinct, so the set of indecomposables that occur more often in one of the decompositions than in the other is nonempty. This set is clearly also finite, so it has -maximal elements. We declare p to be such a -maximal element, and assume, without loss of generality, that p occurs more often in d 1 than in d 2 . Then we have that (A) d 1 (p) > d 2 (p); and (B) d 1 (q) = d 2 (q) for all indecomposables q such that p ≺ q.

We shall distinguish two cases, based on how the difference between d 1 and d 2 manifests itself, and derive a contradiction in both cases:

1. d 1 (p) > d 2 (p) + 1 or d 1 (q) = 0 for some indecomposable q distinct from p;

we refer to this case by saying that d 1 and d 2 are too far apart. 2. d 1 (p) = d 2 (p) + 1 and d 1 (q) = 0 for all q distinct from p; we refer to this case by saying that d 1 and d 2 are too close together.

Case 1: d 1 and d 2 are too far apart We argue that d 1 has a predecessor d in which p occurs more often than in any predecessor of d 2 , while, on the other hand, the choice of a minimal counterexample implies that every predecessor of d 1 is also a predecessor of d 2 . The arguments leading to a contradiction in this case are analogous to the arguments in the proof in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF]; the only important difference is the use of the ordering instead of .

Case 2: d 1 and d 2 are too close together In [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF] it is proved, via a sophisticated argument, that the composition of d 2 is a -predecessor of p. Hence, by strict compatibility, the composition of d 2 is an -predecessor of d 1 , which is in contradiction with the assumption that the decompositions d 1 and d 2 are equivalent.

That is not strictly compatible, but just compatible, leaves the possibility that d 1 and d 2 are equivalent even if the composition of d 2 is a predecessor of p. For B fin and W fin this possibility can be ruled out by noting that the composition of d 2 can be reached from p by τ -transitions, and proving that every transition of p can be simulated by a transition of the composition of d 2 . The following notion formalises this reason in the abstract setting of commutative monoids with a weak decomposition order.

Definition 27 Let M be a partial commutative monoid, and let be a weak decomposition order on M . We say that satisfies power cancellation if for all x, y ∈ M , for every indecomposable p ∈ M such that p ≺ x, y, and for all k ∈ N it holds that p k x = p k y, then x = y.

Suppose that on M has power cancellation, let k = d 2 (p) and let x be the composition of d 2 . Then from d 1 ≡ d 2 it follows that p k p = p k x. Clearly, p ≺ p and, since d 2 consists of indecomposables q such that p ≺ q, it follows that also p ≺ x. Hence, since has power cancellation, p = x, so d 2 = p . It follows that d 1 = d 2 , which contradicts that (d 1 , d 2 ) is a counterexample against unique decomposition.

Theorem 28 Let M be a commutative monoid with a weak decomposition order that satisfies power cancellation. If every element of M has a decomposition, then M has unique decomposition.

In the previous section we have already established that in the commutative monoids B fin and W fin every element has a decomposition and that is a weak decomposition order on B fin and W fin . To be able to conclude from Theorem 28 that B fin and W have unique decomposition, it remains to establish that on these commutative monoids satisfies power cancellation.

Proposition 29

on B fin and W fin satisfies power cancellation.

By Corollary 24 and Propositions 25 and 29, the commutative monoids B fin and W fin are endowed with a weak decomposition order satisfying power cancellation, and, moreover, all elements of B fin and W fin have at least one decomposition. Hence, by Theorem 28, we obtain the following corollary.

Corollary 30 B fin and W fin have unique decomposition.

Concluding remarks

We have presented a general sufficient condition on partial commutative monoids that implies the property of unique decomposition, and is applicable to commutative monoids of behaviour incorporating a notion of unobservability. We have illustrated the application of our condition in the context of a very simple process calculus with an operation for pure interleaving as parallel composition. The applicability is, however, not restricted to settings with this particular type of parallel composition. In fact, it is to be expected that our condition, similarly as in [START_REF] Luttik | Decomposition orders-another generalisation of the fundamental theorem of arithmetic[END_REF], can also be used to prove unique decomposition results in settings with more complicated notions of parallel composition operator allowing, e.g., synchronisation between components. We leave for future investigations to what extent our theory of unique decomposition can be applied to variants of πcalculus; the report [START_REF] Dreier | On unique decomposition of processes in the applied π-calculus[END_REF], in which unique parallel decomposition is established for a fragment of Applied π-calculus, will serve as a starting point.

In [START_REF] Balabonski | A geometric approach to the problem of unique decomposition of processes[END_REF], Balabonski and Haucourt address the problem of unique parallel decomposition in the context of a concurrent programming language with a geometric semantics. It is less clear whether our general theory of unique decomposition is applicable there too; at least, the geometric semantics does not as naturally induce a candidate decomposition order on processes as in a process calculus with a transition system semantics. It would be interesting to compare the approaches.

Fig. 1 .

 1 Fig. 1. Transition graph associated with P P.

  P modulo ↔ b or ↔ w , respectively, by [P ] b and [P ] w . Then, we define B = P/↔ b = {[P ] b : P ∈ P} and W = P/↔ w = {[P ] w : P ∈ P} .

Proposition 10 B

 10 and W are commutative monoids under . Note that, by Lemma 6, whenever an equivalence class [P] contains a weakly bounded process expression, it consists entirely of weakly bounded process expressions. We define subsets B fin ⊆ B tn ⊆ B and W fin ⊆ W tn ⊆ W by B fin = {[P ] b : P ∈ P & P is weakly bounded} ; B tn = {[P ] b : P ∈ P & P is totally normed} ; W fin = {[P ] w : P ∈ P & P is weakly bounded} ; and W tn = {[P ] w : P ∈ P & P is totally normed} . Corollary 11 The sets B fin and B tn are commutative submonoids of B, and the sets W fin and W tn are commutative submonoids of W.

  will be called the composition associated with the decomposition p 1 , . . . , p k , and, conversely, we say that p 1 , . . . , p k is a decomposition of the element p 1 • • • p k of M . Decompositions d = p 1 , . . . , p k and d = p 1 , . . . , p are equivalent in M (notation: d ≡ d ) if they have the same compositions, i.e., if p 1

  We write d d if d = d or d d . Note that if d d , x is the composition of d, and y is the composition of d , then, by compatibility, x y.

  1 , d 2 ) and (d 1 , d 2 ), we write (d 1 , d 2 ) × (d 1 , d 2 ) if d 1 d 1 and d 2 d 2 . A pair of decompositions (d 1 , d 2 ) is said to be a counterexample against unique decomposition if d 1 and d 2 are distinct but equivalent, i.e., if d 1


Paul Klint

Loren Roosendaal

Riemer Van Rozen

Game Developers need Lua AiR Static Analysis of Lua using Interface Models

Game development businesses often choose Lua for separating scripted game logic from reusable engine code. Lua can easily be embedded, has simple interfaces, and offers a powerful and extensible scripting language. Using Lua, developers can create prototypes and scripts at early development stages. However, when larger quantities of engine code and script are available, developers encounter maintainability and quality problems. First, the available automated solutions for interoperability do not take domain-specific optimizations into account. Maintaining a coupling by hand between the Lua interpreter and the engine code, usually in C++, is labour intensive and error-prone. Second, assessing the quality of Lua scripts is hard due to a lack of tools that support static analysis. Lua scripts for dynamic analysis only report warnings and errors at run-time and are limited to code coverage. A common solution to the first problem is developing an Interface Definition Language (IDL) from which "glue code", interoperability code between interfaces, is generated automatically. We address quality problems by proposing a method to complement techniques for Lua analysis. We introduce Lua AiR (Lua Analysis in Rascal), a framework for static analysis of Lua script in its embedded context, using IDL models and Rascal.

Introduction

Game developers use script languages to develop and maintain game logic separately from game engine libraries. Lua is a script language [START_REF] Ierusalimschy | Programming in Lua, Second Edition[END_REF] in the form of an ANSI C library 4 developed by Ierusalimschy, de Figuieredo and Celes. During its evolution [START_REF] Ierusalimschy | The Evolution of Lua[END_REF] Lua has gradually matured and has remained light-weight. Moreover, it is an embeddable, minimalistic yet extensible, general purpose, dynamically typed script language. Its language design trade-offs, displayed in Table 1, have shaped the co-development of the embedding API and script features [START_REF] Ierusalimschy | Passing a Language through the Eye of a Needle[END_REF]. Lua is popular in game development. Using Lua, developers can quickly create prototypes. However, using Lua also comes at a cost. In later development stages, when larger quantities of engine library code and game script are available, developers encounter maintainability and quality problems. First, using a standard generator for the coupling between Lua and the game libraries sacrifices speed, and maintaining a hand-written coupling with domainspecific optimizations is labour intensive and error-prone. Second, assessing the quality of Lua scripts is hard due to a lack of tools that support source level static analysis, which entails computing information about scripts before runtime. The commonly used Lua scripts for dynamic analysis only report warnings and errors at run-time, and are limited to code coverage. Static analyses do exist, but are mainly applied to intermediate representations in Single Static Assignment (SSA) forms for run-time optimization, e.g. LuaJIT 5 and the runtime specializations of Williams et al. [START_REF] Williams | Dynamic Interpretation for Dynamic Scripting Languages[END_REF].

Both problems increase with scale and special measures are necessary for ensuring maintainability and code quality. A common solution to the first problem is to develop an Interface Definition Language (IDL) from which optimized "glue code", interoperability code between interfaces, is generated automatically. However, code quality problems remain to be addressed. Quality problems are not unique to Lua. Blow [START_REF] Blow | Game Development: Harder Than You Think[END_REF] expresses increased complexity and lack of development tools and White et al. [START_REF] White | Better Scripts, Better Games[END_REF] describe the need for better script notation. Ramsey and Assis [START_REF] Ramsey | Almost Good Enough to Scale: A Lua Mail Handler and Spam Filter[END_REF] express the need of the Lua community for machine-checkable APIs including types, whole-program and modular static analysis and static type inference. Providing practical methods for static analysis of Lua is hard because static analysis algorithms are subject to a trade-off between speed and precision and developers require exact and immediate feedback during development.

We address script quality problems by proposing a method to complement analysis techniques of Lua. We describe an approach in collaboration with IC3D Media that uses the Rascal Meta-Programming Language6 [START_REF] Klint | RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation[END_REF]. IC3D Media is a Dutch SME located in Breda, active in games for entertainment and training. We introduce Lua Analysis in Rascal (Lua AiR), a framework for static analysis of Lua script in its embedded context, using IDL models.

Static Analysis of Lua

We can think of scripts as having many run-time states reachable via possibly many execution paths. Running every program path is infeasible, but abstracting 2 enumerates static analysis features applicable to Lua and compares existing analysis tools. Features include distinguishing between global and local variables [START_REF] Ierusalimschy | Programming in Lua, Second Edition[END_REF] and relating declarations to uses (4), possibly using syntax highlighting. Many of these features (1-6) can be approximated by data flow analysis techniques [START_REF] Nielson | Principles of Program Analysis[END_REF] such as reaching definitions, which computes for each program point which assignments can reach it. Others features require no flow analysis [START_REF] Ramsey | Almost Good Enough to Scale: A Lua Mail Handler and Spam Filter[END_REF][START_REF] Klint | RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation[END_REF] or require more advanced inference techniques (9-13). Figure 1 illustrates features described in Table 2 using comments and references (fn), where (a) illustrates features 1, 2, 4, 7, 8 and 9 and (b) shows features 1-3. e l s e 5 p r i n t ( h a e l t h ) --( f2 ) must be undefined 6 end 7 s e l f . h e a l t h = s e l f . h e a l t h -damage 8 p r i n t ( isDown ) --( f3 ) may be nil or true 9 r e t u r n s e l f 10 end 11 u n i t = { h e a l t h =10} --create a test unit 12 u n i t = h i t ( u n i t , 4 ) --call hit , bind unit , 4 13 u n i t = h i t ( u n i t , 8 ) --call hit , bind unit , 8 7 is an Eclipse plug-in that provides remote debugging and rudimentary static analysis for highlighting and refactoring. Lua Inspect 8 is an experimental static analysis tool that infers values, but incorrectly for conditional assignments. Lua Checker 9 is a basic command-line tool that checks local variable declarations against their uses. Lua for IDEA 10 enriches call sites with API structure (e.g. for World of Warcraft). LDT and Lua Inspect are based on Metalua [START_REF] Fleutot | Contrasting Compile-Time Meta-Programming in Metalua and Converge[END_REF], a Lua extension for static meta-programming.

Lua AiR Framework

This section explains the approach of the Lua AiR framework. IC3D Media has developed two languages for interoperability between Lua and their Logos3D game engine called Interface Definition Language (IDL) and Interface Generator Language (IGL). IDL defines function signatures and data types. IGL defines the generator format of the mapping between engine functionality defined in IDL models and Lua. Unlike other approaches shown in Table 2, we utilize information from the embedded context in our analysis. Functions and data structures exposed to Lua, and managed by the Logos3D engine, are statically defined and strongly typed. Sharing function signatures and data types modeled in IDL between the embedded environment and Lua enables checking function call site arguments against formal parameter types. Furthermore, it reduces the need for type inference and saves computation time in inter-procedural analysis. Additionally, code documentation can be shared between script proxies and the embedded context.

Lua AiR is a Rascal meta-program that implements the analysis as a pipeline, as illustrated by Figure 2. Rascal generates a specialized Eclipse IDE for Lua editing, highlighting, and static analysis. The analysis consists of the following model transformations. 1) The Lua script under analysis is fed into the parser 3 Discussion and Future Work

This section discusses problems and describes opportunities for future work. Empirical validation. We believe that providing developers with better tools will improve code quality, but we have no proof yet this assumption is correct. Our approach can be validated by verifying if programmers can improve code quality by using our framework.

Improved precision. Our analysis is context insensitive with respect to individual program states and execution paths and lacks type inference. Our analyis can be improved by using context sensitive techniques based generating and evaluating logical constraints [START_REF] Klint | RASCAL: A Domain Specific Language for Source Code Analysis and Manipulation[END_REF][START_REF] Nielson | Principles of Program Analysis[END_REF].

Tool integration. Our framework cannot be used yet by existing tools. We plan to create a Query API to interface with other tools.

DLSs. Lua lacks the domain-specific notation which non-programmer game developers need to model software artefacts. A separation of concerns, as shown in Figure 3, is necessary to tackle challenges resulting from increased complexity in game development. Games can be modeled using sets of complementary lightweight little languages, one for each concern, as demonstrated by Palmer [START_REF] Palmer | Ficticious: MicroLanguages for Interactive Fiction[END_REF] and advocated by Furtado [START_REF] Furtado | SharpLudus Revisited: from ad hoc and Monolithic Digital Game DSLs to Effectively Customized DSM Approaches[END_REF]. We observe that Lua AiR can be extended to support DLSs for higher level game concerns such as world events, character behavior and mission design, using IDL bindings to check if models conform to the interfaces of their library foundations.

In this paper we related Lua script quality problems to a lack of tools that support its static analysis. We evaluated the features of available tools and proposed a method to complement techniques for analysing Lua. We introduced Lua AiR, a framework for static analysis of Lua script in its embedded context, using IDL models and Rascal. Its main goal is to provide the immediate script analysis developers need to improve code quality. Preliminary results show that Lua AiR can provide additional information about Lua scripts. In future case studies we plan to use Lua AiR to analyse existing game code on a larger scale.

1

  function f ( c ) --( f1 ) assign function to f f4 ) call f , bind c to "4" 10 p r i n t ( a ) --( f4 ) 4, read global a 11 d = 2 . . a --( f9 ) coerces 2 to string 12 d = d / "12" --( f9 ) coerces 12 to number 13 p r i n t ( c , d ) --( f2 ) nil 2, undeclared c (a) Sequential Assignments 1 function h i t ( s e l f , damage ) 2 i f s e l f . h e a l t h < damage then 3 isDown = true --( f1 ) assign global 4

Fig. 1 :

 1 Fig. 1: Lua Script demonstrating potential errors that static analysis can find

Fig. 2 :

 2 Fig. 2: Lua AiR Model Transformations

Fig. 3 :

 3 Fig. 3: Increased Complexity requires Separating Concerns

Table 1 :

 1 Lua Design Trade-offs

	Lua feature	Trade-off	Mitigating argument
	Light-weight	Large responsibility to its users Well-defined responsibilities
	Dynamic typing Lack of static type checking	Flexibility of use
	Maintainable C Lack of pure speed	Embedded in efficient C
	General-purpose Lack of domain-specific features Extensible script language
	Simple	High use of few APIs	Low learning curve
	Embeddable	Need for interoperability code This code can be generated

Table 2 :

 2

				Tools
		LDT	Lua Inspect Lua Checker Lua for IDEA Lua AiR
	tool characterization	Eclipse IDE	SciTE/VIM	command-line	IntelliJIDEA	Meta-
			plug-in,	simplifier	&	plug-in	Framework,
			HTML output	checker tools			Eclipse IDE
	based on	Metalua	Metalua	lex/yacc, Lua Kahlua	Rascal MPL
	affiliation	Eclipse, Sierra	David Manura Google		Jon Akhtar	HvA,	CWI,
		Wireless					EQuA project
	1 globals & locals (definition and use) yes	yes	strict declare	yes	yes
				before use
	Features

Static Analysis: Features and Tools from specific execution states enables us to reason about software properties and to compute them timely. Static analysis refers to the extraction of information about states and behavior from a software application without executing it. Table

http://luajit.org/

http://www.rascal-mpl.org/

var use must be undefined

Acknowledgements We thank the reviewers for their constructive comments.

This work is part of the EQuA project. http://www.equaproject.nl/

//www.eclipse.org/


Seneca, SC, USA A Joe Turner

Bertrand Meyer

Bernard Cornu

Ronald Waxman

Jacques Henry

Barbara Pernici

Max A Bramer

Annelise Mark Pejtersen

Ryohei Nakatsu

Michele Bezzi
email: michele.bezzi@sap.com

Penny Duquenoy
email: p.duquenoy@mdx.ac.uk

Simone Fischer-Hübner
email: simone.fischer-huebner@kau.se

Ge Zhang
email: ge.zhang@kau.se

Marit Hansen

IFIP -The International Federation for Information Processing

IFIP was founded in 1960 under the auspices of UNESCO, following the First World Computer Congress held in Paris the previous year. An umbrella organization for societies working in information processing, IFIP's aim is two-fold: to support information processing within its member countries and to encourage technology transfer to developing nations. As its mission statement clearly states, IFIP's mission is to be the leading, truly international, apolitical organization which encourages and assists in the development, exploitation and application of information technology for the benefit of all people.

IFIP is a non-profitmaking organization, run almost solely by 2500 volunteers. It operates through a number of technical committees, which organize events and publications. IFIP's events range from an international congress to local seminars, but the most important are: The working conferences are structured differently. They are usually run by a working group and attendance is small and by invitation only. Their purpose is to create an atmosphere conducive to innovation and development. Refereeing is less rigorous and papers are subjected to extensive group discussion.

Publications arising from IFIP events vary. The papers presented at the IFIP World Computer Congress and at open conferences are published as conference proceedings, while the results of the working conferences are often published as collections of selected and edited papers.

Any national society whose primary activity is in information may apply to become a full member of IFIP, although full membership is restricted to one society per country. Full members are entitled to vote at the annual General Assembly, National societies preferring a less committed involvement may apply for associate or corresponding membership. Associate members enjoy the same benefits as full members, but without voting rights.

Preface

New Internet developments pose greater and greater privacy dilemmas. In the Information Society, the need for individuals to protect their autonomy and retain control over their personal information is becoming more and more important. Today, information and communication technologies-and the people responsible for making decisions about them, designing, and implementing them-scarcely consider those requirements, thereby potentially putting individuals' privacy at risk. The increasingly collaborative character of the Internet enables anyone to compose services and contribute and distribute information. It may become hard for individuals to manage and control information that concerns them and particularly how to eliminate outdated or unwanted personal information, thus leaving personal histories exposed permanently. These activities raise substantial new challenges for personal privacy at the technical, social, ethical, regulatory, and legal levels: How can privacy in emerging Internet applications such as collaborative scenarios and virtual communities be protected? What frameworks and technical tools could be utilized to maintain life-long privacy?

During September 3-10, 2009, IFIP (International Federation for Information Processing) working groups 9.2 (Social Accountability), 9.6/11.7 (IT Misuse and the Law), 11.4 (Network Security) and 11.6 (Identity Management) held their 5th International Summer School in cooperation with the EU FP7 integrated project PrimeLife in Sophia Antipolis and Nice, France. The focus of the event was on privacy and identity management for emerging Internet applications throughout a person's lifetime.

The aim of the IFIP Summer Schools has been to encourage young academic and industry entrants to share their own ideas about privacy and identity management and to build up collegial relationships with others. As such, the Summer Schools have been introducing participants to the social implications of information technology through the process of informed discussion.

Following the holistic approach advocated by the involved IFIP working groups and by the PrimeLife project, a diverse group of participants ranging from young doctoral students to leading researchers in the field engaged in discussions, dialogues and debates in an informal and supportive setting. The interdisciplinary, and international, emphasis of the Summer School allowed for a broader understanding of the issues in the technical and social spheres.

All topical sessions started with introductory lectures by invited speakers in the mornings, followed by parallel workshops and seminars in the afternoons. The workshops consisted of short presentations based on the contributions submitted by participating PhD students, followed by active discussions.

Contributions combining technical, social, ethical or legal perspectives were solicited. Keynote speeches provided the focus for the theme of the Summer School-Lifelong Privacy, Privacy Aspects of Social Networks, Privacy of Data, Transparency and Data subject Access, Privacy Principles for Identity Management, Economic Privacy Aspects, Identity and Legal, Technical and Economic Aspects of a new regulatory Framework-and the contributions from participants enhanced the ideas generated by the keynote speeches. The Summer School was a very successful event. More than 50 delegates from more than 15 countries actively participated. We succeeded in initiating intensive discussions between PhD students and established researchers from different disciplines.

These proceedings include both keynote papers and submitted papers accepted by the Program Committee, which were presented at the Summer School. The review process consisted of two steps. In the first step, contributions for presentation at the Summer School were selected based on reviews of submitted short papers by the Summer School Program Committee. The second step took place after the Summer School, when the authors had an opportunity to submit their final full papers addressing discussions at the Summer School. The submissions were again reviewed, by three reviewers each, and those included in these proceedings were carefully selected by the International Summer School Program Committee and by additional reviewers according to common quality criteria.

It is our pleasure to thank the members of the Program Committee, the additional reviewers, the members of the Organizing Committee as well as all the speakers. Without their work and dedication, this Summer School would not have been possible. Last but not least, we owe special thanks to the PrimeLife project, SAP, Microsoft Research, Eurecom, HumanIT at Karlstad University as well as IFIP for their support.

March 2010

Michele Bezzi Penny Duquenoy Simone Fischer-Hübner Marit Hansen

•

  The IFIP World Computer Congress, held every second year; • Open conferences; • Working conferences.The flagship event is the IFIP World Computer Congress, at which both invited and contributed papers are presented. Contributed papers are rigorously refereed and the rejection rate is high.

	As with the Congress, participation in the open conferences is open to all and
	papers may be invited or submitted. Again, submitted papers are stringently ref-
	ereed.

  Corresponding members are not represented in IFIP bodies. Affiliated membership is open to non-national societies, and individual and honorary membership schemes are also offered.

	Michele Bezzi Penny Duquenoy
	Simone Fischer-Hübner Marit Hansen
	Ge Zhang (Eds.)
	Privacy and
	Identity Management
	for Life
	5th IFIP WG 9.2, 9.6/11.7, 11.4, 11.6/PrimeLife
	International Summer School
	Nice, France, September 7-11, 2009
	Revised Selected Papers

Program Committee

Jan Camenisch IBM Research, Switzerland, IFIP WP 11.4 Chair Mark Gasson University of Reading, UK Hans Hedbom Karlstad University, Sweden Tom Keenan University of Calgary, Canada Dogan Kesdogan Siegen University, Germany Kai Kimppa University of Turku, Finland Eleni Kosta KU Leuven, Belgium Ronald Leenes Tilburg University, The Netherlands Elisabeth de Leeuw Ordina, The Netherlands, IFIP WG 11.6 Chair Marc van Lieshout Joint Research Centre, Spain Javier Lopez University of Malaga, Spain Vaclav Matyas Masaryk University, Brno, Czech Republic Martin Meints Independent Centre for Privacy Protection Schleswig-Holstein, Kiel, Germany Jean-Christophe Pazzaglia SAP Research, France Uli Pinsdorf Europäisches Microsoft Innovations Center GmbH/EMIC, Germany Andreas Pfitzmann TU Dresden, Germany

Organization

The PrimeLife/IFIP Summer School 2009 was organized by the EU FP7 Project PrimeLife and the IFIP Working Groups 9. 2, 9.6/11.7, 11.4 and 11.6.

General Chair


Zoltan Dombovari

Jokin Munoa

Rachel Kuske

Gabor Stepan

Non-smooth torus to identify domain of attraction of stable milling processes

The presented work shows a possible model dealing with the non-smooth flyover effect in milling processes. The excitation force of the general modal model of milling process is delayed, nonlinear, time-periodic and piecewise smooth. Apart from a state independent switch originated from the so-called radial immersion, flyover causes difficulties in connection with accurate depiction of the anyway quasi-periodic solution. From industrial point of view, the 'size' of this non-smooth quasi-periodic solution is essential to predict approximately the attraction zone of the stable time-periodic stationary solution calculated using linear theories.

Introduction

Recent technological trends tend to introduce cyber physical system (CPS, [START_REF] Monostori | Cyberphysical systems in manufacturing[END_REF]) solutions in machine tools to self-sense and self-act during cutting operations. These capabilities of this envisioned enhanced machine tool [START_REF] Munoa | Active suppression of structural chatter vibrations using machine drives and accelerometers[END_REF] need to be strengthened by more accurate modelling of the combined controlled cutting process. To ensure quality and productivity requirements vibration must be attenuated. The regeneration, when the past motion of the tool excites the dynamics via the just cut surface is known since the middle of the last century published by the Pioneers in [START_REF] Tlusty | Self-excited vibrations on machine tools[END_REF] and in [START_REF] Tobias | Machine-tool Vibration[END_REF]. Mathematically, the system can be represented by delay differential equations (DDEs), which generate infinite dimensional phase space. Particularly, milling is a time periodic delayed system [START_REF] Dombovari | General Milling Stability Model for Cylindrical Tools[END_REF]. By this form, the asymptotic stability of the stationary cutting solution can be predicted as an important technological requirement in the industry. Unstable stationary cutting leads to the onset of growing vibration limited by a threshold effect when cutting edges, often irregularly, leave and enter the cutting state. This, generally high amplitude limiting vibration is mathematically stable. In its developed form, it is referred as chatter vibration, while the threshold effect that limits the vibration is called as fly-over by the machine tool industry. Apart from the purely nonlinear origin bistable region caused by smooth quasi-periodic solutions in milling [START_REF] Dombovari | On the bistable zone of milling processes[END_REF], tight attraction zone can be formed around the stable stationary solution due to only the non-smooth fly-over effect. This was first experienced using time-domain solution in the motivational work in [START_REF] Munoa | Interaction between multiple modes in milling processes[END_REF]. In this article island-like stability domain (figure 1a) were presented that are enclosed by Hopf-and period doubling (PD)-kind stability boundaries. As it was shown in that paper, this was originated from the interactions of multiple modes through modulations of the main vibration frequency of the critical 'self-excited' solution. However, in the presented particular example, this island was experienced to have tight attraction zone (figure 1b) by simulation of the corresponding piecewise linear but fly-over model. This work shows methods to predict the size of the attraction zone approximately and also to envision a general numerical description to calculate the real threshold case as a quasi-periodic solution.

Milling model with fly-over

In order to have an industrially acceptable model multiple modes are considered with their modal coordinates q. The model shown below includes proportionally damped modes with modal damping ratios ξ k and natural angular frequencies ω n,k characterised by real-valued mode shapes U. Spatial solution is r(t) = Uq(t) (r = col(x, y, z)), while the state is given by q t (ϑ) = q(t + ϑ) if ϑ  [-τ max ; 0]. In this case the governing equation and the regenerative force are given as

                                       Z i t i i i i p t t k k k t h t g t t g a t t t t t 1 T 2 , n , n , , , , 2
       r f T r F r F U q q q    (1)
and described completely in [START_REF] Dombovari | On the bistable zone of milling processes[END_REF]. Possible nonliearities are originated from the specific cutting force characteristics f (h), which carries the regeneration (delay) effect denoted symbolically by r t (ϑ) in momentary chip thickness h i (t, r t (ϑ)). This model is able to describe milling processes with momentary positions φ i (t) of the uniformly placed edges of the rotating milling tool. The asymptotic stability of the time periodic stationary cutting solution q p (t) = q p (t + T) (T = 2π/Ω ) can be determined by perturbation u(t) = q(t) -q p (t) and linearisation of (1) around q p , which results in the so-called stability lobe diagrams (see figure 1a).

Different discontinuity effects in milling

The switching function in (1) swaps different excitation patterns causing discontinuities in second derivatives of q(t). It can be separated to a state independent screen function related to the radial immersion g ri and a state dependent fly-over related one g fo as

                 t i i t i i t g t g t g t g q q , , : , fo ri   (2)
Considering the state independent radial immersion with entry φ en and exit φ ex angles is straightforward and widely taken into account in piecewise analytical and numerical solutions with g ri (φ i (t)) = 1 if φ en < (φ i (t)mod2π) < φ ex , otherwise g ri (φ i (t)) = 0. The time and state dependent switching conditions h i (t, q t (θ)) = 0 (see figure 1c) are causing the real problems in this framework. These are described with g fo,i (t, q t (ϑ)) = 1 if h i (t, q t (ϑ)) > 0, otherwise g fo,i (t, q t (ϑ)) = 0. Remark that, in required stable stationary solution, when lim t→∞ q(t) = q p (t) the g fo,i 's are simply not active. Instability on stationary solution or nonlinearity induced unstable tori solutions (bistability, see [START_REF] Dombovari | On the bistable zone of milling processes[END_REF]) 'push' the solution to reach g fo,i 's.

Figure 1: a) stability chart with and island, b) time domain simulations at γ, c) fly-over in milling according to [START_REF] Dombovari | On the bistable zone of milling processes[END_REF].

A prediction of chattering amplitude

The case presented in figure 1a contains an island with tight attraction zone tested in figure 1b. Accordingly, a method is needed that only serves a rough answer for the size of the attraction zone, and can be used for characterization of 'linearly' stable domain easily using the results of the asymptotic stability analysis of q p (t). Time domain based asymptotic methods like semi-discretization (SD) is able to determine the so-called Floquet multipliers μ for the corresponding time periodic system with T Z = T/Z. At the stability border its magnitude is simply |μ cr | = 1. By using the corresponding eigenvector s cr , a

sample perturbation            cr cr cr cr s s u  
can be given along the stability boundary that can be used for constructing a prototype of the quasi-periodic solution with frequencies ω Z,l = 2π/T Z l and ω q = |arg μ cr +2πq|/T Z . These latter ones are described in the numerical solution of s cr (θ) originated from the SD. As ω Z,l and ω q are not locked, and the correct 'phase shift' is granted by SD between q p and u, the quasi-periodic solution densely occupies the invariant torus with q QP (t, r) = q p (t)+ru(t). If f (h) in ( 1) is linear, and we assume only slight change in spectrum ω q , the switching conditions can be granted with h i (t, q QP (t, r)) = 0 for i = 1, 2, …, Z. Then r gives an idea what magnitude the attraction zone can have around the region in question. Of course, in linear case, there is no nonlinearity induced bistability as it is described in [START_REF] Dombovari | On the bistable zone of milling processes[END_REF], but perhaps the encirclement of the island in figure 1a by three different borders creates an only non-smooth bistability region. Apart from predicting roughly the attraction zone, this prediction can be used as a prototype solution for unstable/stable transition for dynamic bifurcation analysis.

Numerical non-smooth boundary solver

For more accurate calculation, a transition between a nonlinear and linear description, Enders' exponential cutting force characteristics can be used. It can be parametrised as f (h) := f E (h, γ) = K e (1-e -h/γ )+K c h. Here γ is the transition parameter, while K e , and K c are technological parameters. By taking the limit of γ toward zero in f E (h, γ), the structure of the nonsmooth induced bistability can be unfolded over the island depicted in figure 1a. In the end, to reveal the real structure of the dynamics 'around' the island, the nonlinear/linear transition has to be followed by an appropriate boundary value problem (BVP) solver. Calculating an invariant torus even for state independent discontinuity g ri has to be represented with an appropriate mesh. Starting from a critical stationary cutting solution, g fo can be reached along the subcritical branch as in [START_REF] Dombovari | On the bistable zone of milling processes[END_REF]. Passing this first grazing of the solution, the non-smooth condition function(s) g fo has(have) to be represented by irregular triangularisation of the invariant torus by using proper interpolation and quadrature schemes.

Acknowledgement

ERC Advanced gran no. 340889., János Bolyai Research Scholarship (BO/00589/13/6) and OTKA grant no. K108779.


Samuel Deslauriers-Gauthier

Jean-Marc Lina

Russell Butler

Pierre-Michel Bernier

Kevin Whittingstall

Rachid Deriche

Maxime Descoteaux

Inference and Visualization of Information Flow in the Visual Pathway using dMRI and EEG

We propose a method to visualize information flow in the visual pathway following a visual stimulus. Our method estimates structural connections using diffusion magnetic resonance imaging and functional connections using electroencephalography. First, a Bayesian network which represents the cortical regions of the brain and their connections is built from the structural connections. Next, the functional information is added as evidence into the network and the posterior probability of activation is inferred using a maximum entropy on the mean approach. Finally, projecting these posterior probabilities back onto streamlines generates a visual depiction of pathways used in the network. We first show the effect of noise in a simulated phantom dataset. We then present the results obtained from left and right visual stimuli which show expected information flow traveling from eyes to the lateral geniculate nucleus and to the visual cortex. Information flow visualization along white matter pathways has potential to explore the brain dynamics in novel ways.

Introduction

The brain can be described as a network of interconnected information processing nodes. Each node, corresponding to a brain region, is specialized for a specific type of information. It is the interaction of the different nodes via the connections of the network that allows the brain to process and appropriately respond to external stimuli. Consider a subject that is asked to reach for and grasp an object when a visual cue is presented. First, visual information is transferred from the retina to the primary visual cortex through the optic nerve, optic tract and optic radiation. It is then expected that the reach and grasp component of the task will be handled separately by subregions of the parietal and premotor cortex [START_REF] Gallivan | Neural coding within humain brain areas involved in actions[END_REF]. Finally, the primary motor cortex will be involved to initiate the reaching movement. Individually, the visual, parietal, premotor, and motor cortex cannot produce the desired task. It is their interaction, or more specifically their exchange of information, that allows the subject to reach and grasp the object. The ability to image and observe the interaction of the different regions of the brain would therefore be invaluable to our understanding of the brain.

In this work, we present a new model of information flow in the brain built on the previous work of [START_REF] Amblard | Biomagnetic source detection by maximum entropy and graphical models[END_REF]. First, we build a Bayesian network which captures the state of the cortical surface of the brain and their connections. The network is subject specific as it is built from the structural connectivity via diffusion magnetic resonance imaging (MRI). Next, we introduce the electroencephalography (EEG) measurements as evidence into this network. Finally, using the principle of maximum entropy on the mean, we infer the posterior probability that cortical regions and connections are active. By projecting activation probabilities of connections back onto the streamlines obtained from diffusion MRI, we generate an animated representation of information flow. Thus, by combining functional information obtained from EEG with anatomical information obtained in diffusion MRI, we infer the information flow in the white matter of the brain.

Theory

We model the cortical activity using a distributed dipole model. The activation of a small area of the cortical surface is modeled by a dipole n that is perpendicular to the surface and whose intensity at a time t is given by x n,t ∈ IR. We distribute thousands of these dipoles on the cortical surface and combine their intensities in a vector x ∈ IR N d Nt where N d and N t are the number of dipoles and samples, respectively. The forward problem can then be modeled as m = Gx + where m ∈ IR NsNt is the vector of EEG measurements with N s the number of sensors. The matrix G is the lead field that projects the dipole intensities onto the sensors. It can be computed using the anatomical MR images of the subject [START_REF] Gramfort | OpenMEEG: opensource software for quasistatic bioelectromagnetics[END_REF] and is therefore a known quantity. The observation are corrupted by the additive noise term . Note that we consider all time samples in a single very large problem which makes the forward operator G block diagonal.

Connectivity informed maximum entropy on the mean

The vector of dipole intensities x represents the cortical activity for a given time window. Estimating these intensities from the measurements m is an ill-posed problem. We have many more intensities to estimate than available measurements. In [START_REF] Amblard | Biomagnetic source detection by maximum entropy and graphical models[END_REF], Amblard et al. propose to group the dipoles into N S cortical regions, which we refer to as clusters. Each cluster is assigned a state variable which dictates the possible intensities of dipoles within the cluster. Let S k represent the state of the k th cluster, that is whether it is active or not. Let S = [S 1 , S 2 , ..., S N S ] be the cluster state vector. Note that like m and x, the vector S incorporates a time component. That is, if the cortical surface is segmented into 60 regions and the data window contains 10 time points, S contains 600 state variables. Let dµ(x, S) = µ(x, S)dx be a reference law that represents the a priori information of the dipole intensities and cluster states. We assume the source amplitudes x k of the k th cluster depends only on the state of the cluster S k to get dµ(x, S) = π(S)

N S k=1 dµ(x k |S k ) (1)
where π(S) is the joint probability law of the cluster states. This distribution, along with the assumption of independent cluster states, was used by [START_REF] Amblard | Biomagnetic source detection by maximum entropy and graphical models[END_REF] to constrain the inverse problem and estimate the dipole intensities.

The output of a tractography pipeline is a set of streamlines which represent the white matter fiber bundles. When streamlines begin in a cluster and end in another, we say that those two clusters are connected. A connection between two clusters is characterized by its length, which is the average length of the streamlines that reach those clusters. We treat these connections as wires or pipes which allow communication between cortical regions. The state of a cluster at a time t 0 can influence the state of a different cluster at a time t ∆ if they are connected. The delay ∆ is proportional to the length of the connection and the speed at which information flows in the connection. For example, if a cluster is known to be active at a time t 0 , it increases the likelihood that its connected counterpart is active at a time t ∆ . This spatio-temporal regularization constitutes an additional prior and is therefore included in the model by modifying the distribution [START_REF] Gallivan | Neural coding within humain brain areas involved in actions[END_REF]. The connections are added as a new set of variable which represent connection states. Much like the state of the clusters affect the dipoles, the state of the connections affect clusters. That is, the state of a connection C i gives us information about the state of the clusters it connects. Like clusters, we assume connections are either active or inactive. Let C be the connection state vector, the updated prior information on sources, clusters, and connections is then given by dµ(x, S, C) = ϕ(C)π(S|C)

N S k=1 dµ(x k |S k ) (2)
where ϕ(C) is the joint probability law of the connection states. The distribution (2) is too general. It allows the state of a cluster to be affected by a connection that does not reach it. We therefore assume that the state of a cluster depends only on the connections that reach it. If we let C γ(k) be the connections that reach the k th cluster, the joint distribution of the cluster states given the connection states is

π(S|C) = N S k=1 π(S k |C γ(k) ). (3)
Finally, we assume that the state of a connection is independent of other connection which, along with (3) yields

dµ(x, S, C) = N C i=1 ϕ(C i ) N S k=1 π(S k |C γ(k) )dµ(x k |S k ). ( 4
)
The distribution (4) contains all of the available prior information. It describes our prior knowledge of the source intensities, cluster states, and connection states given no EEG measurements. The next step is to insert the observed EEG measurements as evidence and thus be able to infer the posterior probability of any given source, cluster, and connection configuration. Let the dipole intensities x have a probability law dp(x), distinct from the reference law dµ(x) described previously. The objective of the MEM algorithm is to find the probability law dp * (x) = p * (x)dx that satisfies m = Gx * with x * = xp * (x)dx [START_REF] Gramfort | OpenMEEG: opensource software for quasistatic bioelectromagnetics[END_REF] while minimizing the distance to the reference law measured using the Kullback-Leibler divergence D KL (p(x)|dµ(x)). In other words, the solution is the probability law dp * (x) closest to the reference law dµ(x) that explains the observations on average. By introducing Lagrange multipliers, minimizing D KL (p(x)|dµ(x)) subject to (5) can be written as minimize p(x),λ,λ0

D KL (p(x)|dµ(x)) + λ T (m -G xp(x)dx) + λ 0 (1 -dp(x)). ( 6
)
The first term is the entropy of the model, the second is the data fit, and the third ensures p(x) is a probability distribution. Equation ( 6) can be thought of as finding the optimal compromise between the uncertainty (i.e. entropy) of the model and the observations. If we assume the noise is Gaussian with zero mean, the unique optimal Lagrange multipliers λ * can be determined by solving [START_REF] Amblard | Biomagnetic source detection by maximum entropy and graphical models[END_REF] λ * = arg min

λ ln Z(λ) + (λ T m -λ T Σ 2 λ) (7)
where Σ 2 is the variance of the additive noise and where Z(λ) is the partition function given by

Z(λ) = exp (λ T Gx)dµ(x). (8)
Note that [START_REF] Girard | Towards quantitative connectivity analysis: reducing tractography biases[END_REF] does not depend on p(x) or λ 0 , which can be determined from the unique minimizer λ * . Finding the optimal Lagrange multipliers from (7) requires evaluating Z(λ) which in turn requires the reference law dµ(x). We propose to obtain this reference law by marginalizing S and C out of (4), that is

dµ(x) = {C} N C i=1 ϕ(C i ) {S} N S k=1 π(S k |C γ(k) )dµ(x k |S k ) (9)
where the sum over {C} indicates a sum over all possible realizations of C. The optimal Lagrange multipliers λ * are identified by solving (7) which requires evaluating Z(λ) repeatedly. The sum over all possible states of C which appears in ( 9) is prohibitive because it generates 2 Nc terms which quickly becomes intractable. This problem can be mitigated by noting that Z(λ) is the unnormalized sum of the marginal probability of any variable in C or S. All terms in the sum need not be evaluated because the state of a cluster depends only on a few connections. Using a suitable variable elimination order, which depends on the specific connections between clusters, the sum of products can be rearranged to compute Z(λ) efficiently.

Methods

Synthetic data

To validate our algorithm, synthetic EEG data was generated using a simplified model of the visual system. The model consists of two clusters of 10 sources representing the left and right primary visual cortices. In addition, the model contains four clusters representing the lateral geniculate nuclei (LGN) and the eyes. These four clusters each have a single invisible source, i.e. their corresponding column of G contains only zeros. Bidirectional connections are present between the LGN and between the visual cortices. Unidirectional connections link the eyes to the LGN and the LGN to the visual cortices. To simulate signals, information is propagated from the eyes to the LGN and to the visual cortex by selecting random connections. When a cluster is activated by one of its connections, the correspond sources are activated. The synthetic EEG signals are then recorded by two sensors located near the visual cortices. Gaussian noise is added to the synthetic EEG measurements to obtain the desired signal to noise ratio (SNR) defined as the variance of the signal over the variance of the noise.

To quantify how the SNR affects our algorithm's ability to recover information flow patterns, synthetic signals were generated with an SNR varying between 1 and 20. These signals were then used to recover the posterior probability that each connection was active. A recovery was deemed successful if all connections used to simulate the data obtained a posterior probability above 0.5 while all other posterior probabilities were below 0.5.

Experimental data acquisition and preprocessing

Magnetic resonance images and EEG signals were acquired on a healthy volunteer. The MR images included diffusion weighted images acquired using a SPLICE sequence (b-value 1000 s/mm 2 , 64 directions) and a T1 weighted image. The SPLICE sequence was selected over a more common EPI sequence because it does not generate distortions near the eyes and allows us to track the optic nerve and optic tract. Fiber orientation distribution functions were computed using constrained spherical deconvolution [START_REF] Tournier | Robust determination of the fibre orientation distribution in diffusion MRI: Non-negativity constrained super-resolved spherical deconvolution[END_REF] implemented in dipy [START_REF] Garyfallidis | Dipy, a library for the analysis of diffusion MRI data[END_REF]. Fiber tracking was performed using anatomically constrained particle filter tractography [START_REF] Girard | Towards quantitative connectivity analysis: reducing tractography biases[END_REF] also implemented in dipy. The surface of the cortex was extracted and segmented from the T1 weighted image using FreeSurfer and then downsampled to 8000 vertices. The forward operator G was computed using OpenMEEG [START_REF] Gramfort | OpenMEEG: opensource software for quasistatic bioelectromagnetics[END_REF][START_REF] Kybic | A common formalism for the integral formulations of the forward EEG problem[END_REF].

After the MR acquisition, the subjects were fitted with a 64 channel acti-CAP (Brain Products GmbH) EEG cap. The subjects were seated in front of a computer screen in a dark quiet room and were asked to fixate on a red circle appearing at the center of the screen. The visual stimuli consisted of a circle appearing on the left or right side of the screen. One run consisted of 50 left and 50 right visual cues randomly interleaved. A total of 10 runs were performed, 5 with each stimuli. The EEG signals were separated into 150ms epochs starting at the stimulus onset. Epochs with blink artifacts were excluded from further analysis. All remaining epochs for each stimuli were averaged and downsampled to 100Hz.

Model parameters

The model presented above relies on several parameters. First, the information velocity must be specified to compute the delay associated with each connection. Here, we assume a constant velocity of 6 m/s [START_REF] Tomasi | Areal differences in diameter and length of corticofugal projections[END_REF] for all connections of the brain. Next, the parameters of the prior distribution dµ(x, S, C) must be given. Connections and clusters are initialized with a 0.9 probability of being inactive. However, when a connection is active, the clusters it connects must also be active. Finally, the intensity of sources follows a Gaussian distribution with zero mean. If the cluster is active or inactive, the variance of the distribution is 1e-4 or 1e-7, respectively.

Results

Figure 1 illustrates the rate of successful information flow recovery averaged over 100 realizations for each SNR. The rate of recovery sharply rises between a SNR of 5 and 10. An example of a successful recovery is illustrated in Figure 2 through the optic nerve and optic chiasm to reach the right LGN. The information then goes through the optic radiation to reach the occipital lobe. Notably, the right LGN and right optic radiation have a higher posterior probability than their left counterpart, consistent with the expected visual activation. Similar results are obtained for the right visual stimuli, however the right and left visual pathways are activated with similar posterior probabilities.

Conclusion

By combining structural connectivity information from diffusion MRI and functional information from EEG, our algorithm is able to infer information in the white matter of the brain. We evaluated the rate of successful recovery using synthetic data and presented preliminary in vivo results of information flow in the visual pathway. In this study, a constant information velocity of 6m/s was assumed for all connections of the brain. However, it should be noted that our model is not specific to this assumption and can accommodate different information velocities for different connections. In the future, it may be possible to tune information speed using additional micro-structure information such as axon diameter or myelination. Our method represents a promising new approach to visualizing brain dynamics and connectomics across white matter pathways.

Fig. 1 .

 1 Fig. 1. Rate of successful information flow recovery at different SNR.

  Figure 1 illustrates the rate of successful information flow recovery averaged over 100 realizations for each SNR. The rate of recovery sharply rises between a SNR of 5 and 10. An example of a successful recovery is illustrated in Figure 2. The left part of the figure presents the posterior probabilities projected back onto the model and animated. Information can be seen flowing through the different clusters. The right part of the figure presents and overview of the same results in the form of a flow diagram. Each row of the graph represents a cortical region and the circles correspond to individual time points. Information flow in connections is illustrated by lines connecting cortical regions at different time points. In both cases, green indicates a high probability that a region or connection is active whereas white indicates a low probability. Reconstruction of the information flow following a left and right visual stimulus is illustrated in Figure 3. For the left visual stimulus, information flow

Fig. 2 .

 2 Fig. 2. Reconstruction of the information flow from the left eye, to the right LGN, to right visual, to the left visual (SNR = 5). The left of the figure is a video of the information flow projected back onto the model. The right of the figure presents the same information in the form of an information flow diagram.

Fig. 3 .

 3 Fig. 3. Video of the reconstructed information flow in the visual pathway for the 120ms following a left (a) or right (b) visual stimulus.

Acknowledgement

This work has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (ERC Advanced Grant agreement No 694665 : CoBCoM -Computational Brain Connectivity Mapping).