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

TL;DR

This paper presents a weighted propositional configuration logic over commutative semirings designed as a specification language for software architectures with quantitative features, including normal form construction and formula equivalence decidability.

Contribution

It introduces a novel weighted logic for architecture specifications, providing normal forms and decidability results for formulas involving quantitative features.

Findings

Normal form construction is efficient

Decidability of formula equivalence is established

Application to well-known architectures with quantitative traits

Abstract

We introduce and investigate a weighted propositional configuration logic over commutative semirings. Our logic is intended to serve as a specification language for software architectures with quantitative features. We prove an efficient construction of full normal forms and decidability of equivalence of formulas in this logic. We illustrate the motivation of this work by describing well-known architectures equipped with quantitative characteristics using formulas in our logic.

Equations

$$\varphi ::=\mathrm{true}\mid p\mid \overline{\varphi }\mid \varphi \vee \varphi$$

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

$$f::=\mathrm{true}\mid \varphi \mid \neg f\mid f\bigsqcup f\mid f+f$$

$$\zeta ::=k\mid f\mid \zeta \oplus \zeta \mid \zeta \otimes \zeta \mid \zeta \uplus \zeta$$

$$\Vert \sim \zeta \Vert (\gamma )={⨁}_{{\gamma }^{\prime }\subseteq \gamma }\Vert \zeta \Vert ({\gamma }^{\prime })$$

$$\Vert \sim \zeta \Vert (\gamma )$$

$$=\Vert \zeta \Vert (\gamma )\oplus \left({⨁}_{\gamma ={\gamma }^{\prime }\text{mathaccent}0\cdot \cup {\gamma }^{\prime \prime }}\left(\Vert \zeta \Vert ({\gamma }^{\prime })\otimes \Vert 1\Vert ({\gamma }^{\prime \prime })\right)\right)$$

$$=\Vert \zeta \Vert (\gamma )\oplus {⨁}_{{\gamma }^{\prime }\gamma }\Vert \zeta \Vert ({\gamma }^{\prime })$$

$$={⨁}_{{\gamma }^{\prime }\subseteq \gamma }\Vert \zeta \Vert ({\gamma }^{\prime })$$

$$\zeta =\sim \left(\left({\phi }_{1,1}\oplus {\phi }_{1,2}\right)\uplus \left({\phi }_{2,1}\oplus {\phi }_{2,2}\right)\right).$$

$$\Vert \zeta \Vert (\gamma )$$

$$=\underset{{\gamma }^{\prime }\subseteq \gamma }{⨁}\Vert \left({\phi }_{1,1}\oplus {\phi }_{1,2}\right)\uplus \left({\phi }_{2,1}\oplus {\phi }_{2,2}\right)\Vert ({\gamma }^{\prime })$$

$$=\underset{{\gamma }^{\prime }\subseteq \gamma }{⨁}\left(\underset{{\gamma }^{\prime }={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert {\phi }_{1,1}\oplus {\phi }_{1,2}\Vert ({\gamma }_1)\otimes \Vert {\phi }_{2,1}\oplus {\phi }_{2,2}\Vert ({\gamma }_2)\right)\right)$$

$$=\underset{{\gamma }^{\prime }\subseteq \gamma }{⨁}\left(\underset{{\gamma }^{\prime }={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\left(\Vert {\phi }_{1,1}\Vert ({\gamma }_1)\oplus \Vert {\phi }_{1,2}\Vert ({\gamma }_1)\right)\otimes \left(\Vert {\phi }_{2,1}\Vert ({\gamma }_2)\oplus \Vert {\phi }_{2,2}\Vert ({\gamma }_2)\right)\right)\right).$$

$$\Vert \zeta \Vert (\gamma )=\underset{{\gamma }^{\prime }\subseteq \gamma }{\min }\left(\underset{{\gamma }^{\prime }={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{\min }\left(\min \left(\Vert {\phi }_{1,1}\Vert ({\gamma }_1),\Vert {\phi }_{1,2}\Vert ({\gamma }_1)\right)+\min \left(\Vert {\phi }_{2,1}\Vert ({\gamma }_2),\Vert {\phi }_{2,2}\Vert ({\gamma }_2)\right)\right)\right)$$

$$\Vert \left({\zeta }_1\uplus {\zeta }_2\right)\uplus {\zeta }_3\Vert (\gamma )$$

$$=\underset{\gamma ={\gamma }^{\prime }\text{mathaccent}0\cdot \cup {\gamma }_3}{⨁}\left(\left(\underset{{\gamma }^{\prime }={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2)\right)\right)\otimes \Vert {\zeta }_3\Vert ({\gamma }_3)\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2\text{mathaccent}0\cdot \cup {\gamma }_3}{⨁}\left(\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2)\right)\otimes \Vert {\zeta }_3\Vert ({\gamma }_3)\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2\text{mathaccent}0\cdot \cup {\gamma }_3}{⨁}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \left(\Vert {\zeta }_2\Vert ({\gamma }_2)\otimes \Vert {\zeta }_3\Vert ({\gamma }_3)\right)\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup \gamma \prime }{⨁}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \left(\underset{{\gamma }^{\prime }={\gamma }_2\text{mathaccent}0\cdot \cup {\gamma }_3}{⨁}\left(\Vert {\zeta }_2\Vert ({\gamma }_2)\otimes \Vert {\zeta }_3\Vert ({\gamma }_3)\right)\right)\right)$$

$$=\Vert {\zeta }_1\uplus \left({\zeta }_2\uplus {\zeta }_3\right)\Vert (\gamma ),$$

$$\Vert {\zeta }_1\uplus ({\zeta }_2\oplus {\zeta }_3)\Vert (\gamma )$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }^{\prime }}{⨁}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \left(\Vert {\zeta }_2\Vert ({\gamma }^{\prime })\oplus \Vert {\zeta }_3\Vert ({\gamma }^{\prime })\right)\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }^{\prime }}{⨁}\left(\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }^{\prime })\right)\oplus \left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_3\Vert ({\gamma }^{\prime })\right)\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }^{\prime }}{⨁}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }^{\prime })\right)\oplus \underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }^{\prime }}{⨁}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_3\Vert ({\gamma }^{\prime })\right)$$

$$=\Vert {\zeta }_1\uplus {\zeta }_2\Vert (\gamma )\oplus \Vert {\zeta }_1\uplus {\zeta }_3\Vert (\gamma )$$

$$=\Vert \left({\zeta }_1\uplus {\zeta }_2\right)\oplus \left({\zeta }_1\uplus {\zeta }_3\right)\Vert (\gamma ),$$

$$\Vert \zeta \otimes ({\zeta }_1\uplus {\zeta }_2)\Vert (\gamma )=\Vert \zeta \Vert (\gamma )\cdot \Vert {\zeta }_1\uplus {\zeta }_2\Vert (\gamma )=\Vert \zeta \Vert (\gamma )\cdot \left(\sum _{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\cdot \Vert {\zeta }_2\Vert ({\gamma }_2)\right)\right)=2\cdot (1+1)=4$$

$$\Vert (\zeta \otimes {\zeta }_1)\uplus (\zeta \otimes {\zeta }_2)\Vert (\gamma )=\sum _{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}\left(\Vert \zeta \otimes {\zeta }_1\Vert ({\gamma }_1)\cdot \Vert \zeta \otimes {\zeta }_2\Vert ({\gamma }_2)\right)=2\cdot 2+2\cdot 2=8.$$

$$\varphi \otimes ({\zeta }_1\uplus {\zeta }_2)\equiv (\varphi \otimes {\zeta }_1)\uplus (\varphi \otimes {\zeta }_2).$$

$$\Vert \varphi \otimes ({\zeta }_1\uplus {\zeta }_2)\Vert (\gamma )$$

$$=\Vert \varphi \Vert (\gamma )\otimes \left(\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2)\right)\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert \varphi \Vert (\gamma )\otimes (\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2))\right).$$

$$\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert \varphi \Vert (\gamma )\otimes (\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2))\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert \varphi \Vert ({\gamma }_1)\otimes \Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert \varphi \Vert ({\gamma }_2)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2)\right)$$

$$=\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert \varphi \otimes {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert \varphi \otimes {\zeta }_2\Vert ({\gamma }_2)\right)$$

$$=\Vert (\varphi \otimes {\zeta }_1)\uplus (\varphi \otimes {\zeta }_2)\Vert (\gamma ).$$

$$\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert \varphi \Vert (\gamma )\otimes (\Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2))\right)=0$$

$$\underset{\gamma ={\gamma }_1\text{mathaccent}0\cdot \cup {\gamma }_2}{⨁}\left(\Vert \varphi \Vert ({\gamma }_1)\otimes \Vert {\zeta }_1\Vert ({\gamma }_1)\otimes \Vert \varphi \Vert ({\gamma }_2)\otimes \Vert {\zeta }_2\Vert ({\gamma }_2)\right)=0,$$

