Architectures in parametric component-based systems: Qualitative and quantitative modelling

TL;DR

This paper develops a formal logical framework for modeling and analyzing both qualitative and quantitative aspects of parametric component-based system architectures, including execution order and recursive interactions.

Contribution

It introduces an extended propositional interaction logic with a first-order level for parametric systems, proving key decidability results and extending to weighted architectures over semirings.

Findings

Decidability of equivalence, satisfiability, and validity of the logic formulas.

Effective modeling of well-known architectures using the logic.

Decidability of the weighted logic formulas over skew fields.

Abstract

One of the key aspects in component-based design is specifying the software architecture that characterizes the topology and the permissible interactions of the components of a system. To achieve well-founded design there is need to address both the qualitative and non-functional aspects of architectures. In this paper we study the qualitative and quantitative formal modelling of architectures applied on parametric component-based systems, that consist of an unknown number of instances of each component. Specifically, we introduce an extended propositional interaction logic and investigate its first-order level which serves as a formal language for the interactions of parametric systems. Our logics achieve to encode the execution order of interactions, which is a main feature in several important architectures, as well as to model recursive interactions. Moreover, we prove the decidability of equivalence, satisfiability, and validity of first-order extended interaction logic formulas, and provide several examples of formulas describing well-known architectures. We show the robustness of our theory by effectively extending our results for parametric weighted architectures. For this, we study the weighted counterparts of our logics over a commutative semiring, and we apply them for modelling the quantitative aspects of concrete architectures. Finally, we prove that the equivalence problem of weighted first-order extended interaction logic formulas is decidable in a large class of semirings, namely the class (of subsemirings) of skew fields.

Figures

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$$

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

$$\zeta$$

$$\phi$$

$$\#(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.$$

