一句话:提出统一范畴框架,用伴随刻画可达性条件,使转移系统的两种不动点/初始代数语义一致,并实例化到马尔可夫链与自动机。
许多转移系统存在两种不同的不动点语义,例如马尔可夫链上的全期望奖励与部分期望奖励语义;在适当条件下二者恰好一致,如几乎必然可达时。本文提出一个统一的范畴框架来刻画这类可达性条件,保证两种语义之间的对应。该框架通过适当的伴随自然导出抽象可达性条件,从而证明不动点乃至更一般的初始代数之间的重合。作者给出若干实例以展示其一般性,包括马尔可夫链的几乎必然可达条件和自动机的无歧义条件;并进一步利用逐点 Kan 扩张研究马尔可夫决策过程实例的规范构造。
Suitable reachability conditions can make two different fixed point semantics of a transition system coincide. For instance, the total and partial expected reward semantics on Markov chains (MCs) coincide whenever the MC at hand is almost surely reachable. In this paper, we present a unifying framework for such reachability conditions that ensures the correspondence of two different semantics. Our categorical framework naturally induces an abstract reachability condition via a suitable adjunction, which allows us to prove coincidences of fixed points, and more generally of initial algebras. We demonstrate the generality of our approach by instantiating several examples, including the almost sure reachability condition for MCs, and the unambiguity condition of automata. We further study a canonical construction of our instance for Markov decision processes by pointwise Kan extensions.