$$\Vert \varphi \otimes ({\zeta }_1\uplus {\zeta }_2)\Vert (\gamma )=0=\Vert (\varphi \otimes {\zeta }_1)\uplus (\varphi \otimes {\zeta }_2)\Vert (\gamma )$$

$$\Vert \sim ({\zeta }_1\oplus {\zeta }_2)\Vert (\gamma )$$

Full text

Keywords: Software architectures, Propositional configuration logic, Weighted propositional configuration logic

1 Introduction

Architecture is a critical issue in design and development of complex software systems. Whenever the construction of a software system is based on a “good” architecture, then the system satisfies most of its functional and quality requirements. But what are the characteristics of a “good” architecture and how can one design it? Despite the huge progress on software architecture, over almost three decades, the field remains relatively immature (cf. [8] for a detailed presentation of the progress of software architecture). Several fundamental matters still remain open, for instance the distinction between architectures and their properties. To address these issues there is a need of a formal treatment of architectures. The very recent work of [12] contributes towards this direction by studying the relation among architectures and architecture styles. An architecture consists of a fixed number of components connected in a concrete topology. An architecture style describes a family of “similar” architectures, i.e., architectures with the same types of components and topologies. The authors of [12] introduced the propositional configuration logic (PCL for short) which was proved sufficient 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. The first-order and second-order extensions of PCL described perfectly the concept of architecture styles. Therefore, PCL and its first- and second-order extensions constitute logics for the specification of architecture styles and hence, an important contribution to rigorous systems design (cf. [16]).

In this paper we extend the work of [12] in a quantitative setup, and specifically we introduce and investigate a weighted PCL (wPCL for short) over a commutative semiring $(K,\oplus,\otimes,0,1)$. Our work is motivated as follows. Propositional configuration logic of [12] describes in a strict mathematical way qualitative features of architectures. Nevertheless, in several practical applications also quantitative characteristics of architectures are required: the costs of the interactions among the components of an architecture, the time needed, the probability of the implementation of a concrete interaction, etc. For instance, the development of IoT and cloud applications based on the well-known Publish/Subscribe architecture [15, 13, 17] requires quantitative characteristics of the architecture. Therefore, a specification language for the study of weighted architectures is needed and our wPCL is intended to play this role. wPCL consists of the PCL of [12] which is interpreted in the same way, and a copy of it which is interpreted quantitatively. This formulation has the advantage that practitioners can use the PCL exactly as they are used to, and the copy of it for the quantitative interpretation. The semantics of wPCL formulas are polynomials with values in the semiring $K$. The semantics of the unweighted PCL formulas take only the values $1$ and [math] corresponding to $\mathrm{true}$ and $\mathrm{false}$, respectively. Weighted logics have been considered so far in other set-ups (cf. for instance [5]).

The main contributions of our work are the following.

• i)

In our first main result, we prove that for every wPCL formula we can effectively construct, in doubly exponential time, an equivalent one in full normal form which is unique up to the equivalence relation. Computation of full normal forms can be done in an automatic way using the Maude system, following a method similar to the one for PCL in [12].

• ii)

The second main result of our work states the decidability of equivalence of wPCL formulas. Because of (i), two wPCL formulas are equivalent iff they have the same full normal form hence, we do not need to check equality for all possible models.

• iii)

We introduce a notion of soundness (for the first time for weighted logics over semirings, according to our best knowledge), and as a third main result of the paper we show that wPCL is sound.

• iv)

We succeed to describe in a strict logical way several well-known software architectures with additional quantitative characteristics, which are motivated by real applications.

A preliminary version of this paper appeared in [14].

2 Preliminaries

A semiring $(K,\oplus,\otimes,0,1)$* *consists of a set $K,$ two binary operations $\oplus$ and $\otimes$ and two constant elements [math] and $1$ such that $(K,\oplus,0)$ is a commutative monoid, $(K,\otimes,1)$ is a monoid, multiplication $\otimes$ distributes over addition $\oplus$, and $0\otimes k=k\otimes 0=0$ for every $k\in K$. If the monoid $(K,\otimes,1)$ is commutative, then the semiring is called commutative. The semiring is denoted simply by $K$ if the operations and the constant elements are understood. The result of the empty product as usual equals to $1$. The semiring $K$ is called (additively) idempotent if $k\oplus k=k$ for every $k\in K$. The following algebraic structures are well-known semirings. The semiring $(\mathbb{N},+,\cdot,0,1)$ of natural numbers, the Boolean semiring $B=(\{0,1\},+,\cdot,0,1)$, the tropical or min-plus semiring $\mathbb{R}_{\min}=(\mathbb{R}_{+}\cup\{\infty\},\min,+,\infty,0)$ where $\mathbb{R}_{+}=\{r\in\mathbb{R}\mid r\geq 0\}$, the arctical or max-plus semiring $\mathbb{R}_{\max}=(\mathbb{R}_{+}\cup\{-\infty\},\max,+,-\infty,0)$, the Viterbi semiring $(\left[0,1\right],\max,\cdot,0,1)$ used in probability theory, and every bounded distributive lattice with the operations $\sup$ and $\inf$.

Let $Q$ be a set. A formal series (or simply series) over $Q$ and $K$ is a mapping $s:Q\rightarrow K$. The support of $s$ is the set $\mathrm{supp}(s)=\{q\in Q\mid s(q)\neq 0\}$. A series with finite support is also called a polynomial. We denote by $K\left\langle Q\right\rangle$ the class of all polynomials over $Q$ and $K$. Let $s,r\in K\left\langle Q\right\rangle$ and $k\in K$. The sum $s\oplus r$, the products with scalars $ks$ and $sk$, and the* Hadamard product* $s\otimes r$ are defined elementwise, respectively by $s\oplus r(v)=s(v)\oplus r(v),ks(v)=k\otimes s(v),sk(v)=s(v)\otimes k,s\otimes r(v)=s(v)\otimes r(v)$ for every $v\in Q$.

Throughout the paper $(K,\oplus,\otimes,0,1)$ will denote a commutative semiring.

3 Weighted propositional interaction logic

In this section, we introduce the weighted propositional interaction logic. For this, we need to recall the propositional interaction logic [12] first.

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 $a\in I(P)$ is called an interaction. The syntax of propositional interaction logic (PIL for short) formulas over $P$ is given by the grammar

[TABLE]

where $p\in P$. As usual, we set $\overline{\overline{\phi}}=\phi$ for every PIL formula $\phi$ and $\mathrm{false}=\overline{\mathrm{true}}$. Then, the conjunction of two PIL formulas $\phi,\phi^{\prime}$ is defined by $\phi\wedge\phi^{\prime}=\overline{\left(\overline{\phi}\vee\overline{\phi^{\prime}}\right)}$. A PIL formula of the form $p_{1}\wedge\ldots\wedge p_{n}$ with $n>0$, and $p_{i}\in P$ or $p_{i}=\overline{p^{\prime}_{i}}$ with $p^{\prime}_{i}\in P$ for every $1\leq i\leq n$, is called a monomial. We shall simply denote a monomial $p_{1}\wedge\ldots\wedge p_{n}$ by $p_{1}\ldots p_{n}$.

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

$a\models_{i}\mathrm{true}$,

• -

$a\models_{i}p$   iff   $p\in a$,

• -

$a\models_{i}\overline{\phi}$   iff   $a\not\models_{i}\phi$,

• -

$a\models_{i}\phi_{1}\vee\phi_{2}$   iff   $a\models_{i}\phi_{1}$ or $a\models_{i}\phi_{2}$.

It should be clear that $a\not\models_{i}\mathrm{false}$ for every $a\in I(P)$. For every interaction $a$ we define its characteristic monomial $m_{a}=\bigwedge\nolimits_{p\in a}p\wedge\bigwedge\nolimits_{p\notin a}\overline{p}$. Then, for every $a^{\prime}\in I(P)$ we trivially get $a^{\prime}\models_{i}m_{a}$ iff $a^{\prime}=a$.

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

Definition 1

The syntax of formulas of the weighted PIL (wPIL for short) over $P$ and $K$ is given by the grammar

[TABLE]

where $k\in K$ and $\phi$ denotes a PIL formula over $P$.

We denote by $PIL(K,P)$ the set of all wPIL formulas $\varphi$ over $P$ and $K$. Next, we represent the semantics of formulas $\varphi\in PIL(K,P)$ as polynomials $\left\|\varphi\right\|\in K\left\langle I(P)\right\rangle$222Since $P$ is finite, the domain of $\|\varphi\|$ is finite and in turn its support is also finite.. For the semantics of PIL formulas $\phi$ we use the satisfaction relation as defined above. In this way, we ensure that the semantics of PIL formulas $\phi$ gets only the values [math] and $1$.

Definition 2

Let $\varphi\in PIL(K,P)$. The semantics of $\varphi$ is a polynomial $\left\|\varphi\right\|\in K\left\langle I(P)\right\rangle$ where for every $a\in I(P)$ the value $\left\|\varphi\right\|(a)$ is defined inductively on the structure of $\varphi$ as follows:

