Vagia Karyoti
email: vagiakaryo@math.auth.gr

Paulina Paraponiari

Weighted PCL over product valuation monoids

Keywords: Software architectures, configuration logics, product valuation monoids, weighted configuration logics, quantitative features

We introduce a weighted propositional configuration logic over a product valuation monoid. Our logic is intended to serve as a specification language for software architectures with quantitative features such as the average of all interactions' costs of the architecture and the maximum cost among all costs occurring most frequently within a specific number of components in an architecture. We provide formulas of our logic which describe well-known architectures equipped with quantitative characteristics. Moreover, we prove an efficient construction of a full normal form which leads to decidability of equivalence of formulas in this logic.

Introduction

Architectures are a critical issue in design and development of complex software systems since they characterize coordination principles among the components of a system. Whenever the construction of a software system is based on a "good" architecture, then the system satisfies most of its functional and quality requirements. Well-defined architectures require a formal treatment in order to efficiently characterize their properties. A recent work towards this direction is [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF], where the authors introduced propositional configuration logic (PCL for short) which was proved sufficient enough to describe architectures: the meaning of every PCL formula is a configuration set, which intuitively represents permissible component connections, and every architecture can be represented by a configuration set on the collection of its components. Furthermore, the authors of [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF] studied the relation among architectures and architecture styles, i.e., architectures with the same types of components and topologies.

PCL is a specification logic of software architectures which is able to describe their qualitative features. However, several practical applications require also quantitative characteristics of architectures such as the cost of the interactions among the components of an architecture, the time needed, or the probability of the implementation of a concrete interaction. For instance, several IoT and cloud applications, which are based on Publish/Subscribe architecture, require quantitative features [START_REF] Olivieri | A publish-subscribe approach to IoT integration: the smart office use case[END_REF][START_REF] Patel | Publish/Subscribe mechanism for IoT: A survey of event matching algorithms and open research challenges[END_REF][START_REF] Yang | Privacy-preserving attributekeyword based data publish-subscribe service on cloud platforms[END_REF]. Moreover, considering a set of components and an architecture style, there may occur several architectures where each of them has a specific amount of some resource (e.g. memory or energy consumption). In such a setting, the most suitable architecture must be chosen, depending on the available resources or the performance. Generally, quantitative properties are essential for performance related properties and for resource-constrained systems.

