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

Dec, 2022

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

Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics

Luke Rickard, Thom Badings, Licio Romao, Nils Jansen, Alessandro Abate

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

Abstract

automated synthesis of provably correct controllers for cyber-physical systems is crucial for deploying these systems in safety-critical scenarios. However, their hybrid features and stochastic or unknown behavio

automated synthesis cyber-physical systems markov jump linear systems probabilistic computation tree logic controllers

发现论文，激发创造

通过正式抽象实现非高斯噪声动态系统的鲁棒控制

该研究论文提出了一种新颖的控制器合成方法，它不需要任何明确表示噪声分布的方式，而是通过将控制系统抽象为捕捉噪声的有限状态模型，然后使用从场景方法中的工具来计算可能正确的限制，基于一些噪声的有限数量样本。通过缩小合成过程的复杂性，该方法在实际控制系统上的应用具有广泛的适用性。

Jan, 2023

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

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

Nov, 2023

概率不够用：针对存在认识不确定性的随机动态模型的形式控制器综合

本文介绍一种使用区间 Markov 决策过程的抽象方式，在连续状态的模型中捕捉随机噪声和不确定参数的 aleatoric 和 epistemic 不确定性，进行控制器的综合。经实验验证，考虑 epistemic 不确定性可以提高控制器的鲁棒性。

Oct, 2022

不确定性引导效率：用于随机混合系统的可扩展形式合成

该研究旨在为线性动态的离散时间随机混合系统开发高效的抽象方法，通过不确定的 MARKOV 决策过程解决了现有形式方法的限制，可以计算精确的抽象误差，并应用于有限和无限时间范围内的合成步骤，大大缩减抽象误差，提高可缩放性。

Jan, 2019

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

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

Sep, 2014

马尔可夫跳跃过程的基础推断模型

使用零样本推理的神经网络模型，能够从嘈杂且稀疏的观察中，推断出具有不同维度的马尔可夫跳跃过程，并且达到与针对目标数据集微调的最先进模型相媲美的性能。

Jun, 2024

带有线性时态逻辑规约的 POMDPs 的随机有限状态控制

本研究提出了一种基于 POMDPs 的任意时间算法，通过在线性时态逻辑（LTL）清单约束条件下最大化满足概率来合成次优随机有限状态控制器（sFSCs），并通过机器人导航案例研究表明了该方法的有效性。

Jan, 2020

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

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

Apr, 2014

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

提出了一种新的方法来解决马尔可夫决策过程（MDPs）和概率超性质的控制器合成问题，该方法在超级概率计时逻辑（HyperPCTL）的基础上增加了合成控制器的结构约束，采用逐步修正策略修剪搜索空间并与先前的 SMT 模型检查工具相比取得了显著的性能改进。

Jul, 2023

使用参数合成对 POMDP 的宽松有限状态控制器

研究了针对给定规范证明正确的、用于部分可观察的马尔可夫决策过程（POMDPs）的有限状态控制器（FSCs）。通过将在 POMDPs 上计算（随机）FSCs 转化为参数化 Markov 链（pMCs）的合成，许多规范下的正确构造 FSCs 可以得到计算，并为其提供了工具。实验结果显示与已知的 POMDP 求解器性能相当。

Oct, 2017