具有不确定动态的马尔可夫跳跃线性系统的形式化控制器综合
系统与控制
2023-08-07 v5 人工智能
机器人学
系统与控制
摘要
为信息物理系统自动综合可证明正确的控制器对于在安全关键场景中的部署至关重要。然而，混合特征以及随机或未知行为使该问题具有挑战性。我们提出一种为马尔可夫跳跃线性系统（MJLSs）——一类信息物理系统的离散时间模型——综合控制器的方法，使其可证明满足概率计算树逻辑（PCTL）公式。MJLS由一组有限的随机线性动态以及由马尔可夫决策过程（MDP）控制的这些动态之间的离散跳跃组成。我们考虑该MDP的转移概率已知至一个区间或完全未知的情况。我们的方法基于一种有限状态抽象，该抽象同时捕获MJLS的离散（模式跳跃）与连续（随机线性）行为。我们将此抽象形式化为区间MDP（iMDP），并使用所谓“情景方法”的采样技术计算其转移概率区间，从而得到概率上可靠的近似。我们将该方法应用于多个现实基准问题，特别是温度控制与飞行器投递问题。
引用
@article{arxiv.2212.00679,
title = {Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics},
author = {Luke Rickard and Thom Badings and Licio Romao and Alessandro Abate},
journal= {arXiv preprint arXiv:2212.00679},
year = {2023}
}
备注
15 pages, accepted to QEST