$\left\|k\right\|(a)=k,$**

• -

\left\|\phi\right\|(a)=\left\{\begin{array}[c]{rl}1&\textnormal{ if }a\models_{i}\phi\\ 0&\textnormal{ otherwise}\end{array},\right.**

• -

$\left\|\varphi\oplus\psi\right\|(a)=\left\|\varphi\right\|(a)\oplus\left\|\psi\right\|(a),$**

• -

$\left\|\varphi\otimes\psi\right\|(a)=\left\|\varphi\right\|(a)\otimes\left\|\psi\right\|(a).$**

The reader should note that the semantics of the wPIL formulas $\phi\vee\phi$ and $\phi\oplus\phi$, where $\phi$ is a PIL formula, are different. Indeed assume that $a\in I(P)$ is such that $a\models_{i}\phi$. Then, by our definition above, we get $\left\|\phi\vee\phi\right\|(a)=1$ whereas $\left\|\phi\oplus\phi\right\|(a)=1\oplus 1$. Next we present an example of a wPIL formula.

Example 3

We recall from [12] the Master/Slave architecture for two masters $M_{1},M_{2}$ and two slaves $S_{1},S_{2}$ with ports $p_{1},p_{2}$ and $q_{1},q_{2}$, respectively (Figure 1). The monomial $\phi_{i,j}=m_{\{q_{i},p_{j}\}}$ for every $1\leq i,j\leq 2$ defines the binary interaction between the ports $q_{i}$ and $p_{j}$. For every $1\leq i,j\leq 2$ we consider a value $k_{i,j}\in K$ and the wPIL formula $\varphi_{i,j}=k_{i,j}\otimes\phi_{i,j}$. Hence, $k_{i,j}$ can be considered, according to the underlying semiring, as the “cost” for the implementation of the interaction $\phi_{i,j}$. For instance if $K$ is the Viterbi semiring, then the value $k_{i,j}\in[0,1]$ represents the probability of the implementation of the interaction between the ports $q_{i}$ and $p_{j}$.

4 Weighted propositional configuration logic

In this section, we introduce and investigate the weighted propositional configuration logic. Firstly, we recall the configuration logic from [12]. More precisely, the syntax of *propositional configuration logic *(PCL for short) formulas over $P$ is given by the grammar

[TABLE]

where $\phi$ denotes a PIL formula over $P$. The operators $\lnot$, $\sqcup$, and $+$ are called *complementation, union, *and coalescing, respectively. We define also the intersection $\sqcap$ and implication $\implies$ operators, respectively as follows:

• $f_{1}\sqcap f_{2}:=\lnot(\lnot f_{1}\sqcup\lnot f_{2}),$

• $f_{1}\implies f_{2}:=\lnot f_{1}\sqcup f_{2}.$

To avoid any confusion, every PCL formula which is a PIL formula will be called an interaction formula. We let $C(P)=\mathcal{P}(I(P))\setminus\{\emptyset\}$. For every PCL formula $f$ and $\gamma\in C(P)$ we define the satisfaction relation $\gamma\models f$ inductively on the structure of $f$ as follows:

$\gamma\models\mathrm{true},$

• -

$\gamma\models\phi$   iff  $\ a\models_{i}\phi$ for every $a\in\gamma,$

• -

$\gamma\models\lnot f$   iff   $\gamma\not\models f,$

• -

$\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}.$

Trivially, we get

• $\gamma\models f_{1}\sqcap f_{2}$   iff   $\gamma\models f_{1}$ and $\gamma\models f_{2},$ and

• $\gamma\models f_{1}\implies f_{2}$   iff   $\gamma\not\models f_{1}$ or $\gamma\models f_{2}.$

We define the closure ${\sim}f$ of every PCL formula $f$ by

• ${\sim}f:=f+\mathrm{true}$,

and the disjunction $f_{1}\vee f_{2}$ of two PCL formulas $f_{1}$ and $f_{2}$ by

• $f_{1}\vee f_{2}:=f_{1}\sqcup f_{2}\sqcup(f_{1}+f_{2})$.

Two PCL formulas $f,f^{\prime}$ are called equivalent, and we denote it by $f\equiv f^{\prime},$ whenever $\gamma\models f$ iff $\gamma\models f^{\prime}$ for every $\gamma\in C(P)$. A PCL formula $f$ is called downward-closed if $\gamma\models f$ implies $\gamma^{\prime}\models f$ for every $\gamma^{\prime}\subseteq\gamma$, and $f$ is called $\cup$-closed if $\gamma\models f$ and $\gamma^{\prime}\models f$ implies $\gamma\cup\gamma^{\prime}\models f$.

In the subsequent Propositions 4-(i) we recall from [12] properties of PCL formulas that will be needed in the sequel. We refer the reader to [12] for further properties of PCL formulas.

Proposition 4

A PCL formula is $\cup$-closed and downward-closed iff it is an interaction formula.

Proposition 5

Let $\phi,\phi^{\prime}$ be interaction formulas. Then

• i)

$\phi+\phi\equiv\phi$.

• ii)

$\phi\wedge\phi^{\prime}\equiv\phi\sqcap\phi^{\prime}$.

Due to Proposition 5(ii) we denote, in the sequel, both conjunction and intersection operations of PCL formulas with the same symbol $\wedge$.

Proposition 6

• (i)

The operators $\sqcup$, $\lnot$, $\wedge$ satisfy the usual axioms of propositional logic.

• (ii)

The coalescing operation is associative, commutative, and has $\mathrm{false}$ as an absorbing element.

Next we introduce our weighted PCL.

Definition 7

The syntax of formulas of the weighted PCL (wPCL for short) over $P$ and $K$ is given by the grammar

[TABLE]

where $k\in K$, $f$ denotes a PCL formula over $P$, and $\uplus$ denotes the coalescing operator among wPCL formulas.

Again, as for PCL formulas, to avoid any confusion, every wPCL formula which is a wPIL formula will be called a weighted interaction formula. We denote by $PCL(K,P)$ the set of all wPCL formulas over $P$ and $K$. We represent the semantics of formulas $\zeta\in PCL(K,P)$ as polynomials $\left\|\zeta\right\|\in K\left\langle C(P)\right\rangle$. For the semantics of PCL formulas we use the satisfaction relation as defined previously.

Definition 8

Let $\zeta\in PCL(K,P)$. The semantics of $\zeta$ is a polynomial $\left\|\zeta\right\|\in K\left\langle C(P)\right\rangle$ where for every $\gamma\in C(P)$ the value $\left\|\zeta\right\|(\gamma)$ is defined inductively as follows:

$\left\|k\right\|(\gamma)=k,$**

• -

\left\|f\right\|(\gamma)=\left\{\begin{array}[c]{rl}1&\textnormal{ if }\gamma\models f\\ 0&\textnormal{ otherwise}\end{array},\right.**

• -

$\left\|\zeta_{1}\oplus\zeta_{2}\right\|(\gamma)=\left\|\zeta_{1}\right\|(\gamma)\oplus\left\|\zeta_{2}\right\|(\gamma),$**

• -

$\left\|\zeta_{1}\otimes\zeta_{2}\right\|(\gamma)=\left\|\zeta_{1}\right\|(\gamma)\otimes\left\|\zeta_{2}\right\|(\gamma),$**

• -

$\left\|\zeta_{1}\uplus\zeta_{2}\right\|(\gamma)=\bigoplus\nolimits_{\gamma=\gamma_{1}\mathbin{\mathaccent 0{\cdot}\cup}\gamma_{2}}\left(\left\|\zeta_{1}\right\|(\gamma_{1})\otimes\left\|\zeta_{2}\right\|(\gamma_{2})\right)$**

where $\mathbin{\mathaccent 0{\cdot}\cup}$ denotes the disjoint union of the sets $\gamma_{1}$ and $\gamma_{2}$.

Since the semantics of every wPCL formula is defined on $C(P)$, the sets $\gamma_{1}$ and $\gamma_{2}$ in $\left\|\zeta_{1}\uplus\zeta_{2}\right\|(\gamma)$ are nonempty. Two wPCL formulas $\zeta_{1},\zeta_{2}$ are called equivalent, and we write $\zeta_{1}\equiv\zeta_{2}$, whenever $\left\|\zeta_{1}\right\|=\left\|\zeta_{2}\right\|$. The *closure *${\sim}\zeta$ of every wPCL formula $\zeta\in PCL(K,P)$ is determined by:

• ${\sim}\zeta:=\zeta\oplus(\zeta\uplus 1)$.

Lemma 9

Let $\zeta\in PCL(K,P)$. Then

[TABLE]

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

Proof. We compute

[TABLE]

for every $\gamma\in C(P)$, where the fourth equality holds since $\gamma^{\prime}$ and $\gamma^{\prime\prime}$ are disjoint.

Remark 10

The reader should notice the difference in the definition of semantics among coalescing in PCL, taken from [12], and coalescing in wPCL. Though $(\gamma_{1},\gamma_{2})$ is not required to be a partition of $\gamma$ for coalescing in PCL, it is used like that in all considered software architectures [12]. More precisely, let us assume that $f_{1}+f_{2}$ is a subformula of a PCL formula $f$ over $P$ representing an architecture. This means that $f_{1}$ describes the topology of a part of the architecture and $f_{2}$ the topology of another part of the architecture. The two parts may have common components but not the same connections (interactions). Hence, if $\gamma\models f_{1}+f_{2}$, then a subset $\gamma_{1}$ of $\gamma$ satisfies $f_{1}$ and its complement $\gamma_{2}$ (according to $\gamma$) satisfies $f_{2}$. Therefore, our definition of coalescing in wPCL does not decrease its usefulness to the description of architectures. On the other hand, our definition intents also to the truth of Lemma 9 which is important for the description of architectures with quantitative characteristics, as it is the corresponding result in PCL (cf. Statement after Definition 4.22 in [12]).

Example 11** (Example 3 continued)**

The four possible configurations of the Master/Slave architecture for two masters $M_{1},M_{2}$ and two slaves $S_{1},S_{2}$ with ports $p_{1},p_{2}$ and $q_{1},q_{2}$, respectively (Figure 1), are given by the PCL formula $\left(\phi_{1,1}\sqcup\phi_{1,2}\right)+\left(\phi_{2,1}\sqcup\phi_{2,2}\right).$ We consider the wPCL formula

[TABLE]

Then for $\gamma\in C\left(\left\{p_{1},p_{2},q_{1},q_{2}\right\}\right)$ we get

[TABLE]

Let for instance $K=\mathbb{R}_{\min}$ and $\gamma=\{\{q_{1},p_{1}\},\{q_{1},p_{2}\},\{q_{2},p_{1}\},\{q_{2},p_{2}\}\}$. Then the value

[TABLE]

is the minimum “cost” among all the implementations of the Master/Slave architecture.

In the sequel, we state several properties of our wPCL formulas.

Proposition 12

Let $\zeta_{1},\zeta_{2},\zeta_{3}\in PCL(K,P)$. Then

• (i)

$\left(\zeta_{1}\uplus\zeta_{2}\right)\uplus\zeta_{3}\equiv\zeta_{1}\uplus\left(\zeta_{2}\uplus\zeta_{3}\right).$**

• (ii)

$\zeta_{1}\uplus 0\equiv 0.$**

• (iii)

$\zeta_{1}\uplus\zeta_{2}\equiv\zeta_{2}\uplus\zeta_{1}.$**

• (iv)

$\zeta_{1}\uplus(\zeta_{2}\oplus\zeta_{3})\equiv(\zeta_{1}\uplus\zeta_{2})\oplus(\zeta_{1}\uplus\zeta_{3}).$**

Proof. We prove only (i) and (iv), the other two statements are straightforward. Let $\gamma\in C(P)$. Then

[TABLE]

and hence $\left(\zeta_{1}\uplus\zeta_{2}\right)\uplus\zeta_{3}\equiv\zeta_{1}\uplus\left(\zeta_{2}\uplus\zeta_{3}\right)$, as required.

Next

[TABLE]

and we are done.

We aim to show that $\otimes$ does not distribute, in general, over $\uplus$. For this, we consider the semiring $\left(\mathbb{N},+,\cdot,0,1\right)$ of natural numbers, the set of ports $P=\{p,q\}$ and the formulas $\zeta,\zeta_{1},\zeta_{2}\ \in PCL(\mathbb{N},P)$ with $\zeta=2$ and $\zeta_{1}=\zeta_{2}=1$. We let $\gamma=\{\{p\},\{q\}\}$. Then

[TABLE]

whereas

[TABLE]

Hence $\zeta\otimes(\zeta_{1}\uplus\zeta_{2})\not\equiv(\zeta\otimes\zeta_{1})\uplus(\zeta\otimes\zeta_{2})$. Nevertheless, this is not the case whenever $\zeta$ is a PIL formula. More precisely, we state the subsequent proposition.

Proposition 13

Let $\phi$ be a PIL formula over $P$ and $\zeta_{1},\zeta_{2}\ \in PCL(K,P)$. Then

[TABLE]

Proof. For every $\gamma\in C(P)$ we have

[TABLE]

We distinguish two cases.

• •

$\|\phi\|(\gamma)=1$. Then by definition, $\gamma\models\phi$ which, by Proposition 4, implies that $\gamma^{\prime}\models\phi$, and hence $\|\phi\|(\gamma^{\prime})=1$ for every $\gamma^{\prime}\subseteq\gamma$. Therefore, we get

[TABLE]

• •

$\|\phi\|(\gamma)=0$. Hence $\gamma\not\models\phi$, i.e., there is an $a\in\gamma$ such that $a\not\models_{i}\phi$. This in turn implies that $\gamma^{\prime}\not\models\phi$ for every $\gamma^{\prime}\subseteq\gamma$ with $a\in\gamma^{\prime}$. Therefore, we get

[TABLE]

and

[TABLE]

i.e.,

[TABLE]

and this concludes our proof.

Proposition 14

Let $\zeta,\zeta_{1},\zeta_{2}\in PCL(K,P)$. Then

• (i)

${\sim}(\zeta_{1}\oplus\zeta_{2})\equiv{\sim}\zeta_{1}\oplus{\sim}\zeta_{2}.$**

If in addition $K$ is idempotent, then

• (ii)

${\sim}(\zeta_{1}\uplus\zeta_{2})\equiv{\sim}\zeta_{1}\uplus{\sim}\zeta_{2}.$**

• (iii)

${\sim}{\sim}\zeta\equiv{\sim}\zeta.$**

Proof. For every $\gamma\in C(P)$ we have

(i)

[TABLE]

(ii)

[TABLE]

where the third equality holds since $K$ is idempotent333For instance, if $\gamma=\{a,b,c\}$, then the product $\|\zeta_{1}\|(a)\otimes\|\zeta_{2}\|(b)$ occurs only once in the left-hand side of the third equality, but two times in the right-hand side one..

(iii)

[TABLE]

where the third equality holds by the idempotency property of $K$.

In the subsequent examples, we present wPCL formulas describing well-known architectures equipped with quantitative features.

Example 15** (Weighted Star architecture)**

Star architecture is a software architecture relating components of the same type. More precisely, given a set of components one of them is considered as the central component and is connected to every other component through a binary interaction. No other interactions are permitted.

Next, we build a wPCL formula representing the Star architecture with five components. We assume that every component has a single port and let $I=\{1,2,3,4,5\}$ and $P=\{s_{1},s_{2},s_{3},s_{4},s_{5}\}$. For simplicity we call every component by its port name. Let us consider firstly that $s_{1}$ is the central component. The architecture is illustrated in Figure 2. We denote by $k_{i}\in K$ the weight of the binary interaction between $s_{1}$ and $s_{i}$ for every $i\in I\setminus\{1\}$. The wPIL formula characterizing this interaction, for every $i\in I\setminus\{1\}$, is given by $\zeta_{i}=k_{i}\otimes m_{\{s_{1},s_{i}\}}$. Since $s_{1}$ interacts with all the other ports, the Star architecture is described by the subsequent wPCL formula:

[TABLE]

Now, we consider the case where every component in the architecture can be the central one, hence we get five versions of the Star architecture with five components. By assuming that the weight of every interaction refers to the cost of its implementation, we should like to compute which version of the Star architecture has the minimum cost and which one has the maximum cost. Therefore, we consider for every $i\in I$ the corresponding architecture with $s_{i}$ being the central component. We denote by $k_{ij}\in K$ the weight of the binary interaction between the central component $s_{i}$ and the component $s_{j}$ with $j\in I\setminus\{i\}$. The wPCL formula characterizing this interaction is given by $\zeta_{ij}=k_{ij}\otimes m_{\{s_{i},s_{j}\}}$. Therefore, the wPCL formula

[TABLE]

describes the binary interactions of the central component $s_{i}$ with the rest of all the other components. We conclude to the next wPCL formula $\zeta^{\prime}$ which describes the five alternative versions of the Star architecture, derived by five components, and the total cost:

[TABLE]

Hence, for $K=\mathbb{R}_{\min}$ (resp. $K=\mathbb{R}_{\max}$) and $\gamma=\{\{s_{i},s_{j}\}\mid i,j\in I\text{ and }i\neq j\}$ we get the architecture with the minimum (resp. maximum) cost.

Example 16** (Weighted Pipes and Filters architecture)**

The Pipes and Filters architecture (cf. [9]) involves two types of components, the pipes and the filters denoted respectively, by the letters $P$ and $F$. Every $P$ component has two ports $p.in$ and $p.out$, and every $F$ component has also two ports $f.in$ and $f.out$ (Figure 3). Every $f.in$ (resp. $f.out$) port of a filter is connected to a $p.out$ (resp. $p.in$) port of a single pipe. The $p.out$ port of any pipe can be connected to at most one filter port $f.in$.

In our example, we develop a wPCL formula characterizing the Pipes and Filters architecture for four pipes and three filters. For this, we let $I=\{1,2,3\}$ and denote the three filter components by $F_{1},F_{2},F_{3}$ with ports $f_{i}.in$ and $f_{i}.out$ for $i\in I$, respectively. Similarly, we let $J=\{1,2,3,4\}$ and denote the four pipe components by $P_{1},P_{2},P_{3},P_{4}$ with ports $p_{j}.in$ and $p_{j}.out$ for $j\in J$, respectively. Hence, the set $P$ of all ports is determined by $P=\{f_{i}.in,f_{i}.out,p_{j}.in,p_{j}.out,\mid i\in I,\ j\in J\}$. For every $i\in I$ and $j\in J$ we shall denote by $k_{ij}\in K$ the weight of the interaction among the ports $f_{i}.in$ and $p_{j}.out$. Similarly, for every $i\in I$ and $j\in J$ the weight of the interaction between the ports $f_{i}.out$ and $p_{j}.in$ is denoted by $k_{ij}^{\prime}\in K.$ The wPCL formula that formalizes the interactions between input ports of filters and output ports of pipes with the corresponding weights is

[TABLE]

whereas the wPCL formula

[TABLE]

describes the interactions and their weights among output ports of filters and input ports of pipes. Furthermore, we need to ensure that the output of a pipe can be connected to at most one input of a filter, and that the pipes can be connected only with filters and vice-versa. These requirements are satisfied respectively, by the following PCL formulas:

[TABLE]

We conclude to the wPCL formula

[TABLE]

for the weighted Pipes and Filters architecture for four pipes and three filters.

Example 17** (Weighted Publish/Subscribe architecture)**

Publish/Subscribe* is a software architecture, relating publishers who send messages, and receivers called subscribers (cf. for instance [7, 11]). The main characteristics of this architecture are as follows. The publishers characterize messages according to classes/topics but they do not know whether there is any subscriber who is interested in a concrete topic. Subscribers, on the other hand, express their interest in one or more topics and receive all messages published to the topics to which they subscribe. All subscribers which are subscribed to a topic will receive the same messages in case such messages exist (Figure 4). A main problem in Publish/Subscribe architecture refers to the priority according to which a topic receives messages from the publishers as well as the priority according to which a subscriber receives messages from several topics (cf. for instance [2, 3, 18]). Recent applications in IoT framework as well as in cloud platforms incorporate Publish/Subscribe architecture (cf. for instance [13, 15, 17]).*

In the sequel, we develop a wPCL formula for the Publish/Subscribe architecture where, according to the semiring used, the weights represent in a natural way the aforementioned priorities. More precisely, we assign weights, describing priorities, to interactions among publishers and topics, and to interactions among topics and subscribers. We consider three types of components namely, publishers, topics, and subscribers denoted by the letters $P,T,S$, respectively. Component $P$ has one port $p$, $T$ has two ports $t_{1}$ and $t_{2}$, and $S$ has the port $s$.

In our example we assume two publisher components $P_{1},P_{2}$ with ports $p_{1},p_{2}$ respectively, four subscriber components $S_{1},S_{2},S_{3},S_{4}$ with ports $s_{1},s_{2},s_{3},s_{4}$ respectively, and three topic components $T_{1},T_{2},T_{3}$ with sets of ports $\{t_{11},t_{12}\}$, $\{t_{21},t_{22}\}$, and $\{t_{31},t_{32}\}$ respectively. Therefore, the set $P$ of all ports is given by $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\in\{1,2,3,4\}$, $j\in\{1,2,3\}$, and $l\in\{1,2\}$ we denote by $k_{ij}\in K$ 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 $w_{lj}\in K$ the weight of the interaction among $P_{l}$ and $T_{j}$, i.e., the priority that the topic $T_{j}$ assigns to the receivement of a message from $P_{l}$. The PIL formula for the interaction between a publisher $P_{l}$ and a topic $T_{j}$, for every $l\in\{1,2\}$ and $j\in\{1,2,3\}$, is given by $\phi_{pt}(p_{l},t_{j1})=m_{\{p_{l},t_{j1}\}}$ and the wPIL formula characterizing this interaction with its corresponding weight is determined by $\varphi_{pt}(p_{l},t_{j1})=w_{lj}\otimes\phi_{pt}(p_{l},t_{j1}).$ Hence, the wPCL formula

[TABLE]

for $j\in\{1,2,3\}$, describes the weighted interactions of the topic $T_{j}$ with the publishers $P_{1}$ and $P_{2}$ and thus

[TABLE]

refers to the weighted part of the Publish/Subscribe architecture among the concrete topic $T_{j}$ and the publishers $P_{1}$ and $P_{2}$.

Next we build wPCL formulas for the description of the interactions among subscribers and topics. More precisely, for every $i\in\{1,2,3,4\}$ and $j\in\{1,2,3\}$, the PIL formula $\phi_{st}(s_{i},t_{j2})=m_{\{s_{i},t_{j2}\}}$ describes the interaction between the subscriber $S_{i}$ and the topic $T_{j}$, and the wPIL formula $\varphi_{st}(s_{i},t_{j2})=k_{ij}\otimes\phi_{st}(s_{i},t_{j2})$ formalizes this interaction with its corresponding weight. Then, the wPCL formula

[TABLE]

characterizes the weighted interactions of subscriber $S_{i}$ with topics $T_{1}$, $T_{2}$, and $T_{3}$.

Finally, for every $i\in\{1,2,3,4\}$, we consider the wPCL formula

[TABLE]

which describes the behavior of subscriber $S_{i}$ with publishers $P_{1},P_{2}$ and topics $T_{1},T_{2},T_{3}$.

For instance, let us consider the subscriber $S_{1}$, the set of interactions

[TABLE]

and $K=\mathbb{R}_{\max}$. Then, the value $\left\|\zeta^{(tp)}_{s_{1}}\right\|(\gamma)$ represents the maximum priority with which the subscriber $S_{1}$ will receive a message. Similarly, for $K=\mathbb{R}_{\min}$, the value $\left\|\zeta^{(tp)}_{s_{1}}\right\|(\gamma)$ corresponds to the minimum priority with which $S_{1}$ receives a message, whereas if $K$ is the Viterbi semiring, it assigns the maximum probability for the receivement of the topics by $S_{1}$.

5 A full normal form for wPCL formulas

In the present section, we show that for every wPCL formula $\zeta$ over $P$ and $K$ we can effectively compute an equivalent formula of a special form. For this, we will use a corresponding result from [12], namely for every PCL formula $f$ over $P$ we can effectively construct a unique equivalent PCL formula of the form $\mathrm{true}$444This trivial case is not considered in [12] but we refer to this in order to show the correspondence with wPCL formulas $k$ for $k\in K$. or $\bigsqcup\nolimits_{i\in I}\sum\nolimits_{i\in J_{i}}m_{i,j}$ which is called *full normal form *(cf. Theorem 4.43. in [12]). The index sets $I$ and $J_{i}$, for every $i\in I$, are finite and $m_{i,j}$’s are full monomials, i.e., monomials of the form $\bigwedge_{p\in P_{+}}p\wedge\bigwedge_{p\in P\_}\overline{p}$ with $P_{+}\cup P\_=P$ and $P_{+}\cap P\_=\emptyset$. Here we firstly prove that the worst case run time for the construction of the full normal form is doubly exponential, whereas the best case is exponential. Then we show that we can effectively build a unique full normal form for every wPCL formula $\zeta\in PCL(K,P)$ . Uniqueness is up to the equivalence relation, and interestingly our algorithm requires the same time complexity as the corresponding one in the boolean case. Then we will use our translation result to show that the equivalence problem for wPCL formulas is decidable.

We start with the subsequent theorem which states the complexity of the construction of full normal forms for PCL formulas.

Theorem 18

Let $P$ be a set of ports. Then, for every PCL formula $f$ over $P$ we can effectively construct, in doubly exponential time, an equivalent PCL formula $f^{\prime}$ in full normal form. The best run time for the construction of $f^{\prime}$ is exponential. Furthermore, $f^{\prime}$ is unique up to equivalence relation.

Proof. The construction of $f^{\prime}$ and its uniqueness has been proved in Theorem 4.43. in [12]. Therefore, we only deal with the complexity result. For this we recall, from [12], the transformations applied to $f$ for the construction of $f^{\prime}$. More precisely, firstly the following rewriting rules are applied for the construction of a PCL formula $f^{\prime\prime}$ in normal form which is equivalent to $f$:

[TABLE]

[TABLE]

[TABLE]

Then, every non-full monomial $m$ in $f^{\prime\prime}$ is transformed into a disjunction of full monomials. This is done in exponential time, since all the subsets of the set $\overline{P}_{m}=P\setminus\{p\in P\mid p\text{ or }\overline{p}\text{ occurs in }m\}$ are computed. Then using the rewriting rule

[TABLE]

every disjunction of full monomials is transformed into a union of coalesced full monomials. Trivially, the application of the last rewriting rule on the derived disjunctions of full monomials needs again exponential time. Therefore, the application of the above rewriting rules requires at most doubly exponential time. This implies that the worst case run time for the computation of $f^{\prime}$ is doubly exponential. On the other hand, if every monomial $m$ in $f^{\prime\prime}$ above is already full, then obviously the best run time for the computation of $f^{\prime}$ is exponential, and this concludes our proof.

Next we introduce the notion of full normal form for wPCL formulas.

Definition 19

*A wPCL formula $\zeta\in PCL(K,P)$ is said to be in *full normal form if either

• •

$\zeta=k$* with $k\in K$, or*

• •

there are finite index sets $I$ and $J_{i}$ for every $i\in I$, $k_{i}\in K$ for every $i\in I$, and full monomials $m_{i,j}$ for every $i\in I$ and $j\in J_{i}$ such that $\zeta=\bigoplus_{i\in I}\left(k_{i}\otimes\sum_{j\in J_{i}}m_{i,j}\right)$.

By our definition above, for every full normal form we can construct an equivalent one satisfying the following statements:

• i)

