Jul, 2023

利用机器学习改进 MDPs 的概率双模拟

PDF
TL;DR我们提出了一种新技术，通过使用给定模型的 PRISM 程序构建一些模型的小版本并训练一个分类器，然后应用机器学习分类技术来近似相关分区，将分区结果作为标准双模拟技术的初始分区，以减少方法的运行时间。实验结果表明，该方法与最先进的工具相比，可以显著减少运行时间。
model checkingstate space explosionbisimulation minimizationprobabilistic bisimulationmachine learning classification
发现论文，激发创造
  • 双仿真学习

    我们介绍了一种基于数据驱动的方法来计算具有非常大，可能是无限状态空间的状态转换系统的有限双模拟。我们的新技术计算确定性系统的阻塞不敏感的双模拟，我们将其描述为学习状态分类器与每个类的排名函数的问题。我们的方法从一个有限的样本状态数据集中学习候选状态分类器和候选排名函数；然后，它使用可满足性模理论求解检查这些是否推广到整个状态空间。如果得到肯定答案，该过程得出结论，该分类器构成了系统的有效阻塞不敏感的双模拟。如果得到否定答案，求解器会生成一个反例状态，该状态违反了该分类器的断言，将其添加到数据集中，并在反例引导的归纳合成循环中重复学习和检查，直到找到有效的双模拟。我们在反应性验证和软件模型检查的一系列基准测试中展示了我们的方法在实践中优于其他最先进的工具的更快验证结果。我们的方法产生简洁的抽象，使得能够有效地验证不包含下一个运算符的线性时态逻辑，并且对于系统诊断具有解释能力。

    May, 2024

  • 确定性马尔科夫决策过程中计算状态相似性的可扩展方法

    本文针对 MDPs 中 Bisimulation Metrics 的计算提出了新的算法，包括适用于连续状态 MDP 的可微损失函数，其中第一算法通过采样保证收敛性，第二算法通过学习实现了对大规模、确定性 MDP 的近似计算。

    Nov, 2019

  • 马尔可夫决策过程中计算状态相似性的方法

    本文运用网络优化和统计抽样技术，克服了计算 Kantorovich 度量在实践中的成本问题，提出了一系列用于 MDP 状态聚合的距离函数，这些函数在时间和空间复杂度以及聚合质量之间存在不同的权衡，并对这些权衡进行了实证评估。

    Jun, 2012

  • 游戏指标算法

    基于模拟和双模拟的指标可以用于系统验证和性能评估，适用于定量的 mu - 演算和相关概率逻辑，对于马尔可夫链，我们提供了一个 PSPACE 算法，以匹配最佳算法，并且这些算法可以通过二分搜索来逼近指标。

    Sep, 2008

  • 概率模型检查和自主性

    本文综述了概率模型检测在 PRISM 和 PRISM-games 模型检查器支持下的可观测和不可观测马尔可夫决策过程、顺序和并发随机博弈以及相关概率时态逻辑，以及其在自主系统中的应用，并探讨了未来研究方向和挑战。

    Nov, 2021

  • 用于计算马尔可夫决策过程近似最优解的模型简化技术

    介绍了一种新方法，用于解决具有非常大状态空间的隐式（分解式）马尔可夫决策流程（MDPs）。该方法通过 epsilon-homogeneous 分区算法将大型 MDP 转化为较小的 BMDP 以分析大型隐式 MDPs。

    Feb, 2013

  • 通过主动的 MDP 学习进行概率性黑盒验证

    我们介绍了一种新的测试随机黑盒系统的方法，该方法通过使用主动马尔科夫决策流程、概率模型检查和统计假设检验等技术，改进了传统的黑盒检查方法，并且在实验结果中表现优于现有方法。

    Jul, 2023

  • 离线强化学习中基于双模拟的表示方法的缺陷及其解决方法

    通过分析发现，离线强化学习任务中缺失的状态转换对于等价关系原则特别有害，导致估计无效。同时，奖励缩放在界定等价度量和其引发的值误差的尺度方面起着至关重要的作用。基于这些发现，我们提出在离线强化学习环境中应用期望分为运算符进行表示学习，从而防止对不完整数据进行过拟合。与此同时，通过引入适当的奖励缩放策略，我们避免了表示空间中特征崩溃的风险。我们在两个最先进的基于等价关系的算法 MICo 和 SimSR 上实现了这些建议，并在两个基准套件 D4RL 和 Visual D4RL 上展示了性能提升。代码可在 https://github.com/zanghyu/Offline_Bisimulation 中找到。

    Oct, 2023

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

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

    Mar, 2024

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

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

    Jun, 2022