马尔可夫决策过程验证学习算法

Mar, 2024

Learning Algorithms for Verification of Markov Decision Processes

Tomáš Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtěch Forejt, Jan Křetínský...

TL;DR提出了一个泛用的框架，应用学习算法和启发式指导来验证马尔可夫决策过程 (MDP)，主要关注概率可达性问题，包括精确和近似的情况，不受时间限制或折扣因子等条件的限制。

Abstract

We present a general framework for applying learning algorithms and heuristical guidance to the verification of markov decision processes (MDPs), based on the ideas of Br\'azdil, T. et al. (2014). Verification of

learning algorithms markov decision processes heuristics probabilistic reachability statistical model-checking

发现论文，激发创造

强健的马尔可夫决策流程即时学习

本文介绍了一种鲁棒的任意学习方法，该方法结合了贝叶斯推断模型和计算稳健策略的方法，以不确定性马尔科夫决策过程（uMDPs）为基础，并通过实验验证了该方法的有效性。

May, 2022

无限时间马尔可夫决策过程解决方案的形式验证方法

本文利用交互式定理证明器 Isabelle/HOL，对于解决马尔科夫决策过程（MDPs）的可执行算法进行正式验证，并基于此分析验证动态规划算法来解决表格 MDPs，实验结果表明该系统可以与最先进的系统竞争甚至超过它们。

Jun, 2022

统计模型检验基础的改进

Markov 决策过程和统计模型检测在未知转移概率、浓度不等式等方面的改进以及实验评估的重要性。

Apr, 2024

马尔可夫决策过程下基于分布式避障特性的认证策略验证与合成

该研究论文介绍了以马尔可夫决策过程为基础的状态转换模型及其在控制器验证和综合方面的应用，特别是在分布到达 - 避免规范下的证书合成问题，并提出了自动化方法来合成证书和策略以及验证其正确性。

May, 2024

马尔可夫决策过程中的主动模型估计

本文研究了基于 Markov 决策过程 (MDP) 环境中的精确建模的高效探索问题，提出一种以加权熵为基础的算法用于解决贪心算法在探索初阶段表现较差的问题，并在简单的具有异构噪音的两个问题上进行了验证。

Mar, 2020

平均奖励马尔科夫决策过程的学习和规划

本研究提出了一种基于平均报酬 MDPs 的学习和规划算法，其中包括第一种无参考状态的普遍证明收敛的无模型控制算法、第一个证明收敛的无政策自由预测算法，以及第一个离线学习算法，其收敛于实际值函数而不是值函数增加一个偏移量。在使用时间差错错误而不是常规错误更新平均报酬估计时，我们的所有算法都基于此。

Jun, 2020

层次概率模型的抽象 - 细化方法

本文介绍了一种通过层次化结构和抽象 - 细化循环来加速分析马尔科夫决策过程，针对重复部分具有局部影响的概率程序，将类似的子程序抽象成参数化模板，在需要时对其进行详细分析，从而缓解著名的状态空间爆炸问题。

Jun, 2022

无折扣 POMDP 中带有可达性目标的声音启发搜索值迭代

该研究论文探讨了部分可观测马尔可夫决策过程（POMDPs）中的最大可达性概率问题（MRPP），研究了一种基于点估计方法和基于试探性启发式搜索的新算法，解决了处理无限时域问题中循环的问题，并在实验评估中表现出优越性。

Jun, 2024

使用 Baum-Welch 算法主动学习马尔可夫决策过程（扩展版）

本文探讨应用自动机学习算法对基于模型验证的关键信息进行提取，实现对物理系统的建模，并基于主动学习和 Baum-Welch 算法对马尔可夫决策过程和马尔可夫链进行学习，最终证明了该种方法可以显著减少建模所需的观测次数。

Oct, 2021

基于分布式 Q 学习的多智能体马尔可夫决策过程和满足性准则

本文提出了一种强化学习算法来解决多智能体马尔可夫决策过程 (MMDP)，通过黑韦尔的可接近性定理，目标是将每个智能体的时间平均成本降低到预先指定的特定界限以下。通过在 Q-learning 算法中结合每个智能体成本的加权组合，其中成本是通过具有 Metropolis-Hastings 或乘法权重形式的传闻算法来调制传闻的平均矩阵，我们使用了多个时间尺度的算法，并证明在温和条件下，它近似实现了每个智能体的期望界限。我们还在具有联合控制的每个阶段成本的更一般的 MMDP 设置中展示了该算法的实证性能。

Nov, 2023