The Participants-as-Interfaces (PaI) approach to system composition suggests that participants in a system can be considered interfaces to the outside world. Given a set of systems, one participant per system is chosen to play the role of an interface. When systems are composed, these interface participants are replaced by gateways that communicate with each other by forwarding messages. The PaI approach for systems of asynchronously communicating finite state machines (CFSMs) has been exploited in the literature for binary composition where the forwarding policy is necessarily unique. In this paper we consider the case of multiple system composition and extend preliminary work to the case where interactions among gateways can be mediated by additional orchestrating participants that comply with a given connection model . We represent the interactions among gateways as CFSM systems (called orchestrated connection policies ) and prove that a number of relevant communication properties (e.g. deadlock-freedom, reception-error-freedom) are preserved by orchestrated PaI multicomposition , provided that the orchestrated connection policy used also satisfies the communication property in question.

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.

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

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.

We study interacting components and their compatibility with respect to synchronous and asynchronous composition. The behavior of components is formalized by I/O-transition systems. Synchronous composition is based on simultaneous execution of shared output and input actions of two components while asynchronous composition uses unbounded FIFO-buffers for message transfer. In both contexts we study compatibility notions based on the idea that any output issued by one component should be accepted as an input by the other. We distinguish between strong and weak versions of compatibility, the latter allowing the execution of internal actions before a message is accepted. We consider open systems and study conditions under which (strong/weak) synchronous compatibility is sufficient and necessary to get (strong/weak) asynchronous compatibility. We show that these conditions characterize half-duplex systems. Then we focus on the verification of weak asynchronous compatibility for possibly non half-duplex systems and provide a decidable criterion that ensures weak asynchronous compatibility. We investigate conditions under which this criterion is complete, i.e. if it is not satisfied then the asynchronous system is not weakly asynchronously compatible. Finally, we discuss deadlock-freeness and investigate relationships between deadlock-freeness in the synchronous and in the asynchronous case.

Abstract Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of reconfigurable systems, i.e., systems with reconfiguration mechanisms governing the dynamic evolution of their execution configurations in response to both external stimuli or internal performance measures. A formal representation of such systems is through transition structures whose states correspond to the different configurations they may adopt. Therefore, each node is endowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. This paper characterises equivalence and refinement for these sorts of models in a way which is independent of (or parametric on) whatever logic (propositional, equational, fuzzy, etc) is found appropriate to describe the local configurations. A Hennessy–Milner like theorem is proved for hybridised logics.

We describe the concepts and design principles of the integrative simulation system DANUBIA, which supports the analysis of water-related global change scenarios in the Upper Danube Basin. DANUBIA provides an Internet-based platform integrating the distributed simulation models of all socioecological and natural science disciplines taking part in the GLOWA-Danube project, which is part of the German Programme on Global Change in the Hydrological Cycle. As a result of coupled simulations, transdisciplinary effects of mutually dependent processes can be analyzed and evaluated. Actually 13 simulation models of meteorology, land surface, water research, and social sciences are integrated in the DANUBIA system. The development of DANUBIA is based on object-oriented software engineering and Web engineering methods and on the Unified Modeling Language (UML), which is used by all partners as a common graphical notation for modeling the integrative aspects of the system. We describe how the mutually exchanged information between components is modeled and documented by interfaces, we discuss spatial aspects and show how simulation areas are represented, and we consider temporal aspects and describe the coordination of local models by a global time controller which constitutes the heart of any integrative DANUBIA simulation. Finally, we provide an overview of the architecture of the DANUBIA implementation that has been realized in Java. The implementation integrates a wrapper framework that hides the technical details of network communications.

Abstract An induction principle, called context induction, is presented which is appropriate for the verification of behavioural properties of abstract data types. The usefulness of the proof principle is documented by several applications: the verification of behavioural theorems over a behavioural specification, the verification of behavioural implementations and the verification of “forget-restrict-identify” implementations. In particular, it is shown that behavioural implementations and “forget-restrict-identify” implementations (under certain assumptions) can be characterised by the same condition on contexts, i.e. (under the given assumptions) both concepts are equivalent. This leads to the suggestion to use context induction as a uniform proof method for correctness proofs of algebraic implementations.