The authors in [START_REF] Paraponiari | On weighted configuration logics[END_REF] introduced and investigated a weighted PCL (wPCL for short) over a commutative semiring (K, ⊕, ⊗, 0, 1) which serves as a specification language for the study of software architectures with quantitative features such as the maximum cost of an architecture or the maximum priority of a component. Nevertheless, operations like average for response time or power consumption cannot be described within the algebraic structure of semirings. Such operations are important for practical applications and have been investigated for weighted automata in [START_REF] Chatterjee | Quantitative languages[END_REF][START_REF] Chatterjee | Expressiveness and closure properties for quantitative languages[END_REF][START_REF] Chatterjee | Computing Average Response Time[END_REF]. In [7,[START_REF] Droste | Weighted automata and weighted MSO logics for average and long-time behaviors[END_REF] the authors provided valuation monoids as a general algebraic framework, which describe several operations that cannot fit in the structure of semirings. More recently, in [START_REF] Otop | Quantitative Automata under Probabilistic Semantics[END_REF] nested weighted automata have been considered under probabilistic semantics for expressing properties such as "the long-run average resource consumption is below a threshold". Also, the authors in [START_REF] Chatterjee | Computing Average Response Time[END_REF] presented algorithms which are designed specifically for computing the average response time on graphs, game graphs, and Markov chains. However, the aforementioned works have not been developed for the setting of systems' architectures and therefore cannot express characteristics such as the average cost of an architecture or the maximum most frequent cost/priority that occurs in an architecture. In this paper, we tackle this problem by extending the work of [START_REF] Paraponiari | On weighted configuration logics[END_REF]. Specifically, we introduce and investigate a weighted PCL over product valuation monoids (w pvm PCL for short) which is proved sufficient to serve as a specification language for software architectures with important quantitative features that are not covered in [START_REF] Paraponiari | On weighted configuration logics[END_REF].

The contributions of our work are the following. We introduce the syntax and semantics of w pvm PCL. The semantics of w pvm PCL formulas are polynomials with values in the product valuation monoid. Then, in our main result, we prove that for every w pvm PCL formula over a set of ports and a product valuation monoid with specific properties, we can effectively construct an equivalent one in full normal form, which is unique up to the equivalence relation. The second main result is the decidability of equivalence of w pvm PCL formulas. Lastly, we describe in a strict logical way several well-known software architectures with quantitative characteristics. We skip detailed proofs of our results which are similar to the corresponding ones of [START_REF] Paraponiari | On weighted configuration logics[END_REF] and [START_REF] Paraponiari | Weighted propositional configuration logics: A specification language for architectures with quantitative features[END_REF]. We refer the reader to the full version of our paper on arXiv [START_REF] Karyoti | Weighted PCL over product valuation monoids[END_REF].

Preliminaries

In this section, we recall valuation monoids and product valuation monoids [START_REF] Droste | Weighted automata and weighted MSO logics for average and long-time behaviors[END_REF]. A valuation monoid (D, ⊕, val, 0) consists of a commutative monoid (D, ⊕, 0) and a valuation function val : D + → D, where D + denotes the set of nonempty finite words over D, with val(d) = d for all d ∈ D and val(d 1 , . . . , d n ) = 0 whenever d i = 0 for some i ∈ {1, . . . , n}.

(D, ⊕, val, ⊗, 0, 1) is a product valuation monoid, or pv-monoid for short if (D, ⊕, val, 0) is a valuation monoid, ⊗ : D 2 → D is a binary operation, 1 ∈ D with val(1) 1≤i≤n = 1 for all n ≥ 1 and 0

⊗ d = d ⊗ 0 = 0, 1 ⊗ d = d ⊗ 1 = d for all d ∈ D.
The pv-monoid is denoted simply by D if the operations and the constant elements are understood. A pv-monoid

D is left-⊕-distributive if d ⊗ (d 1 ⊕ d 2 ) = (d ⊗ d 1 ) ⊕ (d ⊗ d 2 ) for any d, d 1 , d 2 ∈ D. Right-⊕-distributivity is defined analogously. If a pv-monoid D is both left-and right-⊕-distributive, then it is ⊕-distributive. If ⊗ is associative, then D is called associative. We call D left-val-distributive if for all n ≥ 1 and d, d i ∈ D with i ∈ {1, . . . , n}, it holds d ⊗ val(d 1 , . . . , d n ) = val(d ⊗ d 1 , . . . , d ⊗ d n ). Moreover, the pv-monoid D is called (additively) idempotent if d ⊕ d = d for every d ∈ D.
In the following we recall some pv-monoids from [START_REF] Droste | Weighted automata and weighted MSO logics for average and long-time behaviors[END_REF]. The algebraic structures (R ∪ {-∞}, max, avg, +, -∞, 0) and (R ∪ {+∞}, min, avg, +, +∞, 0) with avg(d 1 , . . . , d n ) = 1 n n i=1 d i are pv-monoids. More precisely, they are left-valdistributive and ⊕-distributive pv-monoids. Also, the structure (R∪{-∞, +∞}, min, maj, max, +∞, -∞), where maj(d 1 , . . . , d n ) is the greatest value among all values that occur most frequently among d 1 , . . . , d n , is a ⊕-distributive pvmonoid but not left-val-distributive. Both avg and maj are symmetric functions, i.e., the value of the function given n arguments is the same no matter the order of the arguments. Moreover, the pv-monoids mentioned before are idempotent.

Throughout the paper (D, ⊕, val, ⊗, 0, 1) will denote an idempotent pvmonoid where val is symmetric.

Let Q be a set. A formal series (or simply series) over Q and D is a mapping s : Q → D. The support of s is the set supp(s) = {q ∈ Q | s(q) = 0}. A series with finite support is called also a polynomial. We denote by D Q the class of all polynomials over Q and D.

Weighted propositional interaction logic

In this section, we introduce the weighted propositional interaction logic over pv-monoids. Firstly, we recall from [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF] the propositional interaction logic.

Let P be a nonempty finite set of ports. We let I(P ) = P(P )\{∅}, where P(P ) denotes the power set of P . Every set α ∈ I(P ) is called an interaction. The syntax of propositional interaction logic (PIL for short) formulas over P is given by the grammar

φ ::= true | p | φ | φ ∨ φ
where p ∈ P . As usual, we set φ = φ for every PIL formula φ and f alse = true. Hence, the conjunction of two PIL formulas φ, φ is defined by φ ∧ φ = φ ∨ φ . A PIL formula of the form p 1 ∧ • • • ∧ p n with n > 0, and p i ∈ P or p i = p i with p i ∈ P for every 1 ≤ i ≤ n, is called a monomial. For simplicity we denote a monomial p 1 ∧ • • • ∧ p n by p 1 . . . p n . Monomials of the form p∈P+ p ∧ p∈P-p with P + ∪ P -= P and P + ∩ P -= ∅ are called full monomials.

Let φ be a PIL formula and α an interaction. We define the satisfaction relation α |= i φ by induction on the structure of φ as follows:

-

α |= i true, -α |= i φ iff α |= i φ, -α |= i p iff p ∈ α, -α |= i φ 1 ∨ φ 2 iff α |= i φ 1 or α |= i φ 2 .
For every α ∈ I(P ) it holds α |= i f alse. Moreover, for every interaction α ∈ I(P ) we define its characteristic monomial m α = p∈α p∧ p ∈α p. A characteristic monomial m α is actually a full monomial that formalises the interaction α. Then, for every α ∈ I(P ) we trivially get α |= i m α iff α = α.

Throughout the paper P will denote a nonempty finite set of ports.

Definition 1. Let D be a pv-monoid. Then, the syntax of formulas of weighted PIL ( w pvm PIL for short) over P and D is given by the grammar

ϕ ::= d | φ | ϕ ⊕ ϕ | ϕ ⊗ ϕ
where d ∈ D and φ denotes a PIL formula over P.

We denote by P IL(D, P ) the set of all w pvm PIL formulas over P and D. Next, we present the semantics of formulas ϕ ∈ P IL(D, P ) as polynomials ϕ ∈ D I(P ) . For the semantics of PIL formulas φ over P we use the satisfaction relation as defined above. Hence, the semantics of PIL formulas φ gets only the values 0 and 1. Definition 2. Let ϕ ∈ P IL(D, P ). The semantics of ϕ is a polynomial ϕ ∈ D I(P ) . For every α ∈ I(P ) the value ϕ (α) is defined inductively on the structure of ϕ as follows:

-

d (α) = d, -ϕ 1 ⊕ ϕ 2 (α) = ϕ 1 (α) ⊕ ϕ 2 (α), -φ (α) = 1 if α |= i φ 0 otherwise , -ϕ 1 ⊗ ϕ 2 (α) = ϕ 1 (α) ⊗ ϕ 2 (α).

Weighted propositional configuration logic

In this section, we introduce and investigate the weighted propositional configuration logic over pv-monoids. But first, we recall the propositional configuration logic (PCL for short) from [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]. The syntax of PCL formulas over P is given by the grammar

f ::= true | φ | ¬f | f f | f + f
where φ denotes a PIL formula over P. The operators ¬, , and + are called complementation, union, and coalescing, respectively. The intersection is defined by

f 1 f 2 := ¬ (¬f 1 ¬f 2 ).
We let C(P ) = P(I(P ))\{∅}. For every PCL formula f and γ ∈ C(P ) the satisfaction relation γ |= f is defined inductively on the structure of f as follows:

-γ |= true, -γ |= ¬f iff γ |= f, -γ |= φ iff α |= i φ for every α ∈ γ, -γ |= f 1 f 2 iff γ |= f 1 or γ |= f 2 , -γ |= f 1 + f 2 iff there exist γ 1 , γ 2 ∈ C(P ) such that γ = γ 1 ∪ γ 2 ,
and

γ 1 |= f 1 and γ 2 |= f 2 .
We define the closure ∼ f of every PCL formula f by ∼ f := f + true.

Two PCL formulas f, f are called equivalent, and we denote it by f ≡ f , whenever γ |= f iff γ |= f for every γ ∈ C(P ). We refer the reader to [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF] and [START_REF] Paraponiari | On weighted configuration logics[END_REF] for properties of PCL formulas.

Next, we introduce our weighted PCL over pv-monoids.

Definition 3. Let D be a pv-monoid. The syntax of formulas of the weighted PCL ( w pvm PCL for short) over P and D is given by the grammar

ζ ::= d | f | ζ ⊕ ζ | ζ ⊗ ζ | ζ ζ | * ζ
where d ∈ D, f denotes a PCL formula over P , and denotes the coalescing operator among w pvm PCL formulas. The operator * is called valuation operator.

We denote by PCL(D,P) the set of all w pvm PCL formulas over P and D. We present the semantics of formulas ζ ∈ P CL(D, P ) as polynomials ζ ∈ D C(P ) . For the semantics of PCL formulas we use the satisfaction relation as defined previously. -

d (γ) = d, -f (γ) = 1 if γ |= f 0 otherwise , -ζ 1 ⊕ ζ 2 (γ) = ζ 1 (γ) ⊕ ζ 2 (γ), -ζ 1 ⊗ ζ 2 (γ) = ζ 1 (γ) ⊗ ζ 2 (γ), -ζ 1 ζ 2 (γ) = γ1 • ∪γ2=γ ( ζ 1 (γ 1 ) ⊗ ζ 2 (γ 2 )), - * ζ (γ) = n>0 • n i=1 γi=γ val ( ζ (γ 1 ), . . . , ζ (γ n ))
where • ∪ denotes that the sets γ 1 , . . . , γ n consist a partition of γ for every n > 0.

It is important to note here that since the semantics of every w pvm PCL formula is defined on C(P ), the sets γ 1 and γ

2 in ζ 1 ζ 2 (γ) and the sets γ 1 , . . . , γ n in * ζ (γ) are nonempty. Trivially in * ζ (γ), the maximum value of n is |γ|, i.e., the cardinality of γ. Hence, * ζ (γ) = n∈{1,...,|γ|} • n i=1 γi=γ val ( ζ (γ 1 ), . . . , ζ (γ n )) .
Moreover, in * ζ (γ), let the sets γ i ∈ C(P ) where i ∈ {1, . . . , n} and Next, we present several properties of our w pvm PCL formulas.

• n i=1 γ i = γ. Consider a permutation (i 1 , . . . , i n ) of (1, . . . , n). Then val( ζ (γ 1 ) . . . , ζ (γ n )) = val( ζ (γ i1 ), . . . , ζ (γ in )). Hence, val( ζ (γ 1 ), . . . , ζ (γ n )) ⊕ val( ζ (γ i1 ), . . . , ζ (γ in )) = val( ζ (γ 1 ), . . . , ζ (γ n ))
Proposition 1. Let ζ, ζ 1 , ζ 2 , ζ 3 ∈ P CL(D, P ) and d ∈ D. Then (i) ζ 0 ≡ 0 ≡ 0 ζ. If ⊗ is commutative, then (ii) ζ 1 ζ 2 ≡ ζ 2 ζ 1 . If D is associative and ⊕-distributive, then (iii) (ζ 1 ζ 2 ) ζ 3 ≡ ζ 1 (ζ 2 ζ 3 ). If D is left-⊕-distributive, then (iv) ζ ⊗ (ζ 1 ⊕ ζ 2 ) ≡ (ζ ⊗ ζ 1 ) ⊕ (ζ ⊗ ζ 2 ). If D is right-⊕-distributive, then (v) (ζ 1 ⊕ ζ 2 ) ⊗ ζ ≡ (ζ 1 ⊗ ζ) ⊕ (ζ 2 ⊗ ζ). Proposition 2. Let ζ ∈ P CL(D, P ) with ζ = d ∈ D. If D is left-val-distributi- ve, then * ζ ≡ d.
Proof. For every γ = {a 1 , . . . , a s } where s ∈ N, we have

* ζ (γ) = n∈{1,...,s} γ1 • ∪... • ∪γn=γ val( ζ (γ 1 ), ..., ζ (γ n )) = val(d) ⊕ val(d, d) ⊕ ... ⊕ val( s times d, ..., d) = (d ⊗ val(1)) ⊕ (d ⊗ val(1, 1)) ⊕ ... ⊕ (d ⊗ val(1, ..., 1)) = (d ⊗ 1) ⊕ (d ⊗ 1) ⊕ ... ⊕ (d ⊗ 1) = d ⊕ ... ⊕ d = d
where the second and the last equalities hold since D is idempotent, and the third one since D is left-val-distributive.

Moreover, D is called ⊕-preservative whenever val(d 1 ⊕ d 2 , d) = val(d 1 , d) ⊕ val(d 2 , d) and val(d, d 1 ⊕ d 2 ) = val(d, d 1 ) ⊕ val(d, d 2 ) for every d, d 1 , d 2 ∈ D.
Proof. Let γ ∈ C(P ). Then * (∼ ζ) (γ) = n>0 γ1 • ∪... • ∪γn=γ val( ∼ ζ (γ 1 ), ... , ∼ ζ (γ n )) = n>0 γ1 • ∪... • ∪γn=γ val   γ 1 ⊆γ1 ζ (γ 1 ), ... , γ n ⊆γn ζ (γ n )   = n>0 γ1 • ∪... • ∪γn=γ γ 1 ⊆γ1
...

γ n ⊆γn val( ζ (γ 1 ), ... , ζ (γ n )) = γ ⊆γ n>0 γ1 • ∪... • ∪γn=γ val( ζ (γ 1 ), ... , ζ (γ n )) = γ ⊆γ * ζ (γ ) = ∼ ( * ζ) (γ)
where the third equality holds since D is ⊕-preservative and the next equalities due to the commutativity of ⊕.

Proposition 5. Let ζ, ζ 1 , ζ 2 ∈ P CL(D, P ). If D is left-⊕-distributive, then ζ (ζ 1 ⊕ ζ 2 ) ≡ (ζ ζ 1 ) ⊕ (ζ ζ 2 ).
Next, we show a special case when ⊗ distributes over . In general ⊗ does not distribute over .

(R ∪ {-∞}, max, avg, +, -∞, 0), then it is easy to show that ζ ⊗ (ζ 1 ζ 2 ) (γ) = (ζ ⊗ ζ 1 ) (ζ ⊗ ζ 2 ) (γ). Hence, ζ ⊗ (ζ 1 ζ 2 ) ≡ (ζ ⊗ ζ 1 ) (ζ ⊗ ζ 2 )
. However, this is not the case when ζ is a PIL formula and D is left-⊕distributive. Proposition 6. Let φ be a PIL formula over P and

ζ 1 , ζ 2 ∈ P CL(D, P ). If D is left-⊕-distributive, then φ ⊗ (ζ 1 ζ 2 ) ≡ (φ ⊗ ζ 1 ) (φ ⊗ ζ 2 ).

Full normal form for w pvm PCL formulas

In this section, we show that for every w pvm PCL formula ζ ∈ P CL(D, P ), where D is a pv-monoid satisfying specific properties, we can effectively construct an equivalent formula of a special form which is called full normal form. For this, we will use corresponding results from [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF] and [START_REF] Paraponiari | On weighted configuration logics[END_REF]. More precisely, for every PCL formula f over P we can effectively construct a unique equivalent PCL formula of the form true 1 or i∈I j∈Ji m i,j (cf. Theorem 4.43 in [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]), and for every weighted PCL formula ζ over P and a commutative semiring (K, ⊕, ⊗, 0, 1) we can construct a unique equivalent weighted PCL formula of the form k or i∈I k i ⊗ j∈Ji m i,j (cf. Theorem 1 in [START_REF] Paraponiari | On weighted configuration logics[END_REF] and Theorem 25 in [START_REF] Paraponiari | Weighted propositional configuration logics: A specification language for architectures with quantitative features[END_REF]). The index sets I and J i , for every i ∈ I, are finite, k and k i ∈ K and m i,j 's are full monomials over P. We show that we can also effectively build a unique full normal form for every w pvm PCL formula over P and a pv-monoid D satisfying specific properties shown below. Uniqueness is up to the equivalence relation. Lastly, we show that the equivalence problem of w pvm PCL formulas is decidable.

J i such that ζ = i∈I d i ⊗ j∈Ji m i,j .
Following [START_REF] Paraponiari | Weighted propositional configuration logics: A specification language for architectures with quantitative features[END_REF], for every full normal form we can construct an equivalent one satisfying the subsequent statements:

(i) j = j implies m i,j ≡ m i,j for every i ∈ I, j, j ∈ J i , and

1 Following [START_REF] Paraponiari | Weighted propositional configuration logics: A specification language for architectures with quantitative features[END_REF] we consider true as a full normal form.

(ii) i = i implies j∈Ji m i,j ≡ j∈J i m i ,j for every i, i ∈ I.

By Lemma 1 in [START_REF] Paraponiari | On weighted configuration logics[END_REF], if m i,j ≡ m i,j for some j = j , then we get m i,j + m i,j ≡ m i,j . So, we replace m i,j + m i,j by m i,j . For the second case, let j∈Ji m i,j ≡ j∈J i m i ,j for some i = i . Then, we replace d i ⊗ j∈Ji m i,j ⊕ d i ⊗ j∈J i m i ,j by its equivalent formula (d i ⊕ d i ) ⊗ j∈Ji m i,j . In the sequel, we assume that every full normal form satisfies Statements (i) and (ii).

For the construction of the full normal form of every ζ ∈ P CL(D, P ) we shall need the next results. Specifically, we omit the proofs of Lemmas 2,3 and Proposition 7 which are similar to the corresponding ones in [START_REF] Paraponiari | Weighted propositional configuration logics: A specification language for architectures with quantitative features[END_REF].

Lemma 2. Let J be an index set and m j full monomials for every j ∈ J. Then, there exists a unique γ ∈ C(P ) such that for every γ ∈ C(P ) we have j∈J m j (γ) = 1 if γ = γ and j∈J m j (γ) = 0, otherwise.

Proposition 7. Let f be a P CL formula over P and D a pv-monoid. Then there exist finite index sets I and J i for every i ∈ I, and full monomials m i,j for every i ∈ I and j ∈ J i such that

f ≡ i∈I j∈Ji m i,j ≡ i∈I   1 ⊗ j∈Ji m i,j   .
Lemma 3. Let m i , m j be full monomials for every i ∈ I and j ∈ J. Then,

i∈I m i ⊗   j∈J m j   ≡ i∈I m i if i∈I m i ≡ j∈J m j , 0 otherwise. Proposition 8. Let d 1 , d 2 ∈ D and ζ 1 , ζ 2 ∈ P CL(D, P ). If D is left-⊕-distribu-
tive and ⊗ is commutative and associative, then

(d 1 ⊗ ζ 1 ) (d 2 ⊗ ζ 2 ) ≡ d 1 ⊗ d 2 ⊗ (ζ 1 ζ 2 ).
Proposition 9. Let m i , m j be full monomials for every i ∈ I and j ∈ J. Then

i∈I m i   j∈J m j   ≡    i∈I m i + j∈J m j if m i ≡ m j
m i,j   (γ) = val(d 1 , . . . , d |I| ) if γ = • i∈I γ i 0 otherwise. = val(d 1 , . . . , d |I| ) ⊗ i∈I j∈Ji m i,j (γ) = val(d 1 , . . . , d |I| ) ⊗   i∈I j∈Ji m i,j   (γ),
and we are done.

Theorem 1. Let D be an associative, idempotent and ⊕-distributive pv-monoid, where ⊗ is commutative. Then, for every w pvm PCL formula ζ ∈ P CL(D, P ) we can effectively construct an equivalent w pvm PCL formula ζ ∈ P CL(D, P ) in full normal form which is unique up to the equivalence relation.

Proof. We prove our theorem by induction on the structure of w pvm PCL formulas over P and D. Let ζ = f be a PCL formula. Then, we conclude our claim by Proposition 7. Next let ζ = d with d ∈ D, then we have nothing to prove.

In the sequel, assume that ζ 1 , ζ 2 ∈ P CL(D, P ). In [START_REF] Karyoti | Weighted PCL over product valuation monoids[END_REF] we show how we can construct w pvm PCL formulas ζ (1) , ζ (2) and ζ (3)

ζ ≡ I 1 ⊆I1   val(d i1 ) i1∈I 1 ⊗   i1∈I 1 j1∈Ji 1 m i1,j1     .
We consider the sets I

(1) 1 , . . . , I

1 with k ∈ N to be an enumeration of all I 1 's such that i1∈I 1 j1∈Ji 1 m i1,j1 ≡ 0. Hence, by Proposition 9, i∈I (s)

1 j∈Ji m i,j ≡ i∈I (s) 1
j∈Ji m i,j for every s ∈ {1, . . . , k}. Moreover, for every s ∈ {1, . . . , k} we let

d s = val(d i ) i∈I (s) 1 . So, ζ ≡ s∈{1,...,k}   d s ⊗    i∈I (s) 1 j∈Ji m i,j       .
Lastly, if i∈I (s) 1 j∈Ji m i,j ≡ i∈I (s ) 1 j∈Ji m i,j for every s, s ∈ {1, . . . , k} with s = s , then we are done. However, let i∈I (s) 1 j∈Ji m i,j ≡ i∈I (s ) 1 j∈Ji m i,j for some s = s . Then, we replace

d s ⊗ i∈I (s) 1 j∈Ji m i,j ⊕ (d s ⊗ i∈I (s ) 1
j∈Ji m i,j by its equivalent formula (d s ⊕d s )⊗ i∈I (s) 1 j∈Ji m i,j . We conclude to a full normal form which by construction, it is equivalent to ζ.

The uniqueness of ζ (1) , ζ (2) , ζ (3) and ζ , up to equivalence, is derived in a straightforward way using Statements (i) and (ii).

In the sequel, we present an example where we compute the full normal form of a w pvm PCL formula.

Example 1. Let P be the set of ports and D a pv-monoid which satisfies the properties of Theorem 1. We consider the w pvm PCL formula

ζ = ((d 1 ⊗ m 1 ) (d 2 ⊗ (m 2 ⊕ m 3 ))) ⊕ (d 3 ⊗ (m 4 + m 5 ))
where d 1 , d 2 , d 3 ∈ D and m i is a full monomial over P for every i ∈ {1, . . . , 5}. We will compute the full normal form of ζ = * ζ. Firstly, we compute the full normal form of ζ.

ζ ≡ ((d 1 ⊗ d 2 ) ⊗ (m 1 + m 2 )) ⊕ ((d 1 ⊗ d 2 ) ⊗ (m 1 + m 3 )) ⊕ (d 3 ⊗ (m 4 + m 5 )).
By Proposition 10 we get

ζ ≡ ((d 1 ⊗ d 2 ) ⊗ (m 1 + m 2 )) ⊕ ((d 1 ⊗ d 2 ) ⊗ (m 1 + m 3 )) ⊕ (d 3 ⊗ (m 4 + m 5 )) ⊕ (val(d 1 ⊗ d 2 , d 3 ) ⊗ (m 1 + m 2 + m 4 + m 5 )) ⊕ (val(d 1 ⊗ d 2 ) ⊗ (m 1 + m 3 + m 4 + m 5 )))
which is in full normal form.

Theorem 2. Let D be an associative, idempotent and ⊕-distributive pv-monoid, where ⊗ is commutative, and P a finite nonempty set of ports. Then for every ζ, ξ ∈ P CL(D, P ) the equality ζ = ξ is decidable.

Proof. We follow the proof of Theorem 26 in [START_REF] Paraponiari | Weighted propositional configuration logics: A specification language for architectures with quantitative features[END_REF]. By Theorem 1 we can effectively construct w pvm PCL formulas ζ , ξ in full normal form such that ζ = ζ and ξ = ξ . Let us assume that ζ = i∈I d i ⊗ j∈Ji m i,j and ξ = l∈L d l ⊗ r∈M l m l,r which moreover satisfy Statements (i) and (ii). Then, by Statement (ii) we get that ζ = ξ iff the following requirements (1)-( 3) hold:

1) card(I) = card(L), 2) {d i | i ∈ I} = {d l | l ∈ L}, and 3) a) if card(I) = card({d i | i ∈ I}), then j∈Ji m i,j ≡ r∈M l m l,r for every i ∈ I and l ∈ L such that d i = d l , or b) if card(I) > card({d i | i ∈ I}), then we get ζ ≡ i ∈I d i ⊗ i∈R i
j∈Ji m i,j where I I, d i 's (i ∈ I ) are pairwise disjoint, and R i (i ∈ I ) is the set of all i in I such that d i = d i .

