# Weighted PCL over Product Valuation Monoids

Vagia Karyoti, Paulina Paraponiari

► To cite this version:

Vagia Karyoti, Paulina Paraponiari. Weighted PCL over Product Valuation Monoids. 22th International Conference on Coordination Languages and Models (COORDINATION), Jun 2020, Valletta, Malta. pp.301-319, 10.1007/978-3-030-50029-0_19. hal-03273981

HAL Id: hal-03273981

https://inria.hal.science/hal-03273981

Submitted on 29 Jun 2021

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la 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.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Weighted PCL over product valuation monoids

Vagia Karyoti¹ and Paulina Paraponiari²,\*

Department of Mathematics
Aristotle University of Thessaloniki
54124 Thessaloniki, Greece

¹vagiakaryo@math.auth.gr, ²parapavl@math.auth.gr

**Abstract.** 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.

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

## 1 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 [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.

PCL is a specification logic of software architectures which is able to describe their qualitative features. However, several practical applications require also

<footnote>\* The research work was supported by the Hellenic Foundation for Research and Innovation (HFRI) under the HFRI PhD Fellowship grant (Fellowship Number: 1200).</footnote>
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, \oplus, \otimes, 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 [5,4,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].
## 2 Preliminaries

In this section, we recall valuation monoids and product valuation monoids [8]. A valuation monoid ($D, \oplus, \text{val}, 0$) consists of a commutative monoid ($D, \oplus, 0$) and a valuation function $\text{val}: D^+ \to D$, where $D^+$ denotes the set of nonempty finite words over $D$, with $\text{val}(d) = d$ for all $d \in D$ and $\text{val}(d_1, \dots, d_n) = 0$ whenever $d_i = 0$ for some $i \in \{1, \dots, n\}$.

($D, \oplus, \text{val}, \otimes, 0, 1$) is a product valuation monoid, or pv-monoid for short if ($D, \oplus, \text{val}, 0$) is a valuation monoid, $\otimes: D^2 \to D$ is a binary operation, $1 \in D$ with $\text{val}(1)_{1 \le i \le n} = 1$ for all $n \ge 1$ and $0 \otimes d = d \otimes 0 = 0$, $1 \otimes d = d \otimes 1 = d$ for all $d \in D$. The pv-monoid is denoted simply by $D$ if the operations and the constant elements are understood. A pv-monoid $D$ is left-$\oplus$-distributive if $d \otimes (d_1 \oplus d_2) = (d \otimes d_1) \oplus (d \otimes d_2)$ for any $d, d_1, d_2 \in D$. Right-$\oplus$-distributivity is defined analogously. If a pv-monoid $D$ is both left- and right-$\oplus$-distributive, then it is $\oplus$-distributive. If $\otimes$ is associative, then $D$ is called associative. We call $D$ left-val-distributive if for all $n \ge 1$ and $d, d_i \in D$ with $i \in \{1, \dots, n\}$, it holds $d \otimes \text{val}(d_1, \dots, d_n) = \text{val}(d \otimes d_1, \dots, d \otimes d_n)$. Moreover, the pv-monoid $D$ is called (additively) idempotent if $d \oplus d = d$ for every $d \in D$.

In the following we recall some pv-monoids from [8]. The algebraic structures $(\mathbb{R} \cup \{-\infty\}, \max, \text{avg}, +, -\infty, 0)$ and $(\mathbb{R} \cup \{+\infty\}, \min, \text{avg}, +, +\infty, 0)$ with $\text{avg}(d_1, \dots, d_n) = \frac{1}{n} \sum_{i=1}^n d_i$ are pv-monoids. More precisely, they are left-val-distributive and $\oplus$-distributive pv-monoids. Also, the structure $(\mathbb{R} \cup \{-\infty, +\infty\}, \min, \max, \max, +\infty, -\infty)$, where $\max(d_1, \dots, d_n)$ is the greatest value among all values that occur most frequently among $d_1, \dots, d_n$, is a $\oplus$-distributive pv-monoid but not left-val-distributive. Both $\min$ and $\max$ 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, \oplus, \text{val}, \otimes, 0, 1$) will denote an idempotent pv-monoid where val is symmetric.

Let $Q$ be a set. A formal series (or simply series) over $Q$ and $D$ is a mapping $s: Q \to D$. The support of $s$ is the set $\text{supp}(s) = \{q \in Q \mid s(q) \neq 0\}$. A series with finite support is called also a polynomial. We denote by $D \langle Q \rangle$ the class of all polynomials over $Q$ and $D$.

## 3 Weighted propositional interaction logic

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) = \mathcal{P}(P) \setminus \{\emptyset\}$, where $\mathcal{P}(P)$ denotes the power set of $P$. Every set $\alpha \in I(P)$ is called an interaction. The syntax of propositional interaction logic (PIL for short) formulas over $P$ is given by the grammar

