The belief construction is a fundamental technique for transforming partially observable systems to fully observable ones while preserving the relevant semantics. It plays a central role in the analysis of partially observable systems, in particular partially observable Markov decision processes (POMDPs), which is a central model in artificial intelligence and formal verification. In this paper, we develop a coalgebraic framework for the belief construction. To handle observations categorically, we lift a monad to slice categories and introduce a belief decomposition that reorganizes states according to their observations. This allows us to introduce a coalgebraic generalization of the belief construction, obtained by combining the belief decomposition with the coalgebraic determinization of Silva, Bonchi, Bonsangue, and Rutten. In this framework, we show that the semantics of a partially observable system coincides with that of the corresponding belief coalgebra. We then study when the latter further agrees with the semantics of its fully observable counterpart, and use this to identify conditions under which the semantics of a partially observable system coincides with that of the corresponding fully observable belief system. As consequences, we recover the standard equivalence between POMDPs and belief MDPs, and obtain a new equivalence result for weighted transition systems with the semimodule monad.
翻译:信念构建是将部分可观测系统转换为完全可观测系统并保持相关语义的基本技术。它在部分可观测系统的分析中起着核心作用,特别是部分可观测马尔可夫决策过程(POMDPs),这是人工智能和形式化验证中的核心模型。在本文中,我们开发了一个用于信念构建的余代数框架。为了分类处理观测,我们将单子提升到切片范畴,并引入一种信念分解,根据观测重新组织状态。这使我们能够引入信念构建的余代数推广,通过将信念分解与Silva、Bonchi、Bonsangue和Rutten的余代数确定性相结合得到。在此框架中,我们证明部分可观测系统的语义与相应的信念余代数的语义一致。然后,我们研究后者何时进一步与其完全可观测对应物的语义一致,并利用这一点来识别部分可观测系统语义与其对应的完全可观测信念系统语义一致的条件。作为结果,我们恢复了POMDP与信念MDP之间的标准等价性,并获得了带半模单子的加权迁移系统的新等价性结果。