$$\varphi=\Bigg{(}\#(p_{d}\wedge p_{r})*\bigg{(}\#(p_{d}\wedge p_{n_{1}})\shuffle\#(p_{d}\wedge p_{n_{2}})\shuffle\#(p_{d}\wedge p_{n_{3}})\bigg{)}*\\ \bigg{(}\varphi_{1}\vee\varphi_{2}\vee\varphi_{3}\vee(\varphi_{1}\shuffle\varphi_{2})\vee(\varphi_{1}\shuffle\varphi_{3})\vee(\varphi_{2}\shuffle\varphi_{3})\vee(\varphi_{1}\shuffle\varphi_{2}\shuffle\varphi_{3})\bigg{)}^{+}\Bigg{)}^{+}$$

$${\phi }_i=\#(p_l\wedge p_{t_i})\ast \#(p_e\wedge p_{w_i}\wedge p_a)$$

$$\rho=\#(p_{d}\wedge p_{r})+\#(p_{d}\wedge p_{n_{1}})+\#(p_{d}\wedge p_{n_{2}})+\#(p_{d}\wedge p_{n_{3}})+\\ \big{(}\phi_{1}\sqcup\phi_{2}\sqcup\phi_{3}\sqcup(\phi_{1}+\phi_{2})\sqcup(\phi_{1}+\phi_{3})\sqcup(\phi_{2}+\phi_{3})\sqcup(\phi_{1}+\phi_{2}+\phi_{3})\big{)}$$

$$\varphi=\big{(}\#(p_{e}\wedge p_{r_{1}})\shuffle\#(p_{e}\wedge p_{r_{2}})\big{)}*\big{(}\xi_{1}\shuffle\xi_{2}\big{)}*\\ \Bigg{(}\bigg{(}\varphi_{11}\vee\varphi_{21}\vee(\varphi_{11}*\varphi_{21})\vee(\varphi_{21}*\varphi_{11})\bigg{)}^{+}\bigvee\bigg{(}\varphi_{12}\vee\varphi_{22}\vee(\varphi_{12}*\varphi_{22})\vee(\varphi_{22}*\varphi_{12})\bigg{)}^{+}\bigvee\\ \bigg{(}\big{(}\varphi_{11}\vee\varphi_{21}\vee(\varphi_{11}*\varphi_{21})\vee(\varphi_{21}*\varphi_{11})\big{)}^{+}\shuffle\\ \big{(}\varphi_{12}\vee\varphi_{22}\vee(\varphi_{12}*\varphi_{22})\vee(\varphi_{22}*\varphi_{12})\big{)}^{+}\bigg{)}^{+}\Bigg{)}^{+}$$

$$\varphi_{1}=\bigg{(}\big{(}\xi_{1}*\varphi_{11}\big{)}\vee\big{(}\xi_{1}*\varphi_{12}\big{)}\vee\big{(}\xi_{1}*\varphi_{13}\big{)}\vee\\ \big{(}\xi_{1}*(\varphi_{11}\shuffle\varphi_{12})\big{)}\vee\big{(}\xi_{1}*(\varphi_{11}\shuffle\varphi_{13})\big{)}\vee\\ \big{(}\xi_{1}*(\varphi_{12}\shuffle\varphi_{13})\big{)}\vee\big{(}\xi_{1}*(\varphi_{11}\shuffle\varphi_{12}\shuffle\varphi_{13})\big{)}\bigg{)}$$

$$\varphi_{2}=\bigg{(}\big{(}\xi_{2}*\varphi_{21}\big{)}\vee\big{(}\xi_{2}*\varphi_{22}\big{)}\vee\big{(}\xi_{2}*\varphi_{23}\big{)}\vee\\ \big{(}\xi_{2}*(\varphi_{21}\shuffle\varphi_{22})\big{)}\vee\big{(}\xi_{2}*(\varphi_{21}\shuffle\varphi_{23})\big{)}\vee\\ \big{(}\xi_{2}*(\varphi_{22}\shuffle\varphi_{23})\big{)}\vee\big{(}\xi_{2}*(\varphi_{21}\shuffle\varphi_{22}\shuffle\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 {\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}$$

$$\#\big{(}p_{i_{1}}(x^{(i_{1})})\wedge\ldots\wedge p_{i_{m}}(x^{(i_{m})})\big{)}::=\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_{k\in[n]\setminus\{i_{1},\ldots,i_{m}\}}\bigwedge_{p\in P(k)}\forall x^{(k)}.\neg p(x^{(k)})\bigg{)}.$$

$$\psi ={\forall }^{\ast }{x}^{(2)}\exists x^{(1)}.\#(p_m(x^{(1)})\wedge p_s(x^{(2)})).$$

$$\psi =\exists x^{(1)}{\forall }^{\ast }{y}^{(1)}(x^{(1)}\ne y^{(1)}).\#(p(x^{(1)})\wedge p(y^{(1)})).$$

$$\psi=\forall^{*}x^{(2)}\exists x^{(1)}\exists y^{(1)}(x^{(1)}\neq y^{(1)}).\bigg{(}\#(p_{o}(x^{(1)})\wedge f_{e}(x^{(2)}))\ast\#(p_{e}(y^{(1)})\wedge f_{o}(x^{(2)}))\bigg{)}\bigwedge\\ \qquad\quad\bigg{(}\forall z^{(1)}\forall y^{(2)}.\bigg{(}\big{(}\forall z^{(2)}(y^{(2)}\neq z^{(2)}).\theta_{1}\big{)}\vee\theta_{2}\bigg{)}\bigg{)}$$

$$\psi =\exists x^{(1)}{\forall }^{\ast }{x}^{(2)}.\#(p_r(x^{(1)})\wedge p_d(x^{(2)})).$$

$$\psi=\Bigg{(}\exists x^{(1)}\exists x^{(2)}.\Bigg{(}\#(p_{d}(x^{(1)})\wedge p_{r}(x^{(2)}))*\bigg{(}\forall^{\shuffle}x^{(3)}.\#(p_{d}(x^{(1)})\wedge p_{n}(x^{(3)}))\bigg{)}*\\ \bigg{(}\exists^{\shuffle}y^{(3)}.\big{(}\#(p_{l}(x^{(2)})\wedge p_{t}(y^{(3)}))*\#(p_{e}(x^{(2)})\wedge p_{w}(y^{(3)})\wedge p_{a}(x^{(1)}))\big{)}\bigg{)}^{+}\Bigg{)}\Bigg{)}^{+}.$$

$$\psi=\bigg{(}\exists x^{(1)}.\bigg{(}\big{(}\forall^{\shuffle}x^{(2)}.\#(p_{e}(x^{(1)})\wedge p_{r}(x^{(2)}))\big{)}*\\ \big{(}\forall^{\shuffle}x^{(3)}.(\#(p_{l}(x^{(3)})\wedge p_{u}(x^{(1)}))*\#(p_{o}(x^{(3)})\wedge p_{t}(x^{(1)})))\big{)}\bigg{)}\bigg{)}*\\ \bigg{(}\exists^{\shuffle}y^{(2)}\exists x^{(4)}\exists^{*}y^{(3)}.\xi\wedge\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{)}^{+}$$

$$\psi=\Bigg{(}\exists^{\shuffle}x^{(2)}.\Bigg{(}\bigg{(}\exists^{\shuffle}x^{(1)}.\big{(}\#(p_{a}(x^{(1)})\wedge p_{n}(x^{(2)}))*\#(p_{t}(x^{(1)})\wedge p_{r}(x^{(2)}))\big{)}\bigg{)}*\\ \bigg{(}\exists^{\shuffle}x^{(3)}.\big{(}\#(p_{e}(x^{(3)})\wedge p_{c}(x^{(2)}))*\#(p_{g}(x^{(3)})\wedge p_{s}(x^{(2)}))*\#(p_{d}(x^{(3)})\wedge p_{f}(x^{(2)}))\big{)}\bigg{)}\Bigg{)}\Bigg{)}^{+}.$$

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

$${\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}}=\Bigg{(}\#_{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{)}^{\oplus}\Bigg{)}^{\oplus}$$

$${\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{)}^{\oplus}\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{)}^{\oplus}\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{)}^{\oplus}\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{)}^{\oplus}\bigg{)}^{\oplus}\Bigg{)}^{\oplus}$$

Full text

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

1. Introduction

Well-founded design is a key principle for complex systems in order to guarantee correctness and performance. Rigorous formalisms in systems engineering are mainly component-based that allow reconfigurability and validation [BS08]. Component-based design lies in constructing multiple components which coordinate through their interfaces in order to generate the global model for a system [GS11]. In such a setting, one of the main issues in the modelling process is defining the communication patterns of systems. Coordination principles among components can be specified by means of architectures, which characterize the permissible interactions and their implementation order, as well as the underlying topology of the systems [MBBS16b, MG16]. Architectures have been proved important in the modelling of systems since they enforce design rules on the components, and hence ensure correctness by construction with respect to basic properties such as mutual exclusion [BHM19, BIS19a, KG06, MBBS16b].

The formal modelling of architectures is a well-known problem of component-based systems and has been investigated with versatile approaches. Some existing frameworks focus on modelling only the components’ connections [MBBS16b, PR17], while other integrate the specification of components’ behavior and communication in order to express requirements [BIS19a, MG16]. In some cases the proposed formal approaches are further supported by graphical languages for characterizing architectures or tools for the verification of component-based systems and their architectures (cf. [KG06, KKW*+*16, MBBS16a, MT00]). Although, there is several work on the qualitative modelling of architectures, this has not been the case for their quantitative aspects. In this paper we propose a formal approach for the characterization of architectures where components’ communication is expressed without incorporating their behavior. Moreover, our framework addresses not only the qualitative but also the weighted setting for specifying architectures, which is the main novelty of our contribution. The consideration of the quantitative properties of architectures is crucial for the efficient design of component-based systems. Cross-cutting concerns involve timing constraints, available resources, energy consumption, probabilities, etc., for implementing the communication among the systems’ components. Consequently, in order to model such optimization issues there is need to study architectures in the weighted setup [ADFL19, BF13, PR17].

The current paper introduces a generic framework for the qualitative and quantitative modelling of architectures applied to a wide class of large systems, and specifically to parametric systems. Parametric systems are component-based systems found in several applications including communication protocols, concurrent processes, and distributed algorithms [AD16, BJK*+*16, DYBH12]. Parametric systems are constructed by a finite number of component types whose number of instances is unknown, i.e., is a parameter for the system. Hence, specifying the architecture of parametric systems is challenging since their components’ number is not known in advance, affecting in turn the interactions that define their communication. On the other hand, efficient characterization of architectures is important in parametric systems’ design for identifying decidable classes of their verification problem, that is undecidable in general if unbounded data is exchanged [AKR*+*18, BJK*+*16, EGLM16].

The formal characterization of parametric architectures proposed in this work is logic-based. In particular, we firstly introduce and investigate a first-order extended interaction logic, namely FOEIL, that models efficiently the qualitative characteristics of parametric architectures. In turn we consider its weighted counterpart, weighted FOEIL over a commutative semiring $K$, in order to address the corresponding non-functional aspects. In contrast to existing logics for modelling parametric architectures [BIS19a, BIS19b, KKW*+*16, MBBS16b], our FOEIL achieves to encode the execution order of the interactions imposed by the corresponding architecture as well as to describe recursive interactions. Specifically, several parametric architectures found in applications, including Publish/Subscribe and Request/Response, impose restrictions on the order of the permissible interactions [Dai12, ZMJ12]. For instance, in a Publish/Subscribe architecture a subscriber cannot receive a message from a topic of its interest if beforehand a publisher has not transferred the message to the particular topic. On the other hand, distinct subscribers may express their interest to the same topic in any order. Our logic is proved sufficient enough to model such order restrictions. Moreover, we allow recursion in the components’ interactions which in turn implies that we can characterize the subsequent implementation of an architecture during a parametric system’s operation. Then, our weighted FOEIL maintains the qualitative attributes of FOEIL, and also models the quantitative properties of parametric architectures, such as the total cost of the interactions or the probability of the implementation of concrete interactions.

In our setting we model components with the standard formalism of labelled transitions systems (cf. [AP11, APR06, BS08]). Then, communication of components is performed by their associated set of labels, called ports. In turn, architectures are modelled by FOEIL formulas encoding the order and recursion of the respective allowed interactions, which are defined by nonempty sets of ports. The presented logic-based modelling framework of architectures does not require the knowledge of the actual transitions of the components since it is constructed on the corresponding set of ports of the given system. As a result our theory does not consider the components’ behavior and can be applied to every component-based framework where the system’s interface is described by a set of ports. For the weighted setup we associate each port with a weight that represents the ‘cost’ of its participation in an interaction. The weights of the ports range over a commutative semiring $K$ and we formalize the quantitative aspects of parametric architectures by weighted FOEIL formulas over $K$. In particular, the contributions of the current paper are the following:

(1) We introduce Extended Propositional Interaction Logic (EPIL for short) over a finite set of ports, which augments PIL from [MBBS16b] with three operators namely the concatenation operator $*$, the shuffle operator $\shuffle$, and the iteration operator +. In contrast to classical PIL, where the satisfaction relation is checked against interactions (nonempty sets of ports), the formulas of EPIL are interpreted over finite words whose letters are interactions over the given set of ports. Intuitively, the semantics of concatenation operator specifies consecutive interactions while the semantics of shuffle operator encodes interleaving, i.e., all possible orders for the execution of permissible interactions in the system. Moreover, the iteration operator serves for modelling recursive interactions in the architecture. We apply EPIL formulas for formalizing the architectures of component-based systems with ordered interactions, and specifically we present three examples with the architectures Blackboard [Cor91], Request/Response [Dai12], and Publish/Subscribe [EFGK03].

(2) We introduce the first-order level of EPIL, namely First-Order Extended Interaction Logic (FOEIL for short), as a modelling language for the architectures of parametric systems. The syntax of FOEIL is equipped with the syntax of EPIL, the common existential and universal quantifiers, and four new quantifiers, namely existential and universal concatenation and shuffle quantifiers. The new quantifiers achieve to encode the partial and whole participation of component instances in sequential and interleaved interactions of parametric architectures. For the semantics of FOEIL we consider triples consisting of a mapping defining the number of component instances in the parametric system, an assignment that attributes a unique identifier to the ports of each component instance, and a finite word of interactions.

(3) We show the expressiveness of FOEIL by providing several examples for architectures of parametric component-based systems. In particular we consider the architectures Blackboard, Request/Response and Publish/Subscribe which impose orders on the implementation of their interactions, as well as Master/Slave [MBBS16b], Star [MBBS16b], Repository [CGB*+*10], and Pipes/Filters [GS93] whose interactions may be executed in arbitrary order.

(4) We study decidability results related with FOEIL. For this, we firstly state an effective translation of FOEIL formulas to finite automata. The best case run time of our translation algorithm is polynomial and the worst case is exponential. In turn, we obtain the decidability of equivalence and validity for FOEIL sentences in doubly exponential time, and the decidability of satisfiability for FOEIL sentences in exponential time.

(5) 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 [PR17, PR20a] with three new weighted operators, namely the weighted concatenation operator $\odot$, the weighted shuffle operator $\varpi$, and the weighted iteration operator ⊕. Intuitively these operators allow to encode the weight of consecutive, interleaving, and recursive interactions in weighted component-based systems, respectively. We interpret wEPIL formulas as series defined over finite words and $K$. In turn, we study the first-order level of wEPIL, namely weighted First-Order Extended Interaction Logic (wFOEIL for short) over $K$ for modelling parametric weighted architectures. wFOEIL is equipped with the corresponding operators and quantifiers of FOEIL in the weighted setup, and is interpreted against series over $K$.

(6) We provide examples which show that wEPIL and wFOEIL serve sufficiently for modelling the quantitative aspects of architectures with ordered and recursive interactions. Then, for different instantiations of the semiring $K$ in our examples we derive alternative interpretations for the resulting cost of the allowed interactions, that corresponds to some quantitative characteristic. Similarly to the unweighted setting, we show that we can also apply wFOEIL, and hence wEPIL, for expressing weighted architectures whose interactions may be executed in arbitrary order.

(7) Finally, we establish a translation of wFOEIL formulas to weighted automata. We show that the worst case run time for our translation algorithm is doubly exponential and the best case run time is exponential. Then, we prove the decidability of equivalence of wFOEIL sentences in doubly exponential time over a large class of semirings, namely (subsemirings of) skew fields. Therefore, the complexity remains the same with the one for the decidability of equivalence of FOEIL sentences, which depicts the robustness of our theory.

A preliminary version of this paper appeared in [PR20b]. The present version extends the work of [PR20b] as follows:

• We equip EPIL and FOEIL with the iteration operator +, and hence we model the repetition of the interactions in parametric architectures. Therefore, the overall results in the paper have been modified accordingly to incorporate recursion.

• We present extensive descriptions for the examples considered in [PR20b] and we provide several new examples of architectures modelled by FOEIL sentences. Moreover, we present the detailed proofs for the decidability results of FOEIL.

-We introduce a whole new section that actually comprises half of the current contribution, and addresses the quantitative formal modelling of parametric architectures. In particular, we provide the weighted counterparts of EPIL and FOEIL, we apply them on concrete weighted architectures, and we investigate the corresponding decidability results.

The structure of the paper is as follows. In Section $2$ we discuss related work and in Section $3$ we recall the basic notions for component-based systems and interactions. Then, in Section $4$ we introduce the syntax and semantics of EPIL and present examples of architectures defined by EPIL formulas. In Section $5$ we introduce the syntax and semantics of our FOEIL and provide examples of FOEIL sentences describing concrete parametric architectures. Section $6$ deals with the decidability results for FOEIL sentences. Then, in Section $7$, we introduce and study wEPIL and wFOEIL over a commutative semiring. Finally, in Conclusion, we present open problems and future work.

2. Related work

Existing work in parametric architectures has investigated their formal modelling mainly in the qualitative setting. Among the several instantiations of the problem is included the study of static [BIS19a, KKW*+*16] or dynamic architectures [BJMS12, CST18, MG16], of architectures with data [BHM19, Hea16] as well as of the architectures’ composition problem [ABB*+*16, BHM19]. On the other hand, some work focus on the modelling of architectures without considering the underlying behavior of the components [KKW*+*16, MBBS16b, PR17], while other deal with the specification both of components’ behavior and communication [BIS19a, MG16]. In some cases the proposed formal approaches are supported by graphical languages or tools for characterizing and verifying architectures (cf. [KG06, KKW*+*16, MBBS16a, MT00]). In the sequel we present an extensive description of some work, in the qualitative and in the weighted setup, that is closely related with our framework. Our modelling approach differs from each of the work discussed below in at least one of following directions: 1) it is logic-based, 2) it deals with ordering constraints and recursion in the parametric communication, 3) it addresses the quantitative modelling of parametric architectures that has not been considered in most of the existing frameworks.

In [MBBS16b] the authors introduced a Propositional Configuration Logic (PCL for short) as a modelling language for the description of architectures. A configuration was defined as a set of interactions over a given set of ports. PCL formulas were obtained by the formulas of PIL using the operations of union, intersection and complementation, as well as a new operator, called coalescing operator, for expressing combination of configuration sets. PCL was interpreted over configurations and the authors proved the decidability of equivalence of its formulas in an automated way using the Maude language. In [MBBS16b] it was also studied the first- and second-order configuration logic for describing parametric architectures (called styles of architectures in that paper). The first-order level of PCL was applied for modelling Master/Slave, Star, Pipes/Filters, Repository, Blackboard, and Request/Response architectures, while the second-order level of PCL encoded Ring, Grid, and Linear architectures. In the subsequent work [MBBS16a] the authors supported their framework with a graphical language, based on architecture diagrams, for describing architecture styles. Both our FOEIL and the first-order of PCL can express sufficiently the same parametric architectures, while the study of second-order level of EPIL is work in progress. Our contribution with respect to the work of [MBBS16b] is that our logics achieve to model the order of implementing components’ interactions, that cannot be captured by PCL. We further clarify this by Remark 2 presented in Section 4.1 that discusses an example on a Blackboard architecture. Another difference is that we also consider recursion in architectures, and mainly that we investigate the quantitative modelling of parametric architectures that has not been addressed in [MBBS16b].

In [KKW*+*16] the first-order level of propositional interaction logic with arithmetics, namely FOIL, was introduced to describe finitely many interactions for parametric systems in BIP (Behavior-Interaction-Priority) framework (cf. [BS08]). The syntax of FOIL was built on a set of ports (of the parametric components), the common disjunction and conjunction operators, the existential and universal quantifiers, and formulas in Presburger arithmetic. FOIL formulas modelled the permissible interactions of parametric architectures as sets. In [KKW*+*16] the authors provided also a framework and a prototype with FOIL templates for identifying the architecture of a random parametric BIP model, which was then associated with a known verification method for the particular type of communication. FOIL served sufficiently for expressing several classical architectures including token-passing rings, rendezvous cliques, broadcast cliques, and rendezvous stars. However, in contrast to our logic, FOIL cannot encode order restrictions imposed on the execution of interactions since its formulas return sets of interactions. For this, FOIL was not applied for modelling complex architectures such as Request/Response or Publish/Subscribe. On the other hand, the use of arithmetic constraints in FOIL formulas allowed the logic to describe token-passing ring architectures, that in our setting could be expressed by the second-order level of EPIL.

In [BIS19a] the authors introduced Monadic Interaction Logic (MIL for short) as an alternative logic for interactions of parametric systems. MIL syntax was equipped with first-order variables referring to instances of the parametric components, equality checking of variables, state and port symbols, the disjunction and negation operations, as well as with the common existential quantifier of first order variables. Although, MIL achieved to encode rendezvous and broadcast communication in parametric systems, it was not considered for modelling architectures since it did not include cardinality constraints. The authors applied in turn MIL for the development of an automated method for detecting deadlocks in parametric systems. In the same line, in [BIS19b] the authors and introduced Interaction Logic with One Successor (IL1S for short) for describing rendezvous and broadcast communication as well as several architectures in parametric systems. In particular, IL1S preserved the syntax and semantics of MIL with the difference that it also involved a cyclic modulo-type successor function, and hence achieved to model architectures of ring, linear, and pipeline type, as well as architectures with tree-like structures. IL1S was proved to be decidable and was used to define parametric invariants for checking correctness of safety properties in parametric systems.

Our work is positioned with respect to the logics presented in [BIS19a, BIS19b] as follows. FOEIL achieves to model architectures in contrast to MIL that described only the communication type among interactions. On the other hand, IL1S described architectures that in our framework can be expressed with the second-order level of EPIL, which we study in a forthcoming paper. However, the work of [BIS19b] did not include the modelling of more involved architectures such as Request/Response or Publish/Subscribe. Moreover, the semantics of MIL and IL1S formulas did not consider recursive interactions and their execution order imposed by each architecture, which is one of our main contributions. Extending our results for the verification of parametric systems against safety properties, following a methodology similar to the work of [BIS19a, BIS19b], is left as future work.

BIP is a modelling framework that supports the rigorous design of behavior and coordination of component-based systems. One of the main features in BIP framework is ‘priorities among interactions’ in a component-based system (cf. for instance [BS08]). A priority system is determined by a strict partial order $\prec$ among the set of permitted interactions. Hence if $a\prec a^{\prime}$ for two interactions $a$ and $a^{\prime}$, then $a^{\prime}$ must be implemented before $a$ since it has higher priority. It should be clear that the priority system of BIP cannot describe the required orders of interactions in complex architectures. Specifically, the set of strings of interactions satisfying an EPIL sentence containing a shuffle operator, cannot be obtained by any strict partial order among the set of interactions.

Hennessy and Milner introduced in 1985 (cf. [HM85]) a logic, called HML, as a calculus for the specification of concurrent programs and their properties. In [FAI17] the authors investigated $\mu$HML, i.e., HML with recursive formulas expressing least and greatest fixpoints and focused on a fragment of that logic which can be monitored for runtime verification of programs’ execution. That logic succeeded to describe simple client/server type processes but it is far from describing complex architectures. Specifically our shuffle operator cannot be described by means of $\mu$HML.

Coordination of distributed systems was also investigated in [GT19] (cf. also [TG18]). Specifically, the authors developed a theoretical framework and a prototype for studying the realizability problem of coordination in terms of pomsets. In that setting the repetition and order of input and output components’ actions were considered. Though, due to the imposed orders of pomsets, our shuffle operator cannot be sufficiently described in this framework. For instance, the subfomula $\varphi_{1}\shuffle\varphi_{2}$ of the EPIL formula $\varphi$ describing the Publish/Subscribe architecture (cf. Example 2) cannot be described by means of pomsets.

Alternative modelling frameworks for the communication patterns of software components include session types and behavioral contracts (cf. [Hea16]). In [DYBH12] the authors introduced a type theory for multiparty sessions to globally specify parametric communication protocols whose interactions carry data and their topology is specified by the Ring, Star, or Grid architectures. The authors showed that their type-checking algorithm ensured type-safety and deadlock-freedom of parameterised multiparty communication protocols. Moreover, in [CDA16] the authors introduced a novel session type system and a language to describe multi-actor communication in parameterized protocols. The proposed type theory included operators for describing exclusive, sequential, concurrent events as well as their arbitrary reorderings using a shuffling operator. Then the authors applied their type system for static verification of asynchronous communication protocols. In contrast to our setting, the parametric framework of [DYBH12] did not address the sequential and interleaving interactions of processes, while the work of [CDA16] did not consider the modelling problem of architectures in parameterized systems.

Although there has been an abundance of work for parametric systems in the qualitative setting this has not been the case for the quantitative one. Some work for quantitative parametric systems was considered in [ADFL19, BF13, EGLM16, Fou15, KP20, PR17, PR20a]. Specifically, in [EGLM16] the authors studied the model checking problem of population protocols against linear-time specifications. Population protocols form a specific class of parametric systems, in which a set of identical and anonymous finite-state processes interact pairwise through rendezvous synchronization. The authors obtained a decidability result for the qualitative problem i.e., deciding if a linear temporal logic formula holds with probability $1$, while undecidability was proved for the quantitative problem that is deciding if the property holds with at least a given probability. Although the work of [EGLM16] studied the quantitative model checking problem in the parameterized setting, it did not actually modelled the quantitative aspects of parametric communication that we address in our framework. Moreover, in contrast to our approach the systems’ architecture was not considered in the design process of [EGLM16]. As result, the order restrictions and recursion in parametric communication was not addressed in the modelling of the protocols’ topologies.

In [BF13, Fou15] the authors considered broadcast communication and clique’s 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 of [ADFL19] 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. Parametric communication in [ADFL19] was defined by clique’s semantics where every message reached every process, and by reconfigurable semantics where the set of receivers was chosen non-deterministically. Then the decidability of reachability problems were studied for parametric timed broadcast protocols in [ADFL19]. The main difference of our contribution and the work of [ADFL19, BF13, Fou15] is that we introduce a logic-based approach for the quantitative modelling of arbitrary parametric architectures. Also, the topologies of the protocols studied in the aforementioned work did not consider recursion. Moreover, we investigate the modelling problem of more complicated parametric architectures such as Publish/Subscribe or Request/Response. On the other hand, the authors of [ADFL19, BF13, Fou15] obtained several nice verification results for concrete parameterized protocols. Applying our framework for the study of parametric verification is left as a future work direction.

Finally, according to our best knowledge the only weighted logic-based approach for the modelling of architectures is found in the recent work of [KP20, PR17, PR20a]. Specifically, in [PR17, PR20a] the authors studied PCL in the weighted setup for modelling the quantitative aspects of architectures. The formulas of the resulting logic, namely weighted PCL (wPCL for short), were interpreted as polynomials with values over a commutative semiring. Soundness was proved for that logic and the authors obtained the decidability for the equivalence problem of its formulas. In [KP20] the authors extended the work of [PR17, PR20a] and studied weighted PCL over a product valuation monoid. That algebraic structure allowed 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 [KP20, PR17, PR20a] described architectures without addressing ordered or recursive interactions. Parametric weighted architectures were considered only in [PR17] using the weighted first-order level of weighted PCL, namely weighted FOCL. Nevertheless, weighted FOCL considered no execution order of the interactions of parametric weighted 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 we let $A^{+}=A^{*}\setminus\{\varepsilon\}$ where $\varepsilon$ denotes the empty word. For every word $w\in A^{\ast}$ we let $|w|$ denote the length of $w$, i.e., the number of letters comprising $w$. 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]

Let $L_{1},L_{2},L\subseteq A^{*}$ be languages over $A$. Then, the Cauchy product $L_{1}*L_{2}$ of $L_{1}$ and $L_{2}$, the shuffle product $L_{1}\shuffle L_{2}$ of $L_{1}$ and $L_{2}$, and the iteration $L^{+}$ of $L$ are defined respectively, by:

$L_{1}*L_{2}=\{w_{1}w_{2}\mid w_{1}\in L_{1},w_{2}\in L_{2}\}$,

• -

$L_{1}\shuffle L_{2}=\bigcup_{w_{1}\in L_{1},w_{2}\in L_{2}}w_{1}\shuffle w_{2}$,

• -

$L^{+}=\bigcup_{\nu\geq 1}L^{\nu}$,   where $L^{1}=L$, $L^{\nu+1}=L^{\nu}*L$, and $\nu$ is a natural number.

Shuffle operation has been widely studied in formal languages and in concurrency theory in order to model parallel composition semantics of concurrent processes [AI07, Res15]. According to the algebraic definition, the shuffle operator returns the set of all possible interleavings of the corresponding objects. Similarly to the work of [CDA16, Hea16], the motivation to introduce a shuffle type of operator and quantifier in our logics lies in encoding any possible order (interleaving) of sequences of interactions within architectures. The study of parametric systems with concurrent semantics is not considered here, though it could be investigated in future work.

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 monoids $(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 are 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}$. The $\nu$-th iteration $s^{\nu}\in K\left\langle\left\langle A^{*}\right\rangle\right\rangle$ ($\nu\geq 1$) is defined inductively by $s^{1}=s$ and $s^{\nu+1}=s^{\nu}\odot s$, for every natural number $\nu\geq 1$. A series $s$ is called proper if $s(\varepsilon)=0$. Then, the iteration $s^{\oplus}$ of $s$ is defined by $s^{\oplus}=\sum\limits_{\nu\geq 1}s^{\nu}$. If $s$ is proper, then for every $w\in A^{+}$ and $\nu>|w|$ we have $s^{\nu}(w)=0$. Hence, $s^{\oplus}(w)=\sum\limits_{1\leq\nu\leq|w|}s^{\nu}(w)$ for every $w\in A^{+}$.

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

3.3. Component-based systems

In this subsection we deal with component-based systems comprised of a finite number of components of the same or different type. In our setup, components are defined by labelled transition systems (LTS for short) like in several well-known component-based modelling frameworks including BIP [BS08], REO [APR06], and B [AP11]. Next 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. This is justified by the fact that the presented logic-based modelling framework for architectures does not require the knowledge of the actual transitions of the components. Indeed, 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., nonempty sets of ports. Interactions can be represented by formulas of a propositional logic, namely propositional interaction logic (PIL for short), which has been used for developing first- and second-order logics applied for the modelling of parametric architectures [BIS19b, KKW*+*16, MBBS16b].

Let us firstly define the notion of atomic components.

{defi}

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 in the above definition, that every port $p\in P$ occurs at most in one transition. Then, we use this condition in the weighted setup in Section 7 in order to associate a unique weight with each port.

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

We now recall PIL. 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$ and $\Gamma(P)=\mathcal{P}(I(P))\setminus\{\emptyset\}$. 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}$.

Note that PIL differs from propositional logic, since it is interpreted over interactions, and thus the name “interaction” is assigned to it.

Two PIL formulas $\phi,\phi^{\prime}$ are called equivalent, and we denote it by $\phi\equiv\phi^{\prime}$, whenever $a\models_{\mathrm{PIL}}\phi$ iff $a\models_{\mathrm{PIL}}\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}}$. We can describe a set of interactions as a disjunction of PIL formulas. More precisely, let $\gamma=\{a_{1},\ldots,a_{m}\}\in\Gamma(P)$, where $a_{\mu}=\left\{p_{1}^{(\mu)},\ldots,p^{(\mu)}_{l_{\mu}}\right\}\in I(P)$ for every $\mu\in[m]$. Then, the PIL formula $\phi_{\gamma}$ of $\gamma$ is $\phi_{\gamma}=\phi_{a_{1}}\vee\ldots\vee\phi_{a_{m}}$, i.e., $\phi_{\gamma}=\bigvee\limits_{\mu\in[m]}\bigwedge\limits_{\lambda\in[l_{\mu}]}p_{\lambda}^{(\mu)}$.

We can now define component-based systems. For this, let $\mathcal{B}=\{B(i)\mid i\in[n]\}$ be a set of components where $B(i)=(Q(i),P(i),q_{0}(i),R(i))$, for $i\in[n]$. We denote with $P_{\mathcal{B}}=\bigcup_{i\in[n]}P(i)$ the set 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]$. We denote by $I_{\mathcal{B}}$ the set of all interactions of $\mathcal{B}$, i.e.,

[TABLE]

and let $\Gamma_{\mathcal{B}}=\mathcal{P}(I_{\mathcal{B}})\setminus\{\emptyset\}$.

{defi}

A component-based system is a pair $({\mathcal{B}},\gamma)$ 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 $\gamma$ is a set of interactions in $I_{{\mathcal{B}}}$.

The set $\gamma$ of interactions of a component-based system $({\mathcal{B}},\gamma)$ specifies the topology with which the components are connected in the system, i.e., the architecture of the system. Due to discussion before Definition 3.3 we can replace the set of interactions $\gamma$ by its corresponding PIL formula $\phi_{\gamma}$, i.e., in a logical directed notation. Expression of software architectures by logics has been considered in several work and gave nice results (cf. for instance [BIS19b, KKW*+*16, MBBS16b]).

4. Extended propositional interaction logic

One of the most important characteristics of component-based systems is the architecture which specifies the coordination primitives of the connected components. Although PIL can describe nicely several architectures, it does not capture an important feature of more complicated ones: the specified order required for the execution of the interactions. Such architectures, with an increased interest in applications, are for instance the Request/Response and Publish/Subscribe. In [PR20b] we introduced a propositional logic that extends PIL by equipping it with two operators, namely the concatenation $*$ and the shuffle operator $\shuffle$. With that logic we succeeded to represent architectures of component-based systems where the order of the interactions is involved. Specifically, the concatenation operator $*$ modelled sequential interactions and the shuffle operator $\shuffle$ interactions executed with interleaving. Here, we further augment PIL with an iteration operator + that serves to encode sequential (at least one) repetition of interactions. This in turn implies, that the resulting logic allows to describe the ongoing implementation of an architecture during the system’s operation. Moreover, our propositional logic with its first-order level is proved to be a sufficient modelling language for the symbolic representation of architectures of parametric component-based systems.

{defi}

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

[TABLE]

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

The binding strength, in decreasing order, of the operators in EPIL is the following: negation, iteration, 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 will ensure 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 formulas in our EPIL. Furthermore, it contributes to a reasonable complexity of translation of first-order extended interaction logic formulas to finite automata. This in turn implies the decidability of equivalence, satisfiability, and validity of first-order extended interaction logic sentences (cf. Section 6).

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. For the semantics of EPIL formulas, we introduce the subsequent notation. For every EPIL formula $\varphi$ over $P$ and natural number $\nu\geq 1$ we define the EPIL formula $\varphi^{\nu}$ by induction on $\nu$ as follows:

$\varphi^{1}=\varphi$,

• -

$\varphi^{\nu+1}=\varphi^{\nu}*\varphi$.

{defi}

Let $\varphi$ be an EPIL formula over $P$ and $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\zeta_{1}\shuffle\zeta_{2}$   iff   there exist $w_{1},w_{2}\in I(P)^{+}$ such that $w\in w_{1}\shuffle 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$,

• -

$w\models\varphi^{+}$   iff   there exists $\nu\geq 1$ such that $w\models\varphi^{\nu}$.

The empty word is not included in the semantics of EPIL since in our framework we do not consider architectures with no interactions.

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)^{+}$.

It can be easily seen that the concatenation operator is not commutative. The proof of the next proposition is straightforward.

Proposition 1**.**

Let $\varphi,\varphi_{1},\varphi_{2},\varphi_{3}$ be EPIL formulas over $P$. Then,

1. (1)

$\varphi_{1}*(\varphi_{2}*\varphi_{3})\equiv(\varphi_{1}*\varphi_{2})*\varphi_{3}$, 2. (2)

$\varphi*(\varphi_{1}\vee\varphi_{2})\equiv(\varphi*\varphi_{1})\vee(\varphi*\varphi_{2})$, 3. (3)

$(\varphi_{1}\vee\varphi_{2})*\varphi\equiv(\varphi_{1}*\varphi)\vee(\varphi_{2}*\varphi)$.

Now, we define an updated version of component-based systems where in comparison to the one in Definition 3.3, we replace the set of interactions $\gamma$ (equivalently its corresponding PIL formula $\phi_{\gamma}$ representing them) by an EPIL formula.

{defi}

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

We should note that the EPIL formula $\varphi$ in the above definition is defined over $P_{{\mathcal{B}}}$. Nevertheless, we will be interested in words $w$ of interactions in $I_{{\mathcal{B}}}$ satisfying $\varphi$.

Observe that in this work we develop no theory about the computation of the semantics of component-based systems, a problem that will be studied in future work. Though it should be clear that we specify how we model the components of systems in order to formalize the corresponding architectures.

4.1. Examples of architectures described by EPIL formulas

Next we present three examples of component-based models whose architectures have ordered interactions encoded by EPIL formulas. Clearly, there exist several variations of the following architectures and their order restrictions, that EPIL formulas could also model sufficiently by applying relevant modifications. We need to define 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]

