Abstract Epistemic ensembles are systems of knowledge-based agents capable of accessing, sharing, and updating information about themselves and their peers. These agents can operate on shared or local epistemic states through actions that dynamically alter the knowledge of some or all members of the ensemble. To support abstract reasoning over such systems, we introduce the notion of focus set — a selected set of logical formulæ that provide an abstraction from the underlying system state. Based on this abstraction, we define global and distributed symbolic representations of epistemic states, along with representable epistemic actions that enable efficient symbolic updates. For formal analysis, we define a generic operational semantics and develop and relate three complementary semantic frameworks: (1) a semantic environment, where system states are modelled as epistemic states, (2) a symbolic environment, where knowledge is represented as sets of logical formulæ, and (3) a distributed environment, represented by a family of local knowledge bases where each agent has its own local symbolic state. We establish a correspondence between these environments via a notion of relative elementary equivalence. Our main result demonstrates that equivalent configurations simulate each other’s behaviour and satisfy the same dynamic epistemic formulæ, ensuring representational consistency across all three perspectives. This provides a robust foundation for reasoning about distributed knowledge and belief dynamics in cooperative multi-agent systems.

Abstract Adaptive systems are designed to modify their behaviour at runtime in response to dynamically changing and open-ended environments as well as evolving requirements. Such systems may operate as individual adaptive entities or as collective adaptive systems composed of multiple collaborating components. Rigorous engineering of these systems requires appropriate methods, models, and tools that ensure reliability, correctness, and alignment with their intended purpose. This paper introduces the second part of the special section on Rigorous Engineering of Collective Adaptive Systems. It presents seven selected contributions and positions them within four major research directions: (i) Large Ensembles and Collective Dynamics, (ii) Knowledge, Consciousness and Emergence, (iii) Automated Reasoning for Better Interaction, and (iv) Analysing Collective Adaptive Systems. Together, they illustrate current progress and emerging challenges in the rigorous engineering of collective adaptive systems.

Abstract Adaptive systems are designed to modify their behaviour at runtime in response to dynamically changing and open-ended environments as well as evolving requirements. Such systems may operate as individual adaptive entities or as collective adaptive systems composed of multiple collaborating components. Rigorous engineering of these systems requires appropriate methods, models, and tools that ensure reliability, correctness, and alignment with their intended purpose. This paper introduces the first part of the special section on Rigorous Engineering of Collective Adaptive Systems. It presents six of the thirteen selected contributions and positions them within two major research directions: (i) Modelling and Engineering Collective Adaptive Systems, and (ii) Analysing Collective Adaptive Systems. Together, these contributions illustrate current progress and emerging challenges in the rigorous engineering of collective adaptive systems.

Ehrenfeucht-Fraïssé games provide means to characterize elementary equivalence for first-order logic, and by standard translation also for modal logics. We propose a novel generalization of Ehrenfeucht-Fraïssé games to hybrid-dynamic logics which is direct and fully modular: parameterized by the features of the hybrid language we wish to include, for instance, the modal and hybrid language operators as well as first-order existential quantification. We use these games to establish a new modular Fraïssé-Hintikka theorem for hybrid-dynamic propositional logic and its various fragments. We study the relationship between countable game equivalence (determined by countable Ehrenfeucht-Fraïssé games) and bisimulation (determined by countable back-and-forth systems). In general, the former turns out to be weaker than the latter, but under certain conditions on the language, the two coincide. As a corollary we obtain an analogue of the Hennessy-Milner theorem. We also prove that for reachable image-finite Kripke structures elementary equivalence implies isomorphism.

