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.

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 Knowledge-based programs specify multi-agent protocols with epistemic guards that abstract from how agents learn and record facts or information about other agents and the environment. Their interpretation involves a non-monotone mutual dependency between the evaluation of epistemic guards over the reachable states and the derivation of the reachable states depending on the evaluation of epistemic guards. We apply the technique of a must/cannot analysis invented for synchronous programming languages to the interpretation problem of knowledge-based programs and demonstrate that the resulting constructive interpretation is monotone and has a least fixed point. We relate our approach with existing interpretation schemes for both synchronous and asynchronous programs. Finally, we describe an implementation of the constructive interpretation and illustrate the procedure by several examples and an application to the Java memory model.

Abstract We present a new approach on how to provide institution-based semantics for communicating UML state machines in form of a hybrid modal logic $$\mathcal {M}^{\downarrow }_{\mathcal {D}}$$ M D ↓ . A theoroidal comorphism maps $$\mathcal {M}^{\downarrow }_{\mathcal {D}}$$ M D ↓ into the $$\textsc {Casl}$$ C A S L institution. This allows for symbolic reasoning on communicating UML state machines.

Dynamic reconfiguration is one of the key challenges in adaptive systems. As many tasks of adaptive systems are carried out by software and flexible machines, adaptation can be mainly defined by reconfiguration. The Real-Time Container Architecture provides a novel framework for these updates by running distributed embedded software in containers and enabling real-time reconfiguration of these software components following a reconfiguration plan. Yet, it limits I/O access of the containerized software components to GPIO, besides UDP-based communication. We extend the platform with new I/O methods and evaluated the extension with the smart factory showcase system Cube Bot. The extensions enable access to a camera and a robot from within the containers in compliance to the platform concepts. Within the application containers, different languages, state-of-the-art AI technology and the serial interface of the robot can be used. This will show the usefulness of the Real-Time Container Architecture in an even broader industrial context and its capability for extension to other use cases.

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.

Event-based systems operate in an environment that signals events upon which the system reacts. Besides the control flow of such systems also their data flow is of major importance. We present an event/data-based institution which is generic in the underlying data state institution. The logic is based on previous developments [14], [8] and is now extended to take into account event parameters, quantification over data, and non-deterministic choice of arguments in an institution-independent way. We show that the resulting framework forms again an institution.

Abstract We propose ε ↓ ( D → ) -logic as a formal foundation for the specification and development of event-based systems with data states. The framework is presented as an institution in the sense of Goguen and Burstall and the logic itself is parametrised by an underlying institution D → whose structures are used to model data states. ε ↓ ( D → ) -logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. It uses modal diamond and box operators over complex actions adopted from dynamic logic. Atomic actions are pairs [inline-graphic not available: see fulltext] where e is an event and ψ a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that ε ↓ ( D → ) -logic is powerful enough to characterise the semantics of an operational specification by a single ε ↓ ( D → ) -sentence. Thus the whole (formal) development process for event/data-based systems relies on ε ↓ ( D → ) -logic and its semantics as a common basis. It is supported by a variety of implementation constructors which can express, among others, event refinement and parallel composition. Due to the genericity of the approach, it is also possible to change a data state institution during system development when needed. All steps of our formal treatment are illustrated by a running example.

Will the cat catch the mouse?One of the early examples illustrating the challenges in analysing hybrid systems was stated by Maler, Manna, and Pnueli in 1991: At time T 0, a mouse starts running from a certain position on the floor in a straight line towards a hole in the wall, which is at a distance X 0 from the initial position.The mouse runs at a constant velocity V m .After a delay of time units, a cat is released at the same initial position and chases the mouse at velocity V c along the same path.Will the cat catch the mouse or will the mouse find sanctuary while the cat crashes against the wall?[MMP91]

We propose $$\mathcal {E}^{\downarrow } $$ -logic as a formal foundation for the specification and development of event-based systems with local data states. The logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. Our logic uses diamond and box modalities over structured actions adopted from dynamic logic. Atomic actions are pairs where e is an event and $$\psi $$ a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that $$\mathcal {E}^{\downarrow } $$ -logic is powerful enough to characterise the semantics of an operational specification by a single $$\mathcal {E}^{\downarrow } $$ -sentence. Thus the whole development process can rely on $$\mathcal {E}^{\downarrow } $$ -logic and its semantics as a common basis. This includes also a variety of implementation constructors to support, among others, event refinement and parallel composition.

Speed of adaptation to changing demand is a critical success factor in factory automation. The key to speed is to enable agile development by independent engineer offices and equipment producers with industrial-grade microservice architectures. The expensive drawback is: While software components evolve over time, manufacturers have to integrate and deploy more and more updates during costly production stops. To avoid production stops as much as possible, we propose reconfiguration extensions to a real-time container architecture proposed earlier. The original container approach addresses both the functional and nonfunctional aspects of integrating embedded software components in late engineering phases. The extended approach allows modifications of the running distributed embedded application even during operation, while continuously ensuring reactivity of the system. The agents running on each node prepare the reconfiguration in background and then synchronously perform the required modifications according to a detailed reconfiguration plan. We demonstrate our concept by describing a synchronous API change between two distributed software components of a running gesture recognition system. An evaluation shows the feasibility of the concepts, but also calls for further research.

