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

## Key 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.