How to Kill Epsilons with a Dagger -- A Coalgebraic Take on Systems with Algebraic Label Structure

TL;DR

This paper introduces a coalgebraic framework using monads and algebraic structures to model and abstract internal transitions in state-based systems, including concurrent systems with complex label structures.

Contribution

It extends standard coalgebraic models by incorporating algebraic label structures via monads, enabling a unified treatment of systems with internal behaviors like silent or epsilon-transitions.

Findings

Provides a semantics for systems with internal transitions using monads and fixpoint operators.

Develops a sound abstraction procedure for internal transitions based on algebraic label structures.

Applies the framework to systems like Mazurkiewicz traces for concurrency.

Abstract

We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $\epsilon$-transitions. Our approach employs monads with a parametrized fixpoint operator $\dagger$ to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems.