Bialgebraic Representation of Controlled Coordination of Interacting System Components
In process calculi, conditional rules of Structural Operational Semantics (SOS) generate behavioural systems, whose states are closed terms over an algebraic signature. A single-sorted algebraic signature can be encoded with an Set-endofunctor and the above-mentioned behaviour can be described by labelled transition systems or, more generally, by coalgebras also based on Set-endofunctors. The bialgebraic framework generalises these SOS rules by natural transformations of the form TD => DT, called distributive laws, where T is the free monad over the signature functor and D is the cofree comonad over the behaviour functor. This abstract SOS setting yields, by certain lifting constructions, an operational and a denotational model from which compositionality can automatically be derived, that is, one can reason about the correctness of a composed term by investigating the correctness of its components. The purpose of SOS rules is to specify behaviour of process terms, whose parts act on the same state space. Typical underlying algebraic operations are prefixing, alternative and parallel composition, but other operations like the zipping of process traces are also possible. It is well-known that in a modular component-based distributed system, the interaction of participating behavioural components can also be specified with operations of an algebraic signature. However, in practical scenarios, the components’ operational semantics are separated from each other (state space separation) and, furthermore, the components’ behaviour types are different: Their observational interaction with the environment depends on their communication capabilities, which may or may not include, e.g., timed aspects, probabilistic behaviour, or name passing, resp. (heterogeneity). Thus, describing the behaviour of the entire system requires two improvements: Heterogeneity enforces the use of abstract distributive laws instead of classical SOS-rules, and separated state spaces require replacing Set by more general base categories. The need to coordinate smaller components in a large system landscape, for example, to prevent concurrent access to mutually used resources, requires controlled component orchestration. The goal of our contribution is to demonstrate how to smoothly extend existing component interaction laws to facilitate this controlled orchestration. We were inspired by an example of a homogeneous zipping operation on streams over a character set L (i.e. coalgebras for the Set-endofunctor B = L x _) defined by the coinductive extension of an SOS rule with alternation encoded in the conclusion of the rule. This inherent alternation (seen as a type of control in the above sense) of character selection is only possible, if the trace’s states belong to a shared state space X of a coalgebra based on a single endofunctor B acting on X. This control is hard to come by, if state spaces are separated as in the case of a heterogeneous zipping operation on streams over two distinct character sets L1 and L2, for example. In this paper, we propose a bialgebraic framework to integrate arbitrary concurrency control patterns (e.g., lock management, transaction scheduling, two-phase commit protocols, etc.), if state spaces are separated and the participating components exhibit heterogeneous behaviour. The ‘‘controller’’ will be explicitly given by a special behavioural component within the framework. Moreover, the resulting distributive laws involve multi-sorted algebraic signatures. Each component type is represented by a sort of this signature and the operations represent possible interaction scenarios. This leads to a description of the components together with the composed system as a single holistic behavioural system, such that compositionality can automatically be derived.
Slides (WADT2024-HaraldKönig.pdf) | 2.43MiB |
Extended abstract (Bialgebraic Representation of Controlled Coordination of Interacting System Components.pdf) | 235KiB |
Mon 8 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30 | WADT Keynote Session 1STAF Keynotes / Research papers at Waaier 3 Chair(s): Tom van Dijk University of Twente | ||
09:00 60mKeynote | WADT Keynote 1 - Some Uses of Modal Semirings STAF Keynotes File Attached | ||
10:00 30mTalk | Bialgebraic Representation of Controlled Coordination of Interacting System Components Research papers File Attached |