key: cord-0045109-oyvtx84b
authors: Karyoti, Vagia; Paraponiari, Paulina
title: Weighted PCL over Product Valuation Monoids
date: 2020-05-13
journal: Coordination Models and Languages
DOI: 10.1007/978-3-030-50029-0_19
sha: 9e16cf5fcdef1664bc0d256f3cc37a553d44ae19
doc_id: 45109
cord_uid: oyvtx84b

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.

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 [13] , 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 [13] studied the relation among architectures and architecture styles, i.e., architectures with the same types of components and topologies.

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

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 [14, 18, 19] . 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 [17] 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 [4] [5] [6] . In [7, 8] 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 [15] 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 [6] 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 [17] . 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 [17] .

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 [17] and [16] . We refer the reader to the full version of our paper on arXiv [11] .

In this section, we recall valuation monoids and product valuation monoids [8] . 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

The pv-monoid is denoted simply by D if the operations and the constant elements are understood.

In the following we recall some pv-monoids from [8] . 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.

In this section, we introduce the weighted propositional interaction logic over pv-monoids. Firstly, we recall from [13] 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 φ :

where p ∈ P . As usual, we set φ = φ for every PIL formula φ and false = 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:

For every α ∈ I(P ) it holds α |= i false. 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

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.

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:

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 [13] . The syntax of PCL formulas over P is given by the grammar

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:

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 [13] and [17] for properties of PCL formulas.

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

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.

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:

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 γ.

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:

for every γ ∈ C(P ).

Next, we present several properties of our w pvm PCL formulas.

where the second and the last equalities hold since D is idempotent, and the third one since D is left-val-distributive.

By a straightforward calculation we can show the next proposition.

where I, J are finite index sets and d i , d j ∈ D for every i ∈ I and j ∈ J.

where the third equality holds since D is ⊕-preservative and the next equalities due to the commutativity of ⊕.

Next, we show a special case when ⊗ distributes over . In general ⊗ does not distribute over . 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 (R ∪ {−∞}, max, avg, +, −∞, 0), then it is easy to show that

. However, this is not the case when ζ is a PIL formula and D is left-⊕distributive.

Let φ be a PIL formula over P and ζ 1 ,

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 [13] and [17] . 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 [13] ), 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 [17] and Theorem 25 in [16] ). 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. Following [16] , for every full normal form we can construct an equivalent one satisfying the subsequent statements:

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 [16] . 

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

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,

and we are done.

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 [11] we show how we can construct w pvm PCL formulas ζ (1) , ζ (2) and ζ (3) 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

We consider the sets I 

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

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 ζ.

By Proposition 10 we get

which is in full normal form.

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 [16] . 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 

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 decidability of equality of sets of interactions corresponding to full monomials, whereas the decidability of equivalences in (3b) is reduced to the decidability of equality of sets whose elements are sets of interactions corresponding to full monomials.

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:

Then, by Proposition 10 we get ζ ≡ val(d 1 , . .

Example 2. We recall from [13] 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 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

Then, the value (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

s 4 dp 1 ,t 11 dp 1 ,t 31 ds 1 ,t 12 ds 1 ,t 32 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 ⊕ ϕ 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 [14] , cloud computing [19] and robots' operating systems [12] . It has three types of components namely, publishers, topics, and subscribers denoted by the letters P, T, S, respectively (cf. [9, 10, 17] ). 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 (Fig. 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

describes the behavior of subscriber S i with publishers P 1 , P 2 and topics T 1 , T 2 ,

, 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

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

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 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 [13] . 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 

In our definition of w pvm PIL and w pvm PCL over P and D, we excluded, following [13] , the empty interaction and the empty set of interactions. The empty interaction satisfies only the PIL formula false. If we consider the empty interaction, then several properties do not hold in PCL of [13] . For instance the equivalence f + false ≡ false (Proposition 4.4 in [13] ) 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 [13] ). 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 [2, 3] ), 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 pvmonoid, 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.

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 [17] . 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.

A general framework for architecture composability

Local reasoning about parametric and reconfigurable component-based systems

Expressiveness and closure properties for quantitative languages

Quantitative languages

Computing average response time

Weighted automata and regular expressions over valuation monoids

Weighted automata and weighted MSO logics for average and long-time behaviors

The many faces of publish/subscribe

Approximate semantic matching of heterogeneous events

Weighted PCL over product valuation monoids

How do you architect your robots? State of the practice and guidelines for ROS-based systems

Configuration logics: modeling architecture styles

A publish-subscribe approach to IoT integration: the smart office use case

Quantitative automata under probabilistic semantics

Weighted propositional configuration logics: a specification language for architectures with quantitative features

On weighted configuration logics

Publish/subscribe mechanism for IoT: a survey of event matching algorithms and open research challenges

Privacy-preserving attributekeyword based data publish-subscribe service on cloud platforms