A coalgebraic treatment of conditional transition systems with upgrades

TL;DR

This paper develops a coalgebraic framework for modeling conditional transition systems with upgrades, using duality and category theory, and adapts minimisation algorithms for behavioral equivalence analysis.

Contribution

It introduces a novel coalgebraic approach for conditional transition systems with upgrades, utilizing Birkhoff's duality and Kleisli categories, and adapts minimisation algorithms for this setting.

Findings

Two equivalent Kleisli categories for the coalgebras are derived.

Behavioral equivalence can be characterized within this framework.

Existing minimisation algorithms are applicable to these coalgebras.

Abstract

We consider conditional transition systems, that model software product lines with upgrades, in a coalgebraic setting. By using Birkhoff's duality for distributive lattices, we derive two equivalent Kleisli categories in which these coalgebras live: Kleisli categories based on the reader and on the so-called lattice monad over $\mathsf{Poset}$. We study two different functors describing the branching type of the coalgebra and investigate the resulting behavioural equivalence. Furthermore we show how an existing algorithm for coalgebra minimisation can be instantiated to derive behavioural equivalences in this setting.