Modelling architectures of parametric weighted component-based systems

TL;DR

This paper introduces a weighted first-order logic for modeling parametric software architectures with quantitative aspects, proving its decidability and demonstrating its effectiveness in describing known architectures.

Contribution

It presents a novel weighted logic framework for parametric architectures, with decidability results and practical modeling capabilities.

Findings

Decidability of the logic's equivalence problem in skew fields

Efficient description of known parametric architectures

A new formalism for quantitative architecture modeling

Abstract

The design of complex software systems usually lies in multiple coordinating components with an unknown number of instances. For such systems a main challenge is modelling efficiently their architecture that determines the topology and the interaction principles among the components. To achieve well-founded design there is need to address the quantitative aspects of software architectures. In this paper we study the modelling problem of software architectures applied on parametric weighted component-based systems where the parameter is the number of instances of each component. For this, we introduce a weighted first-order extended interaction logic over a commutative semiring in order to serve as a modelling language for parametric quantitative architectures. We prove that the equivalence problem of formulas of that logic is decidable in the class (of subsemirings) of skew fields. Moreover, we show that our weighted logic can efficiently describe well-known parametric architectures with quantitative characteristics.

Equations

$$w\text{shuffle}u=\{w_1{u}_1\dots w_m{u}_m\mid w_1,\dots ,w_m,u_1,\dots ,u_m\in A^{\ast }\text{ and }w=w_1\dots w_m,u=u_1\dots u_m\}.$$

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

$$\zeta$$

$$\phi$$

$$I_{\mathcal{B}}=\left\{a\in I(P_{\mathcal{B}})\mid |a\cap P(i)|\le 1\text{ for every }i\in [n]\right\}.$$

$$\tilde{\phi }::=k\mid \phi \mid {\tilde{\phi }}_1\oplus {\tilde{\phi }}_2\mid {\tilde{\phi }}_1\otimes {\tilde{\phi }}_2\mid {\tilde{\phi }}_1\odot {\tilde{\phi }}_2\mid {\tilde{\phi }}_1\varpi {\tilde{\phi }}_2$$

$${\tilde{\varphi }}_a$$

$$\equiv (wt(j_1)(p_{j_1})\otimes \dots \otimes wt(j_m)(p_{j_m}))\otimes (p_{j_1}\otimes \dots \otimes p_{j_m})$$

$$\equiv (wt(j_1)(p_{j_1})\otimes \dots \otimes wt(j_m)(p_{j_m}))\otimes (p_{j_1}\wedge \dots \wedge p_{j_m})$$

$$\#(p_{i_1}\wedge \dots \wedge p_{i_m})::=p_{i_1}\wedge \dots \wedge p_{i_m}\wedge \underset{p\in P\setminus \{p_{i_1},\dots ,p_{i_m}\}}{\bigwedge }\neg p.$$