{exa}

(Blackboard) We consider a component-based system $({\mathcal{B}},\varphi)$ with the Blackboard architecture. Blackboard architecture is applied to multi-agent systems for solving problems with nondeterministic strategies that result from multiple partial solutions (cf. Chapter 2 in [BMR*+*96],[Cor91]). Applications based on a Blackboard architecture, include planning and scheduling (cf. [SR14]) as well as artificial intelligence [Nii86]. Blackboard architecture involves three component types, one blackboard component, one controller component and the knowledge sources components [BMR*+*96, Cor91, Nii86]. 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. If there is sufficient information for a source to provide its partial solution, then the 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 blackboard.

For our example we consider three knowledge sources components. Therefore, we have ${\mathcal{B}}=\{B(i)\mid i\in[5]\}$ where $B(1),B(2),B(3),B(4),B(5)$ refer to blackboard, controller and the three sources components, respectively. The set of ports of each component is $P(1)=\{p_{d},p_{a}\},P(2)=\{p_{r},p_{l},p_{e}\},$ $P(3)=\{p_{n_{1}},p_{t_{1}},p_{w_{1}}\}$, $P(4)=\{p_{n_{2}},p_{t_{2}},p_{w_{2}}\}$, and $P(5)=\{p_{n_{3}},p_{t_{3}},p_{w_{3}}\}$. Figure 1 depicts an instantiation of the permissible interactions among the five components of our component-based system. Blackboard has two ports $p_{d},p_{a}$ to declare the state of the problem and add the new data as obtained by a knowledge source, respectively. Knowledge sources have three ports $p_{n_{\kappa}},p_{t_{\kappa}},p_{w_{\kappa}}$, for $\kappa=1,2,3$, for being notified about the existing data on blackboard, the trigger of the source, and for writing the partial solution on 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 on blackboard. Here we assume that all knowledge sources are triggered, i.e., that all available sources participate in the architecture. The permissible interactions in the architecture range over $I_{{\mathcal{B}}}$ and are obtained as follows:

• •

The sets $\{p_{d},p_{r}\}$ and $\{p_{d},p_{n_{\kappa}}\}$, for $\kappa=1,2,3$, capture the interactions of blackboard with controller and the three sources, respectively, for presenting the state of the problem. The corresponding connections are shown in Figure 1 by the four black lines.

• •

The sets $\{p_{l},p_{t_{\kappa}}\}$, for $\kappa=1,2,3$, refer to the log process of triggered sources in the controller. The orange lines in Figure 1 depict a possible scenario of such connections between the controller and each of the sources $B(3)$ and $B(5)$.

• •

Finally, the sets $\{p_{e},p_{w_{\kappa}},p_{a}\}$, for ${\kappa}=1,2,3$, refer to the connection of the sources with blackboard through its controller for adding the new data. These interactions are shown with the green lines in Figure 1, for the case that sources $B(3)$ and $B(5)$ have been triggered.

The EPIL formula $\varphi$ describing the ordered and recursive interactions of Blackboard architecture is

[TABLE]

where

[TABLE]

for $i=1,2,3$. The first PIL subformula encodes the connection between blackboard and controller. The EPIL subformula between the two concatenation operators represents the connections of the three knowledge sources with blackboard in order to be informed for existing data. The last part of $\varphi$ captures the connection of some of the three knowledge sources with controller and blackboard for the triggering and the writing process. The use of shuffle operator in $\varphi$ serves for capturing any possible order, among the sources, for implementing the corresponding connections with controller and blackboard. On the other hand, the two concatenation operators in the first line of $\varphi$ ensure respectively that the sources are informed after the controller for the data on blackboard and before the triggering and writing process. The use of the inner iteration operator allows the repetition of the triggering and writing process of some of the sources based on the blackboard’s data at one concrete point. Moreover, the outer iteration operator describes the recursive permissible interactions in the architecture at several points. This implies that as new data are added on blackboard, then the controller and the sources are informed anew in each communication ‘cycle’ for these data, and then the sources decide whether they are able to write on blackboard or not. Therefore, combining the two iteration operators we achieve to describe the subsequent implementation of Blackboard architecture in the given component-based system ${\mathcal{B}}$.

Before our second example we show the expressive difference among EPIL and PCL formulas of [MBBS16b].

Remark 2**.**

Consider the Blackboard architecture presented in the previous example. Then the corresponding PCL formula $\rho$ (cf. [MBBS16b]) describing that architecture is

[TABLE]

where $+$ denotes the coalescing operator, $\sqcup$ denotes the union operator, and

$\phi_{i}=\#(p_{l}\wedge p_{t_{i}})+\#(p_{e}\wedge p_{w_{i}}\wedge p_{a})$**

for $i=1,2,3$.

Then, the PCL formula $\rho$ is interpreted over sets of interactions in $\mathcal{P}(I(P))\setminus\{\emptyset\}$ which trivially cannot express the required order for implementing the interactions. For instance the set of interactions \big{\{}\{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_{e},p_{w_{2}},p_{a}\}\big{\}} satisfies $\rho$ but represents no order of the interactions’ execution.

Note that the first-order logics studied in [BIS19a, BIS19b, KKW*+*16] were built over PIL. Although PIL served as the basis for developing logics that encode parametric architectures (still without addressing ordering constraints), it is far from describing complex architectures like Blackboard, Request/Response, or Publish/Subscribe.

{exa}

(Request/Response)

We consider a component-based system $({\mathcal{B}},\varphi)$ with the Request/Response architecture. These architectures are classical interaction patterns and widely used for web services [Dai12]. A Request/Response architecture refers to clients and services. In order for a service to be made available it should be enrolled in the service registry. The enrollment of a service in the registry allows service consumers, simply called clients, to search the existing services. Once services are signed up, then clients search the corresponding registry and take the address of the services. 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 [MBBS16b] the authors described this process by adding, for each service, a third component type called coordinator. Coordinator takes care that only one client is connected to a service until the process among them is completed.