One of the key challenges in dynamic reconfiguration of time-critical distributed embedded applications is state transfer: For consistency, the old component is usually blocked and its state is first extracted, then potentially transmitted and transformed and finally injected to the new component, before it can take over. However, as the technical process needs to be controlled continuously, there is technically no time for blocking. We present an approach to reconfigure stateful distributed embedded applications during operation either without or at least with bounded quality degradation. Using an extended prototype of our real-time container architecture the state transfer can be performed temporally deterministic and coordinated across nodes. By means of the reconfiguration plan the plant operator can employ strategies to keep up the system functionality for a limited time frame while specific components and messages are blocked. We describe a case study with three different reconfigurations showing the applicability of the proposed approach to various scenarios. We also discuss trade-offs and opportunities for future improvement of our approach.

UML allows the multi-viewpoint modelling of systems. One important question is whether an interaction as specified by a sequence diagram can be actually realised in the system. Here, the latter is specified as a combination of several state machines (one for each lifeline in the interaction) by a composite structure diagram. In order to tackle this question, we formalise the involved UML diagram types as institutions, and their relations as institution (co)morphisms.

In future production systems the speed of adaptation to changing market needs becomes increasingly important. As automation processes are carried out by flexible, software-defined machines like robots, adaptivity could be achieved largely through software updates. For technical and economic reasons it would be an advantage to update the automation system without stopping production. The challenge is to enable consistent software updates to running distributed embedded applications while keeping the timing requirements of messages and tasks. We describe the kinds of updates to be supported and give a brief first outline of our technical solution for this problem: A real-time container infrastructure that runs embedded components and is able to reconfigure the running distributed application due to a reconfiguration plan to be designed by the plant operator and to be verified by the plant engineering system.

We consider the question of how to treat existing, context-based test inputs when contextual conditions change. Simply ignoring the voided inputs reduces confidence in the correctness of the system under test (SuT). Instead, we suggest to adjust the parameters of those inputs to the new conditions in a way that retains their original intention. This often comprises behavioral assumptions, e.g., because of coverage or risk considerations. Transferred test inputs should consequently trigger similar behavior of the SuT within the new environment as the original ones did in the old. We formalize this claim by a distance function on test inputs which compares the expected reactions of the SuT. The more similar the responses, the closer the test inputs. The proposed metric can thus be used for guiding test input transfer. In addition to a recursive definition, we present an algorithm that utilizes neural models to estimate the metric by simply observing a given simulation which sketches the intended behavior of the SuT. As this approach seems to specifically match the prerequisites when testing proactive systems, motivation and first experiments consider a simplified instance of those: an exemplary smart vacuum system.

Partial constraint satisfaction and soft constraints enable to deal with over-constrained problems in practice. Constraint relationships have been introduced to provide a qualitative approach to specifying preferences over the constraints that should be satisfied. In contrast to quantitative approaches like weighted or fuzzy CSPs, the preferences just rely on a directed acyclic graph. The approach is particularly aimed at scenarios where soft-constraint problems stemming from several independently modeled agents have to be aggregated into one problem in a multi-agent system. Existing transformations into weighted CSP introduce unintended, additional preference decisions. We first illustrate the application of constraint relationships in a case study from energy management along with deficiencies of existing work. We then show how to embed constraint relationships into the soft constraint frameworks of partial valuation structures and further c-semi rings by means of free constructions. We finally provide a prototypical implementation of heuristics for the well-known branch-and-bound algorithm along with an empirical evaluation.

We address the question of how to select test cases in a controlled model-based software product line development process. CVL, the common variability language, provides a framework for materialization of product models from a given variability model and resolution model. Reflecting common practice, we assume that test case development for product line is independent from product development. In such a setting, the question arises which test cases can be applied to which products. To this end, we describe a procedure and tool set for assigning the outcome of a test case on an arbitrary member of a software product line using UML base and CVL variability models. As a case study, we demonstrate our approach with the example of a product line of automatic espresso machines.

Today's applications do not react to the ad-hoc, dynamic changes in locality, performance and environment that are characteristic of virtualized infrastructure. We illustrate exemplary effects experienced by distributed programs in reaction to change in the infrastructure and explore call interception, library replacement and aspect-oriented programming as alternatives for remedy. We demonstrate the remedial effect of adaptive code introduced without change to the original application code, or its bindings. We sketch a software architecture to make available management knowledge as a base for adaptation.

Operation contracts consisting of pre- and postconditions are a well-known means of specifying operations. In this paper we deal with the problem of operation contract simulation, i.e., determining operation results satisfying the postconditions based on input data supplied by the user; simulating operation contracts is an important technique for requirements validation and prototyping. Current approaches to operation contract simulation exhibit poor performance for large sets of input data or require additional guidance from the user. We show how these problems can be alleviated and describe an efficient as well as fully automatic approach. It is implemented in our tool OCLexec that generates from UML/OCL operation contracts corresponding Java implementations which call a constraint solver at runtime. The generated code can serve as a prototype. A case study demonstrates that our approach can handle problem instances of considerable size.

Traditionally, diagrams play an important role in many disciplines such as electrical engineering (e.g. Karnaugh-diagrams), civil and mechanical engineering (construction plans), geography (maps), etc. In Software Engineering today, diagrammatic languages like IDEF, UML or ARIS are commonplace, and with the rise of model driven development and domain specific languages, the use of such languages will become even more widespread in the future. All in all, diagrams play an important role in communication between engineers.

Provides an abstract of the tutorial presentation and a brief professional biography of the presenter. The complete presentation was not made available for publication as part of the conference proceedings.