Similarly, we get ξ ≡ l ∈L d l ⊗ l∈S l r∈M l m l,r where L L, d l 's (l ∈ L ) are pairwise disjoint, and S l (l ∈ L ) is the set of all l in L such that d l = d l . Then i∈R i j∈Ji m i,j ≡ l∈S l r∈M l m l,r for every i ∈ I and l ∈ L such that d i = d l .

By Lemma 2 the decidability of equivalences in (3a) is reduced to decidabilty of equality of sets of interactions corresponding to full monomials, whereas the decidabilitty of equivalences in (3b) is reduced to the decidability of equality of sets whose elements are sets of interactions corresponding to full monomials.

Examples

In this section, we provide w pvm PCL formulas which describe well-known architectures equipped with quantitative features. But first, we introduce a new symbol which we use in order to simplify the form of the formulas in our examples.

Let ζ be a w pvm PCL formula. By Theorem 1, ζ can be written in full normal form, hence ζ ≡ i∈I d i ⊗ j∈Ji m i,j . We define the full valuation ζ of ζ by:

-

ζ := ( * ζ) ⊗ i∈I j∈Ji m i,j .
Then, by Proposition 10 we get

ζ ≡ val(d 1 , . . . , d |I| ) ⊗ i∈I j∈Ji m i,j .
Example 2. We recall from [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF] the Master/Slave architecture for two masters M 1 , M 2 and two slaves S 1 , S 2 with ports m 1 , m 2 and s 1 , s 2 , respectively. Masters can interact only with slaves, and vice versa, and each slave can interact with only one master. In the following we present four different w pvm PCL formulas, which according to the underlying pv-monoid we get interesting results. The monomial φ i,j = m {si,mj } for every i, j ∈ {1, 2} represents the binary interaction between the ports s i and m j . For every i, j ∈ {1, 2} we consider a value d i,j ∈ D and the w pvm PIL formula ϕ i,j = d i,j ⊗φ i,j . Hence, d i,j can be considered as the "cost" for the implementation of the interaction {s i , m j }. For our example we consider the configuration set γ = {{s 1 , m 1 }, {s 1 , m 2 }, {s 2 , m 1 }, {s 2 , m 2 }} and the pv-monoid (R ∪ {-∞}, max, avg, +, -∞, 0).