$$ \phi ::= true \mid p \mid \bar{\phi} \mid \phi \lor \phi $$
where $p \in P$. As usual, we set $\bar{\phi} = \phi$ for every PIL formula $\phi$ and $false = true$. Hence, the conjunction of two PIL formulas $\phi, \phi'$ is defined by $\phi \wedge \phi' = (\bar{\phi} \vee \bar{\phi'})$. A PIL formula of the form $p_1 \wedge \dots \wedge p_n$ with $n > 0$, and $p_i \in P$ or $p_i = \bar{p}'_i$ with $p'_i \in P$ for every $1 \le i \le n$, is called a *monomial*. For simplicity we denote a monomial $p_1 \wedge \dots \wedge p_n$ by $p_1 \dots p_n$. Monomials of the form $\bigwedge_{p \in P_+} p \wedge \bigwedge_{p \in P_-} \bar{p}$ with $P_+ \cup P_- = P$ and $P_+ \cap P_- = \emptyset$ are called *full monomials*.

Let $\phi$ be a PIL formula and $\alpha$ an interaction. We define the satisfaction relation $\alpha \models_i \phi$ by induction on the structure of $\phi$ as follows:

- $\alpha \models_i true$, $\alpha \models_i \bar{\phi}$ iff $\alpha \not\models_i \phi$,

- $\alpha \models_i p$ iff $p \in \alpha$, $\alpha \models_i \phi_1 \vee \phi_2$ iff $\alpha \models_i \phi_1$ or $\alpha \models_i \phi_2$.

For every $\alpha \in I(P)$ it holds $\alpha \not\models_i false$. Moreover, for every interaction $\alpha \in I(P)$ we define its characteristic monomial $m_\alpha = \bigwedge_{p \in \alpha} p \wedge \bigwedge_{p \notin \alpha} \bar{p}$. A characteristic monomial $m_\alpha$ is actually a full monomial that formalises the interaction $\alpha$. Then, for every $\alpha' \in I(P)$ we trivially get $\alpha' \models_i m_\alpha$ iff $\alpha' = \alpha$.

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

$$ \varphi ::= d \mid \phi \mid \varphi \oplus \varphi \mid \varphi \otimes \varphi $$

where $d \in D$ and $\phi$ denotes a PIL formula over $P$.

We denote by $PIL(D, P)$ the set of all $w_{pvm}$PIL formulas over $P$ and $D$. Next, we present the semantics of formulas $\varphi \in PIL(D, P)$ as polynomials $\|\varphi\| \in D \langle I(P) \rangle$. For the semantics of PIL formulas $\phi$ over $P$ we use the satisfaction relation as defined above. Hence, the semantics of PIL formulas $\phi$ gets only the values 0 and 1.

**Definition 2.** Let $\varphi \in PIL(D, P)$. The semantics of $\varphi$ is a polynomial $\|\varphi\| \in D \langle I(P) \rangle$. For every $\alpha \in I(P)$ the value $\|\varphi\|(\alpha)$ is defined inductively on the structure of $\varphi$ as follows:

- $\|d\|(\alpha) = d$, $\|\varphi_1 \oplus \varphi_2\|(\alpha) = \|\varphi_1\|(\alpha) \oplus \|\varphi_2\|(\alpha)$,

- $\|\phi\|(\alpha) = \begin{cases} 1 & \text{if } \alpha \models_i \phi \\ 0 & \text{otherwise,} \end{cases}$ $\|\varphi_1 \otimes \varphi_2\|(\alpha) = \|\varphi_1\|(\alpha) \otimes \|\varphi_2\|(\alpha)$.

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

$$ f ::= true \mid \phi \mid \neg f \mid f \sqcup f \mid f + f $$

where $\phi$ denotes a PIL formula over $P$. The operators $\neg$, $\sqcup$, and $+$ are called *com-implementation*, *union*, and *coalescing*, respectively. The intersection $\sqcap$ is defined by $f_1 \sqcap f_2 := \neg(\neg f_1 \sqcup \neg f_2)$.
We let $C(P) = \mathcal{P}(I(P))\setminus\{\emptyset\}$. For every PCL formula $f$ and $\gamma \in C(P)$ the satisfaction relation $\gamma \models f$ is defined inductively on the structure of $f$ as follows:

- $\gamma \models true,$

- $\gamma \models \neg f$ iff $\gamma \not\models f,$

- $\gamma \models \phi$ iff $\alpha \models_i \phi$ for every $\alpha \in \gamma,$

- $\gamma \models f_1 \sqcup f_2$ iff $\gamma \models f_1$ or $\gamma \models f_2,$

- $\gamma \models f_1 + f_2$ iff there exist $\gamma_1, \gamma_2 \in C(P)$ such that $\gamma = \gamma_1 \cup \gamma_2,$

and $\gamma_1 \models f_1$ and $\gamma_2 \models f_2$.

We define the closure $\sim \models f$ of every PCL formula $f$ by $\sim \models := f + true$.

Two PCL formulas $f, f'$ are called equivalent, and we denote it by $f \equiv f'$, whenever $\gamma \models f$ iff $\gamma \models f'$ for every $\gamma \in C(P)$. We refer the reader to [13] and [17] 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

$$ \zeta ::= d \mid f \mid \zeta \oplus \zeta \mid \zeta \otimes \zeta \mid \zeta \uplus \zeta \mid *\zeta $$

where $d \in D$, $f$ denotes a PCL formula over $P$, and $\oplus$ 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 $\zeta \in PCL(D,P)$ as polynomials $\|\zeta\| \in D\langle C(P) \rangle$. For the semantics of PCL formulas we use the satisfaction relation as defined previously.

**Definition 4.** Let $\zeta \in PCL(D,P)$. The semantics of $\zeta$ is a polynomial $\|\zeta\| \in D\langle C(P) \rangle$ where for every $\gamma \in C(P)$ the value $\|\zeta\|(\gamma)$ is defined inductively on the structure of $\zeta$ as follows:

- $\|d\|(\gamma) = d,$

- $\|f\|(\gamma) = \begin{cases} 1 & \text{if } \gamma \models f \\ 0 & \text{otherwise} \end{cases},$

- $\|\zeta_1 \oplus \zeta_2\|(\gamma) = \|\zeta_1\|(\gamma) \oplus \|\zeta_2\|(\gamma),$

- $\|\zeta_1 \otimes \zeta_2\|(\gamma) = \|\zeta_1\|(\gamma) \otimes \|\zeta_2\|(\gamma),$

- $\|\zeta_1 \uplus \zeta_2\|(\gamma) = \bigoplus_{\gamma_1 \cup \gamma_2 = \gamma} (\|\zeta_1\|(\gamma_1) \otimes \|\zeta_2\|(\gamma_2)),$

- $\|*\zeta\|(\gamma) = \bigoplus_{n>0} \bigoplus_{\cup_{i=1}^n \gamma_i = \gamma} \text{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n))$

where $\cup$ denotes that the sets $\gamma_1, \dots, \gamma_n$ consist a partition of $\gamma$ 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 $\gamma_1$ and $\gamma_2$ in $\|\zeta_1 \oplus \zeta_2\|(\gamma)$ and the sets $\gamma_1, \dots, \gamma_n$ in $\|*\zeta\|(\gamma)$ are nonempty. Trivially in $\|*\zeta\|(\gamma)$, the maximum value of $n$ is $|\gamma|$, i.e., the cardinality of $\gamma$. Hence,

$$ \|*\zeta\|(\gamma) = \bigoplus_{n \in \{1, \dots, |\gamma|\} \cup \bigcup_{i=1}^n \gamma_i = \gamma} \text{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n)). $$
Moreover, in $\|\ast\zeta\|(\gamma)$, let the sets $\gamma_i \in C(P)$ where $i \in \{1, \dots, n\}$ and $\cup_{i=1}^n \gamma_i = \gamma$. Consider a permutation $(i_1, \dots, i_n)$ of $(1, \dots, n)$. Then

$$ \mathrm{val}(\|\zeta\|(\gamma_1)\dots, \|\zeta\|(\gamma_n)) = \mathrm{val}(\|\zeta\|(\gamma_{i_1}), \dots, \|\zeta\|(\gamma_{i_n})). $$

Hence, $\mathrm{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n)) \oplus \mathrm{val}(\|\zeta\|(\gamma_{i_1}), \dots, \|\zeta\|(\gamma_{i_n})) = \mathrm{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n))$ by the idempotency of $D$. Therefore, for every analysis of $\gamma = \cup_{i=1}^n \gamma_i$, the value $\mathrm{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n))$ in $\|\ast\zeta\|(\gamma)$ is computed only once.