$j\neq j^{\prime}$ implies $m_{i,j}\not\equiv m_{i,j^{\prime}}$ for every $i\in I$, $j,j^{\prime}\in J_{i}$, and

• ii)

$i\neq i^{\prime}$ implies $\sum_{j\in J_{i}}m_{i,j}\not\equiv\sum_{j\in J_{i^{\prime}}}m_{i^{\prime},j}$ for every $i,i^{\prime}\in I$.

Indeed, for the first one, if $m_{i,j}\equiv m_{i,j^{\prime}}$ for some $j\neq j^{\prime}$, then since $m_{i,j},m_{i,j^{\prime}}$ are interaction formulas, by Proposition 5(i), we can replace the coalescing $m_{i,j}+m_{i,j^{\prime}}$ with $m_{i,j}$. For (ii), let us assume that $\sum_{j\in J_{i}}m_{i,j}\equiv\sum_{j\in J_{i^{\prime}}}m_{i^{\prime},j}$ for some $i\neq i^{\prime}$. Then, we can replace the sum $\left(k_{i}\otimes\sum_{j\in J_{i}}m_{i,j}\right)\oplus\left(k_{i^{\prime}}\otimes\sum_{j\in J_{i^{\prime}}}m_{i^{\prime},j}\right)$ with the equivalent one $\left(k_{i}\oplus k_{i^{\prime}}\right)\otimes\sum_{j\in J_{i}}m_{i,j}$. Hence, in the sequel, we assume that every full normal form satisfies Statements (i) and (ii).

