Specification and analysis of systems with dynamic structure

In many areas of Computer Science we face systems with dynamic structure, i.e. where components and resources may dynamically join and leave, or even get combined. When analyzing these systems one is not only interested in properties about global behaviours (e.g. correctness or safety), but also about the evolution of single components or of their interrelations. In order to achieve this, logic-based specification languages and techniques equipped with a neat handling of components and their dynamicity are needed. Our solution belongs to the family of quantified μ-calculi, i.e. languages combining quantifiers with the fix-point and modal operators of temporal logics, for which we propose a novel approach to their semantics. We use counterpart models as semantic domain, i.e. labeled transition systems where states are algebras, and transitions are enriched with counterpart relations (partial morphisms) between states, explicitly encoding the evolution of components. Formulae are interpreted as sets of assignments, associating formula variables to state components. Our proposal allows to deal with the peculiarities of the considered systems, and avoids limitations of existing approaches, often enforcing restrictions of the transition relation. Unfortunately, dynamicity may easily lead to infinite-state systems, paradigmatic examples being those with unbounded creation of components. Verification can become intractable, calling for approximation techniques. In this direction, we propose a general notion of model approximation, and exploit it by resorting to a type system which denotes formulae as reflected or preserved, together with an approximated model checking technique based on sets of approximations.