Certification methods for stochastic systems provide sufficient proof rules, based on real-valued supermartingale certificates, to determine the almost-sure satisfaction of $ω$-regular properties (and therefore of linear temporal logic) over general state spaces, encompassing both countably infinite and continuous state spaces. Conversely, reinforcement learning (RL) methods for $ω$-regular tasks have received considerable attention, but they typically lack formal guarantees that the learned policy satisfies the specification, except possibly for finite state and action spaces. We bridge these two lines of research by establishing a novel theoretical connection: under an appropriate reward, the value function associated to a policy that almost surely satisfies an $ω$-regular property encodes a Streett supermartingale certificate for that specification. Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.

翻译：随机系统的认证方法提供了基于实值超鞅凭证的充分证明规则，用于确定在包括可数无穷和连续状态空间的一般状态空间上，$ω$-正则属性（因此也包括线性时序逻辑）的几乎必然满足性。反之，针对$ω$-正则任务的强化学习方法虽受到广泛关注，但除有限状态和动作空间外，通常缺乏对所学策略满足规范的形式化保证。我们通过建立一项新颖的理论联系来弥合这两个研究方向：在适当奖励下，与几乎必然满足$ω$-正则属性的策略相关联的值函数编码了该规范的一个Streett超鞅凭证。我们的结果在有限马尔可夫决策过程上经过实验验证，适用于有限、可数无穷和连续状态空间，为通过强化学习进行凭证合成提供了一条原理性路径。