Traces form a coarse notion of semantic equivalence between states of a process, and have been studied coalgebraically for various types of system. We instantiate the finitary coalgebraic trace semantics framework of Hasuo et al. for controller-versus-environment games, encompassing both nondeterministic and probabilistic environments. Although our choice of monads is guided by the constraints of this abstract framework, they enable us to recover familiar game-theoretic concepts. Concretely, we show that in these games, each element in the trace map corresponds to a collection (a subset or distribution) of plays the controller can force. Furthermore, each element can be seen as the outcome of following a controller strategy. Our results are parametrised by a weak distributive law, which computes what the controller can force in a single step.

翻译：轨迹作为过程状态间语义等价性的粗粒度概念，已在各类系统的余代数研究中得到广泛探讨。本文针对控制器与环境博弈场景，实例化了Hasuo等人提出的有限余代数轨迹语义框架，该框架同时涵盖非确定性与概率性环境。尽管我们对单子的选择受限于该抽象框架的约束条件，但这些单子使我们能够复现经典博弈论概念。具体而言，我们证明在此类博弈中，轨迹映射中的每个元素对应控制器可强制实现的博弈路径集合（子集或概率分布）。进一步地，每个元素可视为遵循控制器策略所产生的结果。我们的研究结果通过弱分配律进行参数化，该定律用于计算控制器在单步博弈中可强制实现的结果。