The Request/Response architecture of our component-based system consists of four component types namely service registry, service, client, and coordinator (Figure 2). For our example we consider seven components, and specifically, the service registry, two services with their associated coordinators, and two clients. Therefore, we have that ${\mathcal{B}}=\{B(i)\mid i\in[7]\}$ where $B(1),\ldots,B(7)$ refer to each of the aforementioned components, respectively. The set of ports of each component is $P(1)=\{p_{e},p_{u},p_{t}\}$, $P(2)=\{p_{r_{1}},p_{g_{1}},p_{s_{1}}\}$, $P(3)=\{p_{r_{2}},p_{g_{2}},p_{s_{2}}\}$, $P(4)=\{p_{m_{1}},p_{a_{1}},p_{d_{1}}\}$, $P(5)=\{p_{m_{2}},p_{a_{2}},p_{d_{2}}\}$, $P(6)=\{p_{l_{1}},p_{o_{1}},p_{n_{1}},p_{q_{1}},p_{c_{1}}\}$, and $P(7)=\{p_{l_{2}},p_{o_{2}},p_{n_{2}},p_{q_{2}},p_{c_{2}}\}$. Figure 2 depicts the permissible interactions among the service registry, service $B(2)$ and the two clients components of our component-based system. The corresponding interactions for service $B(3)$, which have been omitted for simplicity, are derived similarly. 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_{\kappa}},p_{g_{\kappa}},p_{s_{\kappa}}$, for ${\kappa}=1,2$, which establish the connection to the service registry for the signing up of the service, and the connection to a client (via coordinator) for getting a request and responding, respectively. Each client $\kappa$ has five ports denoted by $p_{l_{\kappa}},p_{o_{\kappa}},p_{n_{\kappa}},p_{q_{\kappa}}$ and $p_{c_{\kappa}}$, for ${\kappa}=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. 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_{\kappa}},p_{a_{\kappa}},p_{d_{\kappa}}$, for ${\kappa}=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 allowed interactions in the architecture range over $I_{{\mathcal{B}}}$ and are obtained as follows:

• •

The sets $\{p_{e},p_{r_{\kappa}}\}$ refer the enrollment of the two services in registry, while the sets $\{p_{l_{\kappa}},p_{u}\}$ and $\{p_{o_{\kappa}},p_{t}\}$ express the interactions of the two clients with registry, for $\kappa=1,2$. The corresponding connections are shown in Figure 2 with black and orange color for the services and clients, respectively.

• •

The sets $\{p_{n_{\kappa}},p_{m_{\lambda}}\}$, $\{p_{q_{\kappa}},p_{a_{\lambda}},p_{g_{\lambda}}\}$, $\{p_{c_{\kappa}},p_{d_{\lambda}},p_{s_{\lambda}}\}$ capture the interactions of each of the two clients with the two services through their coordinators, for $\kappa,\lambda=1,2$. The green lines in Figure 2 depict a possible case for these connections, and specifically between the two client components and service $B(2)$ through its coordinator $B(4)$.

Then, the EPIL formula $\varphi$ describing the Request/Response architecture, with its permissible ordered and recursive interactions, is

[TABLE]

where

$\xi_{1}=\#(p_{l_{1}}\wedge p_{u})*\#(p_{o_{1}}\wedge p_{t})$

• -

$\xi_{2}=\#(p_{l_{2}}\wedge p_{u})*\#(p_{o_{2}}\wedge p_{t})$

describe the interactions of the two clients with the service registry and

$\varphi_{11}=\#(p_{n_{1}}\wedge p_{m_{1}})*\#(p_{q_{1}}\wedge p_{a_{1}}\wedge p_{g_{1}})*\#(p_{c_{1}}\wedge p_{d_{1}}\wedge p_{s_{1}})$

• -

$\varphi_{12}=\#(p_{n_{1}}\wedge p_{m_{2}})*\#(p_{q_{1}}\wedge p_{a_{2}}\wedge p_{g_{2}})*\#(p_{c_{1}}\wedge p_{d_{2}}\wedge p_{s_{2}})$

• -

$\varphi_{21}=\#(p_{n_{2}}\wedge p_{m_{1}})*\#(p_{q_{2}}\wedge p_{a_{1}}\wedge p_{g_{1}})*\#(p_{c_{2}}\wedge p_{d_{1}}\wedge p_{s_{1}})$

• -

$\varphi_{22}=\#(p_{n_{2}}\wedge p_{m_{2}})*\#(p_{q_{2}}\wedge p_{a_{2}}\wedge p_{g_{2}})*\#(p_{c_{2}}\wedge p_{d_{2}}\wedge p_{s_{2}})$

encode the connections of each of the two clients with the two services through their coordinators.

The EPIL formula $\varphi$ is interpreted as follows. The two subformulas at the left of the first two concatenation operators encode the interleaving connections of the two services and the two clients with registry, respectively. Then, each of the three subformulas connected with the big disjunctions express that either one of the two clients or both of them (one at each time) are connected with the first service only, the second service only, or both of the services, respectively. Observe that in these subformulas we make use of the concatenation operator for the connection of the two clients with the same service. This results from the fact that the architecture requires that a unique client should be connected with each service through its coordinator. On the other hand, there is no restriction for the connection of a client with multiple services, and hence we use the shuffle operator to connect the corresponding subformulas at the third and fourth line of the EPIL formula $\varphi$. Then, the first iteration operator in EPIL formula $\varphi$ allows the repetition of the interactions of only first, only second, or both of clients with the first service through its coordinator. Analogously, the next four iteration operators encode the recursive interactions for some of the clients with the second service or with both of the services (applied consecutively) through their coordinators. Finally, the use of last iteration operator describes the repetition of the interactions for any of the aforementioned cases.

{exa}

(Publish/Subscribe)

We consider a component-based system $({\mathcal{B}},\varphi)$ with the Publish/Subscribe architecture. The latter is widely used in IoT applications (cf. for instance [ORM15, PJMT17]), and recently in cloud systems [YZJ*+*17] and robotics [MLS*+*20]. Publish/Subscribe architecture involves three types of components, namely publishers, subscribers, and topics. Publishers advertise and transmit to topics the type of messages they are able to produce. Then, subscribers are connected with the 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 [EFGK03].

For our example we consider two publisher components, two topic components and three subscriber components. Hence, we have that ${\mathcal{B}}=\{B(i)\mid i\in[7]\}$ where $B(1),\ldots,B(7)$ refer to the aforementioned components, respectively. The set of ports of each component is $P(1)=\{p_{a_{1}},p_{t_{1}}\},P(2)=\{p_{a_{2}},p_{t_{2}}\},P(3)=\{p_{n_{1}},p_{r_{1}},p_{c_{1}},p_{s_{1}},p_{f_{1}}\},P(4)=\{p_{n_{2}},p_{r_{2}},p_{c_{2}},p_{s_{2}},p_{f_{2}}\},$ $P(5)=\{p_{e_{1}},p_{g_{1}},p_{d_{1}}\}$, $P(6)=\{p_{e_{2}},p_{g_{2}},p_{d_{2}}\}$, and $P(7)=\{p_{e_{3}},p_{g_{3}},p_{d_{3}}\}$. Figure 3 depicts one of the possible instantiations for the interactions among the components of our system. The ports $p_{a_{\kappa}}$ and $p_{t_{\kappa}}$, for $\kappa=1,2$, are used from the 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_{\kappa}}$ and $p_{r_{\kappa}}$, for $\kappa=1,2$, respectively. Ports $p_{c_{\kappa}},p_{s_{\kappa}}$ and $p_{f_{\kappa}}$, for $\kappa=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_{\mu}},p_{g_{\mu}},p_{d_{\mu}}$, for $\mu=1,2,3$, for connecting with the topic (express interest), getting a message from the topic, and disconnecting from the topic, respectively. The permissible interactions in the architecture range over $I_{{\mathcal{B}}}$ which includes the following sets:

• •

The sets $\{p_{a_{\kappa}},p_{n_{\lambda}}\}$ and $\{p_{t_{\kappa}},p_{r_{\lambda}}\}$ that refer to the connections of the two publishers with each of the two topics for advertising and transferring their messages, for $\kappa,\lambda=1,2$. The black lines in Figure 3 depict a possible case for these interactions, and specifically between publisher $B(1)$ with topic $B(3)$ and publisher $B(2)$ with both topics.

• •

The sets $\{p_{c_{\kappa}},p_{e_{\mu}}\}$, $\{p_{s_{\kappa}},p_{g_{\mu}}\}$ and $\{p_{f_{\kappa}},p_{d_{\mu}}\}$ that capture the interactions between topics and subscribers, for $\kappa=1,2$ and $\mu=1,2,3$. Figure 3 represents with orange lines a possible instantiation of these connections, and in particular for topic $B(3)$ with subscribers $B(5)$ and $B(6)$ as well as for topic $B(4)$ with subscriber $B(7)$.

Then, the EPIL formula $\varphi$ for the Publish/Subscribe architecture is \varphi=\big{(}\varphi_{1}\vee\varphi_{2}\vee(\varphi_{1}\shuffle\varphi_{2})\big{)}^{+} with

[TABLE]

and

[TABLE]

where we make use of the following auxiliary subformulas:

$\xi_{1}=\xi_{11}\vee\xi_{12}\vee(\xi_{11}\shuffle\xi_{12})$

• -

$\xi_{2}=\xi_{21}\vee\xi_{22}\vee(\xi_{21}\shuffle\xi_{22})$

encode that each of the two topics connects only with the first publisher $B(1)$, or with the second publisher $B(2)$ or with both of them, and

$\xi_{11}=\#(p_{n_{1}}\wedge p_{a_{1}})*\#(p_{r_{1}}\wedge p_{t_{1}})$

• -

$\xi_{12}=\#(p_{n_{1}}\wedge p_{a_{2}})*\#(p_{r_{1}}\wedge p_{t_{2}})$

• -

$\xi_{21}=\#(p_{n_{2}}\wedge p_{a_{1}})*\#(p_{r_{2}}\wedge p_{t_{1}})$

• -

$\xi_{22}=\#(p_{n_{2}}\wedge p_{a_{2}})*\#(p_{r_{2}}\wedge p_{t_{2}})$

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

$\varphi_{11}=\#(p_{c_{1}}\wedge p_{e_{1}})*\#(p_{s_{1}}\wedge p_{g_{1}})*\#(p_{f_{1}}\wedge p_{d_{1}})$

• -

$\varphi_{12}=\#(p_{c_{1}}\wedge p_{e_{2}})*\#(p_{s_{1}}\wedge p_{g_{2}})*\#(p_{f_{1}}\wedge p_{d_{2}})$

• -

$\varphi_{13}=\#(p_{c_{1}}\wedge p_{e_{3}})*\#(p_{s_{1}}\wedge p_{g_{3}})*\#(p_{f_{1}}\wedge p_{d_{3}})$

• -

$\varphi_{21}=\#(p_{c_{2}}\wedge p_{e_{1}})*\#(p_{s_{2}}\wedge p_{g_{1}})*\#(p_{f_{2}}\wedge p_{d_{1}})$

• -

$\varphi_{22}=\#(p_{c_{2}}\wedge p_{e_{2}})*\#(p_{s_{2}}\wedge p_{g_{2}})*\#(p_{f_{2}}\wedge p_{d_{2}})$

• -

$\varphi_{23}=\#(p_{c_{2}}\wedge p_{e_{3}})*\#(p_{s_{2}}\wedge p_{g_{3}})*\#(p_{f_{2}}\wedge p_{d_{3}})$.

describe the connections of the two topics with each of the three subscribers. Each of $\varphi_{1}$ and $\varphi_{2}$ encode the interactions of first and second topic, respectively, with some of the publisher and subscriber components. The use of the shuffle operator in each of $\varphi_{1}$ and $\varphi_{2}$ expresses that the interactions among distinct subscribers may be executed with any order. Then, the EPIL formula $\varphi$ captures the participation of only the first, or only the second, or both topics in the implementation of the architecture. Since there are no order restrictions for the interactions among multiple topics, the EPIL subformulas $\varphi_{1}$ and $\varphi_{2}$ are connected in $\varphi$ with the shuffle operator. Finally, the use of the iteration operator in EPIL formula $\varphi$ permits the repetition of the interactions of one or both of the topics with some of the available publishers and subscribers.

The presented examples illustrate that EPIL formulas are expressive enough to encode the execution order of the permissible interactions as well as to specify the subsequent implementation of a component-based system’s architecture through recursive interactions. We note that in [PR20b] we described Blackboard, Publish/Subscribe, and Request/Response architectures, without applying any iteration operator, and hence without allowing recursion in the corresponding interactions.

5. Parametric component-based systems

In this section we deal with component-based systems in the parametric setting. Component-based systems considered in Subsection 3.3 are comprised of a finite number of components which are of the same or distinct type. On the other hand, in the parametric setting a component-based model is comprised of a finite number of distinct 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, we consider parametric component-based systems, i.e., component-based systems with infinitely many instances of every component type.

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)$.

Remark 3**.**

Observe that in the parametric setting we use an index “$i$” in order to specify the type of a component. Specifically, we let $B(i,j)$ denote the $j$-th instance of a component of type $i$, for $i\in[n]$ and $j\geq 1$. On the other hand, for simplicity we avoided such a notation for component-based systems in the non-parametric setting. In particular we presented a sequential enumeration of the several, finite in number, components of the same or different type by $B(i)$, for $i\in[n]$. This explains why in the parametric setting we use the term “component type”. For instance in the Request/Response architecture of Example 2, we denote by $B(2),B(3)$ the two service components. On the other hand, in a parametric Request/Response architecture we would let $B(2,1)$ and $B(2,2)$ refer to two component instances of the service component type. For this, we arbitrarily choose $i=2$ to denote the type of service, and in turn we let $j=1,2$ refer to the two instances of that type.

As it is already mentioned, in practical applications we do not know how many instances of each component type are connected at a concrete time. This means that we cannot define interactions of $p\mathcal{B}$ in the same way as we did for finite sets of components. Hence, we need a symbolic representation to describe interactions, and in turn architectures, of parametric systems. For this, we introduce the first-order extended interaction logic which is proved sufficient to describe a wide class of architectures of parametric component-based systems. Similarly to EPIL the semantics of our logic encodes the order and iteration of the interactions implemented within a parametric architecture. Formalization of such aspects is important for constructing well-defined architectures, and hence parametric systems which are less error prone and satisfy most of their requirements [AKR*+*18, BJK*+*16, DYBH12].

5.1. First-order extended interaction logic

In this subsection we introduce the first-order extended interaction logic as a modelling language for describing the interactions of parametric component-based systems. For this, we need to equip EPIL formulas with variables. Due to the nature of parametric systems we need to distinguish variables referring to different component types. Let $p\mathcal{B}=\{B(i,j)\mid i\in[n],j\geq 1\}$ be a set of parametric components. We consider pairwise disjoint countable sets of first-order variables $\mathcal{X}^{(1)},\ldots,\mathcal{X}^{(n)}$ referring to instances of component types $B(1),\ldots,B(n)$, respectively. First-order 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 component type $B(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\}$.

{defi}

