Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications
Divergent stutter bisimulation abstraction for controller synthesis with linear temporal logic specifications
复制标题
用于具有线性时序逻辑规范的控制器综合的发散口吃互仿真抽象
DOI：
10.1016/j.automatica.2021.109723
复制
发表时间：
2021
期刊：
影响因子：
6.4
通讯作者：
Ozay, Necmiye
中科院分区：
文献类型：
--
作者：
Mohajerani, Sahar;Malik, Robi;Wintenberg, Andrew;Lafortune, Stéphane;Ozay, Necmiye
本文提出了一种方法来综合控制器的系统可能有无穷多个状态，满足一个规格作为一个LTL的设计公式。处理这个问题的一种常见方法是首先计算原始状态空间的有限状态抽象，然后为抽象合成控制器。本文提出了一种称为发散口吃互模拟的抽象方法来抽象系统的状态空间。由于发散的口吃互模拟因素口吃的步骤，它通常会导致一个粗糙的，因此更小的抽象，在不保留时间的“下一个”操作符的代价。本文利用发散口吃互模拟模型检查的结果，并表明，发散口吃互模拟是一个健全的和完整的抽象方法时，合成控制器的规格在LTL控制器。
This paper proposes a method to synthesise controllers for systems with possibly infinite number of states that satisfy a specification given as an LTL∖∘ formula. A common approach to handle this problem is to first compute a finite-state abstraction of the original state space and then synthesise a controller for the abstraction. This paper proposes to use an abstraction method called divergent stutter bisimulation to abstract the state space of the system. As divergent stutter bisimulation factors out stuttering steps, it typically results in a coarser and therefore smaller abstraction, at the expense of not preserving the temporal “next” operator. The paper leverages results about divergent stutter bisimulation from model checking and shows that divergent stutter bisimulation is a sound and complete abstraction method when synthesising controllers subject to specifications in LTL∖∘.
登录
查看更多内容
一种用于抽象控制系统的类互模拟算法
DOI：
10.1109/allerton.2016.7852282
发表时间：
2016
期刊：
2016 54th Annual Allerton Conference on Communication, Control, and Computing (Allerton)
影响因子：
--
作者：
Andrew J. Wagenmaker;N. Ozay
通讯作者：
N. Ozay
影响因子：
6.8
作者：
Reissig, Gunther;Weber, Alexander;Rungger, Matthias
通讯作者：
Rungger, Matthias
使用三值抽象实现安全性和可达性规范的惰性控制器综合
DOI：
10.1109/cdc.2018.8619649
发表时间：
2018
期刊：
2018 IEEE Conference on Decision and Control (CDC
影响因子：
--
作者：
Hussien, Omar;Tabuada, Paulo
通讯作者：
Tabuada, Paulo
影响因子：
2.1
作者：
N. Megawati;A. Schaft
通讯作者：
A. Schaft
互模拟等价
DOI：
10.1007/978-0-387-09766-4_2227
发表时间：
2011
期刊：
ACM Transactions on Computational Logic (TOCL)
影响因子：
--
作者：
Andrew J. Wagenmaker;N. Ozay
通讯作者：
N. Ozay