Emmy-Noether-Seminar: "Graded Monads in the Semantics of Concurrent Systems"
Graded Monads in the Semantics of Concurrent Systems
Lutz Schröder (FAU)
Abstract: Concurrent systems are classically equipped with a range of behavioural equivalences on states that depend on models of interaction with the system; behavioural equivalences of varying granularity are arranged on the famous linear time/branching-time spectrum, with fine-grained branching-time equivalences such as bisimilarity on one end, and coarse-grained linear-time equivalences such as trace equivalence on the other end. At the same time, concurrent systems vary with regard to their branching type, which may be, e.g., non-deterministic, alternating, probabilistic, weighted, or game-based. Variation in the system type is captured uniformly in the framework of universal coalgebra; on the other hand, generic notions of behavioural equivalences provided by the coalgebraic framework have long been limited to branching-time equivalences. Several general approaches to more coarse grained equivalences have emerged recently; we discuss an approach via so-called graded monads, which in universal-algebraic terms correspond to algebraic theories in which operations are equipped with a notion of depth, and terms and equations are restricted to have uniform depth. In particular, we will take a look at characteristic logics and at game-based methods for graded behavioural equivalences. Time permitting, we will look beyond behavioural equivalences, in particular at behavioural preorders and behavioural metrics.