Let $p\mathcal{B}=\{B(i,j)\mid i\in[n],j\geq 1\}$ be a set of parametric components. Then the syntax of first-order extended interaction logic (FOEIL for short) 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)}$ are first-order variables in $\mathcal{X}^{(i)}$, $\exists^{*}$ denotes the existential concatenation quantifier, $\forall^{*}$ the universal concatenation quantifier, $\exists^{\shuffle}$ is the existential shuffle quantifier, and $\forall^{\shuffle}$ is the 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}}$. As usual, 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, 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)}$. If $\varphi$ is an EPIL formula over $P_{p{\mathcal{B}}(\mathcal{V})}$, then $\sigma(\varphi)$ is an EPIL formula over $P_{p{\mathcal{B}}(r)}$ which is obtained by $\varphi$ by replacing every port $p(x^{(i)})$ in $\varphi$ by $p(\sigma(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)}^{+}$. As for EPIL formulas, we define for every FOEIL formula $\psi$ over $p{\mathcal{B}}$ and natural number $\nu\geq 1$, the FOEIL formula $\psi^{\nu}$ over $p{\mathcal{B}}$ by induction on $\nu$: $\psi^{1}=\psi$ and $\psi^{\nu+1}=\psi^{\nu}*\psi$. The semantics of formulas of the form $\exists^{*}x^{(i)}.\psi$ and $\forall^{*}x^{(i)}.\psi$ (resp. $\exists^{\shuffle}x^{(i)}.\psi$ and $\forall^{\shuffle}x^{(i)}.\psi$) refer to satisfaction of $\psi$ by subwords of $w$. The subwords correspond to component instances which are determined by the application of the assignment $\sigma$ to $x^{(i)}$, and $w$ results by the $*$ (resp. $\shuffle$) operator among the subwords.

{defi}

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\psi^{+}$ iff there exists $\nu\geq 1$ such that $(r,\sigma,w)\models\psi^{\nu}$,

• -

$(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 exists $1\leq k\leq r(i)$ and $w_{l_{1}},\ldots,w_{l_{k}}\in I_{p{\mathcal{B}}(r)}^{+}$ with $1\leq l_{1}<\ldots<l_{k}\leq r(i)$ such that $w=w_{l_{1}}\ldots w_{l_{k}}$ and $(r,\sigma[x^{(i)}\rightarrow j],w_{j})\models\psi$ for every $j=l_{1},\ldots,l_{k}$,

• -

$(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 exists $1\leq k\leq r(i)$ and $w_{l_{1}},\ldots,w_{l_{k}}\in I_{p{\mathcal{B}}(r)}^{+}$ with $1\leq l_{1}<\ldots<l_{k}\leq r(i)$ such that $w\in w_{l_{1}}\shuffle\ldots\shuffle w_{l_{k}}$ and $(r,\sigma[x^{(i)}\rightarrow j],w_{j})\models\psi$ for every $j=l_{1},\ldots,l_{k}$,

• -

$(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)]$.

By definition of parametric systems, all instances of each component type are identical, hence the order specified above in the semantics of $\exists^{*},\forall^{*},\exists^{\shuffle},\forall^{\shuffle}$ quantifiers causes no restriction in the derived architecture. Moreover, it is important for the complexity of the translation algorithm of FOEIL formulas to finite automata (cf. proof of Proposition 6).

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)$.

Note that in [MBBS16b] the authors considered a universe of component types and hence, excluded in their logic formulas the erroneous types for each architecture. Such a restriction is not needed in our setting since we consider a well-defined set $[n]$ of component types for each architecture. Now we are ready to formally define the concept of a parametric component-based system.

{defi}

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

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

For our examples in the next subsection, we shall need the following macro FOEIL formula. Let $p{\mathcal{B}}=\{B(i,j)\mid i\in[n],j\geq 1\}$ and $1\leq i_{1},\ldots,i_{m}\leq n$ be pairwise different indices. Then we set

[TABLE]

The first $m-1$ conjunctions, in the above formula, express that the ports appearing in the argument of $\#$ participate in the interaction. 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 component 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.

5.2. Examples of FOEIL sentences for parametric architectures

In this subsection we present several examples of FOEIL sentences describing concrete parametric architectures. In what follows we often refer to a component instance simply by instance. Moreover, whenever is defined a unique instance for a component type we may also consider the corresponding set of variables as a singleton.

{exa}

(Parametric Master/Slave) We present a FOEIL sentence for the parametric Master/Slave architecture. Master/Slave architecture concerns two types of components, namely masters and slaves [MBBS16b]. We denote by $p_{m}$ the unique port of master component and by $p_{s}$ the unique port of slave component. Every slave must be connected with exactly one master. Interactions among masters (resp. slaves) are not permitted. An instantiation of the architecture for two masters and two slaves with all the possible cases of the allowed interactions is shown in Figure 4.

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

[TABLE]

In the above sentence, the universal concatenation quantifier accompanied with the existential one encodes that every slave instance should be connected with a master instance through their corresponding ports, and the distinct slave instances may apply these interactions consecutively.

{exa}

(Parametric 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.

The FOEIL sentence $\psi$ for parametric Star architecture is as follows:

[TABLE]

The universal concatenation quantifier preceded by the existential quantifier in $\psi$ encodes that each of the instances in the architecture should be connected with the center instance consecutively.

{exa}

(Parametric Pipes/Filters) Pipes/Filters architecture involves two types of components, namely pipes and filters [GS93]. 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. An instantiation of the architecture for four pipe and three filter components is shown in Figure 6. We denote by $\mathcal{X}^{(1)}$ and $\mathcal{X}^{(2)}$ the sets of variables corresponding to pipe and filter component instances, respectively. The subsequent FOEIL sentence $\psi$ describes the parametric Pipes/Filters architecture.

[TABLE]

where the EPIL formulas $\theta_{1}$ and $\theta_{2}$ are given respectively, by:

\theta_{1}=\big{(}\big{(}(p_{o}(z^{(1)})\wedge f_{e}(y^{(2)}))\shuffle\mathrm{true}\big{)}\wedge\big{(}\neg\big{(}(p_{o}(z^{(1)})\wedge f_{e}(z^{(2)}))\shuffle\mathrm{true}\big{)}\big{)}\big{)}

and

\theta_{2}=\big{(}\neg\big{(}(p_{o}(z^{(1)})\wedge f_{e}(y^{(2)}))\shuffle\mathrm{true}\big{)}\big{)}.

In the above sentence, the universal concatenation quantifier ($\forall^{*}x^{(2)}$) in conjunction with the two existential ones ($\exists x^{(1)},\exists y^{(1)}$) describe that every filter instance is connected with two distinct pipe instances, and these interactions are implemented consecutively. The arguments of $\#$ express the connection of a filter entry (resp. output) port with a pipe output (resp. entry) port excluding by definition erroneous port connections. Then, the subformula after the big conjunction ensures that no more than one filter entry port will be connected to the same pipe output port.

{exa}

(Parametric Repository) Repository architecture involves two types of components, namely repository and data accessor [CGB*+*10]. 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 denoted by $p_{r},p_{d}$, respectively. Figure 7 shows an instantiation of the architecture with four data accessors.

The subsequent FOEIL sentence $\psi$ characterizes the parametric Repository architecture. Variable set $\mathcal{X}^{(1)}$ refers to instances of repository component and variable set $\mathcal{X}^{(2)}$ to instances of data accessor component. Then, the use of the universal concatenation operator combined with the existential one serves to encode that each of the data accessor instances interact with the repository instance in consecutive order.

[TABLE]

Observe that in Examples 5.2-5.2 we use the concatenation quantifier to describe the execution of the interactions for the several component instances. On the other hand, the shuffle quantifier would not provide the encoding of any different implementation of the corresponding architectures. This is because the above parametric architectures do not impose order restrictions on the execution of the permissible interactions. For this reason, we also omit the application of the iteration operator in these examples. Hence, FOEIL can describe sufficiently parametric architectures with no order restrictions in the allowed interactions. Next, we provide three more examples of parametric architectures, namely Blackboard, Request/Response, and Publish/Subscribe, where the order of interactions constitutes a main feature.

{exa}

(Parametric Blackboard) The subsequent FOEIL sentence $\psi$ encodes the interactions of Blackboard architecture, described in Example 4.1, in the parametric setting. We consider three sets of variables, namely $\mathcal{X}^{(1)},\mathcal{X}^{(2)},\mathcal{X}^{(3)}$ for the instances of blackboard, controller, and knowledge sources components, respectively.

[TABLE]

We interpret the above FOEIL sentence as follows: There exists a blackboard and a controller instance ($\exists x^{(1)},\exists x^{(2)}$) so that the former informs the latter for the available data. In turn, the parentheses with the universal shuffle quantifier ($\forall^{\shuffle}x^{(3)}$) encodes that all the sources instances are informed from blackboard in arbitrary order. Finally, the parenthesis with the existential shuffle quantifier ($\exists^{\shuffle}y^{(3)}$) describes the triggering and writing process of some of the sources instances, implemented with interleaving. Similarly to the non-parametric version of the architecture, the iteration operators describe the repetition of the corresponding parametric interactions. An instantiation of parametric Blackboard architecture with three sources is presented in Example 4.1 of Subsection 4.1.

{exa}

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

[TABLE]

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

$\xi=\#(p_{n}(y^{(3)})\wedge p_{m}(x^{(4)}))*\#(p_{q}(y^{(3)})\wedge p_{a}(x^{(4)})\wedge p_{g}(y^{(2)}))*\#(p_{c}(y^{(3)})\wedge p_{d}(x^{(4)})\wedge p_{s}(y^{(2)}))$,

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

and

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

The first two lines of FOEIL sentence $\psi$ express the connections of every service and client instance with the service registry instance, respectively. Moreover, the several instances of services as well as of clients interact with the registry instance in arbitrary order and for this, we use the universal shuffle quantifiers $\forall^{\shuffle}x^{(2)}$ and $\forall^{\shuffle}x^{(3)}$, respectively. Then, the last line of $\psi$ captures that for some of the service instances ($\exists^{\shuffle}y{{}^{(2)}}$) there exist some client instances ($\exists^{\ast}y^{(3)}$) that are interested in the former, and hence are connected consecutively through the services’ coordinator instance ($\exists x^{(4)}$). Recall that only a unique client instance is allowed to interact with a service instance which justifies the use of the concatenation quantifier $\exists^{\ast}y^{(3)}$. On the other hand, the interactions of the distinct service instances with the interested client instances are implemented with interleaving, since there are no order restrictions from the architecture, which is expressed by the shuffle quantifier $\exists^{\shuffle}y{{}^{(2)}}$. Then, the 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 $\psi$ serves as a constraint to ensure that a unique coordinator instance is assigned to each service instance. Finally, the application of the iteration operator allows the repetition of the permissible interactions in the parametric architecture. An instantiation of the parametric architecture for two clients and two services is discussed in Example 2 of Subsection 4.1.

{exa}

(Parametric Publish/Subscribe)

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

[TABLE]

The FOEIL sentence $\psi$ is interpreted as follows: The big parenthesis with the existential shuffle quantifier $\exists^{\shuffle}x^{(1)}$ preceded by $\exists^{\shuffle}x^{(2)}$ describes that given some topic instances, some of the publisher instances advertise and in turn transmit their messages to the former with interleaving. For the same topic instances, in turn, the parenthesis at the second line with the existential shuffle quantifier $\exists^{\shuffle}x^{(3)}$ encodes the arbitrary order among some of the subscriber instances for executing three types of consecutive interactions, namely the connection with the interested subscriber instance, the transfer of the message and their disconnection. The communication steps described above are implemented for the distinct topic instances with interleaving (captured by the first existential shuffle quantifier $\exists^{\shuffle}x^{(2)}$). Finally, the iteration operator is applied to the whole sentence in order to describe the recursion of the aforementioned interactions, and hence models the subsequent implementation of the architecture within the parametric system. Example 2 presented in Subsection 4.1 is an instantiation of the parametric Publish/Subscribe architecture for two publishers, two topics, and three subscribers.

In [MBBS16b] the authors described a simpler version of Request/Response and Blackboard architectures. Though the resulting sets of interactions do not depict the order in which they should be performed (cf. Remark 2). Publish/Subscribe architecture has not been considered in the related work [BIS19b, KKW*+*16, MBBS16b]. A weighted version of Publish/Subscribe architecture was described by a weighted propositional configuration logic formula in [PR17]. Nevertheless, even if we consider that formula without weights, it is not possible to express the required order of the implementation of the interactions. Moreover, the versions of the parametric architectures studied in [BIS19b, KKW*+*16, MBBS16b, PR17] do not allow recursive interactions. Our Examples 5.2, 5.2, and 7 show that for a parametric component-based system with any of the aforementioned architectures, the semantics of the corresponding FOEIL formula encodes the required order of recursive interactions.

6. Decidability results for FOEIL

In this section, we prove decidability results for FOEIL sentences. Specifically, we show that the equivalence and validity problems for FOEIL sentences are decidable in doubly exponential time, whereas the satisfiability problem is decidable in exponential time. For this, we establish an effective translation of every FOEIL formula to an expressive equivalent finite automaton, and hence we take advantage of well-known computational results for finite automata. For the reader’s convenience we briefly recall basic notions and results on finite automata.

Let $A$ be an alphabet. A (nondeterministic) finite automaton (NFA for short) over $A$ is a five-tuple $\mathcal{A}=(Q,A,I,\Delta,F)$ where $Q$ is the finite state set, $I\subseteq Q$ is the set of initial states, $\Delta\subseteq Q\times A\times Q$ is the set of transitions, and $F$ is the final state set.

Let $w=a_{1}\ldots a_{n}\in A^{*}$. A path of $\mathcal{A}$ over $w$ is a sequence of transitions $((q_{i-1},a_{i},q_{i}))_{1\leq i\leq n}$. The path is called successful if $q_{0}\in I$ and $q_{n}\in F$. A word $w\in A^{*}$ is accepted (or recognized) by $\mathcal{A}$ if there a successful path of $\mathcal{A}$ over $w$. The language $L(\mathcal{A})$ of $\mathcal{A}$ is the set of all words accepted by $\mathcal{A}$.

The finite automaton $\mathcal{A}$ is called deterministic (DFA for short) (resp. complete) if $I=\{q_{0}\}$ and for every $q\in Q$ and $a\in A$ there is at most (resp. exactly) one state $q^{\prime}\in Q$ such that $(q,a,q^{\prime})\in\Delta$. In this case we write $\mathcal{A}=(Q,A,q_{0},\Delta,F)$. Two finite automata $\mathcal{A}$ and $\mathcal{A}^{\prime}$ over $A$ are called equivalent if $L(\mathcal{A})=L(\mathcal{A}^{\prime})$. For our translation algorithm of FOEIL formulas to finite automata we shall need folklore results in automata theory. We collect them in the following proposition (cf. for instance [KN01, Sak09a, Sip13]).

Proposition 4**.**

• 1)

Let $\mathcal{A}=(Q,A,I,\Delta,F)$ be an NFA over $A$. Then, we can construct an equivalent complete finite automaton $\mathcal{A}^{\prime}$ with state set $\mathcal{P}(Q)$ over $A$. The run time of the algorithm is exponential.

• 2)

*Let $\mathcal{A}_{1}=(Q_{1},A,I_{1},\Delta_{1},F_{1})$ and $\mathcal{A}_{2}=(Q_{2},A,I_{2},\Delta_{2},F_{2})$ be two NFA’s over $A$. Then, the intersection $L(\mathcal{A}_{1})\cap L(\mathcal{A}_{2})$ is accepted by the NFA $\mathcal{A}=(Q_{1}\times Q_{2},A,I_{1}\times I_{2},\Delta,F_{1}\times F_{2})$ where $\Delta=\{((q_{1},q_{2}),a,(q^{\prime}_{1},q^{\prime}_{2}))\mid(q_{1},a,q^{\prime}_{1})\in\Delta_{1},(q_{2},a,q_{2}^{\prime})\in\Delta_{2}\}$. If $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ are DFA’s, then $\mathcal{A}$ is also a DFA. The finite automaton $\mathcal{A}$ is called the product automaton of $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$. *

