一句话：通过余代数广义幂集构造统一刻画非确定性、概率与终止系统的迹等价，并与既有定义比较。
论文研究同时包含非确定性与概率选择的系统的迹等价，并考虑终止行为。作者从余代数视角出发，将已知的广义幂集构造（generalised powerset construction）实例化到相应 monad 上，从而导出迹语义。文章刻画并比较了由此得到的多种迹等价与文献中已有定义，说明它们在何种条件下一致或不同。技术核心在于 monad 与其代数理论表示之间的相互作用，借此统一处理非确定性、概率和终止的组合。该工作为这类系统的行为等价提供了统一的范畴论框架。
This paper studies trace-based equivalences for systems combining nondeterministic and probabilistic choices. We show how trace semantics for such processes can be recovered by instantiating a coalgebraic construction known as the generalised powerset construction. We characterise and compare the resulting semantics to known definitions of trace equivalences appearing in the literature. Most of our results are based on the exciting interplay between monads and their presentations via algebraic theories.
@article{paperbot1689,
title = {The Theory of Traces for Systems with Nondeterminism, Probability, and Termination},
author = {Filippo Bonchi and Ana Sokolova and Valeria Vignudelli},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:21)2022}
}