We intend to show that for every wPCL formula $\zeta\in PCL(K,P)$ we can effectively construct an equivalent wPCL formula $\zeta^{\prime}\in PCL(K,P)$ in full normal form. Moreover, $\zeta^{\prime}$ will be unique up to the equivalence relation555Since wPCL formulas are defined syntactically, we get for instance $\zeta_{1}\uplus\zeta_{2}\neq\zeta_{2}\uplus\zeta_{1}$ whereas $\zeta_{1}\uplus\zeta_{2}\equiv\zeta_{2}\uplus\zeta_{1}$.. We shall need a sequence of preliminary results. All index sets occurring in the sequel are finite.

Lemma 20

Let $k_{1},k_{2}\in K$ and $\zeta_{1},\zeta_{2}\in PCL(K,P)$. Then

[TABLE]

Proof. For every $\gamma\in C(P)$ we have

[TABLE]

where the first equivalence holds by commutativity of $K$.

Lemma 21

Let $J$ be an index set and $m_{j}$ a full monomial for every $j\in J$. Then, there exists a unique $\overline{\gamma}\in C(P)$ such that for every $\gamma\in C(P)$ we have $\left\|\sum\nolimits_{j\in J}m_{j}\right\|(\gamma)=1$ if $\gamma=\overline{\gamma}$ and $\left\|\sum\nolimits_{j\in J}m_{j}\right\|(\gamma)=0$ otherwise.

Proof. For every $m_{j}$, $j\in J$, there exists a unique interaction $a_{j}$ such that $a_{j}\models_{i}m_{j}$. Then, it is straightforward to show that $\overline{\gamma}=\{a_{j}\mid j\in J\}$ satisfies our claim.

Proposition 22

Let $f$ be a $PCL$ formula over $P$. 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

[TABLE]

Proof. By Theorem 4.43. in [12] there exists a unique full normal form such that $f\equiv\bigsqcup_{i\in I}\sum_{j\in J_{i}}m_{i,j}$ where $m_{i,j}$ are full monomials. Using similar arguments as the ones after Definition 19 we can assume, without any loss, that the full normal form satisfies Statements (i) and (ii).  By Lemma 21, for every $i\in I$ there exists a unique $\overline{\gamma}_{i}\in C(P)$ such that for every $\gamma\in C(P)$ we have $\left\|\sum_{j\in J_{i}}m_{i,j}\right\|(\gamma)=1$ if $\gamma=\overline{\gamma}_{i}$ and $\left\|\sum_{j\in J_{i}}m_{i,j}\right\|(\gamma)=0$ otherwise. Then we have

[TABLE]

for every $\gamma\in C(P)$, where the last but one equality holds by Statement (ii). Hence we get $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)$ and we are done.

Lemma 23

Let $m_{i},m_{j}^{\prime}$ be full monomials for every $i\in I$ and $j\in J$. Then

[TABLE]

Proof. By Lemma 21 there exist $\overline{\gamma},\overline{\gamma}^{\prime}\in C(P)$ such that for every $\gamma\in C(P)$ we have $\left\|\sum\nolimits_{i\in I}m_{i}\right\|(\gamma)=1$ if $\gamma=\overline{\gamma}$ and $\left\|\sum\nolimits_{i\in I}m_{i}\right\|(\gamma)=0$ otherwise, and $\left\|\sum\nolimits_{j\in J}m_{j}^{\prime}\right\|(\gamma)=1$ if $\gamma=\overline{\gamma}^{\prime}$ and $\left\|\sum\nolimits_{j\in J}m_{j}^{\prime}\right\|(\gamma)=0$ otherwise. Therefore, for every $\gamma\in C(P)$ we get

[TABLE]

which concludes our claim.

Lemma 24

Let $m_{i},m_{j}^{\prime}$ be full monomials for every $i\in I$ and $j\in J$. If $m_{i}\equiv m^{\prime}_{j}$ for some $i\in I$ and $j\in J$, then

[TABLE]

Proof. By Lemma 21 there exist $\overline{\gamma},\overline{\gamma}^{\prime}\in C(P)$ such that for every $\gamma\in C(P)$ we have $\left\|\sum\nolimits_{i\in I}m_{i}\right\|(\gamma)=1$ if $\gamma=\overline{\gamma}$ and $\left\|\sum\nolimits_{i\in I}m_{i}\right\|(\gamma)=0$ otherwise, and $\left\|\sum\nolimits_{j\in J}m_{j}^{\prime}\right\|(\gamma)=1$ if $\gamma=\overline{\gamma}^{\prime}$ and $\left\|\sum\nolimits_{j\in J}m_{j}^{\prime}\right\|(\gamma)=0$ otherwise. Therefore, if $\overline{\gamma}\cap\overline{\gamma}^{\prime}\neq\emptyset$, then by definition of the coalescing operator on wPCL formulas, we get

[TABLE]

for every $\gamma\in C(P)$, and this concludes our claim.

Theorem 25

Let $K$ be a commutative semiring and $P$ a set of ports. Then, for every wPCL formula $\zeta\in PCL(K,P)$ we can effectively construct an equivalent wPCL formula $\zeta^{\prime}\in PCL(K,P)$ in full normal form which is unique up to the equivalence relation. The worst case run time for the construction algorithm is doubly exponential and the best case is exponential.

Proof. We prove our theorem by induction on the structure of wPCL formulas $\zeta$ over $P$ and $K$. If $\zeta=k$ with $k\in K$, then we have nothing to prove. Though, we shall need to use instead the equivalent full normal form $\zeta^{\prime}=\bigoplus_{\emptyset\not=N\subseteq M}\left(k\otimes\sum_{m\in N}m\right)$ where $M$ is the set of all full monomials over $P$ such that for every $m,m^{\prime}\in M$ if $m\neq m^{\prime}$, then $m\not\equiv m^{\prime}$. Next let $\zeta=f$ be a PCL formula. Then, we conclude our claim by Proposition 22.