Let us assume that we want to compute the average cost of each of the possible architectures and then the maximum of those values. We consider the w pvm PCL formula

ζ =∼ i,j∈{1,2} (ϕ 1,i ⊕ ϕ 2,j ) .
Then, the value

ζ (γ) = ∼ i,j∈{1,2} (ϕ 1,i ⊕ ϕ 2,j ) (γ) = max {avg(d 1,1 , d 2,1 ), avg(d 1,1 , d 2,2 ), avg(d 1,2 , d 2,1 ), avg(d 1,2 , d 2,2 )}
computes the average cost for each of the four possible instances and then the maximum of those values. It is interesting to note that ζ (γ) = ζ (γ ) for every γ ∈ C(P ) with γ ⊆ γ .

Moreover, let the following w pvm PCL formula

ζ = i,j∈{1,2} ∼ ( (ϕ 1,i ⊕ ϕ 2,j )) .
Then, the value

ζ (γ) = avg(d 1,1 , d 2,1 ) + avg(d 1,2 , d 2,1 ) + avg(d 1,1 , d 2,2 ) + avg(d 1,2 , d 2,2 )
is the sum of the average costs of all architecture schemes. As a third case, we want to compute the slave which has the maximum average cost with the existing masters. Therefore, we consider the following w pvm PCL formula: Then we get

ζ =∼ i∈{1,2} ( (ϕ i,1 ⊕ ϕ i,2 )) . P 1 p 1 P 2 p 2 T 1 t
ζ (γ) = ∼ i∈{1,2} ( (ϕ i,1 ⊕ ϕ i,2 )) (γ) = max{avg(d 1,1 , d 1,2 ), avg(d 2,1 , d 2,2 )}
which is the wanted outcome.

Example 3. Publish/Subscribe is a software architecture used in development of applications in IoT [START_REF] Olivieri | A publish-subscribe approach to IoT integration: the smart office use case[END_REF], cloud computing [START_REF] Yang | Privacy-preserving attributekeyword based data publish-subscribe service on cloud platforms[END_REF] and robots' operating systems [START_REF] Malavolta | How do you Architect your Robots? State of the Practice and Guidelines for ROS-based Systems[END_REF]. It has three types of components namely, publishers, topics, and subscribers denoted by the letters P, T, S, respectively (cf. [START_REF] Eugster | The many faces of publish/subscribe[END_REF][START_REF] Hasan | Approximate semantic matching of heterogeneous events[END_REF][START_REF] Paraponiari | On weighted configuration logics[END_REF]). Publishers send messages to subscribers but they do not have any information about subscribers and vice versa. So, in order to send messages, publishers characterize messages according to classes/topics. Subscribers, on the other hand, express their interest in one or more topics and receive all messages which have been published to the topics to which they subscribe (Figure 1).

In our example we assign weights, describing priorities, to interactions among publishers and topics, and to interactions among topics and subscribers. Component P has one port p, T has two ports t 1 and t 2 , and S has the port s. We assume two publisher components P 1 , P 2 , four subscriber components S 1 , S 2 , S 3 , S 4 and three topic components T 1 , T 2 , T 3 . Hence, the set of ports is P = {p 1 , p 2 , s 1 , s 2 , s 3 , s 4 , t 11 , t 12 , t 21 , t 22 , t 31 , t 32 }. For every i ∈ {1, 2, 3, 4}, j ∈ {1, 2, 3} and k ∈ {1, 2} we denote by d si,tj2 ∈ D the weight of the interaction among S i and T j , i.e., the priority that the subscriber S i assigns to the receivement of a message from T j , and by d p k ,tj1 ∈ D, the weight of the interaction among P k and T j , i.e., the priority that the topic T j assigns to the receivement of a message from P k .

In the sequel, we develop w pvm PCL formulas whose semantics compute the maximum average priority with which a subscriber will receive a message and also the maximum most frequent priority of each topic. For every i ∈ {1, 2} and j ∈ {1, 2, 3}, the w pvm PIL formula ϕ pt (p i , t j1 ) = d pi,tj1 ⊗ m {pi,tj1} characterizes the interaction between a publisher P i and a topic T j with its corresponding weight. Moreover, for every i ∈ {1, 2, 3, 4} and j ∈ {1, 2, 3}, the w pvm PIL ϕ st (s i , t j2 ) = d si,tj2 ⊗m {si,tj2} characterizes the interaction between a subscriber S i and a topic T j with its corresponding weight. Then, the w pvm PCL formula

ζ si = j∈{1,2,3} k∈{1,2} (ϕ pt (p k , t j1 ) ⊕ ϕ st (s i , t j2 ))
describes the behavior of subscriber S i with publishers P 1 , P 2 and topics T 1 , T 2 , T 3 . Let the configuration set γ = {{p i , t j1 }, {s k , t j2 } | i ∈ {1, 2}, j ∈ {1, 2, 3}, k ∈ {1, 2, 3, 4}} , and the pv-monoid (R ∪ {-∞}, max, avg, +, -∞, 0). Then the value ∼ ζ si (γ) represents the maximum average priority with which the subscriber S i will receive a message. Also, consider the w pvm PCL formula ζ = i∈{1,2,3,4} (∼ ζ si ). Then, the following value

ζ (γ) = i∈{1,2,3,4} max j∈{1,2,3} avg(d p1,tj1 , d si,tj2 ), avg(d p2,tj1 , d si,tj2 ) is the sum of the values ∼ ζ si (γ) for i ∈ {1, 2, 3, 4}.
Moreover, let us assume that we want to erase one component of the architecture in case, for example, where the system is overloaded and needs to be 'lightened'. Consider the case where we choose to erase a topic which is not as popular as the others. A way to do this is to compute for every topic the most frequent priorities that the publishers and subscribers give to that component and then the maximum one of those. Hence, the topic that has the minimum most frequent priority among the other topics is the least popular topic and so it can be erased. The following w pvm PCL formula