Two $w_{\mathrm{pvm}}$PCL formulas $\zeta_1, \zeta_2$ are called equivalent, and we write $\zeta_1 \equiv \zeta_2$, whenever $\|\zeta_1\|(\gamma) = \|\zeta_2\|(\gamma)$ for every $\gamma \in C(P)$. The closure $\sim \zeta$ of every $w_{\mathrm{pvm}}$PCL formula $\zeta \in PCL(D, P)$ is determined by:

$$ - \sim \zeta := \zeta \oplus (\zeta \oplus 1). $$

**Lemma 1.** Let $\zeta \in PCL(D, P)$. Then

$$ \|\sim\zeta\|(\gamma) = \bigoplus_{\gamma' \subseteq \gamma} \|\zeta\|(\gamma') $$

for every $\gamma \in C(P)$.

Next, we present several properties of our $w_{\mathrm{pvm}}$PCL formulas.

**Proposition 1.** Let $\zeta, \zeta_1, \zeta_2, \zeta_3 \in PCL(D, P)$ and $d \in D$. Then

$$ (i) \quad \zeta \oplus 0 \equiv 0 \equiv 0 \oplus \zeta. $$

If $\otimes$ is commutative, then

$$ (ii) \quad \zeta_1 \oplus \zeta_2 \equiv \zeta_2 \oplus \zeta_1. $$

If $D$ is associative and $\oplus$-distributive, then

$$ (iii) \quad (\zeta_1 \oplus \zeta_2) \oplus \zeta_3 \equiv \zeta_1 \oplus (\zeta_2 \oplus \zeta_3). $$

If $D$ is left-$\oplus$-distributive, then

$$ (iv) \quad \zeta \otimes (\zeta_1 \oplus \zeta_2) \equiv (\zeta \otimes \zeta_1) \oplus (\zeta \otimes \zeta_2). $$

If $D$ is right-$\oplus$-distributive, then

$$ (v) \quad (\zeta_1 \oplus \zeta_2) \otimes \zeta \equiv (\zeta_1 \otimes \zeta) \oplus (\zeta_2 \otimes \zeta). $$

**Proposition 2.** Let $\zeta \in PCL(D, P)$ with $\zeta = d \in D$. If $D$ is left-val-distributive, then

$$ \ast\zeta \equiv d. $$
*Proof.* For every $\gamma = \{a_1, \dots, a_s\}$ where $s \in \mathbb{N}$, we have

$$ \|*\zeta\|(\gamma) = \bigoplus_{n \in \{1, \dots, s\}} \bigoplus_{\gamma_1 \cup \dots \cup \gamma_n = \gamma} \mathrm{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n)) $$

$$ = \mathrm{val}(d) \oplus \mathrm{val}(d, d) \oplus \dots \oplus \mathrm{val}(\overbrace{d, \dots, d}^{s \text{ times}}) $$

$$ = (d \otimes \mathrm{val}(1)) \oplus (d \otimes \mathrm{val}(1, 1)) \oplus \dots \oplus (d \otimes \mathrm{val}(1, \dots, 1)) $$

$$ = (d \otimes 1) \oplus (d \otimes 1) \oplus \dots \oplus (d \otimes 1) = d \oplus \dots \oplus 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 $\oplus$-preservative whenever $\mathrm{val}(d_1 \oplus d_2, d) = \mathrm{val}(d_1, d) \oplus \mathrm{val}(d_2, d)$ and $\mathrm{val}(d, d_1 \oplus d_2) = \mathrm{val}(d, d_1) \oplus \mathrm{val}(d, d_2)$ for every $d, d_1, d_2 \in D$. The pv-monoids $(\mathbb{R} \cup \{-\infty\}, \max, \mathrm{avg}, +, -\infty, 0)$ and $(\mathbb{R} \cup \{+\infty\}, \min, \mathrm{avg}, +, +\infty, 0)$, are $\oplus$-preservative

By a straightforward calculation we can show the next proposition.

**Proposition 3.** Let $D$ be a valuation monoid. If $\mathrm{val}$ is $\oplus$-preservative, then

$$ \mathrm{val} \left( \bigoplus_{i \in I} d_i, \bigoplus_{j \in J} d'_j \right) = \bigoplus_{i \in I, j \in J} \mathrm{val} (d_i, d'_j) $$

where $I, J$ are finite index sets and $d_i, d'_j \in D$ for every $i \in I$ and $j \in J$.

**Proposition 4.** Let $\zeta \in \mathrm{PCL}(D, P)$. If $D$ is $\oplus$-preservative, then

$$ \sim (*\zeta) \equiv *(\sim \zeta). $$

*Proof.* Let $\gamma \in C(P)$. Then

$$ \|*(\sim \zeta)\|(\gamma) = \bigoplus_{n>0} \bigoplus_{\gamma_1 \cup \dots \cup \gamma_n = \gamma} \mathrm{val}(\|\sim \zeta\|(\gamma_1), \dots, \|\sim \zeta\|(\gamma_n)) $$

$$ = \bigoplus_{n>0} \bigoplus_{\gamma_1 \cup \dots \cup \gamma_n = \gamma} \mathrm{val} \left( \bigoplus_{\gamma'_1 \subseteq \gamma_1} \|\zeta\|(\gamma'_1), \dots, \bigoplus_{\gamma'_n \subseteq \gamma_n} \|\zeta\|(\gamma'_n) \right) $$

$$ = \bigoplus_{n>0} \bigoplus_{\gamma_1 \cup \dots \cup \gamma_n = \gamma} \bigoplus_{\gamma'_1 \subseteq \gamma_1} \dots \bigoplus_{\gamma'_n \subseteq \gamma_n} \mathrm{val}(\|\zeta\|(\gamma'_1), \dots, \|\zeta\|(\gamma'_n)) $$

$$ = \bigoplus_{\gamma' \subseteq \gamma} \bigoplus_{n>0} \bigoplus_{\gamma_1 \cup \dots \cup \gamma_n = \gamma'} \mathrm{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n)) $$

$$ = \bigoplus_{\gamma' \subseteq \gamma} \|*\zeta\|(\gamma') = \|\sim (*\zeta)\|(\gamma) $$

where the third equality holds since $D$ is $\oplus$-preservative and the next equalities due to the commutativity of $\oplus$.
**Proposition 5.** Let $\zeta, \zeta_1, \zeta_2 \in PCL(D, P)$. If $D$ is left-⊕-distributive, then

$$ \zeta \uplus (\zeta_1 \oplus \zeta_2) \equiv (\zeta \uplus \zeta_1) \oplus (\zeta \uplus \zeta_2). $$