Assume now that $\zeta_{1},\zeta_{2}\in PCL(K,P)$ and let $\zeta_{1}^{\prime}=\bigoplus_{i_{1}\in I_{1}}\left(k_{i_{1}}\otimes\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\right)$ and $\zeta_{2}^{\prime}=\bigoplus_{i_{2}\in I_{2}}\left(k_{i_{2}}\otimes\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}\right)$ be their equivalent full normal forms, respectively.

Let firstly $\zeta=\zeta_{1}\oplus\zeta_{2}$ and assume that not both of $\zeta_{1}$, $\zeta_{2}$ are constants in $K$. We consider the formula $\zeta_{1}^{\prime}\oplus\zeta_{2}^{\prime}$. If $\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\not\equiv\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}$ for every $i_{1}\in I_{1}$ and $i_{2}\in I_{2}$, then we set $\zeta^{\prime}=\zeta_{1}^{\prime}\oplus\zeta_{2}^{\prime}$. If this is not the case, let us assume that $\sum_{j_{1}\in J_{i_{1}^{\prime}}}m_{i_{1}^{\prime},j_{1}}\equiv\sum_{j_{2}\in J_{i_{2}^{\prime}}}m_{i_{2}^{\prime},j_{2}}$ for some $i_{1}^{\prime}\in I_{1}$ and $i_{2}^{\prime}\in I_{2}$. Then we have

[TABLE]

We continue in the same way, and we conclude to a full normal form $\zeta^{\prime}$, which, by construction, it is equivalent to $\zeta$.

If $\zeta=k_{1}$ and $\zeta_{2}=k_{2}$ with $k_{1},k_{2}\in K$, then we let $\zeta^{\prime}=k_{1}\oplus k_{2}$.

Next let $\zeta=\zeta_{1}\otimes\zeta_{2}$ and assume that neither $\zeta_{1}$ nor $\zeta_{2}$ is a constant in $K$. We set

$\xi=\bigoplus_{i_{1}\in I_{1}}\bigoplus_{i_{2}\in I_{2}}\left(k_{i_{1}}\otimes k_{i_{2}}\otimes\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\otimes\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}\right)$ and we have

[TABLE]

where the second equivalence follows by the distributivity property of $K$.

Now, we translate $\xi$ to an equivalent full normal form $\zeta^{\prime}$ as follows. By Lemma 23, for every $i_{1}\in I_{1}$, $i_{2}\in I_{2}$, we get $\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\otimes\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}\equiv\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}$ if $\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\equiv\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}$, and $\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\otimes\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}\equiv 0$ otherwise. Hence, in the first case we replace $\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\otimes\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}$ by $\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}$, whereas in the second case by [math]. Obviously, $\zeta^{\prime}$ is the required full normal form.

If $\zeta_{1}=k$ (resp. $\zeta_{2}=k$) with $k\in K$, then we set $\zeta^{\prime}=\bigoplus_{i_{2}\in I_{2}}\left(k\otimes k_{i_{2}}\otimes\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}\right)$ (resp. $\zeta^{\prime}=\bigoplus_{i_{1}\in I_{1}}\left(k\otimes k_{i_{1}}\otimes\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\right)$. If $\zeta=k_{1}$ and $\zeta_{2}=k_{2}$ with $k_{1},k_{2}\in K$, then we let $\zeta^{\prime}=k_{1}\otimes k_{2}$.

Finally let $\zeta=\zeta_{1}\uplus\zeta_{2}$. We set

$\zeta^{\prime}=\bigoplus_{i_{1}\in I_{1}}\bigoplus_{i_{2}\in I_{2}}\left(k^{\prime}_{i_{1}}\otimes k^{\prime}_{i_{2}}\otimes\left(\left(\sum_{j_{1}\in J_{i_{1}}}m_{i_{1},j_{1}}\right)+\left(\sum_{j_{2}\in J_{i_{2}}}m_{i_{2},j_{2}}\right)\right)\right)$ where $k^{\prime}_{i_{1}}$ and $k^{\prime}_{i_{2}}$ are defined for every $i_{1}\in I_{1}$ and $i_{2}\in I_{2}$ respectively, as follows. If $m_{i_{1},j_{1}}\not\equiv m_{i_{2},j_{2}}$ for every $j_{1}\in J_{i_{1}}$ and $j_{2}\in J_{i_{2}}$, then we set $k^{\prime}_{i_{1}}=k_{i_{1}}$ and $k^{\prime}_{i_{2}}=k_{i_{2}}$, otherwise we let $k^{\prime}_{i_{1}}=k^{\prime}_{i_{2}}=0$. Then we get

[TABLE]

where the first equivalence holds by definition of $k^{\prime}_{i_{1}}$ ($i_{1}\in I_{1}$) and $k^{\prime}_{i_{2}}$ ($i_{2}\in I_{2}$) and Lemma 24. The second equivalence follows by Lemma 20, and the third and fourth ones by Proposition 12(iv). By definition of $k^{\prime}_{i_{1}}$ for every $i_{1}\in I_{1}$ and $k^{\prime}_{i_{2}}$ for every $i_{2}\in I_{2}$, we conclude that $\zeta^{\prime}$ is the required full normal form satisfying Statements (i) and (ii).

Therefore, we have shown that for every $\zeta\in PCL(K,P)$ we can construct an equivalent $\zeta^{\prime}\in PCL(K,P)$ in full normal form. The uniqueness of $\zeta^{\prime}$, up to equivalence, is derived in a straightforward way using Statements (i) and (ii). It remains to prove our claim for the time complexity of the above presented algorithm for the construction of $\zeta^{\prime}$. We should note that the input of the algorithm consists of the set $P$ of ports and the wPCL formula $\zeta$. If $\zeta=k$ with $k\in K$, and $\zeta$ is involved in an $\oplus$ or $\uplus$ operation, then we use the full normal form $\zeta^{\prime}=\bigoplus_{\emptyset\not=N\subseteq M}\left(k\otimes\sum_{m\in N}m\right)$. The computation of $\zeta^{\prime}$ requires a doubly exponential time since we compute firstly the set $M$ all full monomials over $P$ and then all nonempty subsets of $M$. If $\zeta=f$ is a PCL formula, then we conclude our claim by Theorem 18 and Proposition 22. Next, by preserving the notations from the first part of our proof, for the induction steps for $\oplus$, $\otimes$, and $\uplus$ operations, we note that the construction of $\zeta^{\prime}$ by $\zeta_{1}^{\prime}$ and $\zeta^{\prime}_{2}$ is polynomial in every case.

Next we show that the equivalence problem for wPCL formulas is decidable in doubly exponential time.

Theorem 26

Let $K$ be a commutative semiring and $P$ a set of ports. Then, for every $\zeta,\xi\in PCL(K,P)$ the equality $\|\zeta\|=\|\xi\|$ is decidable in doubly exponential time.

Proof. By Theorem 25 we can effectively construct, in doubly exponential time, wPCL formulas $\zeta^{\prime},\xi^{\prime}$ in full normal form such that $\|\zeta\|=\|\zeta^{\prime}\|$ and $\|\xi\|=\|\xi^{\prime}\|$. Let us assume that $\zeta^{\prime}=\bigoplus_{i\in I}\left(k_{i}\otimes\sum_{j\in J_{i}}m_{i,j}\right)$ and $\xi^{\prime}=\bigoplus_{l\in L}\left(k^{\prime}_{l}\otimes\sum_{r\in M_{l}}m^{\prime}_{l,r}\right)$ which moreover satisfy Statements (i) and (ii). Then, by Statement (ii) we get that $\|\zeta^{\prime}\|=\|\xi^{\prime}\|$ iff the following requirements (1)-(3) hold:

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

• 2)

$\{k_{i}\mid i\in I\}=\{k^{\prime}_{l}\mid l\in L\}$, and

• 3)

• a)

if $\mathrm{card}(I)=\mathrm{card}(\{k_{i}\mid i\in I\})$, then $\sum_{j\in J_{i}}m_{i,j}\equiv\sum_{r\in M_{l}}m^{\prime}_{l,r}$ for every $i\in I$ and $l\in L$ such that $k_{i}=k^{\prime}_{l}$,

• or
• b)