Epistemic processes describe the dynamic behaviour of multi-agent systems driven by the knowl- edge of agents, which perform epistemic actions that may lead to knowledge updates. Executing epistemic processes directly on epistemic states, given in the traditional way by pointed Kripke structures, quickly becomes computationally expensive due to the semantic update constructions. Based on an abstraction to formulæ of interest, we introduce a symbolic epistemic state representation and a notion of representable epistemic action with efficient symbolic updates. In contrast to existing work on belief or knowledge bases, our approach can handle epistemic actions modelled by arbitrary action models. We introduce an epistemic process calculus and a propositional dynamic logic for specifying process properties that can be interpreted both on the concrete semantic and the symbolic level. We show that our abstraction technique preserves and reflects behavioural properties of epistemic processes whenever processes are started in a symbolic state that is an abstraction of a semantic epistemic state.

Abstract An adaptive system is able to adapt at runtime to dynamically changing environments and to new requirements. Adaptive systems can be single adaptive entities or collective ones that consist of several collaborating entities. Rigorous engineering requires appropriate methods and tools that help guaranteeing that an adaptive system lives up to its intended purpose. This paper introduces the special section on “Rigorous Engineering of Collective Adaptive Systems.” It presents the 11 contributions of the section categorizing them into five distinct research lines: correctness by design and synthesis, computing with bio-inspired communication, new system models, machine learning, and programming and analyzing ensembles.

Abstract An ensemble consists of a set of computing entities which collaborate to reach common goals. We introduce epistemic ensembles that use shared knowledge for collaboration between agents. Collaboration is achieved by different kinds of knowledge announcements. For specifying epistemic ensemble behaviours we use formulas of dynamic logic with compound ensemble actions. Our semantics relies on an epistemic notion of ensemble transition systems as behavioural models. These transition systems describe control flow over epistemic states for expressing knowledge-based collaboration of agents. Specifications are implemented by epistemic processes that are composed in parallel to form ensemble realisations. We give a formal operational semantics of these processes that generates an epistemic ensemble transition system. A realisation is correct w. r. t. an ensemble specification if its semantics is a model of the specification.

Abstract Full a posteriori verification of the correctness of modern software systems is practically infeasible due to the sheer complexity resulting from their intrinsic concurrent nature. An alternative approach consists of ensuring correctness by construction. We discuss the Rigorous System Design (RSD) approach, which relies on a sequence of semantics-preserving transformations to obtain an implementation of the system from a high-level model while preserving all the properties established along the way. In particular, we highlight some of the key requirements for the feasibility of such an approach, namely availability of (1) methods and tools for the design of correct-by-construction high-level models and (2) definition and proof of the validity of suitable domain-specific abstractions. We summarise the results of the extended versions of seven papers selected among those presented at the $$1\mathrm {st}$$ 1 st and the $$2\mathrm {nd}$$ 2 nd International Workshops on Methods and Tools for Rigorous System Design (MeTRiD 2018–2019), indicating how they contribute to the advancement of the RSD approach.

Abstract An adaptive system is able to adapt at runtime to dynamically changing environments and to new requirements. Adaptive systems can be single adaptive entities or collective ones that consist of several collaborating entities. Rigorous engineering requires appropriate methods and tools that help guaranteeing that an adaptive system lives up to its intended purpose. This paper introduces the special section on “Rigorous Engineering of Collective Adaptive Systems.” It presents the seven contributions of the section and gives a short overview of the field of rigorously engineering collective adaptive systems by structuring it according to three topics: systematic development, methods and theories for modelling and analysis, and techniques for programming and operating collective adaptive systems.

The algebraic specification of the semantics of programming languages is outlined. Particular emphasis is given to the problem of specifying least-fixed points by first-order conditional equations. To cover this issue, the theory of specifying partial heterogeneous algebras by abstract data types is slightly extended by a more general notion of homomorphism. In this framework the semantics of programming languages can be uniquely specified in a purely algebraic way, using particular models of a hierarchy of abstract types. This approach is demonstrated for a simple procedural programming language. Several increasingly complex versions of iterations are treated and analyzed with respect to their theoretical consequences. Finally, as a complementary algebraic technique, transformational semantics is explained and applied to our examples.