$${\#}_w(p_{i_1}\otimes \dots \otimes p_{i_m})::=(k_{i_1}\otimes p_{i_1})\otimes \dots \otimes (k_{i_m}\otimes p_{i_m})\otimes \underset{p\in P\setminus \{p_{i_1},\dots ,p_{i_m}\}}{\bigwedge }\neg p.$$

$${\#}_w(p_{i_1}\otimes \dots \otimes p_{i_m})$$

$$\displaystyle\equiv(k_{i_{1}}\otimes\ldots\otimes k_{i_{m}})\otimes\bigg{(}(p_{i_{1}}\wedge\ldots\wedge p_{i_{m}})\wedge\bigwedge_{p\in P\setminus\{p_{i_{1}},\ldots,p_{i_{m}}\}}\neg p\bigg{)}$$

$$=(k_{i_1}\otimes \dots \otimes k_{i_m})\otimes \#(p_{i_1}\wedge \dots \wedge p_{i_m}).$$

$${\tilde{\varphi}}=\#_{w}(p_{d}\otimes p_{r})\odot\bigg{(}\#_{w}(p_{d}\otimes p_{n_{1}})\varpi\#_{w}(p_{d}\otimes p_{n_{2}})\varpi\#_{w}(p_{d}\otimes p_{n_{3}})\bigg{)}\odot\\ \bigg{(}{\tilde{\varphi}}_{1}\oplus{\tilde{\varphi}}_{2}\oplus{\tilde{\varphi}}_{3}\oplus({\tilde{\varphi}}_{1}\varpi{\tilde{\varphi}}_{2})\oplus({\tilde{\varphi}}_{1}\varpi{\tilde{\varphi}}_{3})\oplus({\tilde{\varphi}}_{2}\varpi{\tilde{\varphi}}_{3})\oplus({\tilde{\varphi}}_{1}\varpi{\tilde{\varphi}}_{2}\varpi{\tilde{\varphi}}_{3})\bigg{)}$$

$${\tilde{\phi }}_i={\#}_w(p_l\otimes p_{t_i})\odot {\#}_w(p_e\otimes p_{w_i}\otimes p_a)$$

$${\tilde{\varphi}}=\big{(}\#_{w}(p_{e}\otimes p_{r_{1}})\varpi\#_{w}(p_{e}\otimes p_{r_{2}})\big{)}\odot\big{(}{\tilde{\xi}}_{1}\varpi{\tilde{\xi}}_{2}\big{)}\odot\\ \Bigg{(}\bigg{(}{\tilde{\varphi}}_{11}\oplus{\tilde{\varphi}}_{21}\oplus({\tilde{\varphi}}_{11}\odot{\tilde{\varphi}}_{21})\oplus({\tilde{\varphi}}_{21}\odot{\tilde{\varphi}}_{11})\bigg{)}\bigoplus\bigg{(}{\tilde{\varphi}}_{12}\oplus{\tilde{\varphi}}_{22}\oplus({\tilde{\varphi}}_{12}\odot{\tilde{\varphi}}_{22})\oplus({\tilde{\varphi}}_{22}\odot{\tilde{\varphi}}_{12})\bigg{)}\bigoplus\\ \bigg{(}\big{(}{\tilde{\varphi}}_{11}\oplus{\tilde{\varphi}}_{21}\oplus({\tilde{\varphi}}_{11}\odot{\tilde{\varphi}}_{21})\oplus({\tilde{\varphi}}_{21}\odot{\tilde{\varphi}}_{11})\big{)}\varpi\\ \big{(}{\tilde{\varphi}}_{12}\oplus{\tilde{\varphi}}_{22}\oplus({\tilde{\varphi}}_{12}\odot{\tilde{\varphi}}_{22})\oplus({\tilde{\varphi}}_{22}\odot{\tilde{\varphi}}_{12})\big{)}\bigg{)}\Bigg{)}$$

$${\tilde{\varphi}}_{1}=\bigg{(}\big{(}{\tilde{\xi}}_{1}\odot{\tilde{\varphi}}_{11}\big{)}\oplus\big{(}{\tilde{\xi}}_{1}\odot{\tilde{\varphi}}_{12}\big{)}\oplus\big{(}{\tilde{\xi}}_{1}\odot{\tilde{\varphi}}_{13}\big{)}\oplus\\ \big{(}{\tilde{\xi}}_{1}\odot({\tilde{\varphi}}_{11}\varpi{\tilde{\varphi}}_{12})\big{)}\oplus\big{(}{\tilde{\xi}}_{1}\odot({\tilde{\varphi}}_{11}\varpi{\tilde{\varphi}}_{13})\big{)}\oplus\\ \big{(}{\tilde{\xi}}_{1}\odot({\tilde{\varphi}}_{12}\varpi{\tilde{\varphi}}_{13})\big{)}\oplus\big{(}{\tilde{\xi}}_{1}\odot({\tilde{\varphi}}_{11}\varpi{\tilde{\varphi}}_{12}\varpi{\tilde{\varphi}}_{13})\big{)}\bigg{)}$$

$${\tilde{\varphi}}_{2}=\bigg{(}\big{(}{\tilde{\xi}}_{2}\odot{\tilde{\varphi}}_{21}\big{)}\oplus\big{(}{\tilde{\xi}}_{2}\odot{\tilde{\varphi}}_{22}\big{)}\oplus\big{(}{\tilde{\xi}}_{2}\odot{\tilde{\varphi}}_{23}\big{)}\oplus\\ \big{(}{\tilde{\xi}}_{2}\odot({\tilde{\varphi}}_{21}\varpi{\tilde{\varphi}}_{22})\big{)}\oplus\big{(}{\tilde{\xi}}_{2}\odot({\tilde{\varphi}}_{21}\varpi{\tilde{\varphi}}_{23})\big{)}\oplus\\ \big{(}{\tilde{\xi}}_{2}\odot({\tilde{\varphi}}_{22}\varpi{\tilde{\varphi}}_{23})\big{)}\oplus\big{(}{\tilde{\xi}}_{2}\odot({\tilde{\varphi}}_{21}\varpi{\tilde{\varphi}}_{22}\varpi{\tilde{\varphi}}_{23})\big{)}\bigg{)}$$

$$\begin{gathered} \psi ::=\phi \mid x^{(i)}=y^{(i)}\mid \neg (x^{(i)}=y^{(i)})\mid \psi \vee \psi \mid \psi \wedge \psi \mid \psi \ast \psi \mid \psi \text{shuffle}\psi \mid \\ \exists x^{(i)}.\psi \mid \forall x^{(i)}.\psi \mid {\exists }^{\ast }{x}^{(i)}.\psi \mid {\forall }^{\ast }{x}^{(i)}.\psi \mid {\exists }^{\text{shuffle}}{x}^{(i)}.\psi \mid {\forall }^{\text{shuffle}}{x}^{(i)}.\psi \end{gathered}$$

$$\begin{gathered} \tilde{\psi }::=k\mid \psi \mid \tilde{\psi }\oplus \tilde{\psi }\mid \tilde{\psi }\otimes \tilde{\psi }\mid \tilde{\psi }\odot \tilde{\psi }\mid \tilde{\psi }\varpi \tilde{\psi }\mid \sum x^{(i)}.\tilde{\psi }\mid \prod x^{(i)}.\tilde{\psi }\mid \\ \sum {}^{\odot }{x}^{(i)}.\tilde{\psi }\mid \prod {}^{\odot }{x}^{(i)}.\tilde{\psi }\mid \sum {}^{\varpi }{x}^{(i)}.\tilde{\psi }\mid \prod {}^{\varpi }{x}^{(i)}.\tilde{\psi } \end{gathered}$$

$$\#_{w}\big{(}p_{i_{1}}(x^{(i_{1})})\otimes\ldots\otimes p_{i_{m}}(x^{(i_{m})})\big{)}::=\big{(}(k_{i_{1}}\otimes p_{i_{1}}(x^{(i_{1})}))\otimes\ldots\otimes(k_{i_{m}}\otimes p_{i_{m}}(x^{(i_{m})}))\big{)}\otimes\\ \bigg{(}\bigg{(}\bigwedge_{j=i_{1},\ldots,i_{m}}\bigwedge_{p\in P(j)\setminus\{p_{j}\}}\neg p(x^{(j)})\bigg{)}\wedge\bigg{(}\bigwedge_{j=i_{1},\ldots,i_{m}}\forall y^{(j)}(y^{(j)}\neq x^{(j)}).\bigwedge_{p\in P(j)}\neg p(y^{(j)})\bigg{)}\wedge\\ \bigg{(}\bigwedge_{t\in[n]\setminus\{i_{1},\ldots,i_{m}\}}\bigwedge_{p\in P(t)}\forall x^{(t)}.\neg p(x^{(t)})\bigg{)}\bigg{)}.$$

$$\#_{w}\big{(}p_{i_{1}}(x^{(i_{1})})\otimes\ldots\otimes p_{i_{m}}(x^{(i_{m})})\big{)}\equiv\big{(}k_{i_{1}}\otimes\ldots\otimes k_{i_{m}}\big{)}\otimes\bigg{(}\big{(}p_{i_{1}}(x^{(i_{1})})\wedge\ldots\wedge p_{i_{m}}(x^{(i_{m})})\big{)}\\ \wedge\bigg{(}\bigwedge_{j=i_{1},\ldots,i_{m}}\bigwedge_{p\in P(j)\setminus\{p_{j}\}}\neg p(x^{(j)})\bigg{)}\wedge\bigg{(}\bigwedge_{j=i_{1},\ldots,i_{m}}\forall y^{(j)}(y^{(j)}\neq x^{(j)}).\bigwedge_{p\in P(j)}\neg p(y^{(j)})\bigg{)}\wedge\\ \bigg{(}\bigwedge_{t\in[n]\setminus\{i_{1},\ldots,i_{m}\}}\bigwedge_{p\in P(t)}\forall x^{(t)}.\neg p(x^{(t)})\bigg{)}\bigg{)}.$$

$$\tilde{\psi }=\prod {}^{\odot }{x}^{(2)}\sum x^{(1)}.{\#}_w(p_m(x^{(1)})\otimes p_s(x^{(2)})).$$

$$\tilde{\psi }=\sum x^{(1)}\prod {}^{\odot }{y}^{(1)}(x^{(1)}\ne y^{(1)}).{\#}_w(p(x^{(1)})\otimes p(y^{(1)})).$$

$${\tilde{\psi}}={\textstyle\prod\nolimits{{}^{\odot}}x^{(2)}}{\textstyle\sum x^{(1)}}{\textstyle\sum y^{(1)}}(x^{(1)}\neq y^{(1)}).\bigg{(}\#_{w}(p_{o}(x^{(1)})\otimes f_{e}(x^{(2)}))\odot\#_{w}(p_{e}(y^{(1)})\otimes f_{o}(x^{(2)}))\bigg{)}\bigotimes\\ \qquad\quad\bigg{(}\forall z^{(1)}\forall y^{(2)}\bigg{(}\forall z^{(2)}(y^{(2)}\neq z^{(2)}).\big{(}\big{(}\mathrm{true}*(p_{o}(z^{(1)})\wedge f_{e}(y^{(2)}))*\mathrm{true}\big{)}\wedge\\ \qquad\qquad\qquad\big{(}\neg\big{(}\mathrm{true}*(p_{o}(z^{(1)})\wedge f_{e}(z^{(2)}))*\mathrm{true}\big{)}\big{)}\big{)}\bigg{)}\vee\bigg{(}\neg\big{(}\mathrm{true}*(p_{o}(z^{(1)})\wedge f_{e}(y^{(2)}))*\mathrm{true}\big{)}\bigg{)}\bigg{)}.$$

$$\tilde{\psi }=\sum x^{(1)}\prod {}^{\odot }{x}^{(2)}.{\#}_w(p_r(x^{(1)})\otimes p_d(x^{(2)})).$$

$${\tilde{\psi}}={\textstyle\sum x^{(1)}}{\textstyle\sum x^{(2)}}.\bigg{(}\#_{w}(p_{d}(x^{(1)})\otimes p_{r}(x^{(2)}))\odot\bigg{(}{\textstyle\prod^{\varpi}x^{(3)}}.\#_{w}(p_{d}(x^{(1)})\otimes p_{n}(x^{(3)}))\bigg{)}\odot\\ \bigg{(}{\textstyle\sum^{\varpi}y^{(3)}}.\big{(}\#_{w}(p_{l}(x^{(2)})\otimes p_{t}(y^{(3)}))\odot\#_{w}(p_{e}(x^{(2)})\otimes p_{w}(y^{(3)})\otimes p_{a}(x^{(1)}))\big{)}\bigg{)}\bigg{)}.$$

$${\tilde{\psi}}=\bigg{(}{\textstyle\sum x^{(1)}}.\bigg{(}\big{(}{\textstyle\prod^{\varpi}x^{(2)}}.\#_{w}(p_{e}(x^{(1)})\otimes p_{r}(x^{(2)}))\big{)}\odot\\ \big{(}{\textstyle\prod^{\varpi}x^{(3)}}.(\#_{w}(p_{l}(x^{(3)})\otimes p_{u}(x^{(1)}))\odot\#_{w}(p_{o}(x^{(3)})\otimes p_{t}(x^{(1)})))\big{)}\bigg{)}\bigg{)}\odot\\ \bigg{(}{\textstyle\sum^{\varpi}y^{(2)}}{\textstyle\sum x^{(4)}}{\textstyle\sum^{\odot}y^{(3)}}.{\tilde{\xi}}\otimes\bigg{(}\forall y^{(4)}\forall z^{(3)}\forall z^{(2)}.\big{(}\theta\vee\big{(}\forall t^{(3)}\forall t^{(2)}(z^{(2)}\neq t^{(2)}).\theta^{\prime}\big{)}\big{)}\bigg{)}\bigg{)}$$

$${\tilde{\psi}}={\textstyle\sum^{\varpi}x^{(2)}}.\Bigg{(}\bigg{(}{\textstyle\sum^{\varpi}x^{(1)}}.\big{(}\#_{w}(p_{a}(x^{(1)})\otimes p_{n}(x^{(2)}))\odot\#_{w}(p_{t}(x^{(1)})\otimes p_{r}(x^{(2)}))\big{)}\bigg{)}\odot\\ \bigg{(}{\textstyle\sum^{\varpi}x^{(3)}}.\big{(}\#_{w}(p_{e}(x^{(3)})\otimes p_{c}(x^{(2)}))\odot\#_{w}(p_{g}(x^{(3)})\otimes p_{s}(x^{(2)}))\odot\#_{w}(p_{d}(x^{(3)})\otimes p_{f}(x^{(2)}))\big{)}\bigg{)}\Bigg{)}.$$

Full text

Keywords: Architecture modelling. Parametric weighted component-based systems. Weighted first-order extended interaction logic.

1 Introduction

One of the key challenges in software systems’ design is the specification of their architecture. Software architectures depict design principles applied to systems in order to characterize the communication rules and the underlying topology [37, 48]. In such a setting systems’ modelling is mainly component-based where the development lies in the coordination of multiple system components [7, 53]. Therefore, as the systems grow large and complex, architectures become important in the design process since they enforce systems to meet most of their requirements by construction. On the other hand, well-founded design involves not only the qualitative features but also the non-functional aspects of the systems [31, 39], and hence of their architectures [41, 49]. Qualitative modelling cannot capture the timing constraints, available resources, energy consumption, etc., for executing the interactions of a system’s architecture. Such optimization and performance aspects require the study of architectures in the quantitative setting.

In this paper we study architectures by a weighted first-order interaction logic. We consider architectures applied on a wide class of component-based systems, namely parametric weighted systems. Parametric systems consist of a finite number of component types with an unknown number of instances [4, 8]. Such systems are found in several applications including cyber-physical systems [35, 51], as well as distributed algorithms and communication protocols [1, 8, 17, 21]. Quantitative analysis is important for parametric architectures for handling communication issues like ‘the battery waste for a particular interaction is’ in a system with restricted power autonomy like sensor networks or ‘the required time for completing the interactions among specific components is’ in time-critical network protocols.

According to our best knowledge a logical directed description of parametric quantitative architectures, using weighted first-order configuration logic, has been only considered in [41] (cf. Section 2). The current paper extends the results of our recent work for modelling parametric architectures [44], in the quantitative setup. Specifically, in this work we model parametric systems by a classical weighted model, namely weighted labelled transition system. The communication is achieved by the labels, called ports, and is defined by interactions, i.e., sets of ports. Each port is associated with a weight that represents the ‘cost’ of its participation in an interaction. The weights of the ports range over the common algebraic structure of a commutative semiring $K$. We formalize parametric quantitative architectures by weighted logic formulas over $K$. Similarly to the work of [44], our weighted logic has the additional attribute of respecting the execution order of the interactions as imposed by each architecture, a main feature of several important architectures found in applications. In particular, the contributions of this work are the following.

(1) We introduce weighted Extended Propositional Interaction Logic (wEPIL for short) over a finite set of ports, and a commutative semiring $K$ for representing the weights. wEPIL extends weighted Propositional Interaction Logic (wPIL for short) from [41, 42] with two new weighted operators, namely the weighted concatenation operator $\odot$ and weighted shuffle operator $\varpi$. Intuitively these two operators allow us to encode the weights of consecutive and interleaving interactions in weighted component-based systems, respectively. We interpret wEPIL formulas as series defined over finite words and $K$. The letters of the words are interactions over the given set of ports. Clearly, the semantics of wEPIL formulas differs from the ones of wPIL formulas. The latter is interpreted over series from sets of interactions, whereas the first one over series of words of interactions, both with values in $K$.

(2) We apply wEPIL formulas for modelling the architectures of weighted component-based systems with ordered interactions, and specifically, we consider the architectures Blackboard [15], Request/Response [16], and Publish/Subscribe [22]. For different instantiations of the semiring $K$ we derive alternative interpretations for the resulting total cost of the allowed interactions, that corresponds to some quantitative characteristic.

(3) We introduce the first-order level of wEPIL, namely weighted First-Order Extended Interaction Logic (wFOEIL for short). The syntax of wFOEIL is equipped with the syntax of wEPIL, the weighted existential and universal quantifiers (similar weighted quantifiers introduced firstly for weighted MSO logics in [18]), and four new weighted quantifiers, namely the weighted existential and universal concatenation and shuffle quantifiers. The weighted existential and universal concatenation (resp. shuffle) quantifiers serve to compute the weight of the partial and whole participation of the instances of a weighted component type in sequentially (resp. interleaving) executed interactions. For the semantics of wFOEIL we consider triples consisting of a mapping defining the number of component instances in the parametric weighted system, an assignment that attributes a unique identifier to ports of each component instance, and a finite word of interactions. Then, we interpret wFOEIL formulas as series from triples of the previous form to elements in $K$.

(4) We show that wFOEIL serves sufficiently for modelling interactions of parametric weighted component-based systems. Specifically, we provide examples of wFOEIL formulas for modelling the quantitative properties of concrete parametric architectures including Master/Slave [37], Star [37], Repository [14], and Pipes/Filters [24] where interactions are executed arbitrarily, as well as for the Blackboard, Request/Response, and Publish/Subscribe architectures.

(5) We prove the decidability of equivalence of wFOEIL formulas in doubly-exponential time provided that the weight structure is (a subesemiring of) a skew field. For this, we follow a methodology similar to the one considered in [44], and establish a doubly exponential translation of wFOEIL formulas to weighted automata. Then, we apply well-known decidability and complexity results for weighted automata over (subsemirings of) skew fields.

The structure of the paper is as follows. In Section $2$ we refer to related work and compare our results with the existing ones found in literature. In Section 3 we recall the notions of weighted component-based systems and weighted interactions. Then, in Section 4 we define the syntax and semantics of wEPIL and present examples of component-based systems whose architectures are defined by wEPIL formulas. In Section $5$ we introduce the syntax and semantics of our wFOEIL and provide examples of wFOEIL sentences for modelling specific architectures of parametric weighted component-based systems. Section $5$ studies the decidability results for wFOEIL sentences. Finally, in Conclusion, we discuss future work directions.

2 Related work

Existing work has recently investigated the architecture modelling problem of parametric systems mainly in the qualitative setting. In particular, in [37] the authors introduced a Propositional Configuration Logic (PCL for short) as a modelling language for the description of architectures. They considered also first- and second-order configuration logic applied for modelling parametric architectures (called styles of architectures in that paper). PCL which is interpreted over sets of interactions has a nice property, namely for every PCL formula one can efficiently construct an equivalent one in a special form called full normal form. This implies the decidability of equivalence of PCL formulas in an automated way using the Maude language.

The weighted version of PCL over commutative semirings was studied in [41, 42]. Soundness was proved for that logic and the authors obtained the decidability for the equivalence problem of its formulas. Weighted PCL was applied for modelling the quantitative aspects of several common architectures. In [29] the authors extended the work of [41, 42] and studied weighted PCL over a product valuation monoid. That algebraic structure allows to compute the average cost as well as the maximum cost among all costs occurring most frequently for executing the interactions within architectures. The authors applied that logic to model several weighted software architectures and proved that the equivalence problem of its formulas is decidable. In contrast to our setting, the work of [29, 37, 41, 42] describes architectures with PCL which though encodes no execution order of the interactions. Parametric weighted architectures were considered only in [41] using the weighted first-order level of weighted PCL, namely weighted FOCL. Nevertheless, weighted FOCL considers no execution order of the interactions of parametric weighted architectures.

In [30] a first-order interaction logic (FOIL for short) was introduced to describe finitely many interactions, for parametric systems modelled in BIP framework. FOIL was applied for modelling classical architectures of parametric systems (such as Ring and Star) and considered in model checking results. In [9] the authors introduced an alternative logic, namely monadic interaction logic (MIL for short) to describe rendezvous and broadcast communication of parametric component-based systems, and also presented a method for detecting deadlocks for these systems. Next, an interaction logic with one successor (IL1S for short) was developed in [10] as a modelling language for architectures of parametric component-based systems. A method for checking deadlock freeness and mutual exclusion of parametric systems was also studied.

Recently we introduced an extended propositional interaction logic (EPIL for short) and its first-order level, namely first-order extended interaction logic (FOEIL for short) [44]. FOEIL was applied for modelling well-known architectures of parametric component-based systems defined by labelled transition systems, and we proved the decidability of equivalence, satisfiability and validity of FOEIL sentences. In comparison to logics of [9, 10, 30, 37], FOEIL not only described the permissible interactions characterizing each architecture, but also encoded the execution order of implementing the interactions, an important feature of several architectures including Publish/Subscribe and Request/Response.

Multiparty session types described efficiently communication protocols and their interactions patterns (cf. for instance [26, 28]). A novel session type system and an associated programming language were introduced in [12] for the description of multi-actor communication in parameterized protocols. The system modelled global types with exclusive and concurrent events as well as their arbitrary reorderings using a shuffling operator, and used for static verification of asynchronous communication protocols. Though no architectures of systems were considered in [12, 26, 28]. In [17] the authors introduced a type theory for multiparty sessions to globally specify parameterized communication protocols whose processes carry data. They also developed decidable projection methods of parameterised global types to local ones and proved type safety and deadlock freedom for well-typed parameterized processes. The framework of [17] did not address the sequential and interleaving interactions of processes.

Some work for quantitative parametric systems was considered in [5, 6, 21, 23]. In [21] the authors studied population protocols, a specific class of parametric systems, modelled by labelled transition systems with Markov chains semantics. Then, a decidability result was obtained for the model checking problem of population protocols against linear-time specifi- cations while undecidability was proved for the corresponding probabilistic properties. The work of [21] does not consider though the systems’ architecture in the design process. In [6, 23] the authors considered broadcast communication and cliques topology for networks of many identical probabilistic timed processes, where the number of processes was a parameter. Then, they investigated the decidability results of several qualitative parameterized verification problems for probabilistic timed protocols. In the subsequent work [5] the authors extended broadcast protocols and parametric timed automata and introduced a model of parametric timed broadcast protocols with two different types of parameters, namely the number of identical processes and the timing features. The decidability of parametric decision problems were also studied for parametric timed broadcast protocols in [5]. In contrast to our framework, the topologies of the protocols studied in the above works, are not formalized by means of weighted logics. Moreover, we investigate the modelling problem of several more complicated quantitative parameteric architectures than those considered in [5, 6, 23].

The motivation to study parametric systems with quantitative features is also depicted in the recent work of [27, 33]. In [33] the authors studied fair termination for parameterized probabilistic concurrent systems modelled by Markov decision processes. They extended the symbolic framework of regular model checking for verifying parameterized concurrent systems in the probabilistic setting. The authors developed a fully-automatic method that was applied for distributed algorithms and systems in evolutionary biology. Moreover, the work of [27] studied the equivalence problem for probabilistic parameterized systems using bisimulations. For this, the first-order theory of universal automatic structures was extended to a probabilistic setup for developing a decidable automatic method for verifying probabilistic bisimulation for parameterized systems. Then, the framework was applied for studying the anonymity property for the dining cryptographers and grades parameterized protocols. Although the works of [27, 33] apply their verification results on parametric protocols with ring or linear topologies, they do not focus on the investigation of a formal modelling framework for quantitative parametric architectures.

3 Preliminaries

3.1 Notations

For every natural number $n\geq 1$ we denote by $[n]$ the set $\{1,\ldots,n\}$. Hence, in the sequel, whenever we use the notation $[n]$ we always assume that $n\geq 1$. For every set $S$ we denote by $\mathcal{P}(S)$ the powerset of $S$. Let $A$ be an alphabet, i.e., a finite nonempty set. As usual we denote by $A^{*}$ the set of all finite words over $A$ and let $A^{+}=A^{*}\setminus\{\varepsilon\}$ where $\varepsilon$ denotes the empty word. Given two words $w,u\in A^{*}$, the shuffle product $w\shuffle u$ of $w$ and $u$ is a language over $A$ defined by

[TABLE]

3.2 Semirings

A semiring $(K,+,\cdot,0,1)$* *consists of a set $K,$ two binary operations $+$ and $\cdot$ and two constant elements [math] and $1$ such that $(K,+,0)$ is a commutative monoid, $(K,\cdot,1)$ is a monoid, multiplication $\cdot$ distributes over addition $+$, and $0\cdot k=k\cdot 0=0$ for every $k\in K$. If the monoid $(K,\cdot,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$. If no confusion arises, we denote sometimes in the sequel the multiplication operation $\cdot$ just by juxtaposition. The following algebraic structures are well-known commutative semirings.

• •

The semiring $(\mathbb{N},+,\cdot,0,1)$ of natural numbers,

• •

the semiring $(\mathbb{Q},+,\cdot,0,1)$ of rational numbers,

• •

the semiring $(\mathbb{R},+,\cdot,0,1)$ of real numbers,

• •

the Boolean semiring $B=(\{0,1\},+,\cdot,0,1)$,

• •

the arctical or max-plus semiring $\mathbb{R}_{\max}=(\mathbb{R}_{+}\cup\{-\infty\},\max,+,-\infty,0)$ where $\mathbb{R}_{+}=\{r\in\mathbb{R}\mid r\geq 0\}$,

• •

the tropical or min-plus semiring $\mathbb{R}_{\min}=(\mathbb{R}_{+}\cup\{\infty\},\min,+,\infty,0)$,

• •

the Viterbi semiring $(\left[0,1\right],\max,\cdot,0,1)$ used in probability theory,

• •

every bounded distributive lattice with the operations $\sup$ and $\inf$, in particular the fuzzy semiring $F=([0,1],\max,\min,0,1)$.

A semiring $(K,+,\cdot,0,1)$ is called a skew field if the $(K,+,0)$ and $(K\setminus\{0\},\cdot,1)$ are groups. For instance, $(\mathbb{Q},+,\cdot,0,1)$ and $(\mathbb{R},+,\cdot,0,1)$ are skew fields, and more generally every field is a skew field.

A formal series (or simply series) over $A^{*}$ and $K$ is a mapping $s:A^{*}\rightarrow K$. The support of $s$ is the set $\mathrm{supp}(s)=\{w\in A^{*}\mid s(w)\neq 0\}$. A series with finite support is called a polynomial. The constant series $\widetilde{k}$ ($k\in K$) is defined, for every $w\in A^{*}$,  by $\widetilde{k}(w)=k$. We denote by $K\left\langle\left\langle A^{*}\right\rangle\right\rangle$ the class of all series over $A^{*}$ and $K$, and by $K\left\langle A^{*}\right\rangle$ the class of all polynomials over $A^{*}$ and $K$. Let $s,r\in K\left\langle\left\langle A^{*}\right\rangle\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 series in $K\left\langle\left\langle A^{*}\right\rangle\right\rangle$ and defined elementwise, respectively by $s\oplus r(w)=s(w)+r(w),(ks)(w)=k\cdot s(w),(sk)(w)=s(w)\cdot k,s\otimes r(w)=s(w)\cdot r(w)$ for every $w\in A^{*}$. It is a folklore result that the structure $\left(K\left\langle\left\langle A^{*}\right\rangle\right\rangle,\oplus,\otimes,\widetilde{0},\widetilde{1}\right)$ is a semiring. Moreover, if $K$ is commutative, then $\left(K\left\langle\left\langle A^{*}\right\rangle\right\rangle\oplus,\otimes,\widetilde{0},\widetilde{1}\right)$ is also commutative. The *Cauchy product *$s\odot r\in K\left\langle\left\langle A^{\ast}\right\rangle\right\rangle$ is determined by $s\odot r(w)=\sum\nolimits_{w=w_{1}w_{2}}s(w_{1})r(w_{2})$ for every $w\in A^{\ast}$, whereas the shuffle product $s\varpi r\in K\left\langle\left\langle A^{\ast}\right\rangle\right\rangle$ is defined by $s\varpi r(w)=\sum\nolimits_{w\in w_{1}\shuffle w_{2}}s(w_{1})r(w_{2})$ for every $w\in A^{\ast}$.

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

3.3 Extended propositional interaction logic

In this subsection we recall from [44] the extended propositional interaction logic. With that logic, we succeeded to describe the order of execution of interactions required by specific architectures. We need to recall firstly propositional interaction logic (PIL for short) (cf. [9, 10, 37]).

Let $P$ be a finite nonempty set of ports. We let $I(P)=\mathcal{P}(P)\setminus\{\emptyset\}$ for the set of interactions over $P$. Then, the syntax of PIL formulas $\phi$ over $P$ is given by the grammar

[TABLE]

where $p\in P$.

We set $\neg(\neg\phi)=\phi$ for every PIL formula $\phi$ and $\mathrm{false}=\neg\mathrm{true}$. As usual the conjunction and the implication of two PIL formulas $\phi,\phi^{\prime}$ over $P$ are defined respectively, by $\phi\wedge\phi^{\prime}:=\neg{\left(\neg\phi\vee\neg\phi^{\prime}\right)}$ and $\phi\rightarrow\phi^{\prime}:=\neg\phi\vee\phi^{\prime}$. PIL formulas are interpreted over interactions in $I(P)$. More precisely, for every PIL formula $\phi$ and $a\in I(P)$ we define the satisfaction relation $a\models_{\mathrm{PIL}}\phi$ by induction on the structure of $\phi$ as follows:

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

• -

$a\models_{\mathrm{PIL}}p$   iff    $p\in a$,

• -

$a\models_{\mathrm{PIL}}\neg\phi$   iff   $a\not\models_{\mathrm{PIL}}\phi$,

• -

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

Two PIL formulas $\phi,\phi^{\prime}$ are called equivalent, and we denote it by $\phi\equiv\phi^{\prime}$, whenever $a\models\phi$ iff $a\models\phi^{\prime}$ for every $a\in I(P)$. A PIL formula $\phi$ is called a monomial over $P$ if it is of the form $p_{1}\wedge\ldots\wedge p_{l}$, where $l\geq 1$ and $p_{\lambda}\in P$ or $p_{\lambda}=\neg p^{\prime}_{\lambda}$ with $p^{\prime}_{\lambda}\in P$, for every $\lambda\in[l]$. For every interaction $a=\{p_{1},\ldots,p_{l}\}\in I(P)$ we consider the monomial $\phi_{a}=p_{1}\wedge\ldots\wedge p_{l}$. Then, it trivially holds $a\models_{\mathrm{PIL}}\phi_{a}$, and for every $a,a^{\prime}\in I(P)$ we get $a=a^{\prime}$ iff $\phi_{a}\equiv\phi_{a^{\prime}}$.

Next we recall the extended propositional interaction logic (EPIL for short) (cf. [44]). Let $P$ be a finite set of ports. The syntax of EPIL formulas $\varphi$ over $P$ is given by the grammar

[TABLE]

where $\phi$ is a PIL formula over $P$, $*$ is the concatenation operator, and $\shuffle$ is the shuffle operator.

The binding strength, in decreasing order, of the operators in EPIL is the following: negation, shuffle, concatenation, conjunction, and disjunction. The reader should notice that we consider a restricted use of negation in the syntax of EPIL formulas. Specifically, negation is permitted in PIL formulas and EPIL formulas of type $\zeta$. The latter ensures exclusion of erroneous interactions in architectures. The restricted use of negation has no impact to description of models characterized by EPIL formulas since most of known architectures can be described by sentences in our EPIL. Furthermore, it contributed to a reasonable complexity of translation of first-order extended interaction logic formulas to finite automata. This in turn implied the decidability of equivalence, satisfiability, and validity of first-order extended interaction logic sentences (cf. [44]).

For the satisfaction of EPIL formulas we consider finite words $w$ over $I(P)$. Intuitively, a word $w$ encodes each of the distinct interactions within a system as a letter. Moreover, the position of each letter in $w$ depicts the order in which the corresponding interaction is executed in the system, in case there is an order restriction.

Definition 1

Let $\varphi$ be an EPIL formula over $P$ and $w\in I(P)^{*}$. If $w=\varepsilon$ and $\varphi=\mathrm{true}$, then we set $w\models\mathrm{true}$. If $w\in I(P)^{+}$, then we define the satisfaction relation $w\models\varphi$ by induction on the structure of $\varphi$ as follows:

$w\models\phi$*   iff   $w\models_{\mathrm{PIL}}\phi$,*

• -

$w\models\zeta_{1}*\zeta_{2}$*   iff   there exist $w_{1},w_{2}\in I(P)^{*}$ such that $w=w_{1}w_{2}$ and $w_{i}\models\zeta_{i}$ for $i=1,2$,*

• -

$w\models\neg\zeta$*   iff   $w\not\models\zeta$,*

• -

$w\models\varphi_{1}\vee\varphi_{2}$*   iff   $w\models\varphi_{1}$ or $w\models\varphi_{2}$,*

• -

$w\models\varphi_{1}\wedge\varphi_{2}$*   iff   $w\models\varphi_{1}$ and $w\models\varphi_{2}$,*

• -

$w\models\varphi_{1}*\varphi_{2}$*   iff   there exist $w_{1},w_{2}\in I(P)^{*}$ such that $w=w_{1}w_{2}$ and $w_{i}\models\varphi_{i}$ for $i=1,2$,*

• -

$w\models\varphi_{1}\shuffle\varphi_{2}$*   iff   there exist $w_{1},w_{2}\in I(P)^{*}$ such that $w\in w_{1}\shuffle w_{2}$ and $w_{i}\models\varphi_{i}$ for $i=1,2$.*

If $\varphi=\phi$ is a PIL formula, then $w\models\phi$ implies that $w$ is a letter in $I(P)$. Two EPIL formulas $\varphi,\varphi^{\prime}$ are called equivalent, and we denote it by $\varphi\equiv\varphi^{\prime}$, whenever $w\models\varphi$ iff $w\models\varphi^{\prime}$ for every $w\in I(P)^{*}$.

3.4 Component-based systems

We recall the concept of component-based systems which are comprised of a finite number of components of the same or different type. In our set up, components are defined by labelled transition systems (LTS for short) like in several well-known component-based modelling frameworks including BIP [7, 52], REO [3], X-MAN [25], and B [2]. We use the terminology of BIP framework for the basic notions and definitions, though we focus only on the communication patterns of components building a component-based system. Communication among components is achieved through their corresponding interfaces. For an LTS, its interface is the associated set of labels, called ports. Then, communication of components is defined by interactions, i.e., sets of ports, or equivalently by PIL formulas. In [44] we replaced PIL formulas by EPIL formulas. Hence, we succeeded to describe the execution order of interactions required by the underlying architecture of every component-based system.

Definition 2

An atomic component is an LTS $B=(Q,P,q_{0},R)$ where $Q$ is a finite set of states, $P$ is a finite set of ports, $q_{0}$ is the initial state and $R\subseteq Q\times P\times Q$ is the set of transitions.

For simplicity we assume that every port in $P$ occurs in at most one transition in $R$. This simplification has been also considered by other authors (cf. for instance [9, 10]). In the sequel, we call an atomic component $B$ a component, whenever we deal with several atomic components. For every set $\mathcal{B}=\{B(i)\mid i\in[n]\}$ of components, with $B(i)=(Q(i),P(i),q_{0}(i),R(i))$, $i\in[n]$, we consider in the paper, we assume that $(Q(i)\cup P(i))\cap(Q(i^{\prime})\cup P(i^{\prime}))=\emptyset$ for every $1\leq i\neq i^{\prime}\leq n$.

Let $\mathcal{B}=\{B(i)\mid i\in[n]\}$ be a set of components. We let $P_{\mathcal{B}}=\bigcup_{i\in[n]}P(i)$ comprising all ports of the elements of $\mathcal{B}$. Then an interaction of ${\mathcal{B}}$ is an interaction $a\in I(P_{\mathcal{B}})$ such that $|a\cap P(i)|\leq 1$, for every $i\in[n]$. If $p\in a$, then we say that $p$ is active in $a$. We denote by $I_{\mathcal{B}}$ the set of all interactions of $\mathcal{B}$, i.e.,

[TABLE]

Definition 3

A component-based system is a pair $({\mathcal{B}},\varphi)$ where ${\mathcal{B}}=\{B(i)\mid i\in[n]\}$ is a set of components, with $B(i)=(Q(i),P(i),q_{0}(i),R(i))$ for every $i\in[n]$, and $\varphi$ is an EPIL formula over $P_{{\mathcal{B}}}$.

In the above definition the EPIL formula $\varphi$ is defined over the set of ports $P_{{\mathcal{B}}}$ and is interpreted over words in $I_{{\mathcal{B}}}^{*}$.

4 Weighted EPIL and component-based systems

In this section, we introduce the notion of weighted EPIL over a set of ports $P$ and the semiring $K$. Furthermore, we define weighted component-based systems and provide examples of architectures with quantitative characteristics.

Definition 4

Let $P$ be a finite set of ports. Then the syntax of weighted EPIL (wEPIL for short) formulas over $P$ and $K$ is given by the grammar

[TABLE]

where $k\in K$, $\varphi$ is an EPIL formula over $P$, and $\oplus$, $\otimes$, $\odot$, and $\varpi$ are the weighted disjunction, conjunction, concatenation, and shuffle operator, respectively.

If $\tilde{\varphi}$ is composed by elements in $K$ and PIL formulas connected with $\oplus$ and $\otimes$ operators only, then it is called also a weighted PIL (wPIL for short) formula over $P$ and $K$ [41, 42] and it will be denoted also by $\tilde{\phi}$.

For the semantics of wEPIL formulas we consider finite words $w$ over $I(P)$ and interpret wEPIL formulas as series in $K\left\langle\left\langle I(P)^{*}\right\rangle\right\rangle$.

Definition 5

Let ${\tilde{\varphi}}$ be a wEPIL formula over $P$ and $K$. The semantics of ${\tilde{\varphi}}$ is a series $\left\|{\tilde{\varphi}}\right\|\in K\left\langle\left\langle I(P)^{*}\right\rangle\right\rangle$. For every $w\in I(P)^{*}$ the value $\left\|{\tilde{\varphi}}\right\|(w)$ is defined inductively on the structure of ${\tilde{\varphi}}$ as follows:

$\left\|k\right\|(w)=k$,

• -

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

• -

$\left\|{\tilde{\varphi}}_{1}\oplus{\tilde{\varphi}}_{2}\right\|(w)=\left\|{\tilde{\varphi}}_{1}\right\|(w)+\left\|{\tilde{\varphi}}_{2}\right\|(w)$,

• -

$\left\|{\tilde{\varphi}}_{1}\otimes{\tilde{\varphi}}_{2}\right\|(w)=\left\|{\tilde{\varphi}}_{1}\right\|(w)\cdot\left\|{\tilde{\varphi}}_{2}\right\|(w)$,

• -

$\left\|{\tilde{\varphi}}_{1}\odot{\tilde{\varphi}}_{2}\right\|(w)=\sum\limits_{w=w_{1}w_{2}}(\left\|{\tilde{\varphi}}_{1}\right\|(w_{1})\cdot\left\|{\tilde{\varphi}}_{2}\right\|(w_{2}))$,

• -

$\left\|{\tilde{\varphi}}_{1}\varpi{\tilde{\varphi}}_{2}\right\|(w)=\sum\limits_{w\in w_{1}\shuffle w_{2}}(\left\|{\tilde{\varphi}}_{1}\right\|(w_{1})\cdot\left\|{\tilde{\varphi}}_{2}\right\|(w_{2}))$.

Next we define weighted component-based systems. For this, we introduce the notion of a weighted atomic component.

Definition 6

A weighted atomic component over $K$ is a pair $wB=(B,wt)$ where $B=(Q,P,q_{0},R)$ is an atomic component and $wt:R\rightarrow K$ is a weight mapping.

Since every port in $P$ occurs in at most one transition in $R$, we consider, in the sequel, $wt$ as a mapping $wt:P\rightarrow K$. If a port $p\in P$ occurs in no transition, then we set $wt(p)=0$.

We call a weighted atomic component $wB$ over $K$ a weighted component, whenever we deal with several weighted atomic components and the semiring $K$ is understood. Let $w{\mathcal{B}}=\{wB(i)\mid i\in[n]\}$ be a set of weighted components where $wB(i)=(B(i),wt(i))$ with $B(i)=(Q(i),P(i),q_{0}(i),R(i))$ for every $i\in[n]$. The set of ports and the set of interactions of $w{\mathcal{B}}$ are the sets $P_{\mathcal{B}}$ and $I_{\mathcal{B}}$ respectively, of the underlying set of components ${\mathcal{B}}=\{B(i)\mid i\in[n]\}$. Let $a=\{p_{j_{1}},\ldots,p_{j_{m}}\}$ be an interaction in $I_{{\mathcal{B}}}$ such that $p_{j_{l}}\in P(j_{l})$ for every $l\in[m]$. Then, the weighted monomial $\tilde{\phi}_{a}$ of $a$ is given by the wPIL formula

[TABLE]

where the first equivalence holds since $K$ is commutative and the second one since $p\otimes p^{\prime}\equiv p\wedge p^{\prime}$ for every $p,p^{\prime}\in P_{{\mathcal{B}}}$.

Definition 7

A weighted component-based system (over $K$)* is a pair $(w{\mathcal{B}},\tilde{\varphi})$ where $w{\mathcal{B}}=\{wB(i)\mid i\in[n]\}$ is a set of weighted components and ${\tilde{\varphi}}$ is a wEPIL formula over $P_{{\mathcal{B}}}$ and $K$.*

We should note that, as in the unweighted case, the wEPIL formula ${\tilde{\varphi}}$ is defined over the set of ports $P_{{\mathcal{B}}}$ and is interpreted as a series in $K\left\langle\left\langle I_{{\mathcal{B}}}^{*}\right\rangle\right\rangle$.

4.1 Examples of architectures described by wEPIL formulas

In this subsection, we present three examples of weighted component-based models whose architectures have ordered interactions encoded by wEPIL formulas. We recall from [44] the following macro EPIL formula. Let $P=\{p_{1},\ldots,p_{n}\}$ be a set of ports. Then, for $p_{i_{1}},\ldots,p_{i_{m}}\in P$ with $m<n$ we let

[TABLE]

Let us now assume that we assign a weight $k_{i_{l}}\in K$ to $p_{i_{l}}$ for every $l\in[m]$. We define the subsequent macro wEPIL formula

[TABLE]

Then, we get

[TABLE]

Clearly the above macro formula $\#_{w}(p_{i_{1}}\otimes\ldots\otimes p_{i_{m}})$ depends on the values $k_{i_{1}},\ldots,k_{i_{m}}$. Though, in order to simplify our wEPIL formulas, we make no special notation about this. If the macro formula is defined in a weighted component-based system, then the values $k_{i_{1}},\ldots,k_{i_{m}}$ are unique in the whole formula.

Example 8

(Weighted Blackboard)* Blackboard architecture is applied to multi-agent systems for solving problems with nondeterministic strategies that result from multiple partial solutions ([15]). Several applications are based on a blackboard architecture, including planning and scheduling (cf. [32, 50]), artificial intelligence (cf. [15]) and web applications [34, 38]. Blackboard architecture involves three component types, one blackboard component, one controller component and the knowledge sources components [11, 15]. Blackboard is a global data store that presents the state of the problem to be solved. Knowledge sources, simply called sources, are expertised agents that provide partial solutions to the given problem. Knowledge sources are independent and do not know about the existence of other sources.Whenever there is sufficient information for a source to provide its partial solution, the corresponding source is triggered i.e., is keen to write on the blackboard. Since multiple sources are triggered and compete to provide their solutions, a controller component is used to resolve any conflicts. Controller accesses both the blackboard to inspect the available data and the sources to schedule them so that they execute their solutions on the blackboard.*

Consider a weighted component-based system $(w{\mathcal{B}},\tilde{\varphi})$ with the Blackboard architecture and three sources. Therefore, we have $w{\mathcal{B}}=\{wB(1),wC(1),wS(1),wS(2),wS(3)\}$ referring to blackboard, controller, and the three sources weighted components, respectively. Figure 1 depicts a possible execution of the permissible interactions in the system. The weight associated with each port in the system is shown at the outside of the port. Blackboard component has two ports $p_{d},p_{a}$ to declare the state of the problem and add the new data as obtained by a source, respectively. Sources have three ports $p_{n_{i}},p_{t_{i}},p_{w_{i}}$, for $i=1,2,3$, for being notified about the existing data on the blackboard, the trigger of the source, and for writing the partial solution on the blackboard, respectively. Controller has three ports, namely $p_{r}$ used to record blackboard data, $p_{l}$ for the log process of triggered sources, and $p_{e}$ for their execution to blackboard. Here we assume that all knowledge sources are triggered, i.e., that all available sources participate in the architecture. The interactions range over $I_{{\mathcal{B}}}$ and the wEPIL formula ${\tilde{\varphi}}$ for the weighted Blackboard architecture is

[TABLE]

where

[TABLE]

for $i=1,2,3$. The first wPIL subformula expresses the cost for the connection of the blackboard and controller. The wEPIL subformula between the two weighted concatenation operators represents the cost of the connection of the three sources to blackboard in order to be informed for existing data. The last part of ${\tilde{\varphi}}$ captures the cost of applying the connection of some of the three sources with controller and blackboard for the triggering and writing process.

Let $w_{1}=\{p_{d},p_{r}\}\{p_{d},p_{n_{1}}\}\{p_{d},p_{n_{2}}\}\{p_{d},p_{n_{3}}\}\{p_{l},p_{t_{2}}\}\{p_{l},p_{t_{3}}\}\{p_{e},p_{w_{2}},p_{a}\}\{p_{e},p_{w_{3}},p_{a}\}$ and $w_{2}=\{p_{d},p_{r}\}\{p_{d},p_{n_{3}}\}\{p_{d},p_{n_{1}}\}\{p_{d},p_{n_{2}}\}\{p_{l},p_{t_{3}}\}\{p_{e},p_{w_{3}},p_{a}\}$ so that in $w_{1}$ the source $wS(2)$ is triggered and writes data before the third source $wS(3)$, and in $w_{2}$ only source $wS(3)$ is triggered and writes data. The values $\left\|{\tilde{\varphi}}\right\|(w_{1})$ and $\left\|{\tilde{\varphi}}\right\|(w_{2})$ represent the cost for executing the interactions with the order encoded by $w_{1}$ and $w_{2}$, respectively. Then, $\left\|{\tilde{\varphi}}\right\|(w_{1})+\left\|{\tilde{\varphi}}\right\|(w_{2})$ is the ‘total’ cost for implementing $w_{1}$ and $w_{2}$. For instance, in the min-plus semiring the value $\min\{\left\|{\tilde{\varphi}}\right\|(w_{1}),\left\|{\tilde{\varphi}}\right\|(w_{2})\}$ gives information for the communication with the minimum cost. On the other hand, in Viterbi semiring, we get the value $\max\{\left\|{\tilde{\varphi}}\right\|(w_{1}),\left\|{\tilde{\varphi}}\right\|(w_{2})\}$ which refers to the communication with the maximum probability to be executed.

Example 9

(Weighted Request/Response)*

Request/Response architectures represent a classical interaction pattern and are widely used for web services [16]. A Request/Response architecture refers to clients and services. Services are offered by service providers through some common (online) platform. In order for a service to be made available the service provider needs to subscribe it in the service registry. The enrollment of a service in the registry allows service consumers, simply called clients, to search the existing services. Once a service is signed up, the client scans the corresponding registry and chooses a service. Then, each client that is interested in a service sends a request to the service and waits until the service will respond. No other client can be connected to the service until the response of the service to the client who sent the request will be completed. In [37] the authors described this process by adding, for each service, a third component called coordinator. Coordinator takes care that only one client is connected to a service until the process among them is completed.*

Let $(w{\mathcal{B}},\widetilde{\varphi})$ be a weighted component-based system with the Request/Response architecture. We consider four weighted component types namely weighted service registry, service, client, and coordinator. Our weighted system consists of seven components, and specifically, the service registry, two services with their associated coordinators, and two clients. Therefore, we have that $w{\mathcal{B}}=\{wR(1),wS(1),wS(2),wD(1),wD(2),wC(1),wC(2)\}$ referring to each of the aforementioned weighted components, respectively. Figure 2 depicts a case for the permissible interactions in the system. Service registry has three ports denoted by $p_{e}$, $p_{u}$, and $p_{t}$ used for connecting with the service for its enrollment, for authorizing the client to search for a service, and for transmitting the address (link) of the service to the client in order for the client to send then its request, respectively. Services have three ports $p_{r_{z}},p_{g_{z}},p_{s_{z}}$, for $z=1,2$, which establish the connection to the service registry for signing up the service, and the connection to a client (via coordinator) for getting a request and responding (sending the response), respectively. Each client $z$ has five ports denoted by $p_{l_{z}},p_{o_{z}},p_{n_{z}},p_{q_{z}}$ and $p_{c_{z}}$ for $z=1,2$. The first two ports are used for connection with the service registry to look up the available services and for obtaining the address of the service that interests the client. The latter three ports express the connection of the client to coordinator, to service (via coordinator) for sending the request, and to service (via coordinator) for collecting its response, respectively. Coordinators have three ports namely $p_{m_{z}},p_{a_{z}},p_{d_{z}}$ for $z=1,2$. The first port controls that only one client is connected to a service. The second one is used for acknowledging that the connected client sends a request, and the third one disconnects the client when the service responds to the request. The interactions in the architecture range over $I_{{\mathcal{B}}}$ and the weight of each port is denoted as in Figure 2. The wEPIL formula ${\tilde{\varphi}}$ describing the weighted Request/Response architecture is

[TABLE]

where

${\tilde{\xi}}_{1}=\#_{w}(p_{l_{1}}\otimes p_{u})\odot\#_{w}(p_{o_{1}}\otimes p_{t})$,

• -

${\tilde{\xi}}_{2}=\#_{w}(p_{l_{2}}\otimes p_{u})\odot\#_{w}(p_{o_{2}}\otimes p_{t})$,

and

${\tilde{\varphi}}_{11}=\#_{w}(p_{n_{1}}\otimes p_{m_{1}})\odot\#_{w}(p_{q_{1}}\otimes p_{a_{1}}\otimes p_{g_{1}})\odot\#_{w}(p_{c_{1}}\otimes p_{d_{1}}\otimes p_{s_{1}})$,

• -

${\tilde{\varphi}}_{12}=\#_{w}(p_{n_{1}}\otimes p_{m_{2}})\odot\#_{w}(p_{q_{1}}\otimes p_{a_{2}}\otimes p_{g_{2}})\odot\#_{w}(p_{c_{1}}\otimes p_{d_{2}}\otimes p_{s_{2}})$,

• -

${\tilde{\varphi}}_{21}=\#_{w}(p_{n_{2}}\otimes p_{m_{1}})\odot\#_{w}(p_{q_{2}}\otimes p_{a_{1}}\otimes p_{g_{1}})\odot\#_{w}(p_{c_{2}}\otimes p_{d_{1}}\otimes p_{s_{1}})$,

• -

${\tilde{\varphi}}_{22}=\#_{w}(p_{n_{2}}\otimes p_{m_{2}})\odot\#_{w}(p_{q_{2}}\otimes p_{a_{2}}\otimes p_{g_{2}})\odot\#_{w}(p_{c_{2}}\otimes p_{d_{2}}\otimes p_{s_{2}})$.

The two wEPIL subformulas at the left of the first two weighted concatenation operators encode the cost for the connections of the two services and the two clients with registry, respectively. Then, each of the three wEPIL subformulas connected with $\bigoplus$ present the cost for the connection of either one of the two clients or both of them (one at each time) with the first service only, the second service only, or both of the services, respectively.

Let $w_{1}=\{p_{e},p_{r_{1}}\}\{p_{e},p_{r_{2}}\}\{p_{l_{1}},p_{u}\}\{p_{l_{2}},p_{u}\}\{p_{o_{1}},p_{u}\}\{p_{o_{2}},p_{u}\}\{p_{n_{1}},p_{m_{2}}\}\{p_{q_{1}},p_{a_{2}},p_{g_{2}}\}\{p_{c_{1}},p_{d_{2}},\\ p_{s_{2}}\}\{p_{n_{2}},p_{m_{2}}\}\{p_{q_{2}},p_{a_{2}},p_{g_{2}}\}\{p_{c_{2}},p_{d_{2}},p_{s_{2}}\}$ and $w_{2}=\{p_{e},p_{r_{2}}\}\{p_{e},p_{r_{1}}\}\{p_{l_{1}},p_{u}\}\{p_{l_{2}},p_{u}\}\{p_{o_{2}},p_{u}\}\\ \{p_{o_{1}},p_{u}\}\{p_{n_{2}},p_{m_{2}}\}\{p_{q_{2}},p_{a_{2}},p_{g_{2}}\}\{p_{c_{2}},p_{d_{2}},p_{s_{2}}\}$. Then $w_{1}$ encodes one of the possible executions for the interactions in which firstly client $wC(1)$ and then client $wC(2)$ connects via $wD(2)$ to service $wS(2)$, and $w_{2}$ shows a possible execution for applying the connection only of client $wC(2)$ via $wD(2)$ to $wS(2)$. Then, in max-plus semiring for instance, the value $\max\{\left\|{\tilde{\varphi}}\right\|(w_{1}),\left\|{\tilde{\varphi}}\right\|(w_{2})\}$ gives information for the communication with the maximum cost.

Example 10

(Weighted Publish/Subscribe)*

Publish/Subscribe architecture is widely used in IoT applications (cf. for instance [40, 43]), and recently in cloud systems [54] and robotics [36]. Publish/Subscribe architecture involves three types of components, namely publishers, subscribers, and topics (Figure 3). Publishers advertise and transmit to topics the type of messages they are able to produce. Then, subscribers are connected with topics they are interested in, and topics in turn transfer the messages from publishers to corresponding subscribers. Once a subscriber receives the message it has requested, then it is disconnected from the relevant topic. Publishers cannot check the existence of subscribers and vice-versa [22].*

Let $(w{\mathcal{B}},\widetilde{\varphi})$ be a weighted component-based system with the Publish/Subscribe architecture. For our example we consider two weighted publisher components, two weighted topic components and three weighted subscriber components. Hence, $w{\mathcal{B}}=\{wB(1),wB(2),wT(1),wT(2),\\ wS(1),wS(2),wS(3)\}$ refer to the aforementioned components, respectively. The corresponding sets of ports are $\{p_{a_{1}},p_{t_{1}}\},\{p_{a_{2}},p_{t_{2}}\},\{p_{n_{1}},p_{r_{1}},p_{c_{1}},p_{s_{1}},p_{f_{1}}\},\{p_{n_{2}},p_{r_{2}},p_{c_{2}},p_{s_{2}},p_{f_{2}}\},$ $\{p_{e_{1}},p_{g_{1}},\\ p_{d_{1}}\}$, $\{p_{e_{2}},p_{g_{2}},p_{d_{2}}\}$, and $\{p_{e_{3}},p_{g_{3}},p_{d_{3}}\}$, respectively. Figure 3 depicts one of the possible instantiations for the interactions among the components of our system. The ports $p_{a_{z}}$ and $p_{t_{z}}$, for $z=1,2$, are used from publishers for advertising and transferring their messages to topic components, respectively. Each of the two topics is notified from the publishers and receives their messages through ports $p_{n_{z}}$ and $p_{r_{z}}$, for $z=1,2$, respectively. Ports $p_{c_{z}},p_{s_{z}}$ and $p_{f_{z}}$, for $z=1,2$, are used from topic components for the connection with a subscriber, the sending of a message to a subscriber and for finalizing their connection (disconnection), respectively. Subscribers use the ports $p_{e_{y}},p_{g_{y}},p_{d_{y}}$, for $y=1,2,3$, for connecting with the topic (express interest), getting a message from the topic, and disconnecting from the topic, respectively. The interactions in the architecture range over $I_{{\mathcal{B}}}$ and the weight of each port is shown in Figure 3. The wEPIL formula ${\tilde{\varphi}}$ for the Publish/Subscribe architecture is ${\tilde{\varphi}}={\tilde{\varphi}}_{1}\oplus{\tilde{\varphi}}_{2}\oplus({\tilde{\varphi}}_{1}\varpi{\tilde{\varphi}}_{2})$ with

[TABLE]

and

[TABLE]

where the following auxiliary subformulas:

${\tilde{\xi}}_{1}={\tilde{\xi}}_{11}\oplus{\tilde{\xi}}_{12}\oplus({\tilde{\xi}}_{11}\varpi{\tilde{\xi}}_{12})$**

• -

${\tilde{\xi}}_{2}={\tilde{\xi}}_{21}\oplus{\tilde{\xi}}_{22}\oplus({\tilde{\xi}}_{21}\varpi{\tilde{\xi}}_{22})$**

represent the cost for the connection of each of the two topics with the first publisher, or the second one or with both of them, and

${\tilde{\xi}}_{11}=\#_{w}(p_{n_{1}}\otimes p_{a_{1}})\odot\#_{w}(p_{r_{1}}\otimes p_{t_{1}})$**

• -

${\tilde{\xi}}_{12}=\#_{w}(p_{n_{1}}\otimes p_{a_{2}})\odot\#_{w}(p_{r_{1}}\otimes p_{t_{2}})$**

• -

${\tilde{\xi}}_{21}=\#_{w}(p_{n_{2}}\otimes p_{a_{1}})\odot\#_{w}(p_{r_{2}}\otimes p_{t_{1}})$**

• -

${\tilde{\xi}}_{22}=\#_{w}(p_{n_{2}}\otimes p_{a_{2}})\odot\#_{w}(p_{r_{2}}\otimes p_{t_{2}})$**

describe the cost of the interactions of the two topics with each of the two publishers, and

${\tilde{\varphi}}_{11}=\#_{w}(p_{c_{1}}\otimes p_{e_{1}})\odot\#_{w}(p_{s_{1}}\otimes p_{g_{1}})\odot\#_{w}(p_{f_{1}}\otimes p_{d_{1}})$**

• -

${\tilde{\varphi}}_{12}=\#_{w}(p_{c_{1}}\otimes p_{e_{2}})\odot\#_{w}(p_{s_{1}}\otimes p_{g_{2}})\odot\#_{w}(p_{f_{1}}\otimes p_{d_{2}})$**

• -

${\tilde{\varphi}}_{13}=\#_{w}(p_{c_{1}}\otimes p_{e_{3}})\odot\#_{w}(p_{s_{1}}\otimes p_{g_{3}})\odot\#_{w}(p_{f_{1}}\otimes p_{d_{3}})$**

• -

${\tilde{\varphi}}_{21}=\#_{w}(p_{c_{2}}\otimes p_{e_{1}})\odot\#_{w}(p_{s_{2}}\otimes p_{g_{1}})\odot\#_{w}(p_{f_{2}}\otimes p_{d_{1}})$**

• -

${\tilde{\varphi}}_{22}=\#_{w}(p_{c_{2}}\otimes p_{e_{2}})\odot\#_{w}(p_{s_{2}}\otimes p_{g_{2}})\odot\#_{w}(p_{f_{2}}\otimes p_{d_{2}})$**

• -

${\tilde{\varphi}}_{23}=\#_{w}(p_{c_{2}}\otimes p_{e_{3}})\odot\#_{w}(p_{s_{2}}\otimes p_{g_{3}})\odot\#_{w}(p_{f_{2}}\odot p_{d_{3}})$.

describe the cost of the connections of each of the three subscribers with the two topics.

Consider $w_{1}=\{p_{a_{1}},p_{n_{1}}\}\{p_{t_{1}},p_{r_{1}}\}\{p_{c_{1}},p_{e_{1}}\}\{p_{s_{1}},p_{g_{1}}\}\{p_{c_{1}},p_{e_{3}}\}\{p_{f_{1}},p_{d_{1}}\}\{p_{s_{1}},p_{g_{3}}\}\{p_{f_{1}},p_{d_{3}}\}$ and $w_{2}=\{p_{a_{1}},p_{n_{1}}\}\{p_{t_{1}},p_{r_{1}}\}\{p_{c_{1}},p_{e_{3}}\}\{p_{c_{1}},p_{e_{1}}\}\{p_{s_{1}},p_{g_{1}}\}\{p_{c_{1}},p_{e_{2}}\}\{p_{s_{1}},p_{g_{2}}\}\{p_{s_{1}},p_{g_{3}}\}\{p_{f_{1}},p_{d_{3}}\}\{p_{f_{1}},\\ p_{d_{1}}\}\{p_{f_{1}},p_{d_{2}}\}$ where $w_{1}$ expresses one of the possible executions for the interactions in which subscribers $wS(1)$ and $wS(2)$ are interested in topic $wT(1)$, and $w_{2}$ encodes a possible implementation for applying the connections of all subscribers to $wT(1)$. For instance, in the Viterbi semiring the value $\max\{\left\|{\tilde{\varphi}}\right\|(w_{1}),\left\|{\tilde{\varphi}}\right\|(w_{2})\}$ shows the interaction executed with the maximum probability.

The above examples demonstrate that wEPIL formulas can efficiently represent the overall cost of ordered interactions within architectures. The resulting value is obtained by the relevant operations of each semiring and the notion of cost serves for representing different quantitative values like the required power consumption, battery waste, or time, for implementing the components’ connections.

5 Parametric weighted component-based systems

In this section we deal with the parametric extension of weighted component-based systems. Weighted component-based systems considered in Subsection 3.4 are comprised of a finite number of weighted components which are of the same or distinct type. On the other hand, in the parametric setting a weighted component-based model is comprised of a finite number of distinct weighted component types where the cardinality of the instances of each type is a parameter for the system. It should be clear, that in real world applications we do not need an unbounded number of components. Nevertheless, the number of instances of every component type is unknown or it can be modified during a process. Therefore, in the sequel we consider parametric weighted component-based systems, i.e., weighted component-based systems with infinitely many instances of every component type. We shall need to recall firstly parametric (unweighted) component-based systems [44].

Let ${\mathcal{B}}=\{B(i)\mid i\in[n]\}$ be a set of component types. For every $i\in[n]$ and $j\geq 1$ we consider a copy $B(i,j)=(Q(i,j),P(i,j),q_{0}(i,j),R(i,j))$ of $B(i)$, namely the $j$-th instance of $B(i)$. Hence, for every $i\in[n]$ and $j\geq 1$, the instance $B(i,j)$ is also a component and we call it a parametric component or a component instance. We assume that $(Q(i,j)\cup P(i,j))\cap(Q(i^{\prime},j^{\prime})\cup P(i^{\prime},j^{\prime}))=\emptyset$ whenever $i\neq i^{\prime}$ or $j\neq j^{\prime}$ for every $i,i^{\prime}\in[n]$ and $j,j^{\prime}\geq 1$. This restriction is needed in order to identify the distinct parametric components. It also permits us to use, without any confusion, the notation $P(i,j)=\{p(j)\mid p\in P(i)\}$ for every $i\in[n]$ and $j\geq 1$. We set $p\mathcal{B}=\{B(i,j)\mid i\in[n],j\geq 1\}$ and call it a set of parametric components. The set of ports of $p{\mathcal{B}}$ is given by $P_{p{\mathcal{B}}}=\bigcup_{i\in[n],j\geq 1}P(i,j)$.

Let $w{\mathcal{B}}=\{wB(i)\mid i\in[n]\}$ be a set of weighed component types. For every $i\in[n]$ and $j\geq 1$ we consider a weighted component $wB(i,j)=(B(i,j),wt(i))$, where $B(i,j)=(Q(i,j),P(i,j),q_{0}(i,j),R(i,j))$ is the $j$-th instance of $B(i)$, and it is called a parametric weighted component or a weighted component instance. We set $pw\mathcal{B}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ and call it a set of parametric weighted components. We impose on $pw{\mathcal{B}}$ the same assumptions as for $p{\mathcal{B}}$. Abusing notations, we denote by $wt(i)$, $i\in[n]$, the weight mapping of $wB(i,j)$, $j\geq 1$, meaning that it assigns the value $wt(i)(p)$ to every port $p(j)\in P(i,j)$.

As it is already mentioned, in practical applications we do not know how many instances of each weighted component type are connected at a concrete time. This means that we cannot define interactions of $pw\mathcal{B}$ in the same way as we did for finite sets of weighted component types. For this, we need a symbolic representation to describe interactions and hence architectures of parametric weighted systems. In [44] we investigated the first-order extended interaction logic (FOEIL for short) which was proved sufficient to describe a wide class of architectures of parametric component-based systems. Here, we introduce a weighted first-order extended interaction logic for the description of architectures of parametric weighted component-based systems.

5.1 Weighted first-order extended interaction logic

In this subsection we introduce the weighted first-order extended interaction logic as a modelling language for describing the interactions of parametric weighted component-based systems.

As in FOEIL we equip wEPIL formulas with variables. Due to the nature of parametric systems we need to distinguish variables referring to different component types. Let $pw\mathcal{B}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ be a set of parametric weighted components. We consider pairwise disjoint countable sets of first-order variables $\mathcal{X}^{(1)},\ldots,\mathcal{X}^{(n)}$ referring to instances of component types $wB(1),\ldots,wB(n)$, respectively. Variables in $\mathcal{X}^{(i)}$, for every $i\in[n]$, will be denoted by small letters with the corresponding superscript. Hence by $x^{(i)}$ we understand that $x^{(i)}\in\mathcal{X}^{(i)}$, $i\in[n]$, is a first-order variable referring to an instance of weighted component type $wB(i)$. We let $\mathcal{X}=\mathcal{X}^{(1)}\cup\ldots\cup\mathcal{X}^{(n)}$ and set $P_{p{\mathcal{B}}(\mathcal{X})}=\left\{p\left(x^{(i)}\right)\mid i\in[n],x^{(i)}\in\mathcal{X}^{(i)},\text{ and }p\in P(i)\right\}$.

We need to recall FOEIL firstly [44]. Let $p\mathcal{B}=\{B(i,j)\mid i\in[n],j\geq 1\}$ be a set of parametric components. Then the syntax of FOEIL formulas $\psi$ over $p\mathcal{B}$111According to our terminology for EPIL formulas, a FOEIL formula should be defined over the set of ports of $p{\mathcal{B}}$. Nevertheless, we prefer for simplicity to refer to the set $p{\mathcal{B}}$ of parametric components. is given by the grammar

[TABLE]

where $\varphi$ is an EPIL formula over $P_{p{\mathcal{B}}(\mathcal{X})}$, $i\in[n]$, $x^{(i)},y^{(i)}\in\mathcal{X}^{(i)}$, $\exists^{*}$ (resp. $\forall^{*}$) denotes the existential (resp. universal) concatenation quantifier, and $\exists^{\shuffle}$ (resp. $\forall^{\shuffle}$) the existential (resp. universal) shuffle quantifier. Furthermore, we assume that whenever $\psi$ contains a subformula of the form $\exists^{*}x^{(i)}.\psi^{\prime}$ or $\exists^{\shuffle}x^{(i)}.\psi^{\prime}$, then the application of negation in $\psi^{\prime}$ is permitted only in PIL formulas and formulas of the form $x^{(j)}=y^{(j)}$.

Let $\psi$ be a FOEIL formula over $p{\mathcal{B}}$. We denote by $\mathrm{free}(\psi)$ the set of free variables of $\psi$. If $\psi$ has no free variables, then it is a sentence. We consider a mapping $r:[n]\rightarrow\mathbb{N}$. The value $r(i)$, for every $i\in[n]$, intends to represent the finite number of instances of the component type $B(i)$ in the parametric system. The mapping characterizes the dynamic behavior of such systems, where components’ instances can appear or disappear, affecting in turn, the corresponding interactions. Hence, for different mappings we obtain a different parametric system. We let $p{\mathcal{B}}(r)=\{B(i,j)\mid i\in[n],j\in[r(i)]\}$ and call it the instantiation of $p{\mathcal{B}}$ w.r.t. $r$. We denote by $P_{p{\mathcal{B}}(r)}$ the set of all ports of components’ instances in $p{\mathcal{B}}(r)$, i.e., $P_{p{\mathcal{B}}(r)}=\bigcup_{i\in[n],j\in[r(i)]}P(i,j)$. The set $I_{p{\mathcal{B}}(r)}$ of interactions of $p{\mathcal{B}}(r)$ is given by $I_{p{\mathcal{B}}(r)}=\{a\in I(P_{p{\mathcal{B}}(r)})\mid|a\cap P(i,j)|\leq 1\text{ for every }i\in[n]\text{ and }j\in[r(i)]\}$.

Let $\mathcal{V}\subseteq\mathcal{X}$ be a finite set of first-order variables. We let $P_{p{\mathcal{B}}(\mathcal{V})}=\{p(x^{(i)})\in P_{p{\mathcal{B}}(\mathcal{X})}\mid x^{(i)}\in\mathcal{V}\}$. To interpret FOEIL formulas over $p{\mathcal{B}}$ we use the notion of an assignment defined with respect to the set of variables $\mathcal{V}$ and the mapping $r$. Formally, a $(\mathcal{V},r)$-assignment is a mapping $\sigma:\mathcal{V}\rightarrow\mathbb{N}$ such that $\sigma(\mathcal{V}\cap\mathcal{X}^{(i)})\subseteq[r(i)]$ for every $i\in[n]$. If $\sigma$ is a $(\mathcal{V},r)$-assignment, then $\sigma[x^{(i)}\rightarrow j]$ is the $(\mathcal{V}\cup\{x^{(i)}\},r)$-assignment which acts as $\sigma$ on $\mathcal{V}\setminus\{x^{(i)}\}$ and assigns $j$ to $x^{(i)}$. Intuitively, a $(\mathcal{V},r)$-assignment $\sigma$ assigns unique identifiers to each instance in a parametric system, w.r.t. the mapping $r$.

We interpret FOEIL formulas over triples consisting of a mapping $r:[n]\rightarrow\mathbb{N}$, a $(\mathcal{V},r)$-assignment $\sigma$, and a word $w\in I_{p{\mathcal{B}}(r)}^{*}$.

Definition 11

Let $\psi$ be a FOEIL formula over a set $p\mathcal{B}=\{B(i,j)\mid i\in[n],j\geq 1\}$ of parametric components and $\mathcal{V}\subseteq\mathcal{X}$ a finite set containing $\mathrm{free}(\psi)$. Then for every $r:[n]\rightarrow\mathbb{N}$, $(\mathcal{V},r)$-assignment $\sigma$, and $w\in I_{p{\mathcal{B}}(r)}^{*}$ we define the satisfaction relation $(r,\sigma,w)\models\psi$, inductively on the structure of $\psi$ as follows:

$(r,\sigma,w)\models\varphi$* iff $w\models\sigma(\varphi)$,*

• -

$(r,\sigma,w)\models x^{(i)}=y^{(i)}$* iff $\sigma(x^{(i)})=\sigma(y^{(i)})$,*

• -

$(r,\sigma,w)\models\neg(x^{(i)}=y^{(i)})$* iff $(r,\sigma,w)\not\models x^{(i)}=y^{(i)}$,*

• -

$(r,\sigma,w)\models\psi_{1}\vee\psi_{2}$* iff $(r,\sigma,w)\models\psi_{1}$ or $(r,\sigma,w)\models\psi_{2}$,*

• -

$(r,\sigma,w)\models\psi_{1}\wedge\psi_{2}$* iff $(r,\sigma,w)\models\psi_{1}$ and $(r,\sigma,w)\models\psi_{2}$,*

• -

$(r,\sigma,w)\models\psi_{1}*\psi_{2}$* iff there exist $w_{1},w_{2}\in I_{p{\mathcal{B}}(r)}^{*}$ such that $w=w_{1}w_{2}$ and $(r,\sigma,w_{i})\models\psi_{i}$ for $i=1,2$,*

• -

$(r,\sigma,w)\models\psi_{1}\shuffle\psi_{2}$* iff there exist $w_{1},w_{2}\in I_{p{\mathcal{B}}(r)}^{*}$ such that $w\in w_{1}\shuffle w_{2}$ and $(r,\sigma,w_{i})\models\psi_{i}$ for $i=1,2$,*

• -

$(r,\sigma,w)\models\exists x^{(i)}.\psi$* iff there exists $j\in[r(i)]$ such that $(r,\sigma[x^{(i)}\rightarrow j],w)\models\psi$,*

• -

$(r,\sigma,w)\models\forall x^{(i)}.\psi$* iff $(r,\sigma[x^{(i)}\rightarrow j],w)\models\psi$ for every $j\in[r(i)]$,*

• -

$(r,\sigma,w)\models\exists^{*}x^{(i)}.\psi$* iff there exist $w_{l_{1}},\ldots,w_{l_{t}}\in I_{p{\mathcal{B}}(r)}^{*}$ with $1\leq l_{1}<\ldots<l_{t}\leq r(i)$ such that $w=w_{l_{1}}\ldots w_{l_{t}}$ and $(r,\sigma[x^{(i)}\rightarrow j],w_{j})\models\psi$ for every $j=l_{1},\ldots,l_{t}$,*

• -

$(r,\sigma,w)\models\forall^{*}x^{(i)}.\psi$* iff there exist $w_{1},\ldots,w_{r(i)}\in I_{p{\mathcal{B}}(r)}^{*}$ such that $w=w_{1}\ldots w_{r(i)}$ and $(r,\sigma[x^{(i)}\rightarrow j],w_{j})\models\psi$ for every $j\in[r(i)]$,*

• -

$(r,\sigma,w)\models\exists^{\shuffle}x^{(i)}.\psi$* iff there exist $w_{l_{1}},\ldots,w_{l_{t}}\in I_{p{\mathcal{B}}(r)}^{*}$ with $1\leq l_{1}<\ldots<l_{t}\leq r(i)$ such that $w\in w_{l_{1}}\shuffle\ldots\shuffle w_{l_{t}}$ and $(r,\sigma[x^{(i)}\rightarrow j],w_{j})\models\psi$ for every $j=l_{1},\ldots,l_{t}$,*

• -

$(r,\sigma,w)\models\forall^{\shuffle}x^{(i)}.\psi$* iff there exist $w_{1},\ldots,w_{r(i)}\in I_{p{\mathcal{B}}(r)}^{*}$ such that $w\in w_{1}\shuffle\ldots\shuffle w_{r(i)}$ and $(r,\sigma[x^{(i)}\rightarrow j],w_{j})\models\psi$ for every $j\in[r(i)]$,*

where $\sigma(\varphi)$ is obtained by $\varphi$ by replacing every port $p(x^{(i)})\in P_{p{\mathcal{B}}(\mathcal{V})}$, occurring in $\varphi$, by $p(\sigma(x^{(i)}))$.

If $\psi$ is a FOEIL sentence over $p{\mathcal{B}}$, then we simply write $(r,w)\models\psi$. Let also $\psi^{\prime}$ be a FOEIL sentence over $p\mathcal{B}$. Then, $\psi$ and $\psi^{\prime}$ are called equivalent w.r.t. $r$ whenever $(r,w)\models\psi$ iff $(r,w)\models\psi^{\prime}$, for every $w\in I_{p{\mathcal{B}}(r)}^{*}$.

In the sequel, we shall write also $x^{(i)}\neq y^{(i)}$ for $\neg(x^{(i)}=y^{(i)})$.

Let $\beta$ be a boolean combination of atomic formulas of the form $x^{(i)}=y^{(i)}$ and $\psi$ a FOEIL formula over $p{\mathcal{B}}$. Then, we define $\beta\rightarrow\psi::=\neg\beta\vee\psi$.

For simplicity sometimes we denote boolean combinations of formulas of the form $x^{(i)}=y^{(i)}$ as constraints. For instance we write $\exists x^{(i)}\forall y^{(i)}\exists x^{(j)}\forall y^{(j)}((x^{(i)}\neq y^{(i)})\wedge(x^{(j)}\neq y^{(j)})).\psi$ for $\exists x^{(i)}\forall y^{(i)}\exists x^{(j)}\forall y^{(j)}.(((x^{(i)}\neq y^{(i)})\wedge(x^{(j)}\neq y^{(j)}))\rightarrow\psi)$.

Now we are ready to introduce our weighted FOEIL.

Definition 12

Let $pw\mathcal{B}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ be a set of parametric weighted components. Then the syntax of weighted first-order extended interaction logic (wFOEIL for short) formulas* ${\tilde{\psi}}$ over $pw\mathcal{B}$ and $K$ is given by the grammar*

[TABLE]

where $k\in K$, $\psi$ is a FOEIL formula over $p{\mathcal{B}}$, $x^{(i)},y^{(i)}$ are first-order variables in $\mathcal{X}^{(i)}$, ${\textstyle\sum}$ (resp. ${\textstyle\prod}$) denotes the weighted existential (resp. universal) quantifier, ${\textstyle\sum\nolimits{{}^{\odot}}}$ (resp. ${\textstyle\prod\nolimits{{}^{\odot}}}$) denotes the weighted existential (resp. universal) concatenation quantifier, and ${\textstyle\sum\nolimits{{}^{\varpi}}}$ (resp. ${\textstyle\prod\nolimits{{}^{\varpi}}}$) the weighted existential (resp. universal) shuffle quantifier. Furthermore, we assume that when ${\tilde{\psi}}$ contains a subformula of the form ${\textstyle\sum\nolimits{{}^{\odot}}}x^{(i)}.{\tilde{\psi}}^{\prime}$ or ${\textstyle\sum\nolimits{{}^{\varpi}}x^{(i)}}.{\tilde{\psi}}^{\prime}$, and ${\tilde{\psi}}^{\prime}$ contains a FOEIL formula $\psi$, then the application of negation in $\psi$ is permitted only in PIL formulas, and formulas of the form $x^{(j)}=y^{(j)}$.

Let ${\tilde{\psi}}$ be a wFOEIL formula over $pw{\mathcal{B}}$ and $r:[n]\rightarrow\mathbb{N}$ a mapping. As for (unweighted) parametric systems the value $r(i)$, for every $i\in[n]$, intends to represent the finite number of instances of the weighted component type $wB(i)$ in the parametric system. We let $pw{\mathcal{B}}(r)=\{wB(i,j)\mid i\in[n],j\in[r(i)]\}$ and call it the instantiation of $pw{\mathcal{B}}$ w.r.t. $r$. The set of ports and the set of interactions of $pw{\mathcal{B}}(r)$ are the same as the corresponding ones in $p{\mathcal{B}}(r)$, hence we use for simplicity the same symbols $P_{p{\mathcal{B}}(r)}$ and $I_{p{\mathcal{B}}(r)}$, respectively.

We interpret wFOEIL formulas ${\tilde{\psi}}$ as series $\|{\tilde{\psi}}\|$ over triples consisting of a mapping $r:[n]\rightarrow\mathbb{N}$, a $(\mathcal{V},r)$-assignment $\sigma$, and a word $w\in I_{p{\mathcal{B}}(r)}^{*}$. Intuitively, the use of weighted existential and universal concatenation (resp. shuffle) quantifiers ${\textstyle\sum\nolimits{{}^{\odot}}}x^{(i)}.{\tilde{\psi}}$ and ${\textstyle\prod\nolimits{{}^{\odot}}x^{(i)}}.{\tilde{\psi}}$ (resp. ${\textstyle\sum\nolimits{{}^{\varpi}}x^{(i)}}.{\tilde{\psi}}$ and ${\textstyle\prod\nolimits{{}^{\varpi}}x^{(i)}}.{\tilde{\psi}}$) serves to compute the weight of the partial and whole participation of the weighted component instances, determined by the application of the assignment $\sigma$ to $x^{(i)}$, in sequential (resp. interleaving) interactions.

Definition 13

Let ${\tilde{\psi}}$ be a wFOEIL formula over a set $pw\mathcal{B}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ of parametric weighted components and $K$, and $\mathcal{V}\subseteq\mathcal{X}$ a finite set containing $\mathrm{free}(\psi)$. Then for every $r:[n]\rightarrow\mathbb{N}$, $(\mathcal{V},r)$-assignment $\sigma$, and $w\in I_{p{\mathcal{B}}(r)}^{*}$ we define the value $\|{\tilde{\psi}}\|(r,\sigma,w)$, inductively on the structure of ${\tilde{\psi}}$ as follows:

$\|k\|(r,\sigma,w)=k$,

• -

\|\psi\|(r,\sigma,w)\left\{\begin{array}[c]{rl}1&\textnormal{ if }(r,\sigma,w)\models\psi\\ 0&\textnormal{ otherwise}\end{array},\right.**

• -

$\|{\tilde{\psi}}_{1}\oplus{\tilde{\psi}}_{2}\|(r,\sigma,w)=\|{\tilde{\psi}}_{1}\|(r,\sigma,w)+\|{\tilde{\psi}}_{2}\|(r,\sigma,w)$,

• -

$\|{\tilde{\psi}}_{1}\otimes{\tilde{\psi}}_{2}\|(r,\sigma,w)=\|{\tilde{\psi}}_{1}\|(r,\sigma,w)\cdot\|{\tilde{\psi}}_{2}\|(r,\sigma,w)$,

• -

$\|{\tilde{\psi}}_{1}\odot{\tilde{\psi}}_{2}\|(r,\sigma,w)=\sum\nolimits_{w=w_{1}w_{2}}(\|{\tilde{\psi}}_{1}\|(r,\sigma,w_{1})\cdot\|{\tilde{\psi}}_{2}\|(r,\sigma,w_{2}))$,

• -

$\|{\tilde{\psi}}_{1}\varpi{\tilde{\psi}}_{2}\|(r,\sigma,w)=\sum\nolimits_{w\in w_{1}\shuffle w_{2}}(\|{\tilde{\psi}}_{1}\|(r,\sigma,w_{1})\cdot\|{\tilde{\psi}}_{2}\|(r,\sigma,w_{2}))$,

• -

$\left\|{\textstyle\sum x^{(i)}}.{\tilde{\psi}}\right\|(r,\sigma,w)=\sum\limits_{j\in[r(i)]}\|{\tilde{\psi}}\|(r,\sigma[x^{(i)}\rightarrow j],w)$,

• -

$\left\|{\textstyle\prod x^{(i)}}.{\tilde{\psi}}\right\|(r,\sigma,w)=\prod\limits_{j\in[r(i)]}\|{\tilde{\psi}}\|(r,\sigma[x^{(i)}\rightarrow j],w)$,

• -

$\left\|{\textstyle\sum\nolimits{{}^{\odot}}}x^{(i)}.{\tilde{\psi}}\right\|(r,\sigma,w)=\sum\limits_{1\leq l_{1}<\ldots<l_{t}\leq r(i)}\sum\limits_{w=w_{l_{1}}\ldots w_{l_{t}}}\prod\limits_{j=l_{1},\ldots,l_{t}}\|{\tilde{\psi}}\|(r,\sigma[x^{(i)}\rightarrow j],w_{j})$,

• -

$\left\|{\textstyle\prod\nolimits{{}^{\odot}}x^{(i)}}.{\tilde{\psi}}\right\|(r,\sigma,w)=\sum\limits_{w=w_{1}\ldots w_{r(i)}}\prod\limits_{1\leq j\leq r(i)}\|{\tilde{\psi}}\|(r,\sigma[x^{(i)}\rightarrow j],w_{j})$,

• -

$\left\|{\textstyle\sum\nolimits{{}^{\varpi}}}x^{(i)}.{\tilde{\psi}}\right\|(r,\sigma,w)=\sum\limits_{1\leq l_{1}<\ldots<l_{t}\leq r(i)}\sum\limits_{w\in w_{l_{1}}\shuffle\ldots\shuffle w_{l_{t}}}\prod\limits_{j=l_{1},\ldots,l_{t}}\|{\tilde{\psi}}\|(r,\sigma[x^{(i)}\rightarrow j],w_{j})$,

• -

$\left\|{\textstyle\prod\nolimits{{}^{\varpi}}}x^{(i)}.{\tilde{\psi}}\right\|(r,\sigma,w)=\sum\limits_{w\in w_{1}\shuffle\ldots\shuffle w_{r(i)}}\prod\limits_{1\leq j\leq r(i)}\|{\tilde{\psi}}\|(r,\sigma[x^{(i)}\rightarrow j],w_{j})$.

If ${\tilde{\psi}}$ is a wFOEIL sentence over $pw{\mathcal{B}}$ and $K$, then we simply write $\|{\tilde{\psi}}\|(r,w)$. Let also ${\tilde{\psi}}^{\prime}$ be a wFOEIL sentence over $pw\mathcal{B}$ and $K$. Then, ${\tilde{\psi}}$ and ${\tilde{\psi}}^{\prime}$ are called equivalent w.r.t. $r$ whenever $\|{\tilde{\psi}}\|(r,w)=\|{\tilde{\psi}}^{\prime}\|(r,w)$, for every $w\in I_{p{\mathcal{B}}(r)}^{*}$.

Now we are ready to formally define the concept of a parametric weighted component-based system.

Definition 14

A parametric weighted component-based system over $K$ is a pair $(pw{\mathcal{B}},{\tilde{\psi}})$ where $pw{\mathcal{B}}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ is a set of parametric weighted components and ${\tilde{\psi}}$ is a wFOEIL sentence over $pw{\mathcal{B}}$ and $K$.

In the sequel, for simplicity we refer to parametric weighted component-based systems simply as parametric weighted systems. We remind that in this work we focus on the architectures of parametric weighted systems. The study of parametric weighted systems’ behavior is left for investigation in subsequent work as a part of parametric quantitative verification.

For our examples in the next subsection, we need the following macro wFOEIL formula. Let $pw{\mathcal{B}}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ and $1\leq i_{1},\ldots,i_{m}\leq n$ be pairwise different indices. Let $p_{i_{1}}\in P(i_{1}),\ldots,p_{i_{m}}\in P(i_{m})$ and $k_{i_{1}},\ldots,k_{i_{m}}$ denote the weights in $K$ assigned to $p_{i_{1}},\ldots,p_{i_{m}}$, respectively, i.e., $k_{i_{1}}=wt(i_{1})(p_{i_{1}}),\ldots,k_{i_{m}}=wt(i_{m})(p_{i_{m}})$. We set

[TABLE]

The weighted conjunctions in the right-hand side of the first line, in the above formula, express that the ports appearing in the argument of $\#_{w}$ participate in the interaction with their corresponding weights. In the second line, the double indexed conjunctions in the first pair of big parentheses disable all the other ports of the participating instances of components of type $i_{1},\ldots,i_{m}$ described by variables $x^{(i_{1})},\ldots,x^{(i_{m})}$, respectively; conjunctions in the second pair of parentheses disable all ports of remaining instances of component types $i_{1},\ldots,i_{m}$. Finally, the last conjunct in the third line ensures that no ports in instances of remaining component types participate in the interaction. Then we get

[TABLE]

5.2 Examples of wFOEIL sentences for parametric weighted architectures

In this subsection we present several examples of wFOEIL sentences describing concrete parametric architectures with quantitative features.

Example 15

(Weighted Master/Slave)* We present a wFOEIL sentence for the parametric weighted Master/Slave architecture. Master/Slave architecture concerns two types of components, namely masters and slaves [37]. Every slave must be connected with exactly one master. Interactions among masters (resp. slaves) are not permitted.*

We let $\mathcal{X}^{(1)},\mathcal{X}^{(2)}$ denote the sets of variables of master and slave weighted component instances, respectively. We denote by $p_{m}$ the port of master weighted component and by $p_{s}$ the port of slave weighted component. Then, the wFOEIL sentence ${\tilde{\psi}}$ representing parametric weighted Master/Slave architecture is

[TABLE]

An instantiation of the weighted parametric Master/Slave architecture for two masters and two slaves, i.e., for $r(1)=r(2)=2$ is shown in Figure 4. Let $\{p_{m}(1),p_{m}(2),p_{s}(1),p_{s}(2)\}$ be the set of ports. Then, consider $w_{1}=\{p_{m}(1),p_{s}(1)\}\{p_{m}(2),p_{s}(2)\}$, $w_{2}=\{p_{m}(1),p_{s}(1)\}\{p_{m}(1),p_{s}(2)\}$, $w_{3}=\{p_{m}(2),p_{s}(1)\}\{p_{m}(1),p_{s}(2)\}$, and $w_{4}=\{p_{m}(2),p_{s}(1)\}\{p_{m}(2),p_{s}(2)\}$, that correspond to the four possible connections for the components in the system as shown in Figure 4. Then, the values $\|{\tilde{\psi}}\|(r,w_{1})$, $\|{\tilde{\psi}}\|(r,w_{2})$, $\|{\tilde{\psi}}\|(r,w_{3})$, and $\|{\tilde{\psi}}\|(r,w_{4})$ return the cost of the implementation of each of the four possible interactions in the architecture, according to the underlying semiring. In turn, the “sum” $\|{\tilde{\psi}}\|(r,w_{1})+\|{\tilde{\psi}}\|(r,w_{2})+\|{\tilde{\psi}}\|(r,w_{3})+\|{\tilde{\psi}}\|(r,w_{4})$ equals for instance, in the semiring of natural numbers to the total cost for executing the possible connections in the architecture.

Example 16

(Weighted Star)* Star architecture has only one component type with a unique port, namely $p$. One instance is considered as the center in the sense that every other instance has to be connected with it. No other interaction is permitted. Figure 5 represents the Star architecture for five instances and center $wS(1,1)$.*

The wFOEIL sentence ${\tilde{\psi}}$ for the parametric weighted Star architecture is as follows:

[TABLE]

Let $a_{1}=\{p(1),p(2)\},a_{2}=\{p(1),p(3)\},a_{3}=\{p(1),p(4)\},a_{4}=\{p(1),p(5)\}$ refer to the interactions of $wS(1,2)$, $wS(1,3)$, $wS(1,4)$, and $wS(1,5)$ respectively, to $wS(1,1)$. The value $\|{\tilde{\psi}}\|(r,w)$ for $w=a_{1}a_{2}a_{3}a_{4}$ is the cost of the implementation of this architecture. Similarly, we get the cost of all possible Star architectures with center $wS(1,2),wS(1,3),wS(1,4),wS(1,5)$, respectively. Then, if we “sum up” those values we get for instance, in the semiring of rational numbers, the total cost.

Example 17

(Weighted Pipes/Filters)* Pipes/Filters architecture involves two types of components, namely pipes and filters [24]. Pipe (resp. filter) component has an entry port $p_{e}$ and an output port $p_{o}$ (resp. $f_{e},f_{o}$). Every filter $F$ is connected to two separate pipes $P$ and $P^{\prime}$ via interactions $\{f_{e},p_{o}\}$ and $\{f_{o},p^{\prime}_{e}\}$, respectively. Every pipe $P$ can be connected to at most one filter $F$ via an interaction $\{p_{o},f_{e}\}$. Any other interaction is not permitted. Figure 6 shows an instantiation of the parametric weighted Pipes/Filters architecture for four pipes and three filters, i.e., for $r(1)=4$ and $r(2)=3$.*

We denote by $\mathcal{X}^{(1)}$ and $\mathcal{X}^{(2)}$ the sets of variables corresponding to pipe and filter weighted component instances, respectively. The subsequent wFOEIL sentence ${\tilde{\psi}}$ describes the parametric weighted Pipes/Filters architecture.

[TABLE]

In the above weighted sentence the arguments of $\#_{w}$ express the cost for the connection of a filter entry (resp. output) port with a pipe output (resp. entry) port. The FOEIL subformula after the big $\otimes$ ensures that no more than one filter entry port will be connected to the same pipe output port.

Let $w_{1}=\{f_{e}(1),p_{o}(2)\}\{f_{o}(1),p_{e}(1)\}\{f_{e}(2),p_{o}(3)\}\{f_{o}(2),p_{e}(2)\}\{f_{e}(3),p_{o}(4)\}\{f_{o}(3),p_{e}(2)\}$ and $w_{2}=\{f_{e}(1),p_{o}(3)\}\{f_{o}(1),p_{e}(4)\}\{f_{e}(2),p_{o}(4)\}\{f_{o}(2),p_{e}(1)\}\{f_{e}(3),p_{o}(2)\}\{f_{o}(3),p_{e}(4)\}$ that encode two possible implementations of the interactions for the architecture instantiation of Figure 6. Then, the value $\|{\tilde{\psi}}\|(r,w_{1})+\|{\tilde{\psi}}\|(r,w_{2})$ represents for instance, in the semiring of natural numbers the total cost of performing the interactions.

Example 18

(Weighted Repository)* Repository architecture involves two types of components, namely repository and data accessor [14]. Repository component is unique and all data accessors are connected to it. No connection among data accessors exists. Both repository and data accessors have one port each called $p_{r},p_{d}$, respectively. Figure 7 shows the instantiation of parametric weighted Repository architecture for four data accessors.*

The subsequent wFOEIL sentence ${\tilde{\psi}}$ characterizes the parametric Repository architecture with weighted features. Variable set $\mathcal{X}^{(1)}$ refers to instances of repository component and variable set $\mathcal{X}^{(2)}$ to instances of data accessor component.

[TABLE]

Let $K$ be the fuzzy semiring, and consider $a_{1}=\{p_{r}(1),p_{d}(1)\}$, $a_{2}=\{p_{r}(1),p_{d}(2)\}$, $a_{3}=\{p_{r}(1),p_{d}(3)\}$, $a_{4}=\{p_{r}(1),p_{d}(4)\}$ which represent each of the four connections for the architecture instantiation of Figure 7. Then, the value $\|{\tilde{\psi}}\|(r,w)$ for $w=a_{1}a_{2}a_{3}a_{4}$ is the cost for implementing the interactions computed in a fuzzy framework system.

The interactions of parametric weighted architectures discussed in Examples 15-18 can be executed with arbitrary order. Hence, wFOEIL can describe sufficiently parametric weighted architectures with no order restrictions in the allowed interactions. Next, we provide three more examples of architectures with quantitative characteristics, namely weighted Blackboard, weighted Request/Response, and weighted Publish/Subscribe where the order of interactions constitutes a main feature.

Example 19

(Weighted Blackboard)* The subsequent wFOEIL sentence ${\tilde{\psi}}$ encodes the cost of the interactions of weighted Blackboard architecture, described in Example 8, in the parametric setting. We consider three set of variables, namely $\mathcal{X}^{(1)},\mathcal{X}^{(2)},\mathcal{X}^{(3)},$ for the weighted component instances of blackboard, controller, and knowledge sources components, respectively.*

[TABLE]

Example 20

(Weighted Request/Response)* Next we present a wFOEIL sentence ${\tilde{\psi}}$ for weighted Request/Response architecture, described in Example 9, in the parametric setting. We consider the variable sets $\mathcal{X}^{(1)},\mathcal{X}^{(2)},\mathcal{X}^{(3)}$, and $\mathcal{X}^{(4)}$ referring to weighted component instances of service registry, service, client, and coordinator component, respectively.*

[TABLE]

where the wEPIL formula ${\tilde{\xi}}$ is given by:

${\tilde{\xi}}=\#_{w}(p_{n}(y^{(3)})\otimes p_{m}(x^{(4)}))\odot\#_{w}(p_{q}(y^{(3)})\otimes p_{a}(x^{(4)})\otimes p_{g}(y^{(2)}))\odot\\ \text{\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad}\#_{w}(p_{c}(y^{(3)})\otimes p_{d}(x^{(4)})\otimes p_{s}(y^{(2)}))$,

and the EPIL formulas $\theta$ and $\theta^{\prime}$ are given respectively, by

$\theta=\neg(\mathrm{true}*\#(p_{q}(z^{(3)})\wedge p_{a}(y^{(4)})\wedge p_{g}(z^{(2)}))*\mathrm{true})$,

and

$\theta^{\prime}=(\mathrm{true}*\#(p_{q}(z^{(3)})\wedge p_{a}(y^{(4)})\wedge p_{g}(z^{(2)}))*\mathrm{true})\wedge\\ \text{ \qquad\qquad\qquad\qquad\qquad\qquad\qquad\ \ \ \ }\neg(\mathrm{true}*\#(p_{q}(t^{(3)})\wedge p_{a}(y^{(4)})\wedge p_{g}(t^{(2)}))*\mathrm{true}).$**

The EPIL subformula \forall y^{(4)}\forall z^{(3)}\forall z^{(2)}.\big{(}\theta\vee\big{(}\forall t^{(3)}\forall t^{(2)}(z^{(2)}\neq t^{(2)}).\theta^{\prime}\big{)}\big{)} in ${\tilde{\psi}}$ serves as a constraint to ensure that a unique coordinator is assigned to each service.

Example 21

(Weighted Publish/Subscribe)*

We consider weighted Publish/Subscribe architecture, described in Example 10, in the parametric setting. In the subsequent wFOEIL sentence ${\tilde{\psi}}$, we let variable sets $\mathcal{X}^{(1)},\mathcal{X}^{(2)},\mathcal{X}^{(3)}$ correspond to publisher, topic, and subscriber weighted component instances, respectively.*

[TABLE]

Existing work [9, 10, 30, 37] studied the architectures of the presented examples in the qualitative setting. On the other hand, the work of [29, 41, 42] consider no execution order of the weighted interactions, and the parametric setting is considered only in [41].

Observe that in the presented examples, whenever it is defined a unique instance for a weighted component type we may also consider the corresponding set of variables as a singleton.

6 Decidability results for wFOEIL

In this section, we state an effective translation of wFOEIL sentences to weighted automata. For this, we use a corresponding result from [44], namely for every FOEIL sentence we can effectively construct, in exponential time, an expressively equivalent finite automaton. Then, we show that the equivalence of wFOEIL sentences over specific semirings is decidable. For the reader’s convenience we briefly recall basic notions and results on weighted automata.

Let $A$ be an alphabet. A (nondeterministic) weighted finite automaton (WFA for short) over $A$ and $K$ is a quadruple $\mathcal{A}=(Q,in,wt,ter)$ where $Q$ is the finite state set, $in:Q\rightarrow K$ is the initial distribution, $wt:Q\times A\times Q\rightarrow K$ is the mapping assigning weights to transitions of $\mathcal{A}$, and $ter:Q\rightarrow K$ is the terminal distribution.

Let $w=a_{1}\ldots a_{n}\in A^{*}$. A path $P_{w}$ of $\mathcal{A}$ over $w$ is a sequence of transitions $P_{w}=((q_{i-1},a_{i},q_{i}))_{1\leq i\leq n}$. The weight of $P_{w}$ is given by $weight(P_{w})=in(q_{0})\cdot\prod_{1\leq i\leq n}wt(q_{i-1},a_{i},q_{i})\cdot ter(q_{n})$. The behavior of $\mathcal{A}$ is the series $\|\mathcal{A}\|:A^{*}\rightarrow K$ which is determined by $\|\mathcal{A}\|(w)=\sum_{P_{w}}weight(P_{w})$.

Two WFA $\mathcal{A}$ and $\mathcal{A}^{\prime}$ over $A$ and $K$ are called equivalent if $\|\mathcal{A}\|=\|\mathcal{A}^{\prime}\|$. For our translation algorithm, of wFOEIL formulas to WFA, we shall need folklore results in WFA theory. We collect them in the following proposition (cf. for instance [19, 46]).

Proposition 22

Let $\mathcal{A}_{1}=(Q_{1},in_{1},wt_{1},ter_{1})$ and $\mathcal{A}_{2}=(Q_{2},in_{1},wt_{2},ter_{2})$ be two WFA’s over $A$ and $K$. Then, we can construct in polynomial time WFA’s $\mathcal{B},\mathcal{C},\mathcal{D},\mathcal{E}$ over $A$ and $K$ accepting the sum, and the Hadamard, Cauchy and shuffle product of $\|\mathcal{A}_{1}\|$ and $\|\mathcal{A}_{2}\|$, respectively.

Next we present the translation algorithm of wFOEIL formulas to WFA’s. Our algorithm requires a doubly exponential time at its worst case. Specifically, we prove the following theorem.

Theorem 23

Let $pw{\mathcal{B}}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ be a set of parametric weighted components over a commutative semiring $K$, and $r:[n]\rightarrow\mathbb{N}$. Then, for every wFOEIL sentence ${\tilde{\psi}}$ over $pw{\mathcal{B}}$ and $K$ we can effectively construct a WFA $\mathcal{A}_{{\tilde{\psi}},r}$ over $I_{p{\mathcal{B}}(r)}$ and $K$ such that $\|{\tilde{\psi}}\|(r,w)=\|\mathcal{A}_{{\tilde{\psi}},r}\|(w)$ for every $w\in I_{p{\mathcal{B}}(r)}^{*}$. The worst case run time for the translation algorithm is doubly exponential and the best case is exponential.

We shall prove Theorem 23 using the subsequent Proposition 25. For this, we need to slightly modify a corresponding result from [44]. More precisely, we state the next proposition.

Proposition 24

Let $\psi$ be a FOEIL formula over a set $p{\mathcal{B}}=\{B(i,j)\mid i\in[n],j\geq 1\}$ of parametric components. Let also $\mathcal{V}\subseteq\mathcal{X}$ be a finite set of variables containing $\mathrm{free}(\psi)$, $r:[n]\rightarrow\mathbb{N}$, and $\sigma$ a $(\mathcal{V},r)$-assignment. Then, we can effectively construct a finite automaton $\mathcal{A}_{\psi,r,\sigma}$ over $I_{p{\mathcal{B}}(r)}$ such that $(r,\sigma,w)\models\psi$ iff $w\in L(\mathcal{A}_{\psi,r,\sigma})$ for every $w\in I_{p{\mathcal{B}}(r)}^{*}$. The worst case run time for the translation algorithm is exponential and the best case is polynomial.

Proof. We modify the proof of Proposition 23 in [44] as follows. If $\psi=\mathrm{true}$, then we consider the complete finite automaton $\mathcal{A}_{\psi,r,\sigma}=(\{q\},I_{p{\mathcal{B}}(r)},q,\Delta,\{q\})$ with $\Delta=\{(q,a,q)\mid a\in I_{p{\mathcal{B}}(r)}\}$. If $\psi=p(x^{(i)})$, then we consider the deterministic finite automaton $\mathcal{A}_{\psi,r,\sigma}=(\{q_{0},q_{1}\},I_{p{\mathcal{B}}(r)},q_{0},\Delta,\{q_{1}\})$ with $\Delta=\{(q_{0},a,q_{1})\mid p(\sigma(x^{(i)}))\in a\}$. Then, we follow accordingly the same induction steps. Concerning the complexity of the translation we use the same arguments (we do not take into account the trivial case $\psi=\mathrm{true}$ where the complexity of the translation is constant).

Proposition 25

Let ${\tilde{\psi}}$ be a wFOEIL formula over a set $pw{\mathcal{B}}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ of parametric weighted components and $K$. Let also $\mathcal{V}\subseteq\mathcal{X}$ be a finite set of variables containing $\mathrm{free}(\psi)$, $r:[n]\rightarrow\mathbb{N}$ and $\sigma$ a $(\mathcal{V},r)$-assignment. Then, we can effectively construct a WFA $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ over $I_{p{\mathcal{B}}(r)}$ and $K$ such that $\|{\tilde{\psi}}\|(r,\sigma,w)=\|\mathcal{A}_{{\tilde{\psi}},r,\sigma}\|(w)$ for every $w\in I_{p{\mathcal{B}}(r)}^{*}$. The worst case run time for the translation algorithm is doubly exponential and the best case is exponential.

Proof. We prove our claim by induction on the structure of the wFOEIL formula ${\tilde{\psi}}$.

• i)

If ${\tilde{\psi}}=k$, then we consider the WFA $\mathcal{A}_{{\tilde{\psi}},r,\sigma}=(\{q\},in,wt,ter)$ over $I_{p{\mathcal{B}}(r)}$ and $K$ with $in(q)=k$, $wt(q,a,q)=1$ for every $a\in I_{p{\mathcal{B}}(r)}$, and $ter(q)=1$.

• ii)

If ${\tilde{\psi}}=\psi$, then we consider the finite automaton $\mathcal{A}_{\psi,r,\sigma}$ derived in Proposition 24. Next, we construct, in exponential time, an equivalent complete finite automaton $\mathcal{A}^{\prime}_{\psi,r,\sigma}=(Q,I_{p{\mathcal{B}}(r)},q_{0},\Delta,F)$. Then, we construct, in linear time, the WFA $\mathcal{A}_{{\tilde{\psi}},r,\sigma}=(Q,in,wt,ter)$ where $in(q)=1$ if $q=q_{0}$ and $in(q)=0$ otherwise, for every $q\in Q$, $wt(q,a,q^{\prime})=1$ if $(q,a,q^{\prime})\in\Delta$ and $wt(q,a,q^{\prime})=0$ otherwise, for every $(q,a,q^{\prime})\in Q\times A\times Q$, and $ter(q)=1$ if $q\in F$ and $ter(q)=0$ otherwise, for every $q\in Q$.

• iii)

If ${\tilde{\psi}}={\tilde{\psi}}_{1}\oplus{\tilde{\psi}}_{2}$ or ${\tilde{\psi}}={\tilde{\psi}}_{1}\otimes{\tilde{\psi}}_{2}$ or ${\tilde{\psi}}={\tilde{\psi}}_{1}\odot{\tilde{\psi}}_{2}$ or ${\tilde{\psi}}={\tilde{\psi}}_{1}\varpi{\tilde{\psi}}_{2}$, then we rename firstly variables in $\mathrm{free}({\tilde{\psi}}_{1})\cap\mathrm{free}({\tilde{\psi}}_{2})$ as well variables which are free in ${\tilde{\psi}}_{1}$ (resp. ${\tilde{\psi}}_{2}$) and bounded (i.e., not free) in ${\tilde{\psi}}_{2}$ (resp. in ${\tilde{\psi}}_{1}$). Then, we extend $\sigma$ on $\mathrm{free}({\tilde{\psi}}_{1})\cup\mathrm{free}({\tilde{\psi}}_{2})$ in the obvious way, and construct $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ from $\mathcal{A}_{{\tilde{\psi}}_{1},r,\sigma}$ and $\mathcal{A}_{{\tilde{\psi}}_{2},r,\sigma}$ by applying Proposition 22.

• iv)

If ${\tilde{\psi}}={\textstyle\sum x^{(i)}}.{\tilde{\psi}}^{\prime}$, then we get $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ as the WFA for the sum of the series $\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow j]}\|$, $j\in[r(i)]$ (Proposition 22).

• v)

If $\psi={\textstyle\prod x^{(i)}}.{\tilde{\psi}}^{\prime}$, then we get $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ as the WFA for the Hadamard product of the series $\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow j]}\|$, $j\in[r(i)]$ (Proposition 22).

• vi)

If ${\tilde{\psi}}={\textstyle\sum^{\odot}x^{(i)}}.{\tilde{\psi}}^{\prime}$, then we compute firstly all nonempty subsets $J$ of $[r(i)]$. For every such subset $J=\{l_{1},\ldots,l_{t}\}$, with $1\leq l_{1}<\ldots<l_{k}\leq r(i)$, we consider the WFA $\mathcal{A}_{{\tilde{\psi}},r,\sigma}^{(J)}$ accepting the Cauchy product of the series $\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow l_{1}]}\|,\ldots,\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow l_{t}]}\|$. Then, we get $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ as the WFA for the sum of the series $\|\mathcal{A}_{{\tilde{\psi}},r,\sigma}^{(J)}\|$ with $\emptyset\neq J\subseteq[r(i)]$ (Proposition 22).

• vii)

If ${\tilde{\psi}}={\textstyle\prod^{\odot}x^{(i)}}.{\tilde{\psi}}^{\prime}$, then we get $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ as the WFA for the Cauchy product of the series $\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow j]}\|$, $j\in[r(i)]$ (Proposition 22).

• viii)

If ${\tilde{\psi}}={\textstyle\sum^{\varpi}x^{(i)}}.{\tilde{\psi}}^{\prime}$, then we compute firstly all nonempty subsets $J$ of $[r(i)]$. For every such subset $J=\{l_{1},\ldots,l_{t}\}$, with $1\leq l_{1}<\ldots<l_{k}\leq r(i)$, we consider the WFA $\mathcal{A}_{{\tilde{\psi}},r,\sigma}^{(J)}$ accepting the shuffle product of the series $\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow l_{1}]}\|,\ldots,\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow l_{t}]}\|$. Then, we get $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ as the WFA for the sum of the series $\|\mathcal{A}_{{\tilde{\psi}},r,\sigma}^{(J)}\|$ with $\emptyset\neq J\subseteq[r(i)]$ (Proposition 22).

• ix)

If ${\tilde{\psi}}={\textstyle\prod^{\varpi}x^{(i)}}.{\tilde{\psi}}^{\prime}$, then we get $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ as the WFA for the shuffle product of the series $\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma[x^{(i)}\rightarrow j]}\|$, $j\in[r(i)]$ (Proposition 22).

By our constructions above, we immediately get $\|{\tilde{\psi}}\|(r,\sigma,w)=\|\mathcal{A}_{{\tilde{\psi}},r,\sigma}\|(w)$ for every $w\in I_{p{\mathcal{B}}(r)}^{*}$ . Hence, it remains to deal with the time complexity of our translation algorithm.

Taking into account the above induction steps, we show that the worst case run time for our translation algorithm is doubly exponential. Indeed, if ${\tilde{\psi}}^{\prime}=\psi$ is a FOEIL formula, then our claim holds by (ii) and Proposition 24. Then the constructions in steps (iii)-(v), (vii) and (ix) require a polynomial time (cf. Proposition 22). Finally, the translations in steps (vi) and (viii) require at most a doubly exponential run time because of the following reasons. Firstly, we need to compute all nonempty subsets of $[r(i)]$ which requires an exponential time. Then, due to our restrictions for ${\tilde{\psi}}^{\prime}$ in ${\tilde{\psi}}={\textstyle\sum^{\odot}x^{(i)}}.{\tilde{\psi}}^{\prime}$ and ${\tilde{\psi}}={\textstyle\sum^{\varpi}x^{(i)}}.{\tilde{\psi}}^{\prime}$, and Proposition 24 (cf. also the proof of Proposition 24 in [44]), if a FOEIL subformula $\psi$ occurs in ${\tilde{\psi}}^{\prime}$, then we need a polynomial time to translate it to a finite automaton and by (ii) an exponential time to translate it to a WFA. We should note that if ${\tilde{\psi}}^{\prime}$ contains a subformula of the form $\exists^{*}x^{(i^{\prime})}.\psi^{\prime\prime}$ or $\exists^{\shuffle}x^{(i^{\prime})}.\psi^{\prime\prime}$ or ${\textstyle\sum^{\odot}x^{(i^{\prime})}}.{\tilde{\psi}}^{\prime\prime}$ or ${\textstyle\sum^{\varpi}x^{(i^{\prime})}}.{\tilde{\psi}}^{\prime\prime}$, then the computation of the subsets of $r[i^{\prime}]$ is independent of the computation of the subsets of $r[i]$. On the other hand, the best case run time of the algorithm is exponential. Indeed, if in step (ii) we get $\mathcal{A}_{\psi,r,\sigma}$ in polynomial time (cf. Proposition 24) and we need no translations of steps (vi) and (viii), then the required time is exponential.