The union $L(\mathcal{A}_{1})\cup L(\mathcal{A}_{2})$ is accepted by the NFA $\mathcal{A}^{\prime}=(Q_{1}\cup Q_{2},A,I_{1}\cup I_{2},\Delta_{1}\cup\Delta_{2},F_{1}\cup F_{2})$ where without loss of generality we assume that $Q_{1}\cap Q_{2}=\emptyset$. The NFA $\mathcal{A}^{\prime}$ is called the disjoint union of $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$.

• 3)

If $\mathcal{A}_{1}$, $\mathcal{A}_{2}$, and $\mathcal{A}$ are finite automata over $A$, then we can construct, from $\mathcal{A}_{1}$, $\mathcal{A}_{2}$, and $\mathcal{A}$ NFA’s $\mathcal{B}$, $\mathcal{C}$, and $\mathcal{D}$ accepting respectively, the languages $L(\mathcal{A}_{1})*L(\mathcal{A}_{2})$, $L(\mathcal{A}_{1})\shuffle L(\mathcal{A}_{2})$, and $L(\mathcal{A})^{+}$. The run time for all the constructions is polynomial.

• 4)

Let $\mathcal{A}_{1}=(Q_{1},A,q_{0,1},\Delta_{1},F_{1})$ and $\mathcal{A}_{2}=(Q_{2},A,q_{0,2},\Delta_{2},F_{2})$ be two complete finite automata over $A$. Then, the union $L(\mathcal{A}_{1})\cup L(\mathcal{A}_{2})$ is accepted by the complete finite automaton $\mathcal{A}=(Q_{1}\times Q_{2},A,(q_{0,1},q_{0,2}),\Delta,(Q_{1}\times F_{2})\cup(F_{1}\times Q_{2}))$ where $\Delta=\{((q_{1},q_{2}),a,(q^{\prime}_{1},q^{\prime}_{2}))\mid(q_{1},a,q^{\prime}_{1})\in\Delta_{1},(q_{2},a,q_{2}^{\prime})\in\Delta_{2}\}$.

• 5)

Let $\mathcal{A}=(Q,A,q_{0},\Delta,F)$ be a DFA over $A$. Then, we can construct an equivalent complete finite automaton $\mathcal{A}^{\prime}=(Q\cup\{\bar{q}\},A,q_{0},\Delta^{\prime},F)$ where $\bar{q}$ is a new state and $\Delta^{\prime}=\Delta\cup\{(q,a,\bar{q})\mid\text{ there is no state }q^{\prime}\in Q\text{ such that }(q,a,q^{\prime})\in\Delta\}\cup\{(\bar{q},a,\bar{q})\mid a\in A\}$.

• 6)

Let $\mathcal{A}=(Q,A,q_{0},\Delta,F)$ be a complete finite automaton over $A$. Then, the complement of $L(\mathcal{A})$ is accepted by the complete finite automaton $\bar{\mathcal{A}}=(Q,A,q_{0},\Delta,Q\setminus F)$.

• 7)

Let $\mathcal{A}=(Q,A,I,\Delta,F)$ be an NFA over $A$. Then, we can decide in linear time whether $L(\mathcal{A})=\emptyset$ or not (emptiness problem).

• 8)

Let $\mathcal{A}=(Q,A,I,\Delta,F)$ be an NFA over $A$. Then, we can decide in exponential time whether $L(\mathcal{A})=A^{*}$ or not (universality problem).

Next we present the translation algorithm of FOEIL sentences to finite automata. Our algorithm requires an exponential time at its worst case. Specifically, we state the following theorem.

Theorem 5**.**

Let $\psi$ be a FOEIL sentence over a set $p{\mathcal{B}}=\{B(i,j)\mid i\in[n],j\geq 1\}$ of parametric components and $r:[n]\rightarrow\mathbb{N}$. Then, we can effectively construct a finite automaton $\mathcal{A}_{\psi,r}$ over $I_{p{\mathcal{B}}(r)}$ such that $(r,w)\models\psi$ iff $w\in L(\mathcal{A}_{\psi,r})$ 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.

We shall prove Theorem 5 using the subsequent proposition. For this, we need the following notations. Let $\mathcal{V}\subseteq\mathcal{X}$ be a finite set of variables. For every $i\in[n]$ and $x^{(i)}\in\mathcal{V}$, we define the set $P(i)(x^{(i)})=\{p(x^{(i)})\mid p\in P(i)\text{ and }x^{(i)}\in\mathcal{V}\}$ and let $I_{p{\mathcal{B}}(\mathcal{V})}=\{a\in I(P_{p{\mathcal{B}}(\mathcal{V})})\mid|a\cap P(i)(x^{(i)})|\leq 1\text{ for every }i\in[n]\text{ and }x^{(i)}\in\mathcal{V}\}$. Next let $\sigma$ be a $(\mathcal{V},r)$ assignment and $L$ a language over $I_{p{\mathcal{B}}(\mathcal{V})}$. We shall denote by $\sigma(L)$ the language over $I(P_{p{\mathcal{B}}(r)})$222The language $\sigma(L)$ is not always over $I_{p{\mathcal{B}}(r)}$. For instance, assume that $a\in L$, with $a\in I_{p{\mathcal{B}}(\mathcal{V})}$, $p(x^{(i)}),p^{\prime}(y^{(i)})\in a$ for some $i\in[n]$, $p,p^{\prime}\in P(i)$, and $\sigma(x^{(i)})=\sigma(y^{(i)})$. Then $\sigma(a)\notin I_{p{\mathcal{B}}(r)}$. which is obtained by $L$ by replacing every variable $x\in\mathcal{V}$ by $\sigma(x)$.

Proposition 6**.**

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)$ and $r:[n]\rightarrow\mathbb{N}$. Then, we can effectively construct a finite automaton $\mathcal{A}_{\psi,r}$ over $I_{p{\mathcal{B}}(\mathcal{V})}$ such that for every $(\mathcal{V},r)$-assignment $\sigma$ and $w\in I_{p{\mathcal{B}}(r)}^{+}$ we have $(r,\sigma,w)\models\psi$ iff $w\in\sigma(L(\mathcal{A}_{\psi,r}))\cap I^{+}_{p{\mathcal{B}}(r)}$. The worst case run time for the translation algorithm is exponential and the best case is polynomial.

Proof 6.1**.**

We prove our claim by induction on the structure of the FOEIL formula $\psi$.

• i)

If $\psi=\mathrm{true}$, then we consider the complete finite automaton $\mathcal{A}_{\psi,r}=(\{q\},I_{p{\mathcal{B}}(\mathcal{V})},q,\Delta,\{q\})$ where $\Delta=\{(q,a,q)\mid a\in I_{p{\mathcal{B}}(\mathcal{V})}\}$.

• ii)

If $\psi=p(x^{(i)})$, then we construct the DFA $\mathcal{A}_{\psi,r}=(\{q_{0},q_{1}\},I_{p{\mathcal{B}}(\mathcal{V})},q_{0},\Delta,\{q_{1}\})$ with $\Delta=\{(q_{0},a,q_{1})\mid a\in I_{p{\mathcal{B}}(\mathcal{V})}\text{ and }p(x^{(i)})\in a\}$.

• iii)

If $\psi=\neg\phi^{\prime}$ or $\psi=\phi_{1}\vee\phi_{2}$ where $\phi^{\prime},\phi_{1},\phi_{2}$ are PIL formulas, and $\mathcal{A}_{\phi^{\prime},r}$, $\mathcal{A}_{\phi_{1},r}$, and $\mathcal{A}_{\phi_{2},r}$ are DFA’s, then we construct $\mathcal{A}_{\psi,r}$ by applying Proposition 4(5),(6) and (4), respectively. Trivially, the finite automaton $\mathcal{A}_{\psi,r}$ is deterministic.

• iv)

If $\psi=\zeta_{1}*\zeta_{2}$, then we construct $\mathcal{A}_{\psi,r}$ by taking the finite automaton accepting the Cauchy product of $L(\mathcal{A}_{\zeta_{1},r})$ and $L(\mathcal{A}_{\zeta_{2},r})$ (cf. Proposition 4(3)).

• v)

If $\psi=\zeta_{1}\shuffle\zeta_{2}$, then we construct $\mathcal{A}_{\psi,r}$ by taking the finite automaton accepting the shuffle product of $L(\mathcal{A}_{\zeta_{1},r})$ and $L(\mathcal{A}_{\zeta_{2},r})$ (cf. Proposition 4(3)).

• vi)

If $\psi=\neg\zeta$, then we construct firstly, from $\mathcal{A}_{\zeta,r}$, an equivalent complete finite automaton $\mathcal{A}^{\prime}$ (cf. Proposition 4(1)). Then, we get $\mathcal{A}_{\psi,r}$ from $\mathcal{A}^{\prime}$ by applying Proposition 4(6).

• vii)

If $\psi=\varphi_{1}\vee\varphi_{2}$ or $\psi=\varphi_{1}\wedge\varphi_{2}$ or $\psi=\varphi_{1}*\varphi_{2}$ or $\psi=\varphi_{1}\shuffle\varphi_{2}$ or $\psi=\varphi^{+}$ where $\varphi_{1},\varphi_{2},\varphi$ are EPIL formulas, then we construct $\mathcal{A}_{\psi,r}$ by taking respectively, the disjoint union and the product automaton of $\mathcal{A}_{\varphi_{1},r}$ and $\mathcal{A}_{\varphi_{2},r}$, the NFA accepting the Cauchy product of $L(\mathcal{A}_{\varphi_{1},r})$ and $L(\mathcal{A}_{\varphi_{2},r})$, the NFA accepting the shuffle product of $L(\mathcal{A}_{\varphi_{1},r})$ and $L(\mathcal{A}_{\varphi_{2},r})$, and the NFA accepting the iteration of $L(\mathcal{A}_{\varphi,r})$.

• viii)

If $\psi=x^{(i)}=y^{(i)}$, then we consider the DFA $\mathcal{A}_{\psi,r}=(\{q\},I_{p{\mathcal{B}}(\mathcal{V})},q,\Delta,\{q\})$ where $\Delta=\{(q,a,q)\mid a\in I_{p{\mathcal{B}}(\mathcal{V})}\text{ such that for every }p,p^{\prime}\in P(i)\text{ if }p(x^{(i)})\in a,\text{ then }p^{\prime}(y^{(i)})\notin a\}$.

• ix)

If $\psi=\neg(x^{(i)}=y^{(i)})$, then we get firstly a complete finite automaton by the DFA corresponding to formula $x^{(i)}=y^{(i)}$ (Proposition 4(5)). Then, we obtain $\mathcal{A}_{\psi,r}$ by applying Proposition 4(6).

• x)

If $\psi=\psi_{1}\vee\psi_{2}$ or $\psi=\psi_{1}\wedge\psi_{2}$ or $\psi=\psi_{1}*\psi_{2}$ or $\psi=\psi_{1}\shuffle\psi_{2}$ or $\psi=\psi^{\prime+}$ where $\psi_{1},\psi_{2},\psi^{\prime}$ are FOEIL formulas, then we apply the same arguments as in (vii) for EPIL formulas.

• xi)

If $\psi=\exists x^{(i)}.\psi^{\prime}$, then we get $\mathcal{A}_{\psi,r}$ as the disjoint union of the finite automata $\mathcal{A}_{\psi^{\prime},r}^{(j)}$, $j\in[r(i)]$, where $\mathcal{A}_{\psi^{\prime},r}^{(j)}$ is obtained by $\mathcal{A}_{\psi^{\prime},r}$ by replacing $x^{(i)}$ by $j$ in $I_{p{\mathcal{B}}(\mathcal{V})}$.

• xii)

If $\psi=\forall x^{(i)}.\psi^{\prime}$, then we get $\mathcal{A}_{\psi,r}$ as the product automaton of the finite automata $\mathcal{A}_{\psi^{\prime},r}^{(j)}$, $j\in[r(i)]$, where $\mathcal{A}_{\psi^{\prime},r}^{(j)}$ is obtained by $\mathcal{A}_{\psi^{\prime},r}$ by replacing $x^{(i)}$ by $j$ in $I_{p{\mathcal{B}}(\mathcal{V})}$.

• xiii)

If $\psi=\exists^{*}x^{(i)}.\psi^{\prime}$, then we compute firstly all nonempty subsets $J$ of $[r(i)]$. For every such subset $J=\{l_{1},\ldots,l_{k}\}$, with $1\leq k\leq r(i)$ and $1\leq l_{1}<\ldots<l_{k}\leq r(i)$, we consider the NFA $\mathcal{A}_{\psi,r}^{(J)}$ accepting the Cauchy product of the languages $L(\mathcal{A}_{\psi^{\prime},r}^{(l_{1})}),\ldots,L(\mathcal{A}_{\psi^{\prime},r}^{(l_{k})})$ where $\mathcal{A}_{\psi^{\prime},r}^{(j)}$, $j\in J$, is obtained by $\mathcal{A}_{\psi^{\prime},r}$ by replacing $x^{(i)}$ by $j$ in $I_{p{\mathcal{B}}(\mathcal{V})}$. Then, we get $\mathcal{A}_{\psi,r}$ as the disjoint union of all finite automata $\mathcal{A}_{\psi^{\prime},r}^{(J)}$ with $\emptyset\neq J\subseteq[r(i)]$.

• xiv)

If $\psi=\forall^{*}x^{(i)}.\psi^{\prime}$, then we get $\mathcal{A}_{\psi,r}$ as the NFA accepting the Cauchy product of the languages $L(\mathcal{A}_{\psi^{\prime},r}^{(1)}),\ldots,L(\mathcal{A}_{\psi^{\prime},r}^{(r(i))})$ where $\mathcal{A}_{\psi^{\prime}r}^{(j)}$, $j\in[r(i)]$, is obtained by $\mathcal{A}_{\psi^{\prime},r}$ by replacing $x^{(i)}$ by $j$ in $I_{p{\mathcal{B}}(\mathcal{V})}$.

• xv)

If $\psi=\exists^{\shuffle}x^{(i)}.\psi^{\prime}$, then we compute firstly all nonempty subsets $J$ of $[r(i)]$. For every such subset $J=\{l_{1},\ldots,l_{k}\}$, with $1\leq k\leq r(i)$ and $1\leq l_{1}<\ldots<l_{k}\leq r(i)$, we consider the NFA $\mathcal{A}_{\psi,r}^{(J)}$ accepting the shuffle product of the languages $L(\mathcal{A}_{\psi^{\prime},r}^{(l_{1})}),\ldots,L(\mathcal{A}_{\psi^{\prime},r}^{(l_{k})})$ where $\mathcal{A}_{\psi^{\prime},r}^{(j)}$, $j\in J$, is obtained by $\mathcal{A}_{\psi^{\prime},r}$ by replacing $x^{(i)}$ by $j$ in $I_{p{\mathcal{B}}(\mathcal{V})}$. Then, we get $\mathcal{A}_{\psi,r}$ as the disjoint union of all finite automata $\mathcal{A}_{\psi^{\prime},r}^{(J)}$ with $\emptyset\neq J\subseteq[r(i)]$.

• xvi)

