一句话：用余代数广义幂集构造统一导出并比较非确定性与概率系统的迹等价语义。
本文研究同时具有非确定性与概率选择的系统的 trace 等价。作者将此类进程的迹语义视为一个 coalgebraic 构造——广义幂集构造——的实例，并借助 monad 与其代数理论表示之间的相互作用，对所得语义进行刻画。论文进一步把该语义与文献中已有的若干 trace 等价定义进行比较，说明它们之间的联系与差异。主要贡献是给出统一的余代数视角，使非确定性与概率组合下的 trace 语义可以被系统导出并对照已有定义。
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.
DOI 原文 ·
@inproceedings{paperbot4975,
title = {The Theory of Traces for Systems with Nondeterminism and Probability},
author = {Filippo Bonchi and Ana Sokolova and Valeria Vignudelli},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785673}
}