Next, we show a special case when $\otimes$ distributes over $\uplus$. In general $\otimes$ does not distribute over $\uplus$. For example, let $P = \{p, q\}$ and the $w_{pvm}$PCL formulas $\zeta, \zeta_1, \zeta_2$, where $\zeta = 2$ and $\zeta_1 = \zeta_2 = 1$. If we consider the set $\gamma = \{\{p\}, \{q\}\}$ and the pv-monoid $(\mathbb{R} \cup \{-\infty\}, \max, \text{avg}, +, -\infty, 0)$, then it is easy to show that $\|\zeta \otimes (\zeta_1 \uplus \zeta_2)\|(\gamma) \neq \|(\zeta \otimes \zeta_1) \uplus (\zeta \otimes \zeta_2)\|(\gamma)$. Hence, $\zeta \otimes (\zeta_1 \uplus \zeta_2) \neq (\zeta \otimes \zeta_1) \uplus (\zeta \otimes \zeta_2)$. However, this is not the case when $\zeta$ is a PIL formula and $D$ is left-⊕-distributive.

**Proposition 6.** Let $\phi$ be a PIL formula over $P$ and $\zeta_1, \zeta_2 \in PCL(D, P)$. If $D$ is left-⊕-distributive, then

$$ \phi \otimes (\zeta_1 \uplus \zeta_2) \equiv (\phi \otimes \zeta_1) \uplus (\phi \otimes \zeta_2). $$

# 5 Full normal form for $w_{pvm}$PCL formulas

In this section, we show that for every $w_{pvm}$PCL formula $\zeta \in PCL(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<fnref n="1" /> or $\bigsqcup_{i \in I} \sum_{j \in J_i} m_{i,j}$ (cf. Theorem 4.43 in [13]), and for every weighted PCL formula $\zeta$ over $P$ and a commutative semiring $(K, \oplus, \otimes, 0, 1)$ we can construct a unique equivalent weighted PCL formula of the form $k$ or $\bigoplus_{i \in I} (k_i \otimes \sum_{j \in J_i} m_{i,j})$ (cf. Theorem 1 in [17] and Theorem 25 in [16]). The index sets $I$ and $J_i$, for every $i \in I$, are finite, $k$ and $k_i \in 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.

**Definition 5.** A $w_{pvm}$PCL formula $\zeta \in PCL(D, P)$ is said to be in full normal form if either

1. $\zeta = d$, with $d \in D$, or

2. there are finite index sets $I$ and $J_i$ for every $i \in I$, $d_i \in D$, and full monomials $m_{i,j}$ for every $i \in I$ and $j \in J_i$ such that $\zeta = \bigoplus_{i \in I} (d_i \otimes \sum_{j \in J_i} m_{i,j})$.

Following [16], for every full normal form we can construct an equivalent one satisfying the subsequent statements:

(i) $j \neq j'$ implies $m_{i,j} \neq m_{i,j'}$ for every $i \in I, j, j' \in J_i$, and

