一句话：用余代数与分配格对偶统一刻画带升级的条件迁移系统，并实例化行为等价最小化算法。
条件迁移系统可用于建模带升级功能的软件产品线。本文将这类系统置于余代数框架中，借助分配格的 Birkhoff 对偶，推导出两种等价的 Kleisli 范畴：一种基于 reader monad，另一种基于 Poset 上的 lattice monad。论文研究了两类描述分支类型的函子，并考察由此产生的行为等价关系。最后，作者说明如何将已有的余代数最小化算法实例化到该设定，从而计算这些行为等价。该工作为带升级条件迁移系统提供了范畴化语义基础，并连接了行为等价与最小化。
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.
@article{paperbot422,
title = {A coalgebraic treatment of conditional transition systems with upgrades},
author = {Harsh Beohar and Barbara König and Sebastian Küpper and Alexandra Silva and Thorsten Wißmann},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 1},
year = {2018},
doi = {10.23638/lmcs-14(1:19)2018}
}