If $\psi=\forall^{\shuffle}x^{(i)}.\psi^{\prime}$, then we get $\mathcal{A}_{\psi,r}$ as the NFA accepting the shuffle product of the languages $L(\mathcal{A}_{\psi^{\prime},r}^{(1)}),\ldots,L(\mathcal{A}_{\psi^{\prime},r}^{(r(i))})$ where $\mathcal{A}_{\psi^{\prime},r}^{(j)}$, $j\in[r(i)]$, is obtained by $\mathcal{A}_{\psi^{\prime},r}$ by replacing $x^{(i)}$ by $j$ in $I_{p{\mathcal{B}}(\mathcal{V})}$.

By our constructions above, we immediately get that for every $(\mathcal{V},r)$-assignment $\sigma$ and $w\in I_{p{\mathcal{B}}(r)}^{+}$ we have $(r,\sigma,w)\models\psi$ iff $w\in\sigma(L(\mathcal{A}_{\psi,r}))\cap 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 exponential. Indeed, if $\psi$ is a PIL formula, then the constructed finite automaton $\mathcal{A}_{\psi,r}$ in steps (i)-(iii) is a DFA and its state-size is polynomial in the size of $\psi$. Specifically, if $\psi=p(x^{(i)})$, then the state-size of $\mathcal{A}_{\psi,r}$ is the same as the size of $\psi$. If $\psi=\neg\zeta$, then by step (vi) we need an exponential time since we construct firstly a complete finite automaton equivalent to the one corresponding to $\zeta$. The cases (iv), (v), (vii)-(xii), (xiv), and (xvi) trivially require polynomial time constructions. Finally, the translations in steps (xiii) and (xv) require an exponential run time since we need to compute all nonempty subsets of $[r(i)]$; every such subset corresponds to a polynomial time construction of a finite automaton. Moreover, this is an upper bound for the complexity in that steps because of the following reasons. Firstly, the FOEIL formula $\psi^{\prime}$ contains no EPIL subformulas of the form $\neg\zeta$. Secondly, if $\psi^{\prime}$ contains a subformula of the form $\exists^{*}x^{(i^{\prime})}.\psi^{\prime\prime}$ or $\exists^{\shuffle}x^{(i^{\prime})}.\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 polynomial since if $\psi$ needs no translation of steps (vi), (xiii), or (xv), then no exponential blow up occurs.*

Proof 6.2** (Proof of Theorem 5).**

We apply Proposition 6. Since $\psi$ is a sentence it contains no free variables. Hence, we get a finite automaton $\mathcal{A}_{\psi,r}$ over $I_{p{\mathcal{B}}(r)}$ such that $(r,w)\models\psi$ iff $w\in L(\mathcal{A}_{\psi,r})$ for every $w\in I^{+}_{p{\mathcal{B}}(r)}$, and this concludes our proof.

We should note that several of the constructions described in the proof of Proposition 6 can be simplified according to the form of the FOEIL sentence $\psi$. For instance consider two ports $p,p^{\prime}$ and the EPIL formula $\varphi=\#(p\wedge p^{\prime})$. Clearly $\varphi$ is satisfied only by the interaction $a=\{p,p^{\prime}\}$ which in turns implies that we get in a straightforward way a finite automaton for $\varphi$. We clarify this in the following example.

{exa}

We consider the parametric Repository architecture and its corresponding FOEIL sentence $\psi=\exists x^{(1)}\forall^{*}x^{(2)}.\#(p_{r}(x^{(1)})\wedge p_{d}(x^{(2)}))$ (cf. Example 5.2). We let $r(1)=1$ and $r(2)=3$, i.e., we assume one repository component instance, as required, and three instances of the data accessor component. Hence, the set of available ports of the architecture w.r.t. $r$ is $\{p_{r}(1),p_{d}(1),p_{d}(2),p_{d}(3)\}$. We consider the interactions $a_{1}=\{p_{r}(1),p_{d}(1)\}$, $a_{2}=\{p_{r}(1),p_{d}(2)\}$, and $a_{3}=\{p_{r}(1),p_{d}(3)\}$ and the DFA’s $\mathcal{A}_{1}=(\{q_{1,0},q_{1,1}\},\{a_{1}\},q_{1,0},\{(q_{1,0},a_{1},\\ q_{1,1})\},\{q_{1,1}\})$, $\mathcal{A}_{2}=(\{q_{2,0},q_{2,1}\},\{a_{2}\},q_{2,0},\{(q_{2,0},a_{2},q_{2,1})\},\{q_{2,1}\})$, and $\mathcal{A}_{3}=(\{q_{3,0},q_{3,1}\},\\ \{a_{3}\},q_{3,0},\{(q_{3,0},a_{3},q_{3,1})\},\{q_{3,1}\})$. Trivially we get $L(\mathcal{A}_{1})=\{a_{1}\}$, $L(\mathcal{A}_{2})=\{a_{2}\}$, and $L(\mathcal{A}_{3})=\{a_{3}\}$, hence we can consider the normalized DFA’s $\mathcal{A}_{1}$, $\mathcal{A}_{2}$, and $\mathcal{A}_{3}$ (cf. for instance [KN01, Sak09a, Sip13]) as the ones corresponding to EPIL formulas $\#(p_{r}(1)\wedge p_{d}(1))$, $\#(p_{r}(1)\wedge p_{d}(2))$, and $\#(p_{r}(1)\wedge p_{d}(3))$, respectively. Then, we construct the DFA $\mathcal{A}_{\psi,r}$, depicted in Figure 8, which corresponds to FOEIL sentence $\psi$ w.r.t. $r$.

Now we are ready to state the decidability result of the equivalence of FOEIL sentences. Specifically, we prove the following theorem.

Theorem 7**.**

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

Proof 6.3**.**

Let $\psi_{1},\psi_{2}$ be FOEIL sentences over $p{\mathcal{B}}$. Then, by Theorem 5 we construct, in exponential time, finite automata $\mathcal{A}_{\psi_{1},r}$ and $\mathcal{A}_{\psi_{2},r}$ such that $(r,w)\models\psi_{i}$ iff $w\in L(\mathcal{A}_{\psi_{i},r})$ for every $w\in I^{+}_{p{\mathcal{B}}(r)}$ and $i=1,2$. The finite automata $\mathcal{A}_{\psi_{1},r}$ and $\mathcal{A}_{\psi_{2},r}$ are in general nondeterministic, hence by Proposition 4(1) we construct complete finite automata $\mathcal{A}^{\prime}_{\psi_{1},r}$ and $\mathcal{A}^{\prime}_{\psi_{2},r}$ equivalent to $\mathcal{A}_{\psi_{1},r}$ and $\mathcal{A}_{\psi_{2},r}$, respectively. In this construction another exponential blow up occurs. Finally, the decidability of equivalence of the complete finite automata $\mathcal{A}^{\prime}_{\psi_{1},r}$ and $\mathcal{A}^{\prime}_{\psi_{2},r}$ requires a linear time (cf. pages 143–145 in [AHU74]), and we are done.

Next, we deal with the decidability of satisfiability and validity results for FOEIL sentences. For this, we recall firstly these notions. More precisely, a FOEIL sentence $\psi$ over $p{\mathcal{B}}$ is called satisfiable w.r.t. $r$ whenever there exists a $w\in I_{p{\mathcal{B}}(r)}^{+}$ such that $(r,w)\models\psi$, and valid w.r.t. $r$ whenever $(r,w)\models\psi$ for every $w\in I_{p{\mathcal{B}}(r)}^{+}$.

Theorem 8**.**

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

Proof 6.4**.**

Let $\psi$ be a FOEIL sentence over $p{\mathcal{B}}$. By Theorem 5 we construct, in exponential time, an NFA $\mathcal{A}_{\psi,r}$ such that $(r,w)\models\psi$ iff $w\in L(\mathcal{A}_{\psi,r})$ for every $w\in I^{+}_{p{\mathcal{B}}(r)}$. Then, $\psi$ is satisfiable iff $L(\mathcal{A}_{\psi,r})\neq\emptyset$ which is decidable in linear time (Proposition 4(7)), and this concludes our proof.

Theorem 9**.**

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

Proof 6.5**.**

Let $\psi$ be a FOEIL sentence over $p{\mathcal{B}}$. By Theorem 5 we construct, in exponential time, an NFA $\mathcal{A}_{\psi,r}$ such that $(r,w)\models\psi$ iff $w\in L(\mathcal{A}_{\psi,r})$ for every $w\in I^{+}_{p{\mathcal{B}}(r)}$. Then, $\psi$ is valid iff $L(\mathcal{A}_{\psi,r})=I^{+}_{p{\mathcal{B}}(r)}$ which is decidable in exponential time (Proposition 4(8)). Hence, we can decide whether $\psi$ is valid or not in doubly exponential time.

7. Parametric weighted architectures

7.1. Weighted EPIL and component-based systems

In this subsection, 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 in the weighted setup.

{defi}

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$, $\varpi$, and ⊕ are the weighted disjunction, conjunction, concatenation, shuffle, and iteration 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$ [PR17, PR20a] and it will be denoted also by $\tilde{\phi}$. The binding strength, in decreasing order, of the operators in wEPIL is the following: weighted iteration, weighted shuffle, weighted concatenation, weighted conjunction, and weighted disjunction.

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

{defi}

Let ${\tilde{\varphi}}$ be a wEPIL formula over $P$ and $K$. Then 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}))$,

• -

$\left\|{\tilde{\varphi}}^{\oplus}\right\|(w)=\sum\limits_{\nu\geq 1}\left\|{\tilde{\varphi}}\right\|^{\nu}$.

By definition, the series $\|{\tilde{\varphi}}\|$ is proper for every wEPIL formula ${\tilde{\varphi}}$ over $P$ and $K$. Two wEPIL formulas ${\tilde{\varphi}}_{1},{\tilde{\varphi}}_{2}$ over $P$ and $K$ are called equivalent and we write ${\tilde{\varphi}}_{1}\equiv{\tilde{\varphi}}_{2}$ if $\|{\tilde{\varphi}}_{1}\|=\|{\tilde{\varphi}}_{2}\|$. Next we define weighted component-based systems. For this, we introduce the notion of a weighted atomic component.

{defi}

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

{defi}

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

Next we consider three examples of weighted component-based models whose architectures have ordered interactions encoded by wEPIL formulas. We recall from the Subsection 4.1 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.

{exa}

(Weighted Blackboard) Consider a weighted component-based system $(w{\mathcal{B}},\tilde{\varphi})$ with the Blackboard architecture described in Example 4.1. We assume the existence of three knowledge source weighted components. Therefore, we have $w{\mathcal{B}}=\{wB(1),wB(2),wB(3),wB(4),wB(5)\}$ referring to blackboard, controller, and the three source weighted components, respectively. Figure 9 depicts each of the weighted components in the system and a possible execution of the permissible interactions. The weight associated with each port in the system is shown at the outside of the port.

The allowed interactions range over $I_{{\mathcal{B}}}$, i.e., they are defined as in the corresponding (unweighted) component-based system ${\mathcal{B}}$ with Blackboard architecture. Then, the wEPIL formula ${\tilde{\varphi}}$ for the weighted Blackboard architecture with three source weighted components is

[TABLE]

where

[TABLE]

for $i=1,2,3$. The first wPIL subformula expresses the cost for the connection of 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. The weighted iteration operators describe the cost of executing recursive interactions in ${\tilde{\varphi}}$. Let $w_{1},w_{2}\in I^{+}_{{\mathcal{B}}}$ encode two distinct sequences of interactions permitted in the given weighted Blackboard architecture. The values $\left\|{\tilde{\varphi}}\right\|(w_{1})$ and $\left\|{\tilde{\varphi}}\right\|(w_{2})$ represent the cost for executing these 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 example, if we consider the max-plus semiring, then the value $\max\{\left\|{\tilde{\varphi}}\right\|(w_{1}),\left\|{\tilde{\varphi}}\right\|(w_{2})\}$ gives information for the communication with the maximum cost. Such information would be important in systems with restricted resources such as battery capacity for instance, in order for the systems to opt for implementing the least ‘expensive’ sequence of interactions.

{exa}

(Weighted Request/Response)

Let $(w{\mathcal{B}},\widetilde{\varphi})$ be a weighted component-based system with the Request/Response architecture presented in Example 2. Our weighted system, shown in Figure 10, consists of seven weighted components, and specifically, the service registry, two services with their associated coordinators, and two clients. Therefore, we have that $w{\mathcal{B}}=\{wB(1),\ldots,wB(7)\}$ referring to each of the aforementioned weighted components, respectively. The allowed interactions range over $I_{{\mathcal{B}}}$, and 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})$

capture the cost of the interactions of the two clients with the service registry 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}})$

describe the connection’s cost of each of the two clients with the two services through their coordinators.

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$ represent 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. Also, the weighted iteration operators in ${\tilde{\varphi}}$ express the cost of repeating the corresponding permissible interactions in the architecture.

Let $w_{1},w_{2}\in I^{+}_{{\mathcal{B}}}$ encode two distinct sequences of interactions in the presented weighted Request/Response architecture. Then, the value $\min\{\left\|{\tilde{\varphi}}\right\|(w_{1}),\left\|{\tilde{\varphi}}\right\|(w_{2})\}$ expresses in min-plus semiring for instance, the communication with the minimum cost. Furthermore, if we interpret the cost as the energy consumption required for implementing the architecture in a network, then we would be able to derive which pattern of interactions, $w_{1}$ or $w_{2}$, requires the minimum energy.

{exa}

(Weighted Publish/Subscribe) Let $(w{\mathcal{B}},\widetilde{\varphi})$ be a weighted component-based system with the Publish/Subscribe architecture described in Example 2. Our weighted system, shown in Figure 11, is comprised of two publisher, two topic, and three subscriber weighted components, hence $w{\mathcal{B}}=\{wB(1),\ldots,wB(7)\}$ referring to these components, respectively. The permissible interactions range over $I_{{\mathcal{B}}}$, and the wEPIL formula ${\tilde{\varphi}}$ for the weighted Publish/Subscribe architecture is ${\tilde{\varphi}}=({\tilde{\varphi}}_{1}\oplus{\tilde{\varphi}}_{2}\oplus({\tilde{\varphi}}_{1}\varpi{\tilde{\varphi}}_{2}))^{\oplus}$ 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 $wB(1)$, or the second publisher $wB(2)$ 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}}\otimes p_{d_{3}})$

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

Each of ${\tilde{\varphi}}_{1}$ and ${\tilde{\varphi}}_{2}$ capture the cost for implementing the interactions of topics $wB(3)$ and $wB(4)$, respectively, with some of the publisher and subscriber components. Then, ${\tilde{\varphi}}_{1}\oplus{\tilde{\varphi}}_{2}\oplus({\tilde{\varphi}}_{1}\varpi{\tilde{\varphi}}_{2})$ expresses the cost for the participation of some of the topics in the architecture, and in turn the use of the weight iteration operator in ${\tilde{\varphi}}$ allows to encode the overall cost of applying these interactions with recursion. Consider for instance the words $w_{1},w_{2}\in I^{+}_{{\mathcal{B}}}$ encoding two interactions in the given weighted Publish/Subscribe architecture. Then, in the Viterbi semiring the value $\max\{\left\|{\tilde{\varphi}}\right\|(w_{1}),\left\|{\tilde{\varphi}}\right\|(w_{2})\}$ shows the sequence of interactions executed with the maximum probability.

7.2. Parametric weighted component-based systems

In this subsection we deal with the parametric extension of weighted component-based systems, i.e., with systems comprised of a finite number of weighted component types where the cardinality of the instances of each type is a parameter for the system.

