Compositionality in Coalgebraic Process Theory (LEGO-CPT)

Process theory investigates formal methods for modelling and analysis of concurrent processes. Its main focus is making formal semantics of models precise. Widely accepted models of processes are the (variants of) labelled transition systems. Special purpose process theories also exist and have grown in separate directions like probabilistic, timed, or process theory for systems with data. Many models are built in a compositional way: Since compositional modelling enhances compositional verification, it is of great interest to study operators for composing models. The aim then is to show that such operators are well-behaved with respect to suitable compositionality properties. Coalgebra theory is one step up in the abstraction pyramid. Coalgebras are mathematical objects based on category theory that generalize the standard process models. The switch between determinism, nondeterminism, probability, time, or data in the standard models is expressed on the coalgebraic level as a choice of a parameter. The success of the theory of coalgebras is due to the generic strong notion of behaviour semantics of coalgebras (coalgebraic bisimilarity) that specializes to many known types of systems, and to the elegant theory of coalgebraic modal logics that covers many known and quite different modal logics. Compositionality is a key issue in the theory of coalgebras. It can be understood in at least two different ways: as compositionality in coalgebraic process theory, or as meta-compositionality (modularity) of types that define the coalgebras. On the practical side, compositional algorithms are essential for real-time systems and applications where predictability and bounded response times is a crucial issue. Designing compositional algorithms is a challenge since the general solution of many algorithmic problems in real-time systems, e.g. the scheduling problem, is not compositional. This project aims at investigating the aspects of compositionality in coalgebra, with applications to concrete models. Particular emphasis will be put on probabilistic systems. In addition, we target formalizing the concepts underlying compositional algorithms in real-time systems, as well as bringing the abstract theoretical study and the more practical side closer together.