ζ ti =   j∈{1,2} ϕ pt (p j , t i1 ) ⊕ k∈{1,2,3,4} ϕ st (s k , t i2 )   for i ∈ {1, 2
, 3} describes the full valuation of the weighted interactions of the topic T i with the publishers P 1 , P 2 and the subscribers S 1 , S 2 , S 3 and S 4 . Consider the configuration γ given above and the pv-monoid (R ∪ {+∞, -∞}, min, maj, max, +∞, -∞). Then,

∼ ζ ti (γ) = maj (d p1,ti1 , d p2,ti1 , d s1,ti2 , d s2,ti2 , d s3,ti2 , d s4,ti2 )
for i ∈ {1, 2, 3} is the maximum priority, among the most frequent ones, that the publishers and subscribers give to topic T i . Lastly, if we consider the w pvm PCL formula

ζ =∼ (ζ t1 ⊕ ζ t2 ⊕ ζ t3 ) , then ζ (γ) = min i∈{1,2,3} {maj (d p1,ti1 , d p2,ti1 , d s1,ti2 , d s2,ti2 , d s3,ti2 , d s4,ti2
)} and so we erase the topic with the minimum value.

Example 4. Consider the Star architecture [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]. Star architecture is a software architecture relating components of the same type. Given a set of components one of them is considered as the central one and is connected to every other component through a binary interaction. No other interactions are permitted.

In our example we consider five components. We assume that each component has a single port, hence the set of ports is P = {s 1 , s 2 , s 3 , s 4 , s 5 }. We denote by d i,j ∈ D the weight of the binary interaction between s i and s j for every i, j ∈ I = {1, . . . , 5} with i = j, when s i is considered as the central component. The w pvm PIL formula characterizing this interaction, for every i, j ∈ I with i = j, is given by ϕ ij = d i,j ⊗ m {si,sj } . Therefore, the w pvm PCL formula

ζ i =   j∈I\{i} ϕ ij  

Discussion

In our definition of w pvm PIL and w pvm PCL over P and D, we excluded, following [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF], the empty interaction and the empty set of interactions. The empty interaction satisfies only the PIL formula f alse. If we consider the empty interaction, then several properties do not hold in PCL of [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]. For instance the equivalence f + false ≡ false (Proposition 4.4 in [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]) for f ≡ false, which is used in the computation of the full normal form of a PCL formula (more specifically in proof of Proposition 4.19 and in turn in proof of Proposition 4.35 in [START_REF] Mavridou | Configuration logics: Modeling architecture styles[END_REF]). Hence, it is clear that if we consider the empty interaction and the empty set of interactions, then we need to rebuilt not only our theory but also the theory of PCL. Moreover, the empty interaction adds no value in single interactions but it does in architectural composition (cf. for instance [START_REF] Attie | A general framework for architecture composability[END_REF][START_REF] Bozga | Local reasoning about parametric and reconfigurable component-based systems[END_REF]), where it represents the case where two architectures cannot be composed. However, this is beyond the scope of this paper.

In our logic we consider the algebraic structure of product valuation monoids. The semantics of w pvm PCL formulas are polynomials with values in the product valuation monoid. In Theorem 1 we prove that for every w pvm PCL formula ζ ∈ P CL(D, P ), where D satisfies specific properties, we can effectively construct an equivalent w pvm PCL formula ζ ∈ P CL(D, P ) in full normal form.

For this, we require D to be an associative, idempotent and ⊕-distributive pv-monoid, where ⊗ is commutative. We need to clarify that a pv-monoid D satisfying those properties is not a semiring since a pv-monoid contains a valuation function which can not be supported by the structure of semirings. For instance, let the pv-monoid (R∪{-∞}, max, avg, +, -∞, 0) which is associative, idempotent, ⊕-distributive and the operator + is commutative. The valuation function avg can not be written using the operations max and + of the semiring (R ∪ {-∞}, max, +, -∞, 0). Hence, the pv-monoids satisfying the above properties constitute a different structure than the one of semirings.

Conclusion

We introduced a weighted PCL over a set of ports and a pv-monoid, and investigated several properties of the class of polynomials obtained as semantics of this logic with the condition that our pv-monoid satisfies specific properties. We proved that for every w pvm PCL formula ζ over a set of ports P and a pv-monoid D which is associative, ⊕-distributive, idempotent and ⊗ is commutative, we can effectively construct an equivalent one ζ in full normal form. This result implied the decidability of the equivalence problem for w pvm PCL formulas. Lastly, we provided examples describing well-known software architectures with quantitative characteristics such as the average cost of an architecture or the maximum most frequent priority of a component in the architecture. These are important properties which can not be represented by the framework of semirings in [START_REF] Paraponiari | On weighted configuration logics[END_REF]. Future work includes the investigation of the complexity for the construction of full normal form for formulas in our logic and the time needed for that construction using the Maude rewriting system [1]. Furthermore, it would be interesting to study the first-order level of w pvm PCL for the description of architecture styles with quantitative features.

Definition 4 .

 4 Let ζ ∈ P CL(D, P ). The semantics of ζ is a polynomial ζ ∈ D C(P ) where for every γ ∈ C(P ) the value ζ (γ) is defined inductively on the structure of ζ as follows:

  by the idempotency of D. Therefore, for every analysis of γ = • n i=1 γ i , the value val ( ζ (γ 1 ), . . . , ζ (γ n )) in * ζ (γ) is computed only once. Two w pvm PCL formulas ζ 1 , ζ 2 are called equivalent, and we write ζ 1 ≡ ζ 2 , whenever ζ 1 (γ) = ζ 2 (γ) for every γ ∈ C(P ). The closure ∼ ζ of every w pvm PCL formula ζ ∈ P CL(D, P ) is determined by: -∼ ζ := ζ ⊕ (ζ 1). Lemma 1. Let ζ ∈ P CL(D, P ). Then ∼ζ (γ) = γ ⊆γ ζ (γ ) for every γ ∈ C(P ).

Proposition 4 .

 4 The pv-monoids (R ∪ {-∞}, max, avg, +, -∞, 0) and (R ∪ {+∞}, min, avg, +, +∞, 0), are ⊕-preservative By a straightforward calculation we can show the next proposition. Proposition 3. Let D be a valuation monoid. If val is ⊕-preservative, then val val d i , d j where I, J are finite index sets and d i , d j ∈ D for every i ∈ I and j ∈ J. Let ζ ∈ P CL(D, P ). If D is ⊕-preservative, then ∼ ( * ζ) ≡ * (∼ ζ).

  For example, let P = {p, q} and the w pvm PCL formulas ζ, ζ 1 , ζ 2 , where ζ = 2 and ζ 1 = ζ 2 = 1. If we consider the set γ = {{p}, {q}} and the pv-monoid

Definition 5 .

 5 A w pvm PCL formula ζ ∈ P CL(D, P ) is said to be in full normal form if either 1. ζ = d, with d ∈ D, or 2. there are finite index sets I and J i for every i ∈ I, d i ∈ D, and full monomials m i,j for every i ∈ I and j ∈