Now we are ready to state the proof of Theorem 23.

Proof of Theorem 23. We apply Proposition 25. Since ${\tilde{\psi}}$ is a weighted sentence it contains no free variables. Hence, we get a WFA $\mathcal{A}_{{\tilde{\psi}},r}$ over $I_{p{\mathcal{B}}(r)}$ and $K$ such that $\|{\tilde{\psi}}\|(r,w)=\|\mathcal{A}_{{\tilde{\psi}},r}\|(w)$ for every $w\in I^{*}_{p{\mathcal{B}}(r)}$, and this concludes our proof. The worst case run time for the translation algorithm is doubly exponential and the best case is exponential.

Next we prove the decidability of the equivalence of wFOEIL sentences over (subsemirings of) skew fields. It is worth noting that the complexity remains the same with the one for the decidability of equivalence for FOEIL formulas [44].

Theorem 26

Let $K$ be a (subsemiring of a) skew field, $pw\mathcal{B}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ a set of parametric weighted components over $K$, and $r:[n]\rightarrow\mathbb{N}$ a mapping. Then, the equivalence problem for wFOEIL sentences over $pw{\mathcal{B}}$ and $K$ w.r.t. $r$ is decidable in doubly exponential time.

Proof. It is well known that the equivalence problem for weighted automata, with weights taken in (a subsemiring of) a skew field, is decidable in cubic time (cf. Theorem 4.2 in [46], [47]). Hence, we conclude our result by Theorem 23.