if $\mathrm{card}(I)>\mathrm{card}(\{k_{i}\mid i\in I\})$, then we get $\zeta^{\prime}\equiv\bigoplus_{i^{\prime}\in I^{\prime}}\left(k_{i^{\prime}}\otimes\bigsqcup_{i\in R_{i^{\prime}}}\sum_{j\in J_{i}}m_{i,j}\right)$ where $I^{\prime}\varsubsetneq I$, $k_{i^{\prime}}$’s ($i^{\prime}\in I^{\prime}$) are pairwise disjoint, and $R_{i^{\prime}}$ ($i^{\prime}\in I^{\prime}$) is the set of all $i$ in $I$ such that $k_{i}=k_{i^{\prime}}$. Similarly, we get $\xi^{\prime}\equiv\bigoplus_{l^{\prime}\in L^{\prime}}\left(k^{\prime}_{l^{\prime}}\otimes\bigsqcup_{l\in S_{l^{\prime}}}\sum_{r\in M_{l}}m^{\prime}_{l,r}\right)$ where $L^{\prime}\varsubsetneq L$, $k^{\prime}_{l^{\prime}}$’s ($l^{\prime}\in L^{\prime}$) are pairwise disjoint, and $S_{l^{\prime}}$ ($l^{\prime}\in L^{\prime}$) is the set of all $l$ in $L$ such that $k^{\prime}_{l}=k^{\prime}_{l^{\prime}}$. Then $\bigsqcup_{i\in R_{i^{\prime}}}\sum_{j\in J_{i}}m_{i,j}\equiv\bigsqcup_{l\in S_{l^{\prime}}}\sum_{r\in M_{l}}m^{\prime}_{l,r}$ for every $i^{\prime}\in I^{\prime}$ and $l^{\prime}\in L^{\prime}$ such that $k_{i^{\prime}}=k^{\prime}_{l^{\prime}}$.

By Lemma 21 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. All the aforementioned full monomials, and hence their corresponding interaction sets, have been computed in the process of the construction of full normal forms $\zeta^{\prime}$ and $\xi^{\prime}$ (cf. the proof of Theorem 25). Therefore, the decidability for the required equalities and equivalences in (1)-(3) above requires at most polynomial time, and our proof is completed.

In the last part of this section, we wish to show that wPCL is sound. For this, we need firstly to introduce the notion of soundness in the setting of wPCL. According to our best knowledge soundness has been defined only for multi-valued logics, with values in the bounded distributive lattice $[0,1]$ with the usual $\mathrm{max}$ and $\mathrm{min}$ operations (cf. [10]). Let $\zeta\in PCL(K,P)$ and $\Sigma=\{\zeta_{1},\ldots,\zeta_{n}\}$ with $\zeta_{1},\ldots,\zeta_{n}\in PCL(K,P)$. We say that $\Sigma$ proves $\zeta$ and write $\Sigma\vdash\zeta$ if $\zeta$ is derived from the formulas in $\Sigma$, using the axioms of PCL (cf. page 17 in [12]) and the equivalences of Propositions 12 and 13. Furthermore, we write $\Sigma\models\zeta$ iff for every $\gamma\in\bigcap_{1\leq i\leq n}\mathrm{supp}(\zeta_{i})$ such that $\left\|\zeta_{1}\right\|(\gamma)=\ldots=\left\|\zeta_{n}\right\|(\gamma)$, then $\left\|\zeta\right\|(\gamma)=\left\|\zeta_{1}\right\|(\gamma)$. Then, we say that wPCL is sound if $\Sigma\vdash\zeta$ implies $\Sigma\models\zeta$. In particular, if $f_{1},\ldots,f_{n},f$ are PCL formulas over $P$, then we write $\{f_{1},\ldots,f_{n}\}\vdash f$ if $f$ is derived from formulas in $\{f_{1},\ldots,f_{n}\}$ using the axioms of PCL (cf. page 17 in [12]). Similarly, we write $\{f_{1},\ldots,f_{n}\}\models f$ if for every $\gamma\in C(P)$ we get $\gamma\models f$ whenever $\gamma\models f_{i}$ for every $1\leq i\leq n$.

Theorem 27

Let $K$ be a commutative semiring and $P$ a set of ports. Then the wPCL over $P$ and $K$ is sound.

Proof. If $\Sigma$ is a set of PCL formulas and $f$ a PCL formula over $P$, then $\Sigma\vdash f$ implies $\Sigma\models f$ holds true since PCL is sound (cf. [12]). If $\Sigma$ is a set of wPCL formulas and $\zeta$ a wPCL formula in $PCL(K,P)$ such that $\Sigma\vdash\zeta$, then we get $\Sigma\models\zeta$ by Definition 8 and Propositions 12 and 13. Therefore, wPCL is sound, and we are done.

Discussion

• a)

In our definition of interactions (cf. page 3) over a set $P$ of ports we excluded, following [12], the empty interaction as well as the empty set of interactions. Though the empty interaction adds no value in single architectures, it plays an important role in architectural composition (cf. for instance [1, 4]). More precisely, the empty set of interactions represents in a strict mathematical way the case where two architectures cannot be composed. It represents also a deadlock state of a component-based system. Nevertheless, we consider no empty interactions in wPCL because of the following reason. Our wPCL is based on PCL of [12] where the authors also consider no empty interactions. Clearly the empty interaction satifies only the PIL formula $\mathrm{false}$. By adding the empty interaction in PCL of [12] several properties do not hold any more. For instance the equivalences $f+\mathrm{false}\equiv\mathrm{false}$ (Proposition 4.4 in [12]) for $f\not\equiv\mathrm{false}$ and $\sim f_{1}+\sim f_{2}\equiv\sim f_{1}\wedge\sim f_{2}$ (Proposition 4.27(2) in [12]) for $f_{1}\not\equiv\mathrm{false}$ and $f_{2}\equiv\mathrm{false}$. Specifically, the first one is used in the computation of the full normal form of a PCL formula (for instance in proof of Proposition 4.19 and in turn in proof of Proposition 4.35 in [12]). We conjecture that one can rebuilt the theory of PCL and of our wPCL by considering the empty interaction, but of course this is beyond the scope of this paper.

• b)

In Theorem 25 we proved that for every wPCL formula $\zeta\in PCL(K,P)$ we can effectively construct an equivalent one $\zeta^{\prime}$ in full normal form, i.e., $\zeta^{\prime}=\bigoplus_{i\in I}\left(k_{i}\otimes\sum_{j\in J_{i}}m_{i,j}\right)$. Furthermore, we used this result to prove decidability of equivalence of wPCL formulas. However our method arises the following question: Why should one follow the technical constructions of Theorem 25 and not consider the “obvious” construction of full formal form as $\zeta^{\prime\prime}=\bigoplus_{\gamma\in C(P)}\left(\left\|\zeta\right\|(\gamma)\otimes\sum_{a\in\gamma}m_{a}\right)$. As we have shown in Theorem 25 the worst case run time for the computation of $\zeta^{\prime}$ is doubly exponential. On the other hand, the construction of $\zeta^{\prime\prime}$ requires “always” doubly exponential time since it computes all $\gamma\in C(P)$. From the application point of view it is desirable to compute full normal forms in an automatic way [12], and for this, the above difference for the time needed for $\zeta^{\prime}$ and $\zeta^{\prime\prime}$ is of great importance. Following the methodology of [12], we developed a code in Maude 2.7.1 rewriting system [19] for the computation of full normal forms of weighted Master/Slave and Publish/Subscribe architectures. The left diagram in Figure 5 presents the time needed for the construction of full normal forms of these architectures for several numbers of components. The right one shows the time needed to compute $C(P)$ for several numbers of $\mathrm{card}(P)$. One can easily see that the time required to compute $C(P)$ for $\mathrm{card}(P)=4$ is greater than the the time required to compute the full normal form of weighted Master/Slave architecture with 6 Masters and 6 Slaves (i.e., 12 ports in total), and it is the same with the time needed to compute the full normal of weighted Publish/Subscribe architecture with 5 Subscribers, 4 Publishers and 3 Topics (i.e., 12 ports in total). Our code run on a 64-bit Linux machine with a 2.10 GHz Intel i3-2310M CPU and 1 Gb memory limit.

Conclusion

We introduced a wPCL over a set of ports $P$ and a commutative semiring $K$ and investigated several properties of the class of polynomials obtained as semantics of this logic. For some of that properties we required our semiring to be idempotent. In our wPCL we slightly modified the coalescing operation in comparison to its boolean counterpart. Definitely, this modification is not an essential restriction since every architecture described in the boolean setup is described as well in our weighted setup, as we showed in our examples. We proved that for every wPCL formula $\zeta$ we can effectively construct, in doubly exponential time, an equivalent one $\zeta^{\prime}$ in full normal form. This result implied the decidability of the equivalence problem for wPCL formulas. We defined a notion of soundness for wPCL and proved that it is sound. It should be noted that though PCL is proved to be complete [12], for wPCL trivially this is not the case, at least with our definitions of $\vdash$ and $\models$. It is an open problem whether we can develop the theory of this paper by relaxing the commutativity property of the semiring $K$ and thus obtaining our results for a larger class of semirings. Furthermore, it should be very interesting to investigate the wPCL over more general weight structures which can describe further properties like average, limit inferior, limit superior, and discounting (cf. for instance [6]). Work on progress investigates the first- and second-order levels of weighted configuration logics which are motivated by applications to architecture styles with quantitative characteristics.

Acknowledgements. We should like to express our gratitude to Joseph Sifakis, Simon Bliudze, and Anastasia Mavridou for useful discussions and clarifications on [12]. We are also grateful to two anonymous reviewers for pointing out a mistake and fruitful suggestions which helped us to improve the presentation of the paper.