Let $w{\mathcal{B}}=\{wB(i)\mid i\in[n]\}$ be a set of weighted 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)$.

Now we can introduce the weighted first-order extended interaction logic as a modelling language for describing the weight of the interactions in parametric weighted component-based systems.

As in FOEIL we equip wEPIL formulas with variables. 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 weighted component types $wB(1),\ldots,wB(n)$, respectively.

{defi}

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)}^{+}$, and $K$. 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.

{defi}

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}))$,

• -

$\|{\tilde{\psi}}^{\oplus}\|(r,\sigma,w)=\sum\nolimits_{\nu\geq 1}\|{\tilde{\psi}}\|^{\nu}(r,\sigma,w)$,

• -

$\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 t\leq r(i)}\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 t\leq r(i)}\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})$.

Similarly to the unweighted setup, all instances of each weighted component type in parametric weighted component-based systems are identical. Hence the order specified above in the semantics of $\textstyle\sum\nolimits{{}^{\odot}},\textstyle\prod\nolimits{{}^{\odot}},{\textstyle\sum\nolimits{{}^{\varpi}}},\textstyle\prod\nolimits{{}^{\varpi}}$ weighted quantifiers causes no restriction in the resulting architecture.

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.

{defi}

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 by parametric weighted systems, and we often omit the term “weighted” when we refer to instances.

For our examples in the sequel, 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 weighted 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 weighted component types $i_{1},\ldots,i_{m}$. Finally, the last conjunct in the third line ensures that no ports in instances of remaining weighted component types participate in the interaction. Then we get

[TABLE]

Next we present three examples of wFOEIL sentences describing concrete parametric architectures with ordered interactions in the weighted setup. We note that as for the examples of FOEIL sentences, whenever is defined a unique instance for a weighted component type we may also consider the corresponding set of variables as a singleton.

{exa}

(Parametric weighted Blackboard) We consider weighted Blackboard architecture, described in Example 7.1, in the parametric setting. Therefore, blackboard’s instance interacts with controller’s instance and all the source instances for presenting the current state of the problem. Then, some of the source instances are triggered and logged in the controller in arbitrary order, and in turn these triggered source instances add the new information on blackboard through the controller, again in any order. Hence we need to describe the overall weight for any possible scenario of the aforementioned interactions among the several instances. We consider three sets of variables, namely $\mathcal{X}^{(1)},\mathcal{X}^{(2)},\mathcal{X}^{(3)}$ for the instances of blackboard, controller, and knowledge source weighted components, respectively. Therefore, the wFOEIL sentence ${\tilde{\psi}}$ that encodes the cost of the interactions of parametric weighted Blackboard architecture is

[TABLE]

The weighted subformula $\#_{w}(p_{d}(x^{(1)})\otimes p_{r}(x^{(2)}))$ with the associated quantifiers ${\textstyle\sum x^{(1)}},{\textstyle\sum x^{(2)}}$ expresses the weight for the connection of blackboard with the controller in order for the latter to be informed for the available information. The subformula with the weighted universal shuffle quantifier ${\textstyle\prod^{\varpi}x^{(3)}}$ captures the weight for the respective connections of blackboard with each of the source instances, in arbitrary order. Then, the last subformula with the weighted existential shuffle quantifier ${\textstyle\sum^{\varpi}y^{(3)}}$ encodes the weight for the triggering process of some source instances, and in turn for updating the information in blackboard through the controller. These interactions may be applied in any order for some instances of the source weighted component, which justifies the use of ${\textstyle\sum^{\varpi}}$ for the variables $y^{(3)}$. The application of the weighted iteration operators allows computing the cost of the repetition of the respective interactions in the architecture. An instantiation of the parametric weighted architecture for three sources is presented in Figure 9 of Example 7.1.

{exa}

(Parametric weighted Request/Response) Next we consider the weighted Request/Response architecture, described in Example 9, in the parametric setting. We recall that all the service instances interact with registry through interleaving for their enrollment, and in turn all the client instances interact with registry in any order for taking the address of the service instances. Then, for some of the service instances there exist some client instances that interact with each of them through their associated coordinator instance. The interactions of distinct client instances take place sequentially for the same service instance and with interleaving, otherwise. Next we present a wFOEIL sentence ${\tilde{\psi}}$ encoding the weight of any possible combination of the permissible interactions in parametric weighted Request/Response architecture described above. 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. Therefore,

[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((p_{q}(z^{(3)})\wedge p_{a}(y^{(4)})\wedge p_{g}(z^{(2)}))\shuffle\mathrm{true})$,

and

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

The wFOEIL subformula at the first line of ${\tilde{\psi}}$ with the weighted universal shuffle quantifier ${\textstyle\prod^{\varpi}x^{(2)}}$ encodes the weight of the interleaving interactions between registry instance (${\textstyle\sum x^{(1)}}$) and each of the service instances for their enrollment. The wFOEIL subformula in the second line of ${\tilde{\psi}}$ captures the weight of the interactions between registry and each of the client instances in order for the latter to connect and take the services’ address from registry. These interactions take place in arbitrary order for each of the distinct client instances, hence their weight should be computed accordingly, which is ensured by the use of the weighted universal shuffle quantifier ${\textstyle\prod^{\varpi}x^{(3)}}$. The wFOEIL subformula in the third line of ${\tilde{\psi}}$ expresses the weight of the connections among client and service instances through their coordinator instance, applying the quantifiers ${\textstyle\sum^{\varpi}y^{(2)}}$,${\textstyle\sum x^{(4)}}$, and ${\textstyle\sum^{\odot}y^{(3)}}$. The use of quantifier ${\textstyle\sum^{\odot}y^{(3)}}$ is justified by the fact that only one client instance should interact with each service instance, and hence the respective weight is computed analogously. On the other hand, for different instances of services interleaving among several client instances is permitted, and hence we derive the respective weight by the wFOEIL subformula quantified by ${\textstyle\sum^{\varpi}y^{(2)}}$. 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 instance is assigned to each service instance. Finally, the weighted iteration operator returns the cost of implementing the corresponding interactions with recursion. An instantiation of the parametric weighted architecture for two clients and services is presented in Figure 10 of Example 9.

{exa}

(Parametric weighted Publish/Subscribe)

We consider weighted Publish/Subscribe architecture, described in Example 10, in the parametric setting. We have that for some of the topic instances there are some publisher instances that advertise and transmit their messages. In turn, the same topic instances perform three consecutive interactions with some of the subscriber instances, in order for the latter to express their interest in some messages, receive the requested messages, and disconnect from the topic instances. In each case the interactions among the distinct instances are executed with interleaving. In the subsequent wFOEIL sentence ${\tilde{\psi}}$ we encode the weight of all the possible cases for the aforementioned permissible interactions. We let $\mathcal{X}^{(1)},\mathcal{X}^{(2)},\mathcal{X}^{(3)}$ denote the variable sets that correspond to publisher, topic, and subscriber weighted component instances, respectively.

[TABLE]

We interpret the wFOEIL sentence ${\tilde{\psi}}$ as follows. The wFOEIL subformula in the first line encodes the weight for the interactions among some of the topic instances (weighted existential shuffle quantifier ${\textstyle\sum^{\varpi}x^{(2)}}$) and some publisher instances (weighted existential shuffle quantifier ${\textstyle\sum^{\varpi}x^{(1)}}$) in order for the latter to advertise and in turn transmit their messages to the former. These interactions may take place in any order for the distinct instances, hence the associated weight needs to be computed accordingly. Then, in the second line the subformula with the weighted existential shuffle quantifier ${\textstyle\sum^{\varpi}x^{(3)}}$ captures the weight of three sequential interactions between each of the topic instances, specified in the first line, and some of the subscriber instances. Since there is no restriction for the execution order of these interactions with respect to the distinct instances, we describe their weight with the corresponding weighted shuffle quantifiers. Finally, the use of the weighted iteration operator serves for computing the cost of the ongoing implementation of the architecture. An instantiation of the parametric weighted architecture is shown in Figure 11 of Example 10.

Parametric architectures of the above examples were considered in [BIS19b, MBBS16b], in the qualitative setting, and in the weighted setup in [PR17]. Though, neither the execution order nor the recursion of interactions was assumed in the work of [BIS19b, MBBS16b, PR17].

Note that similarly to FOEIL, its weighted counterpart, wFOEIL, can also be applied for the quantitative modelling of parametric architectures without order restrictions, i.e., for Examples 5.2-5.2. Next we present the wFOEIL sentences describing the parametric weighted Master/Slave and Repository, while the rest of the architectures can be described in the weighted setup analogously.

{exa}

(Parametric weighted Master/Slave) We consider the parametric Master/Slave architecture, described in Example 5.2, in the weighted setting. We let $\mathcal{X}^{(1)},\mathcal{X}^{(2)}$ denote the sets of variables of master and slave weighted component instances, respectively. Then, the wFOEIL sentence ${\tilde{\psi}}$ representing parametric weighted Master/Slave architecture is

[TABLE]

In the above sentence the weighted universal concatenation quantifier accompanied with the existential one encodes the weight of the interactions between every slave instance and a master instance. These connections are applied consecutively for the distinct slave instances, hence their weight is computed accordingly. Consider the instantiation of the architecture with two master and two slave weighted component instances. We let $w_{1}$, $w_{2}$, $w_{3}$, and $w_{4}$ correspond to the four possible connections for the components in the system, defined as in the unweighted case and 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 connections 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 in the semiring of natural numbers for instance, to the total cost for executing these connections in the architecture.

{exa}

(Parametric weighted Repository) The subsequent wFOEIL sentence ${\tilde{\psi}}$ characterizes the parametric Repository architecture, presented in Example 5.2, with weighted features. We let $\mathcal{X}^{(1)}$ and $\mathcal{X}^{(2)}$ denote the variable sets that refer to instances of repository and data accessor weighted components, respectively. Then,

[TABLE]

Let $a_{1}$, $a_{2}$, $a_{3}$, $a_{4}$ represent each of the four interactions for the architecture instantiation of Figure 7, in the weighted setup. Then, the value $\|{\tilde{\psi}}\|(r,w)$ for $w=a_{1}a_{2}a_{3}a_{4}$ is the ‘total’ cost for implementing the interactions in the system.

7.3. Decidability results for wFOEIL

In this subsection, we state an effective translation of wFOEIL sentences to weighted automata. For this, we use the corresponding result of Theorem 5, 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. Firstly, 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 [DKV09, Sak09a]).

Proposition 10**.**

Let $\mathcal{A}_{1}=(Q_{1},in_{1},wt_{1},ter_{1})$, $\mathcal{A}_{2}=(Q_{2},in_{2},wt_{2},ter_{2})$ and $\mathcal{A}=(Q,in,wt,ter)$ be three 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. Moreover, if $\|\mathcal{A}\|$ is proper, then we can construct in polynomial time WFA $\mathcal{A}^{\prime}$ over $A$ and $K$ accepting the iteration of $\|\mathcal{A}\|$.

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

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 11 using the subsequent Proposition 13. For this, we need to slightly modify the corresponding result of Proposition 6. More precisely, we state the next proposition.

Proposition 12**.**

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

We modify the proof of Proposition 6 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 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$. 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 7.2**.**

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 12. 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 10.

• iv)

If ${\tilde{\psi}}={\tilde{\psi}}^{\prime}{{}^{\oplus}}$, then we get $\mathcal{A}_{{\tilde{\psi}},r,\sigma}$ as the WFA for the iteration of the series $\|\mathcal{A}_{{\tilde{\psi}}^{\prime},r,\sigma}\|$ by applying Proposition 10.

• v)

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 10).

• vi)

If ${\tilde{\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 10).

• vii)

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 t\leq r(i)$ and $1\leq l_{1}<\ldots<l_{t}\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 10).

• viii)

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 10).

• ix)

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 t\leq r(i)$ and $1\leq l_{1}<\ldots<l_{t}\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 10).

• x)

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 10).

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 12. Then the constructions in steps (iii)-(vi), (viii) and (x) require a polynomial time (cf. Proposition 10). Finally, the translations in steps (vii) and (ix) 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 12 (recall also the proof of Proposition 6), 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 12) and we need no translations of steps (vii) and (ix), then the required time is exponential.

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

Proof 7.3** (Proof of Theorem 11).**

We apply Proposition 13. 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 sentences (see Section 6).

Theorem 14**.**

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

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.10 in [Sak09a], [Sak09b]). Hence, we conclude our result by Theorem 11.

Corollary 15**.**

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.

8. Conclusion

Efficient modelling of architectures plays a key role in component-based systems in order to be well-defined. In this paper we propose the formal study of architectures for parametric component-based systems that consist of a finite number of component types with an unknown number of instances. Specifically, we introduce a propositional logic, EPIL, which augments PIL from [MBBS16b] with a concatenation, a shuffle, and an iteration operator. We then interpret EPIL formulas on finite words over the set of interactions defined for a given set of ports. We also study FOEIL, the first-order level of EPIL, as a modelling language for the architectures of parametric systems. EPIL and FOEIL are proved expressive enough to return the permissible interactions and the order restrictions of architectures, as well as to encode recursive interactions. Several examples are presented for modelling parametric architectures with or without ordered interactions by FOEIL sentences. Also, we show that the equivalence and validity problems for FOEIL sentences are decidable in doubly exponential time, and the satisfiability problem for FOEIL sentences is decidable in exponential time. Moreover, we show the robustness of our theory by extending our results for the quantitative modelling of parametric architectures. For this, we introduce and study wEPIL and wFOEIL over a commutative semiring. Our weighted logics maintain the qualitative attributes of EPIL and FOEIL, and also model the quantitative properties of architectures, such as the ‘total’ cost or the maximum probability of implementing concrete interactions. We show that the equivalence problem for wFOEIL sentences over (a subsemiring of) a skew field is decidable in doubly exponential time, hence the complexity remains the same with the one for the decidability of FOEIL sentences. Furthermore, we apply wFOEIL for describing the quantitative aspects of several parametric architectures.

Work in progress involves the study of the second-order level of EPIL and wEPIL in order to model parametric architectures in the qualitative and weighted setup, respectively, that cannot be formalized by first-order logics such as Ring, Linear, and Grid [DYBH12, MBBS16b]. Future work is also investigating the verification problem of parametric systems against formal properties [AD16, BIS19b], and specifically the application of architectures modelled by our logics for studying the behavior and proving properties (such as deadlock-freedom) in parametric systems. Moreover, it would be interesting to extend our logic-based framework for the investigation of dynamic and reconfigurable architectures [BJMS12, CST18, MG16] as well as for addressing the architecture composition problem [ABB*+*16, BHM19]. Another research direction is the study of our logics over alternative weight structures, found in applications, like for instance valuation monoids [DM11, KP20]. Formal approaches for architectures are often extended with tools or graphical languages for supporting architectures’ specification (cf. [APR06, KG06, KKW*+*16, MBBS16a, MT00]). Therefore, in addition to theoretical directions, future work includes also the development of a tool and a language in order to facilitate the architecture modelling and identification process of parametric (weighted) systems. Finally, in a subsequent work we investigate parametric systems and their architectures in the fuzzy framework in order to address uncertainty and imprecision resulting from the components’ communication.

Acknowledgment

We are deeply grateful to Simon Bliudze for valuable discussions on a previous version of the paper. Also, we thank anonymous referees for their constructive comments and suggestions that brought the paper in its current form.