Corollary 27

Let $pw\mathcal{B}=\{wB(i,j)\mid i\in[n],j\geq 1\}$ be a set of parametric weighted components over $\mathbb{Q}$ and $r:[n]\rightarrow\mathbb{N}$ a mapping. Then, the equivalence problem for wFOEIL sentences over $pw{\mathcal{B}}$ and $\mathbb{Q}$ w.r.t. $r$ is decidable in doubly exponential time.

7 Conclusion

In this paper we studied the modelling of architectures for parametric weighted component-based systems. We introduced a weighted first-order extended interaction logic, wFOEIL, over a finite set of ports and a commutative semiring to characterize quantitative aspects of architectures, such as the minimum cost or the maximum probability of the implementation of interactions, depending on the underlying semiring. Our wFOEIL models parametric weighted interactions by preserving their execution order as imposed by the corresponding architecture. Moreover, we showed that the equivalence problem for wFOEIL sentences over (a subsemiring of) a skew field is decidable in doubly exponential time. Furthermore, we applied wFOEIL for describing well-known parametric architectures in the quantitative setting.

Work in progress involves the investigation of the second-order level of our wEPIL over semirings, in order to capture the quantitative aspects of more complicated parametric architectures such as Ring, Pipeline, or Grid (cf. [10, 37]). Future research also includes the study of our weighted logics over alternative weight structures, found in applications, like for instance valuation monoids [20, 29]. Existing work has extensively studied the verification problem for parametric qualitative systems with specific topology or communication rules against invariant properties [9, 10, 45, 55] or temporal properties [4, 8, 13]. On the other hand, a few works have investigated verification problems of probabilistic parametric systems [5, 6, 21]. Therefore, it would be very interesting to study verification problems of parametric weighted systems within our modelling architecture framework. Finally, another research direction is the implementation of our results in component-based frameworks for automating the modelling and architecture identification of arbitrary parametric weighted systems.