随机系统上Büchi规范的符号控制器综合
系统与控制
2020-02-17 v2 系统与控制
摘要
我们考虑离散时间演进的连续状态受控马尔可夫过程的策略综合问题，其规范给定为Büchi条件（无限频繁访问一组状态）。我们将满足Büchi条件的最大概率计算分解为两步。第一步是计算最大定性赢集，从中可以概率一强制Büchi条件。第二步是求到达已计算的定性赢集的最大概率。与有限状态模型相反，我们表明此类计算仅给出最大概率的下界，且间隙可能非零。本文聚焦于近似定性赢集，同时指出已有的无界可达性计算方法可解决第二步。我们提供一种基于抽象的技术，通过同时使用概率转移关系的过近似与欠近似来近似定性赢集。由于我们关注定性性质，该抽象是非概率的；相反，概率转移被假设处于（公平）对手的控制之下。因此，我们将原策略综合问题归约为公平假设下的Büchi博弈，并将赢集的上下界刻画为-演算中的嵌套不动点表达式。该刻画立即给出一种符号算法框架。此外，在抽象博弈上计算的获胜策略可精化为受控马尔可夫过程上的策略。我们描述了一种具体抽象过程，并在两个案例研究中演示了我们的算法。
引用
@article{arxiv.1910.12137,
title = {Symbolic Controller Synthesis for B\"uchi Specifications on Stochastic Systems},
author = {Rupak Majumdar and Kaushik Mallik and Sadegh Soudjani},
journal= {arXiv preprint arXiv:1910.12137},
year = {2020}
}