<footnote n="1">¹ Following [16] we consider true as a full normal form.</footnote>
(ii) $i \neq i'$ implies $\sum_{j \in J_i} m_{i,j} \neq \sum_{j \in J_{i'}} m_{i',j}$ for every $i, i' \in I$.

By Lemma 1 in [17], if $m_{i,j} \equiv m_{i,j'}$ for some $j \neq j'$, then we get $m_{i,j} + m_{i,j'} \equiv m_{i,j}$. So, we replace $m_{i,j} + m_{i,j'}$ by $m_{i,j}$. For the second case, let $\sum_{j \in J_i} m_{i,j} \equiv \sum_{j \in J_{i'}} m_{i',j}$ for some $i \neq i'$. Then, we replace $(d_i \otimes \sum_{j \in J_i} m_{i,j}) \oplus (d_{i'} \otimes \sum_{j \in J_{i'}} m_{i',j})$ by its equivalent formula $(d_i \oplus d_{i'}) \otimes \sum_{j \in J_i} 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 $\zeta \in PCL(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].

**Lemma 2.** Let $J$ be an index set and $m_j$ full monomials for every $j \in J$. Then, there exists a unique $\bar{\gamma} \in C(P)$ such that for every $\gamma \in C(P)$ we have $\|\sum_{j \in J} m_j\|(\gamma) = 1$ if $\gamma = \bar{\gamma}$ and $\|\sum_{j \in J} m_j\|(\gamma) = 0$, otherwise.

**Proposition 7.** Let $f$ be a PCL formula over $P$ and $D$ a pv-monoid. Then there exist finite index sets $I$ and $J_i$ for every $i \in I$, and full monomials $m_{i,j}$ for every $i \in I$ and $j \in J_i$ such that

$$f \equiv \bigoplus_{i \in I} \sum_{j \in J_i} m_{i,j} \equiv \bigoplus_{i \in I} \left( 1 \otimes \sum_{j \in J_i} m_{i,j} \right).$$

**Lemma 3.** Let $m_i, m'_j$ be full monomials for every $i \in I$ and $j \in J$. Then,

$$\left(\sum_{i \in I} m_i\right) \otimes \left(\sum_{j \in J} m'_j\right) \equiv \left\{ \begin{array}{ll} \sum_{i \in I} m_i & \text{if } \sum_{i \in I} m_i \equiv \sum_{j \in J} m'_j, \\ 0 & \text{otherwise.} \end{array} \right.$$

**Proposition 8.** Let $d_1, d_2 \in D$ and $\zeta_1, \zeta_2 \in PCL(D, P)$. If $D$ is left-⊕-distributive and $\otimes$ is commutative and associative, then

$$(d_1 \otimes \zeta_1) \oplus (d_2 \otimes \zeta_2) \equiv d_1 \otimes d_2 \otimes (\zeta_1 \oplus \zeta_2).$$

**Proposition 9.** Let $m_i, m'_j$ be full monomials for every $i \in I$ and $j \in J$. Then

$$\left(\sum_{i \in I} m_i\right) \oplus \left(\sum_{j \in J} m'_j\right) \equiv \left\{ \begin{array}{ll} \sum_{i \in I} m_i + \sum_{j \in J} m'_j & \text{if } m_i \neq m'_j \text{ for every } i \in I \\ 0 & \text{and } j \in J \end{array} \right. \text{ otherwise.}$$

**Proposition 10.** Let $\zeta \in PCL(D, P)$ which is in full normal form, i.e., $\zeta = \bigoplus_{i \in I} (d_i \otimes \sum_{j \in J_i} m_{i,j})$. Then

$$i. \ \ast\zeta \equiv \bigoplus_{I' \subseteq I} (\text{val}(d_i)_{i \in I'} \otimes (\biguplus_{i \in I'} \sum_{j \in J_i} m_{i,j})),$$

$$ii. \ (\ast\zeta) \otimes (\biguplus_{i \in I} \sum_{j \in J_i} m_{i,j}) \equiv \text{val}(d_1, \dots, d_{|I|}) \otimes (\biguplus_{i \in I} \sum_{j \in J_i} m_{i,j}).$$
*Proof.* i. Let $\gamma \in C(P)$. Then we get

$$ \|*\zeta\|(\gamma) = \bigoplus_{n>0} \bigoplus_{\bigcup_{i=1}^n \gamma_i = \gamma} \mathrm{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n)). $$

By Lemma 2, for every $i \in I$ there exists a unique $\bar{\gamma}_i \in C(P)$ such that for every $\gamma \in C(P)$ we have $\|\sum_{i \in J_i} m_{i,j}\|(\gamma) = 1$ if $\gamma = \bar{\gamma}_i$ and $\|\sum_{i \in J_i} m_{i,j}\|(\gamma) = 0$, otherwise. Hence, $\mathrm{val}(\|\zeta\|(\gamma_1), \dots, \|\zeta\|(\gamma_n)) \neq 0$ when for every $i \in \{1, \dots, n\}$ there exists $j_i \in I$ such that $\gamma_i = \bar{\gamma}_{j_i}$ and, by definition of $\|*\zeta\|(\gamma)$, the sets $\gamma_1, \dots, \gamma_n$ consist a partition of $\gamma$. Moreover,

$$ \mathrm{val}(\|\zeta\|(\bar{\gamma}_{j_1}), \dots, \|\zeta\|(\bar{\gamma}_{j_n})) = \mathrm{val}(d_{j_1}, \dots, d_{j_n}). $$

Since $\mathrm{val}$ is a symmetric function and $D$ is idempotent, we get $\|*\zeta\|(\gamma) = \bigoplus_{I'' \subseteq I} \mathrm{val}(d_i)_{i \in I''}$ where for every $I'' \subseteq I$ it holds $\gamma = \bigcup_{i \in I'' \setminus \gamma_i}$ or equivalently $\|\bigcup_{i \in I''} \sum_{j \in J_i} m_{i,j}\|(\gamma) = 1$. For every other $I'''$ subset of $I$ it holds $\|\bigcup_{i \in I'''} \sum_{j \in J_i} m_{i,j}\|(\gamma) = 0$. So, we get the following $*\zeta = \bigoplus_{I' \subseteq I} (\mathrm{val}(d_i)_{i \in I'} \otimes (\bigcup_{i \in I'} \sum_{j \in J_i} m_{i,j}))$. ii. Let $\gamma \in C(P)$. Then we get

$$ \|(*\zeta) \otimes \left( \bigcup_{i \in I} \sum_{j \in J_i} m_{i,j} \right) \|(\gamma) = \|*\zeta\|(\gamma) \otimes \left\| \bigcup_{i \in I} \sum_{j \in J_i} m_{i,j} \right\|(\gamma). $$

We can easily prove that $\|\bigcup_{i \in I} \sum_{j \in J_i} m_{i,j}\|(\gamma) = 1$ if $\gamma = \bigcup_{i \in I} \bar{\gamma}_i$ and $\|\bigcup_{i \in I} \sum_{j \in J_i} m_{i,j}\|(\gamma) = 0$ otherwise. If $\gamma = \bigcup_{i \in I} \bar{\gamma}_i$, then since $D$ is idempotent we get $\|*\zeta\|(\gamma) = \mathrm{val}(d_1, \dots, d_{|I|})$. Hence,

$$ \begin{aligned} \|(*\zeta) \otimes \left( \bigcup_{i \in I} \sum_{j \in J_i} m_{i,j} \right) \|(\gamma) &= \begin{cases} \mathrm{val}(d_1, \dots, d_{|I|}) & \text{if } \gamma = \bigcup_{i \in I} \bar{\gamma}_i \\ 0 & \text{otherwise.} \end{cases} \\ &= \mathrm{val}(d_1, \dots, d_{|I|}) \otimes \left\| \bigcup_{i \in I} \sum_{j \in J_i} m_{i,j} \right\|(\gamma) \\ &= \left\| \mathrm{val}(d_1, \dots, d_{|I|}) \otimes \left( \bigcup_{i \in I} \sum_{j \in J_i} m_{i,j} \right) \right\|(\gamma), \end{aligned} $$

and we are done.

**Theorem 1.** Let $D$ be an associative, idempotent and $\oplus$-distributive pv-monoid, where $\otimes$ is commutative. Then, for every $w_{\mathrm{pvm}}$PCL formula $\zeta \in \mathrm{PCL}(D, P)$ we can effectively construct an equivalent $w_{\mathrm{pvm}}$PCL formula $\zeta' \in \mathrm{PCL}(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 $\zeta = f$ be a PCL formula. Then, we conclude our claim by Proposition 7. Next let $\zeta = d$ with $d \in D$, then we have nothing to prove.

In the sequel, assume that $\zeta_1, \zeta_2 \in PCL(D, P)$. In [11] we show how we can construct $w_{pvm}$PCL formulas $\zeta^{(1)}, \zeta^{(2)}$ and $\zeta^{(3)}$ in full normal form which are equivalent to $\zeta_1 \oplus \zeta_2, \zeta_1 \otimes \zeta_2$ and $\zeta_1 \uplus \zeta_2$, respectively.

Finally, let $\zeta = *\zeta_1$ and $\zeta'_1 = \bigoplus_{i_1 \in I_1} (d_{i_1} \otimes \sum_{j_1 \in J_{i_1}} m_{i_1, j_1})$ be its equivalent $w_{pvm}$PCL formula in full normal form. We consider the formula $\zeta' = *\zeta'_1$. By Proposition 10, $\zeta'$ can be equivalently written as follows

$$ \zeta' \equiv \bigoplus_{I'_1 \subseteq I_1} \left( \mathrm{val}(d_{i_1})_{i_1 \in I'_1} \otimes \left( \biguplus_{i_1 \in I'_1} \sum_{j_1 \in J_{i_1}} m_{i_1, j_1} \right) \right). $$

We consider the sets $I_1^{(1)}, \dots, I_1^{(k)}$ with $k \in \mathbb{N}$ to be an enumeration of all $I'_1$'s such that $\biguplus_{i_1 \in I'_1} \sum_{j_1 \in J_{i_1}} m_{i_1, j_1} \neq 0$. Hence, by Proposition 9, $\biguplus_{i \in I_1^{(s)}} \sum_{j \in J_i} m_{i, j} \equiv \sum_{i \in I_1^{(s)}} \sum_{j \in J_i} m_{i, j}$ for every $s \in \{1, \dots, k\}$. Moreover, for every $s \in \{1, \dots, k\}$ we let $d'_s = \mathrm{val}(d_i)_{i \in I_1^{(s)}}$. So,

$$ \zeta' \equiv \bigoplus_{s \in \{1, \dots, k\}} \left( d'_s \otimes \left( \sum_{i \in I_1^{(s)}} \sum_{j \in J_i} m_{i, j} \right) \right). $$

Lastly, if $\sum_{i \in I_1^{(s)}} \sum_{j \in J_i} m_{i, j} \neq \sum_{i \in I_1^{(s')}} \sum_{j \in J_i} m_{i, j}$ for every $s, s' \in \{1, \dots, k\}$ with $s \neq s'$, then we are done. However, let $\sum_{i \in I_1^{(s)}} \sum_{j \in J_i} m_{i, j} \equiv \sum_{i \in I_1^{(s')}} \sum_{j \in J_i} m_{i, j}$ for some $s \neq s'$. Then, we replace $(d'_s \otimes (\sum_{i \in I_1^{(s)}} \sum_{j \in J_i} m_{i, j})) \oplus (d'_{s'} \otimes (\sum_{i \in I_1^{(s')}} \sum_{j \in J_i} m_{i, j}))$ by its equivalent formula $(d'_s \oplus d'_{s'}) \otimes \sum_{i \in I_1^{(s)}} \sum_{j \in J_i} m_{i, j}$. We conclude to a full normal form which by construction, it is equivalent to $\zeta$.

The uniqueness of $\zeta^{(1)}, \zeta^{(2)}, \zeta^{(3)}$ and $\zeta'$, 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

$$ \zeta = ((d_1 \otimes m_1) \uplus (d_2 \otimes (m_2 \oplus m_3))) \oplus (d_3 \otimes (m_4 + m_5)) $$

where $d_1, d_2, d_3 \in D$ and $m_i$ is a full monomial over $P$ for every $i \in \{1, \dots, 5\}$. We will compute the full normal form of $\zeta' = *\zeta$. Firstly, we compute the full normal form of $\zeta$.

$$ \zeta \equiv ((d_1 \otimes d_2) \otimes (m_1 + m_2)) \oplus ((d_1 \otimes d_2) \otimes (m_1 + m_3)) \oplus (d_3 \otimes (m_4 + m_5)). $$
By Proposition 10 we get

$$ \zeta' \equiv ((d_1 \otimes d_2) \otimes (m_1 + m_2)) \oplus ((d_1 \otimes d_2) \otimes (m_1 + m_3)) \oplus (d_3 \otimes (m_4 + m_5)) \oplus \\ (\mathrm{val}(d_1 \otimes d_2, d_3) \otimes (m_1 + m_2 + m_4 + m_5)) \oplus \\ (\mathrm{val}(d_1 \otimes d_2) \otimes (m_1 + m_3 + m_4 + m_5))) $$

which is in full normal form.

**Theorem 2.** Let $D$ be an associative, idempotent and $\oplus$-distributive pv-monoid, where $\otimes$ is commutative, and $P$ a finite nonempty set of ports. Then for every $\zeta, \xi \in PCL(D, P)$ the equality $\|\zeta\| = \|\xi\|$ is decidable.

*Proof.* We follow the proof of Theorem 26 in [16]. By Theorem 1 we can effectively construct $w_{pvm}$PCL formulas $\zeta', \xi'$ in full normal form such that $\|\zeta\| = \|\zeta'\|$ and $\|\xi\| = \|\xi'\|$. Let us assume that $\zeta' = \bigoplus_{i \in I} (d_i \otimes \sum_{j \in J_i} m_{i,j})$ and $\xi' = \bigoplus_{l \in L} (d'_l \otimes \sum_{r \in M_l} m'_{l,r})$ which moreover satisfy Statements (i) and (ii). Then, by Statement (ii) we get that $\|\zeta'\| = \|\xi'\|$ iff the following requirements (1)-(3) hold:

1) $\mathrm{card}(I) = \mathrm{card}(L)$,

2) $\{d_i | i \in I\} = \{d'_l | l \in L\}$, and

3) a) if $\mathrm{card}(I) = \mathrm{card}(\{d_i | i \in I\})$, then $\sum_{j \in J_i} m_{i,j} = \sum_{r \in M_l} m'_{l,r}$ for every $i \in I$ and $l \in L$ such that $d_i = d'_l$, or

b) if $\mathrm{card}(I) > \mathrm{card}(\{d_i | i \in I\})$, then we get $\zeta' = \bigoplus_{i' \in I'} (d_{i'} \otimes \bigsqcup_{i \in R_{i'}} \sum_{j \in J_i} m_{i,j})$ where $I' \subsetneq I$, $d_{i'}$'s ($i' \in I'$) are pairwise disjoint, and $R_{i'}$ ($i' \in I'$) is the set of all $i$ in $I$ such that $d_i = d'_{i'}$. Similarly, we get $\xi' = \bigoplus_{l' \in L'} (d'_{l'} \otimes \bigsqcup_{l \in S_{l'}} \sum_{r \in M_l} m'_{l,r})$ where $L' \subsetneq L$, $d'_{l'}$'s ($l' \in L'$) are pairwise disjoint, and $S_{l'}$ ($l' \in L'$) is the set of all $l$ in $L$ such that $d'_l = d'_{l'}$. Then $\bigsqcup_{i \in R_{i'}} \sum_{j \in J_i} m_{i,j} = \bigsqcup_{l \in S_{l'}} \sum_{r \in M_l} m'_{l,r}$ for every $i' \in I'$ and $l' \in 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.

# 6 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 $\zeta$ be a $w_{pvm}$PCL formula. By Theorem 1, $\zeta$ can be written in full normal form, hence $\zeta = \bigoplus_{i \in I} (d_i \otimes \sum_{j \in J_i} m_{i,j})$. We define the full valuation $\otimes\zeta$ of $\zeta$ by:
$$ - \circled{\circ} \zeta := (\ast \zeta) \otimes (\bigcup_{i \in I} \sum_{j \in J_i} m_{i,j}). $$

Then, by Proposition 10 we get $\circled{\circ} \zeta \equiv \text{val}(d_1, \dots, d_{|I|}) \otimes (\bigcup_{i \in I} \sum_{j \in J_i} m_{i,j})$.

**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_{\text{pvm}}$PCL formulas, which according to the underlying pv-monoid we get interesting results.

The monomial $\phi_{i,j} = m_{\{s_i, m_j\}}$ for every $i, j \in \{1, 2\}$ represents the binary interaction between the ports $s_i$ and $m_j$. For every $i, j \in \{1, 2\}$ we consider a value $d_{i,j} \in D$ and the $w_{\text{pvm}}$PCL formula $\varphi_{i,j} = d_{i,j} \otimes \phi_{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 $\gamma = \{\{s_1, m_1\}, \{s_1, m_2\}, \{s_2, m_1\}, \{s_2, m_2\}\}$ and the pv-monoid $(\mathbb{R} \cup \{-\infty\}, \max, \text{avg}, +, -\infty, 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_{\text{pvm}}$PCL formula

$$ \zeta = \underset{i,j \in \{1,2\}}{\oplus} \circled{\circ} (\varphi_{1,i} \oplus \varphi_{2,j}). $$

Then, the value

$$ \begin{aligned} \|\zeta\|(\gamma) &= \left\| \bigoplus_{i,j \in \{1,2\}} \circled{\circ} (\varphi_{1,i} \oplus \varphi_{2,j}) \right\| (\gamma) \\ &= \max \{\text{avg}(d_{1,1}, d_{2,1}), \text{avg}(d_{1,1}, d_{2,2}), \text{avg}(d_{1,2}, d_{2,1}), \text{avg}(d_{1,2}, d_{2,2})\} \end{aligned} $$

computes the average cost for each of the four possible instances and then the maximum of those values. It is interesting to note that $\|\zeta\|(\gamma) = \|\zeta\|(\gamma')$ for every $\gamma' \in C(P)$ with $\gamma \subseteq \gamma'$.

Moreover, let the following $w_{\text{pvm}}$PCL formula

$$ \zeta = \bigotimes_{i,j \in \{1,2\}} \circled{\circ} (\varphi_{1,i} \oplus \varphi_{2,j}). $$

Then, the value

$$ \|\zeta\|(\gamma) = \text{avg}(d_{1,1}, d_{2,1}) + \text{avg}(d_{1,2}, d_{2,1}) + \text{avg}(d_{1,1}, d_{2,2}) + \text{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_{\text{pvm}}$PCL formula:

$$ \zeta = \underset{i \in \{1,2\}}{\oplus} \circled{\circ} (\varphi_{i,1} \oplus \varphi_{i,2}). $$
<figure><img src="image_2.png" /><figcaption>Fig. 1. Weighted Publish/Subscribe architecture.</figcaption></figure>

Then we get

$$ \|\zeta\|(\gamma) = \left\| \bigoplus_{i \in \{1,2\}} (\circledast (\varphi_{i,1} \oplus \varphi_{i,2})) \right\| (\gamma) = \max\{\text{avg}(d_{1,1}, d_{1,2}), \text{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 (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₁ and t₂, and S has the port s. We assume two publisher components P₁, P₂, four subscriber components S₁, S₂, S₃, S₄ and three topic components T₁, T₂, T₃. Hence, the set of ports is P = {p₁, p₂, s₁, s₂, s₃, s₄, t₁₁, t₁₂, t₂₁, t₂₂, t₃₁, t₃₂}. For every i ∈ {1, 2, 3, 4}, j ∈ {1, 2, 3} and k ∈ {1, 2} we denote by dᵢⱼᵢⱼ ∈ D the weight of the interaction among Sᵢ and Tⱼ, i.e., the priority that the subscriber Sᵢ assigns to the receivement of a message from Tⱼ, and by dᵢⱼᵢⱼ ∈ D, the weight of the interaction among Pₖ and Tⱼ, i.e., the priority that the topic Tⱼ assigns to the receivement of a message from Pₖ.

In the sequel, we develop wᵢⱼₖₘₚₖₘₚ 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 \in \{1, 2\}$ and $j \in \{1, 2, 3\}$, the $w_{\text{pvm}}$ PIL formula $\varphi_{pt}(p_i, t_{j1}) = d_{p_i, t_{j1}} \otimes m_{\{p_i, t_{j1}\}}$ characterizes the interaction between a publisher $P_i$ and a topic $T_j$ with its corresponding weight. Moreover, for every $i \in \{1, 2, 3, 4\}$ and $j \in \{1, 2, 3\}$, the $w_{\text{pvm}}$ PIL $\varphi_{st}(s_i, t_{j2}) = d_{s_i, t_{j2}} \otimes m_{\{s_i, t_{j2}\}}$ characterizes the interaction between a subscriber $S_i$ and a topic $T_j$ with its corresponding weight. Then, the $w_{\text{pvm}}$ PCL formula

$$ \zeta_{s_i} = \bigoplus_{j \in \{1,2,3\}} \bigoplus_{k \in \{1,2\}} \otimes (\varphi_{pt}(p_k, t_{j1}) \oplus \varphi_{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 $\gamma = \{\{p_i, t_{j1}\}, \{s_k, t_{j2}\} | i \in \{1, 2\}, j \in \{1, 2, 3\}, k \in \{1, 2, 3, 4\}\}$, and the pv-monoid $(\mathbb{R} \cup \{-\infty\}, \max, \text{avg}, +, -\infty, 0)$. Then the value $\|\zeta_{s_i}\|(\gamma)$ represents the maximum average priority with which the subscriber $S_i$ will receive a message. Also, consider the $w_{\text{pvm}}$ PCL formula $\zeta = \bigotimes_{i \in \{1,2,3,4\}} (\sim \zeta_{s_i})$. Then, the following value

$$ \|\zeta\|(\gamma) = \sum_{i \in \{1,2,3,4\}} \left( \max_{j \in \{1,2,3\}} \{\text{avg}(d_{p_1,t_{j1}}, d_{s_i,t_{j2}}), \text{avg}(d_{p_2,t_{j1}}, d_{s_i,t_{j2}})\} \right) $$

is the sum of the values $\|\zeta_{s_i}\|(\gamma)$ for $i \in \{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_{\text{pvm}}$ PCL formula

$$ \zeta_{t_i} = \bigotimes \left( \bigoplus_{j \in \{1,2\}} \varphi_{pt}(p_j, t_{i1}) \oplus \bigoplus_{k \in \{1,2,3,4\}} \varphi_{st}(s_k, t_{i2}) \right) $$

for $i \in \{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 $\gamma$ given above and the pv-monoid $(\mathbb{R} \cup \{+\infty, -\infty\}, \min, \max, +, -\infty)$. Then,

$$ \|\zeta_{t_i}\|(\gamma) = \max(d_{p_1,t_{i1}}, d_{p_2,t_{i1}}, d_{s_1,t_{i2}}, d_{s_2,t_{i2}}, d_{s_3,t_{i2}}, d_{s_4,t_{i2}}) $$

for $i \in \{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_{\text{pvm}}$ PCL formula

$$ \zeta' = \sim (\zeta_{t_1} \oplus \zeta_{t_2} \oplus \zeta_{t_3}), $$

then $\|\zeta'\|(\gamma) = \min_{i \in \{1,2,3\}} \{\max(d_{p_1,t_{i1}}, d_{p_2,t_{i1}}, d_{s_1,t_{i2}}, d_{s_2,t_{i2}}, d_{s_3,t_{i2}}, d_{s_4,t_{i2}})\}$ 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} \in D$ the weight of the binary interaction between $s_i$ and $s_j$ for every $i, j \in I = \{1, \dots, 5\}$ with $i \neq j$, when $s_i$ is considered as the central component. The $w_{\text{pvm}}$PIL formula characterizing this interaction, for every $i, j \in I$ with $i \neq j$, is given by $\varphi_{ij} = d_{i,j} \otimes m_{\{s_i, s_j\}}$. Therefore, the $w_{\text{pvm}}$PCL formula

$$ \zeta_i = \bigoplus \left( \bigoplus_{j \in I \setminus \{i\}} \varphi_{ij} \right) $$

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_{\text{pvm}}$PCL formula $\zeta = \bigoplus_{i \in I} \zeta_i$ which describes the five alternative versions of the Star architecture. Let $\gamma = \{\{s_i, s_j\} / i, j \in I \text{ and } i \neq j\}$ and $(\mathbb{R} \cup \{+\infty\}, \min, \text{avg}, +, +\infty, 0)$, then we get

$$ \|\zeta\|(\gamma) = \min\{\text{avg}(d_{1,2}, d_{1,3}, d_{1,4}, d_{1,5}), \dots, \text{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.

# 7 Discussion

In our definition of $w_{\text{pvm}}$PIL and $w_{\text{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 \equiv false$ (Proposition 4.4 in [13]) for $f \neq 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_{\text{pvm}}$PCL formulas are polynomials with values in the product valuation monoid. In Theorem 1 we prove that for every $w_{\text{pvm}}$PCL formula $\zeta \in PCL(D, P)$, where $D$ satisfies specific properties, we can effectively construct an equivalent $w_{\text{pvm}}$PCL formula $\zeta' \in PCL(D, P)$ in full normal form.
For this, we require $D$ to be an associative, idempotent and $\oplus$-distributive pv-monoid, where $\otimes$ 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 $(\mathbb{R}\cup\{-\infty\}, \max, \avg, +, -\infty, 0)$ which is associative, idempotent, $\oplus$-distributive and the operator $+$ is commutative. The valuation function $\avg$ can not be written using the operations $\max$ and $+$ of the semiring $(\mathbb{R}\cup\{-\infty\}, \max, +, -\infty, 0)$. Hence, the pv-monoids satisfying the above properties constitute a different structure than the one of semirings.

# 8 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 $\zeta$ over a set of ports $P$ and a pv-monoid $D$ which is associative, $\oplus$-distributive, idempotent and $\otimes$ is commutative, we can effectively construct an equivalent one $\zeta'$ 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.

# References

1. http://maude.cs.illinois.edu/w/index.php/The_Maude_System

2. Attie, P., Baranov, E., Bliutze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Formal Aspects of Computing **28**(2), 207–231 (2016). https://doi.org/10.1007/s00165-015-0349-8

3. Bozga, M., Iosif, R., Sifakis, J.: Local reasoning about parametric and reconfigurable component-based systems. hal-02267423 (2019)

4. Chatterjee, K., Doyen, L., Henzinger, T.: Expressiveness and closure properties for quantitative languages. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science. pp. 199–208. IEEE (2009). https://doi.org/10.1109/LICS.2009.16

5. Chatterjee, K., Doyen, L., Henzinger, T.: Quantitative languages. ACM Transactions on Computational Logic **11**(4), 1–38 (2010). https://doi.org/10.1145/1805950.1805953

6. Chatterjee, K., Henzinger, T., Otop, J.: Computing Average Response Time. In: Principles of Modeling, pp. 143–161. Springer (2018). https://doi.org/10.1007/978-3-319-95246-8_9
7. Droste, M., Meinecke, I.: Weighted automata and regular expressions over valuation monoids. International Journal of Foundations of Computer Science **22**(08), 1829–1844 (2011). https://doi.org/10.1142/S0129054111009069

8. Droste, M., Meinecke, I.: Weighted automata and weighted MSO logics for average and long-time behaviors. Information and Computation **220**, 44–59 (2012). https://doi.org/10.1016/j.ic.2012.10.001

9. Eugster, P., Felber, P., Guerraoui, R., Kermarrec, A.M.: The many faces of publish/subscribe. ACM computing surveys **35**(2), 114–131 (2003). https://doi.org/10.1145/857076.857078

10. Hasan, S., O'Riain, S., Curry, E.: Approximate semantic matching of heterogeneous events. In: Proceedings of the 6th ACM International Conference on Distributed Event-Based Systems. pp. 252–263 (2012). https://doi.org/10.1145/2335484.2335512

11. Karyoti, V., Paraponiari, P.: Weighted PCL over product valuation monoids. arXiv preprint https://arxiv.org/abs/2002.10973 (2020)

12. Malavolta, I., Lewis, G., Schmerl, B., Lago, P., Garlan, D.: How do you Architect your Robots? State of the Practice and Guidelines for ROS-based Systems. In: Proceedings of ICSE-CEIP. ACM (2020). https://doi.org/10.1145/3377813.3381358

13. Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Configuration logics: Modeling architecture styles. Journal of Logical and Algebraic Methods in Programming **86**(1), 2–29 (2017). https://doi.org/10.1016/j.jlamp.2016.05.002

14. Olivieri, A., Rizzo, G., Morand, F.: A publish-subscribe approach to IoT integration: the smart office use case. In: Proceedings of the 29th International Conference on Advanced Information Networking and Applications Workshops. pp. 644–651. IEEE (2015). https://doi.org/10.1109/WAINA.2015.28

15. Otop, J., Henzinger, T., Chatterjee, K.: Quantitative Automata under Probabilistic Semantics. Logical Methods in Computer Science **15**(3) (2019). https://doi.org/10.23638/LMCS

16. Paraponiari, P., Rahonis, G.: Weighted propositional configuration logics: A specification language for architectures with quantitative features. Inform. and Comput. (accepted). Available at https://arxiv.org/abs/1704.04969

17. Paraponiari, P., Rahonis, G.: On weighted configuration logics. In: Proença, J., Lumpe, M. (eds.) Proceedings of FACS 2017. pp. 98–116. LNCS, Springer (2017). https://doi.org/10.1007/978-3-319-68034-7 6

18. Patel, S., Jardosh, S., A.Makwana, Thakkar, A.: Publish/Subscribe mechanism for IoT: A survey of event matching algorithms and open research challenges. In: Proceedings of International Conference on Communication and Networks, Advances in Intelligent Systems and Computing. pp. 287–294. Springer (2017). https://doi.org/10.1007/978-981-10-2750-5-30

19. Yang, K., Zhang, K., Jia, X., Hasan, M.A., Shen, X.: Privacy-preserving attribute-keyword based data publish-subscribe service on cloud platforms. Information Sciences **387**, 116–131 (2017). https://doi.org/10.1016/j.ins.2016.09.020