Jul, 2023

概率超性质的演绎式控制合成

PDF
TL;DR提出了一种新的方法来解决马尔可夫决策过程（MDPs）和概率超性质的控制器合成问题，该方法在超级概率计时逻辑（HyperPCTL）的基础上增加了合成控制器的结构约束，采用逐步修正策略修剪搜索空间并与先前的 SMT 模型检查工具相比取得了显著的性能改进。
probabilistic hyperpropertiescontroller synthesismarkov decision processeslogic hyperpctlabstraction refinement strategy
发现论文，激发创造
  • 使用 HyperPCTL * 的多智能体系统贝叶斯统计模型检验

    本文介绍了基于贝叶斯方法的统计模型检查（SMC）算法，用于在离散时间马尔可夫链（DTMC）上检查指定于逻辑 HyperPCTL * 的概率超性质；我们提出了一种基于递归算法的 SMC 超算法，该算法基于修改后的贝叶斯测试，考虑了递归可满足结果的不确定性，并在一个 Python 工具箱 HyProVer 中实现；我们的实验评估表明，与基于 SPRT 的 SMC 相比，我们的贝叶斯 SMC 算法在验证时间和推断给定 HyperPCTL * 公式的可满足条件所需的样本数量方面表现更好。

    Sep, 2022

  • 超属性验证的非确定性规划

    验证超性质的自动化的算法，通过构建一个非确定性多机器人规划实例，确保一个规划存在则满足验证问题。

    May, 2024

  • 基于因果推理的马尔可夫决策过程时间推理

    本文介绍了一种新的概率时序逻辑，用于验证马尔可夫决策过程，其中包含因果推理操作符，使我们能够表达干预和反事实查询。

    Dec, 2022

  • 不确定性下的安全控制

    本文提出了一种新的逻辑 PrSTL 作为表达随机性质和强制其概率保证的表现语言，并展示了如何使用这种逻辑对具有随机性质的智能物理系统进行控制器合成，其关键特点是适应性逻辑并随着系统遇到附加数据而变化，并通过合成多种情况下无人机和自主车辆的控制器来演示我们的方法。

    Oct, 2015

  • 一种基于学习的方法，用于控制合成线性时间逻辑规范的马尔可夫决策过程

    使用学习理论中的技术，通过构建包含确定性 Rabin 自动机的乘积 MDP，其奖励函数来源于 Rabin 自动机的接受条件，即可合成满足线性时态逻辑（LTL）规范的控制策略，该方法在交通控制案例研究中证明可以产生合理的控制策略，即使无法保证满足 LTL 规范。

    Sep, 2014

  • 具有不确定性动态的 Markov 跳跃线性系统的形式控制器综合

    该论文提出了一种使用概率计算树逻辑规范的方法来综合 Markov 跳变线性系统 (MJLS) 的控制器，该方法基于所生成的有限状态抽象，该抽象通过采样技术从 “场景方法” 中计算转换概率的区间，从而生成 MJLS 的概率上合理的近似，并将该近似评估到实际的温度控制，与空中飞行器交付问题等多个基准测试问题中。

    Dec, 2022

  • 基于形式抽象的随机和不确定动态模型自动构造控制

    自动化合成控制器，基于概率时间逻辑规范的随机动态模型，通过状态验证技术构建的 iMDP（带概率区间的马尔科夫决策过程），解决安全关键场景中面临的挑战。

    Nov, 2023

  • 概率系统容错控制器综合

    本文提出了一种基于概率系统建模的控制器合成技术，该技术通过使用惩罚函数减少未来对控制器性能可能造成的影响，并最终生成一个具有多策略选择、适应性强的鲁棒性控制器。

    Apr, 2015

  • 在时间逻辑约束下的大致近似正确的 MDP 学习与控制

    此篇论文探讨了在未知、随机环境中，通过建立模型、构造符合某些临时逻辑规则要求的 MDP，并通过 PAC-MDP 的方法，利用数据、空间和时间进行迭代更新，得到了一个在一定条件下接近最优的策略，从而达到在给定规则下最大化概率的目的。

    Apr, 2014

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

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

    May, 2024