for every i ∈ I and j ∈ J 0 otherwise. Proposition 10 .(

 10 Let ζ ∈ P CL(D, P ) which is in full normal form, i.e., ζ = i∈I d i ⊗ j∈Ji m i,j . Then i. * ζ ≡ I ⊆I val(d i ) i∈I ⊗ i∈I j∈Ji m i,j , ii. ( * ζ) ⊗ i∈I j∈Ji m i,j ≡ val(d 1 , . . . , d |I| ) ⊗ i∈I j∈Ji m i,j . Proof. i. Let γ ∈ C(P ). Then we get * ζ (γ) = n>0 • n i=1 γi=γ val ( ζ (γ 1 ), . . . , ζ (γ n )) . By Lemma 2, for every i ∈ I there exists a unique γ i ∈ C(P ) such that for every γ ∈ C(P ) we have i∈Ji m i,j (γ) = 1 if γ = γ i and i∈Ji m i,j (γ) = 0, otherwise. Hence, val ( ζ (γ 1 ), . . . , ζ (γ n )) = 0 when for every i ∈ {1, . . . , n} there exists j i ∈ I such that γ i = γ ji and, by definition of * ζ (γ), the sets γ 1 , . . . , γ n consist a partition of γ. Moreover, val ( ζ (γ j1 ), . . . , ζ (γ jn )) = val (d j1 , . . . , d jn ) . Since val is a symmetric function and D is idempotent, we get * ζ (γ) = I ⊆I val(d i ) i∈I where for every I ⊆ I it holds γ = • i∈I γ i or equivalently i∈I j∈Ji m i,j (γ) = 1. For every other I subset of I it holds i∈I j∈Ji m i,j (γ) = 0. So, we get the following * ζ ≡ I ⊆I (val(d i ) i∈I ⊗ i∈I j∈Ji m i,j . ii. Let γ ∈ C(P ). Then we get ) = * ζ (γ) ⊗ i∈I j∈Ji m i,j (γ). We can easily prove that i∈I j∈Ji m i,j (γ) = 1 if γ = • i∈I γ i and i∈I j∈Ji m i,j (γ) = 0 otherwise. If γ = • i∈I γ i , then since D is idempotent we get * ζ (γ) = val d 1 , . . . , d |I| . Hence,

  in full normal form which are equivalent to ζ 1 ⊕ ζ 2 , ζ 1 ⊗ ζ 2 and ζ 1 ζ 2 , respectively. Finally, let ζ = * ζ 1 and ζ 1 = i1∈I1 d i1 ⊗ j1∈Ji 1 m i1,j1 be its equivalent w pvm PCL formula in full normal form. We consider the formula ζ = * ζ 1 . By Proposition 10, ζ can be equivalently written as follows

Fig. 1 .

 1 Fig. 1. Weighted Publish/Subscribe architecture.

  describes the full valuation of the binary interactions of the central component s i with the rest of all other components. Next, consider the w pvm PCL formula ζ =∼ i∈I ζ i which describes the five alternative versions of the Star architecture. Let γ = {{s i , s j }/ i, j ∈ I and i = j} and (R ∪ {+∞}, min, avg, +, +∞, 0), then we getζ (γ) = min{avg(d 1,2 , d 1,3 , d 1,4 , d 1,5 ), ..., avg(d 5,1 , d 5,2 , d 5,3 , d 5,4 )}which is the minimum value among the average costs of each component when it is considered as the central one.

The research work was supported by the Hellenic Foundation for Research and Innovation (HFRI) under the HFRI PhD Fellowship grant (Fellowship Number: 1200).


Alex Coto
email: alex.coto@gssi.it

Roberto Guanciale
email: robertog@kth.se

Emilio Tuosto
email: emilio.tuosto@gssi.it

Choreographic Development of Message-Passing Applications

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

Introduction

Choreographic approaches advocate model-driven engineering (MDE) based on two different views of distributed applications. A global view specifies the interactions among the various distributed components (aka participants) while a local view models each component of the system. This tutorial illustrates how global and local views enable both top-down and bottom-up engineering of message-passing applications. This interplay can be described by the following diagram: In the top-down engineering approach, designers provide the global view which can then be "projected" to obtain local views. Developers can independently realise components and test their "compliance" with the corresponding local view. In the bottom-up approach, one can extract the local view from existing components, check for their compatibility, and generate a global view. Besides documenting the composition and enhancing program comprehension, global views yield an abstract model that can be used to evolve the system.

Choreographic development of message-passing applications offers, among others, the following advantages:

-Global views are amenable to being expressed using visual languages understandable to lay stakeholders (akin to BPMN [START_REF]Object Management Group: Business Process Model and Notation[END_REF] or UML diagrams [START_REF] Micskei | Uml 2.0 sequence diagrams' semantics[END_REF], message-sequence charts [START_REF] Harel | Message sequence charts[END_REF], etc.). -Local views can be algorithmically projected from global specifications. Also, projected local views:

• come with correctness guarantees when global views satisfy sufficient conditions (well-formedness) for communication soundness, • are typically executable models that can be developed independently.

-The execution model of local views is close to several programming languages and environments like Golang, Erlang, Elixir, Akka, or JMS.

Model-driven approaches provide some support, but require care: models may be incomplete or have subtle issues that can lead to misbehaviour such as deadlocks or message loss.

Structure of the paper § 2 surveys the models used in the tutorial. § 3 shows how the top-down approach works in a simple scenario. § 4 highlights some of the problems that a "bad design" may cause. § 5 discusses how to analyse and fix design errors. § 6 demonstrates the support that choreographic development may provide when amendments are necessary. § 7 shows choreographic bottom-up engineering. § 8 draws some conclusions.

Our Models

A global view can be represented in terms of a distributed workflow (e.g., BPMN [START_REF]Object Management Group: Business Process Model and Notation[END_REF] diagrams) or as specifications (similar to UML sequence diagrams or message-sequence charts). We survey the formal models that we use to represent global and local views of choreographies. This is an informal presentation; the referred literature yields the technical details.

Hereafter, we assume two disjoint sets: participants and messages, respectively ranged over by A, B, etc. and by m.

Partially ordered multisets

Pomsets [START_REF] Pratt | Modeling concurrency with partial orders[END_REF] model concurrency in terms of partial orders of multisets of events. Pomsets provide a general model of concurrency; for instance message-sequence charts are a particular class of pomsets. We use pomsets of communication events as defined in [START_REF] Tuosto | Semantics of global view of choreographies[END_REF] (which also provide a formal overview of pomsets).

Roughly speaking, we consider pomsets as directed-acyclic graphs where nodes are labelled by communication actions and edges capture causality among communications. A simple example illustrates this. The following diagram

r (1) =   A B!int A B?int A B!bool A B?bool   (1)
represents a pomset r (1) capturing the causality relations among the communication events between participants A and B; in (1), horizontal arrows establish the causality relations induced by the interactions of participants, while vertical arrows order the communications events of each participant (marked with background colours for the sake of illustration). More precisely, A sends to B a message of type int and one of type bool; the two leftmost nodes are indeed the output events labelled with A B!int and A B!bool while the rightmost nodes are the corresponding input events A B?int and A B?bool. Moreover, the edges establish that the each output event precedes the corresponding input event (the horizontal edges in (1)) and that the events involving integers precede those involving booleans. Intuitively, r (1) models process A that first sends a int and then a bool message to B, which on turn receives the messages in the sending order.

To represent alternative executions we simply take collections of pomsets. For instance, the set made of the following two pomsets

  A B!int A B?int A B!int A B?int     A B!bool A B?bool A B!bool A B?bool   (2)
represents a system where A sends B either two int or two bool messages. We remark that events involving the same participants are not ordered unless explicitly stated by the pomset. For instance, if we remove the rightmost vertical edge imposing an order of the input events from the pomset (1) then the messages sent by A can be received in any order by B.

A workflow model

The global view of a choreography can be suitably specified as workflows. We use global choreographies [START_REF] Tuosto | Semantics of global view of choreographies[END_REF][START_REF] Guanciale | An abstract semantics of the global view of choreographies[END_REF] (g-choreographies for short), a structured version of global graphs [START_REF] Lange | From Communicating Machines to Graphical Choreographies[END_REF][START_REF] Deniélou | Multiparty Session Types Meet Communicating Automata[END_REF]. This model is appealing as it has a syntactic and diagrammatic presentation amenable of a formal semantics in terms of pomsets.

The syntax of g-choreographies is given by the following grammar: The empty g-choreography (o) yields no interactions; trailing occurrences of (o) may be omitted. An interaction A-→B : m represents the exchange of a message of type m between A and B, provided that A = B. We remark that data values are abstracted away: the payload m in A-→B : m is not a value and should rather be thought of as (the name of) a data type. G-choreographies can be composed sequentially or in parallel (G; G and G | G ). A (non-deterministic) choice sel {G 1 + • • • + G n } specifies the possibility to continue according to either of the g-choreographies G 1 , . . . , G n . The syntax of g-choreographies can be visually depicted as in Fig. 1. A global graph G is represented as a rooted graph with a single "enter" and "exit" nodes, respectively called source (graphically •) and sink (graphically ). Special nodes, dubbed gates, are used for branch and fork points (respectively depicted as + and | ). Each fork or branch gate in our visual notation will have a corresponding join and merge "closing" gate.

G ::= (o) empty A-→B : m interaction G; G sequential G | G fork sel {G + • • • + G} choice
The semantics of a global graph is a family of pomsets; each pomset in the family partially orders the communication events on a particular "trace" of g-choreography. For instance, the semantics [[(o)]] is simply the set { } containing the empty pomset while for interactions we have

[[A-→B : m]] = [ A B!m A B?m ]
namely, the semantics of an interaction is a pomset where the output event precedes the input event. The semantics of the other operations is basically obtained by composing the semantics of sub g-choreographies. More precisely,

-for a choice we have [[G + G ]] = [[G]] ∪ [[G ]]; -the

When all goes fine

We use a simple yet representative application to highlight a top-down choreographic approach to the design and prototyping of message-passing applications.

A server S allows client C to convert strings into a date format and vice versa (we assume a basic data type dateFmt to represent formats). Both C and S use a logger service L to record their requests and responses respectively; for this, data types reqLog and resLog are used.

We first consider a couple of solutions that straightforwardly model the scenario above. Take the global specification

s e l { {C -→ L : l o g R e q | C -→ S : dateFmt } ; . . d a t e 2 s t r i n g & l o g g i n g S -→ L : l o g R e s ; S -→ C : s t r i n g + {C -→ L : l o g R e q | C -→ S : s t r i n g } ;
. . s t r i n g 2 d a t e & l o g g i n g S -→ L : l o g R e s ; S -→ C : dateFmt } Despite its simplicity, it is not immediate that the g-choreography above is sound. To illustrate this, consider that the first interaction between the client C and the server allows S to determine which service is requested (convert a date to a string or vice versa), the logger behaves uniformly through the choice (since it first receives the log message of a request and then the one of a response).

Notice that, although L is oblivious of the choice, its behaviour cannot be syntactically factored out without violating some dependencies among communications.

A variant of the above g-choreography is

s e l { {C -→ L : l o g R e q | C -→ S : dateFmt } ; s e l { S -→ L : l o g R e s + . . S may s e n d l e s s i n f o r m a t i v e l o g s S -→ L : b a s i c L o g } ; S -→ C : s t r i n g + {C -→ L : l o g R e q | C -→ S : s t r i n g } ; S -→ L : l o g R e s ; S -→ C : dateFmt }
where, once a request to transform a date into a string is made, S may decide to log the response either fully or send L less information with basicLog. Note that C is now unaware of this choice between S and L while L can discern the initial choice made by C.

Once the soundness of a g-choreography is attained, local behaviours can be automatically projected either to local specifications or to executable code. For instance, ChorGram can generate communicating finite-state machines [START_REF] Brand | On Communicating Finite-State Machines[END_REF] that specify the behaviour of each component of the system as well as executable Erlang code implementing the communication pattern of the g-choreography. Notably, this approach is an instance of a correctness-by-design principle: the projected behaviour is communication sound in the sense that it does not exhibit misbehaviour such as deadlocks or loss of messages (provided that the communication infrastructure does not fail).

Designing Problems

Models featuring distributed workflows (such as BPMN or the g-choreographies adopted here) may introduce inconsistency related to distributed choices. In scenario-based models, the designer may overlook cases that may lead to runtime errors. This is illustrated with the following examples.

Consider the protocol specified by the following two pomsets

  A B!tx start A B?tx start B A?tx abort B A!tx abort              A B!tx start A B?tx start B A?string B A!string B A?tx commit B A!tx commit B C!int B C?int            (3)
Participant A starts a transaction with B by sending message tx start and then engages in a distributed choice where either B aborts the transaction immediately, or it send a string with A and commits the transaction before sending an integer with C. This specification leaves C uncertain about whether the integer from B is going to be sent or not. Hence C could locally decide to (a) terminate immediately and not receive the integer from B or (b) to wait for the integer, even if B opted to abort the transaction.

Relying on the pomset semantics of g-choreographies, in [START_REF] Tuosto | Semantics of global view of choreographies[END_REF] we defined termination awareness in order to avoid reaching run-time configurations where non-terminating participants unnecessarily lock resources once the coordination is completed. This condition requires that in no accepting configuration the participants of interest have input transitions. More precisely, a set of pomsets R violates the terminating condition for participant A if there are two pomsets r and r in R such that an execution trace of A in r is a prefix of an execution trace of A in r and the difference between the two traces starts with an input. Basically, the designer can specify which participants should be aware of the termination of the choreography. Note that, depending on the application requirements, termination awareness may be important for B, but not for C; in the example above for instance, the termination of C is not crucial if it is not locking resources or if it is immaterial that such resources are left locked.

A C!l1 A B!int A C!r1 A B!int B C!l2 A B?int B C!l3 B C!
In [START_REF] Tuosto | Semantics of global view of choreographies[END_REF], besides the terminating condition above, we identified two other pomset-based conditions dubbed CC2-POM and CC3-POM to check realisability of global specifications. We briefly describe those closure conditions.

Intuitively, CC2-POM takes into consideration the executions emerging from "confusion" caused by different threads in a pomset (such as the one in ( 4)). For a given set of pomsets R, the satisfaction of CC2-POM ensures that if an execution trace t cannot be distinguished by any of the participants from a valid trace of R then t is a trace of R. To check CC2-POM, one needs to compute a closure set of pomsets out of R; the closure set yields the pomsets characterising the execution traces due to inter-participants' concurrency. This closure generates all "acceptable" matches between output and input events entailed by a pomset capturing the behaviour of a participant. We borrow and adapt Fig. 2 from [START_REF] Tuosto | Semantics of global view of choreographies[END_REF] to give an intuition of this construction. The participants A, B, and C there have each two threads, the "left" and the "right" thread; those are identified by sorts l i and r i which are meta-variables on sorts immaterial here (with the only assumption that l i = r i for each i ∈ {1, 2, 3}). The bottom-most solid edges from the threads of A to those of B represent the causality relations specified in the original design. The closure of the original design however yields also the execution with the causality relations given by the bottom-most dashed edges.

The condition CC3-POM accounts for implied executions that may break distributed choices. It is similar to CC2-POM barred that the closure set is built by checking all the prefixes of the traces of the pomsets.

We remark that our framework focuses on the identification of communication problems that are data-oblivious. For this reason the implementations of some specifications may exhibit unintended interactions even if they satisfy the verification conditions. Consider the following example:

  A B!int A B?int A B!bool A B?bool A B!string A B?string A B!bool A B?bool   (4)
which specifies two concurrent threads3 whereby A (threads with green background) and B (threads with orange background) exchange two boolean values after exchanging an integer and a string. In an asynchronous setting, the boolean values may "swap", namely the one sent by the thread which sent the integer is received by the thread which received the string, and vice-versa. Notice that this does not yield communication problems, but may violate the dependencies among data induced by the causal dependencies specified in the pomset.

To sum up, we address termination awareness, thread confusion (CC2), and undetermined choices (CC3). The violation of termination awareness could lead to participants oblivious of the termination of the protocol, the violation of CC2 could make messages to be consumed by a unintended threads of a participant, CC3 could lead to participants to follow one branch of a choice while other participants are executing another branch.

When Something Goes Wrong

We now consider some examples where development is not as straightforward as in the examples of § 3. More precisely, we consider scenarios where the closure properties CC2-POM or CC3-POM may be violated, or termination awareness does not hold for some participants. For the analysis we rely on PomCho, part of the ChorGram tool chain that supports choreographic development through the models discussed in § 2.

Let us start with the following (erroneous) g-choreography giving another variant of the protocol in § 3 where a less informative log message is sent when C requests to transform a date in a string and a more informative one otherwise: The attentive reader may have noticed a problem: the exchange of basicLog should go the other way around. This intentional mistake is instrumental to illustrate the analysis of the g-choreography above, summarised by the screenshots in Fig. 3. Before doing so, we briefly digress about the GUI. After loading, ChorGram computes the g-choreography to analyse as shown in the left-most screenshot in Fig. 3. The other screenshot presents a counterexample of the violation of termination awareness once such analysis is executed. Note that the hierarchical menu in the left pane is dynamically expanded to include clickable Let us return to our analysis. The screenshots in Fig. 3 show that while the closure properties are satisfied, termination awareness is violated for L. By inspecting the pomset in the top-right screenshot we can notice that the logging information in the two branches wrongly goes from L to S (instead of going the other way around). This is immediately evident from the projection on L reported in the bottom-most screenshot of Fig. 3; notice that state 1 is a mixed-choice state, namely that it has both input and output outgoing transitions.

Swapping the sender and the receiver in the introduced interaction solves all the issues (which results in ChorGram displaying empty lists of counterexamples). One could argue that this is such a blunt glitch that one could spot it immediately and without the use of tools. While this might be true for simple examples like this one, these mishaps might not be as obvious in larger designs.

The next variant of our protocol exhibits a subtle problem. Consider

s e l { {C -→ L : l o g R e q | C -→ S : dateFmt } ;
The output of logReqExt precedes the one of basicLog (implying that S opted for the left-most branch of the g-choreography). However, the corresponding input events of L are in the opposite order (making L follow the right-most branch). The analysis must take into account the semantics of communication. In particular, asynchronous communications require care. In fact, if the messages are buffered and accessed according to a FIFO discipline, in the above g-choreography the message basicLog is before (resp. after) the message logResExt in the buffer from S to L when the first (resp. second) branch is chosen. However, when the order of sent messages is not guaranteed problems may arise, as highlighted by the screenshots of PomCho in Fig. 4. Although the screenshot on the left suggests that the interactions happen in the order specified in the g-choreography, L may "misunderstand" the choice taken by C. In fact, suppose that C selects the left branch and that the message basicLog may reach L before the message logResExt and, consequently, L may behave according to the branch on the right. Both closure properties are violated because the order of messages no longer allows L to distinguish which branch S opted for. The pomset depicted in the screenshot on the right shows possible executions where the order of outputs is not preserved.

The above problem can be fixed by letting L acknowledge the first message from the server S, namely s e l { {C -→ L : l o g R e q | C -→ S : dateFmt } ; This variant enjoys all our closure conditions.

Suggesting amendments

This section illustrates an experimental feature recently added to ChorGram. As seen earlier, the top-down approach of choreographic design requires gchoreographies to enjoy well-formedness properties. For instance, the closure properties surveyed in § 4 ensure the realisability of g-choreographies by components coordinating through asynchronous message-passing.

Attaining well-formedness requires some ingenuity. In fact, designers can easily overlook problems and introduce defects leading to communication problems such as those in the scenarios of § 5. When this happens, as seen in the previous examples, ChorGram identifies counterexamples that highlight defects. It may therefore be helpful to have advice on how to possibly fix problems.

Possible amendments are suggested by ChorGram as a g-choreography, determined out of the initial one and the counterexample identified in the analysis. We demonstrate this by considering a further variation of the application used in § 5. The following g-choreography models a protocol where a less informative log message is sent when C requests to transform a date into a string: Notice that L informs S about the format of the log. The analysis in Fig. 5 shows that, while CC2-POM is satisfied (since no counterexample exists), CC3-POM is however violated due to an unsound choice. In fact, the screenshot on the right of Fig. 5 represents the pomset missing from the semantics of the global model. In this counterexample, S gets stuck after receiving the two parallel inputs from C and L. Here, the problem arises because L cannot identify which message should be sent to S, since L receives the same message in both branches. Accordingly, L is not informed about the branch selected by C. This problem is evident in the screenshots of Fig. 6, which report the projection of L, the g-choreography corresponding to the counterexample, and a model consisting of a suggested amendment. This model maps the counterexample back to the initial g-choreography. This is attained by computing the "minimal" transformation required on the original design to match the counterexample. More precisely, ChorGram applies an edit-distance algorithm to the (part of the) original design to be changed so that it corresponds to the counterexample. The algorithm can be tuned up by setting a cost to edit operations.

The edit operations are node insertion/deletion edge insertion/deletion modifications to sender/receivers/payload of interactions.

Pictorially, nodes and edges in green represent unchanged elements, those in blue represent additions to make, and those in dashed gray represent elements to be deleted. For instance, the amendment in Fig. 6 suggests to preserve the right-most branch and change the left-most branch by removing the nodes and edges in gray, adding the blue edges, and modifying the payload of the communication from C to S (from string to dateFmt). Note that the suggested amendments are computed without "interpreting" the g-choreography and therefore they may not be meaningful. The designer still needs to vet and approve them. As said, this is an experimental feature added to ChorGram, and we plan to investigate how to improve it. For instance, an interesting development could be to identify how to assign costs depending on the applications at hand. In fact, in some cases it may not be reasonable to apply some of the operations above. This can be improved upon by properly assigning costs (undesired operations should have a higher cost than admissible ones).

Going bottom-up

We now consider how choreographies can support bottom-up engineering. There are two key motivations for which this support is appealing. Firstly, the validation of composition of distributed components. For instance, service-oriented architectures such as micro-services envisage software development as the composition of publicly available services. One would like to validate that such compositions communicate as expected. Secondly, software evolution possibly compromises the communication soundness of an application.

In the rest of the section, such a scenario is used to show the kind of support offered by choreographies in bottom-up engineering. To this purpose we look at a possible evolution of the last g-choreography in § 5: Suppose that the developers want to deploy a new version of the logger service L that requires specific formats for the log information sent by the server S. Therefore, developers implement a new version of L, say Lfmt, that behaves according to the CFSM in Fig. 7. (Note that the CFSMs of C and S do not change.) After the request of the client, the new logger informs S of the format (transitions q1→q2 and q1→q3 of Lfmt). The server reacts accordingly with transitions from its initial state.

It is worth remarking that what usually happens is that the code implementing L evolves without modifying the corresponding models (if any). After a new version of a component is released, one could extract4 a model like the CFSM on the left to describe its behaviour. This is what we assume in this scenario. Fig. 7 yields a problematic system: The bottom-up analysis of ChorGram (done before deploying Lfmt) flags the problem with the message: Branching representability: [Bp "C" "q4", Bp "C" "q5", Bp "C" "q6", Bp "L" "q1",Bp "L" "q2",Bp "L" "q3",Bp "L" "q4", Bp "S" "q0",Bp "S" "q1",Bp "S" "q3",Bp "S" "q4", Bp "S" "q5",Bp "S" "q6",Bp "S" "q7"] which we now decipher. This message basically reports the CFSMs whose transitions are not reflected in their parallel composition due to some branching.

For instance, in our model, Bp "S" "q0" states that some transitions expected from state q0 of the server S cannot be fired in a configuration of the systems where the local state of S is q0; in fact, in configuration q4 of the system, the local machine of S is in state q0, which has the transition S L!basicLog (not reflected in the system).

This analysis can be conducted in a more user-friendly way by inspecting the models in Fig. 8, also provided by ChorGram.

The g-choreography contains the "sound" interactions only. In fact, the transition system in Fig. 8 highlights two configurations, q4 and q5, that violate the branching property. This is due to the fact that S is not aware of the choice taken in the local state q1 of the CFSM Lfmt in Fig. 7. This problem can be solved by modifying S, as illustrated in the CFSM of Fig. 9.

Concluding remarks

Tool support for analyzing realisability of global specifications is necessary to enable model-driven development of choreographies. Indeed, as observed in [START_REF] Alur | Inference of Message Sequence Charts[END_REF], a source of problems is that there could be some specifications that are impossible to implement using the local views in a given communication model. Several works addressed the realisability of scenario-based global models, like message-sequence charts (MSCs) [START_REF]Formal description techniques (FDT) -Message Sequence Chart[END_REF][START_REF] Gaudin | Property Verification with MSC[END_REF][START_REF] Muscholl | Deciding Properties of Message Sequence Charts[END_REF][START_REF] Harel | Come, let's play: scenario-based programming using LSCs and the play-engine[END_REF][START_REF] Gunter | Compositional Message Sequence Charts[END_REF][START_REF] Gunter | Compositional message sequence charts[END_REF][START_REF] Alur | An analyzer for message sequence charts[END_REF]. A mechanism to statically detect realisability in MSCs is proposed in [START_REF] Ben-Abdallah | Syntactic detection of process divergence and non-local choice in message sequence charts[END_REF]. The notions of non-local choices and of termination considered in [START_REF] Ben-Abdallah | Syntactic detection of process divergence and non-local choice in message sequence charts[END_REF] are less permissive than our verification conditions since intra-participant concurrency is not allowed and termination awareness is not enforced. Closure conditions for realisability have been initially proposed in [START_REF] Alur | Inference of Message Sequence Charts[END_REF] to study realisability of MSC and have been extended in [START_REF] Guanciale | Realisability of pomsets[END_REF] to handle sets of pomsets (the latter were reviewed in § 2). This extension yields more general results and more efficient analyses, since it enables multi-threaded participants and does not require to explicitly compute all possible executions (which can be large due to the number of possible interleaving of concurrent threads) of the global model.

In the context of choreographies, the integration of ChorGram features in the CHOReVOLUTION platform [START_REF] Autili | Chorevolution: Automating the realization of highly-collaborative distributed applications[END_REF] is of particular interest to us. In fact, CHOReVOLUTION is a rather sophisticated platform for the top-down development featuring many important aspects complementary to the functionalities of ChorGram (e.g., low-level binding of components, or security aspects).

Other possible integrations are with tools based on behavioural types [START_REF] Hüttel | Foundations of session types and behavioural contracts[END_REF]. The tools proposed in this context (see [START_REF]Behavioural Types: from Theory to Tools[END_REF] for a survey) are typically based on theories defining constraints aimed to guarantee the soundness of the projections of global specifications (as e.g., in [START_REF] Bocchi | Resolving non-determinism in choreographies[END_REF][START_REF] Carbone | A Calculus of Global Interaction based on Session Types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF]). A peculiarity of ChorGram is that it can provide some feedback to support model-driven engineering of applications. This is not usually the case in other contexts based on behavioural types where, for instance, behavioural type checkers do not provide feedback.

  by the EU H2020 RISE programme under the Marie Sk lodowska-Curie grant agreement No 778233 and by the MIUR project PRIN 2017FTXR7S "IT-MaTTerS" (Methods and Tools for Trustworthy Smart Systems).

  semantics of the parallel composition G | G is essentially built by taking the set of the disjoint union of each pomset in [[G]] with each one in [[G ]]; the semantics of the sequential composition [[G; G ]] is the set of the disjoint union of each pomset in [[G]] with each one in [[G ]] and adding causal relations from events in [[G]] to those in [[G ]] if they are executed by the same participant (i.e., making the former precede the latter).

Figure 2 .

 2 Figure 2. Inter-participant closure

  s e l { {C -→ L : l o g R e q | C -→ S : dateFmt } ; L -→ S : b a s i c L o g ; . . o o p s S -→ C : s t r i n g + {C -→ L : l o g R e q | C -→ S : s t r i n g } ; S -→ L : l o g R e s ; S -→ C : dateFmt }

  The left-hand pane allows the user to select the model onto which to apply the next operation; results are displayed in the pane on the right-hand side.A possible way of representing local views is by communicating finite-state machines[START_REF] Brand | On Communicating Finite-State Machines[END_REF] which basically are finitestate automata where transitions are labelled by communication actions. A projection function of ChorGram can generate CFSMs of participants from a gchoreography as illustrated for L here.

Figure 3 .

 3 Figure 3. Violation of termination awareness and projection on L

Figure 4 .

 4 Figure 4. Problems with non-FIFO asynchrony

Figure 5 .

 5 Figure 5. An unexpected execution

Figure 6 .

 6 Figure 6. A possible amendment

Figure 7 .

 7 Figure 7. The system with the evolved L

Figure 8 .Figure 9 .

 89 Figure 8. G-choreography and transition system determined by bottom-up analysis

Note the bracketing here: enclosing the two groups of events in different brackets would correspond to specifying a choice between the pomsets.

This operation can be done either by inferring the model from the code (if possible) or by learning it by observing the behaviour of the new version of the component.

Acknowledgments We warmly thank Simon Bliudze for his helpful comments which allowed us to improve the presentation of this paper.