Lazy Controller Synthesis using Three-valued Abstractions for Safety and Reachability Specifications
Lazy Controller Synthesis using Three-valued Abstractions for Safety and Reachability Specifications
复制标题
使用三值抽象实现安全性和可达性规范的惰性控制器综合
DOI：
10.1109/cdc.2018.8619649
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Tabuada, Paulo
中科院分区：
文献类型：
--
作者：
Hussien, Omar;Tabuada, Paulo
综合设计正确的控制软件是解决形式验证复杂的计算机物理系统的众所周知的困难的一个很有前途的方向。尽管这种方法前景看好，但它目前仅限于小型系统，因为它通常需要计算有限状态抽象，其大小随着连续状态的数量呈指数增长。本文提出了一种新的方法来解决控制软件综合缺乏可扩展性的问题，采用了一种懒惰控制器综合方法。不是使用整个系统的预计算抽象来合成控制器，而是根据安全性和可达性规范的需要延迟计算抽象。通过不同的例子，我们说明了这种懒惰的方法如何显著地减少了综合按设计正确的控制器所需的总时间。
The synthesis of correct-by-design control software is a promising direction to address the well known difficulties in formally verifying complex cyber-physical systems. Despite the promise of this approach, it is currently limited to small systems since it typically requires the computation of a finite-state abstraction whose size grows exponentially with the number of continuous states. In this paper we present a new way to tackle the lack of scalability of control software synthesis by adopting a lazy controller synthesis approach. Instead of synthesizing a controller using a precomputed abstraction of the full system, the abstraction is computed lazily as needed for safety and reachability specifications. We illustrate, through different examples, how this lazy approach significantly reduces the total time required for the synthesis of correct-by-design controllers.
登录
查看更多内容
随机控制系统有限状态抽象的组合构造
DOI：
10.1109/cdc.2017.8263720
发表时间：
2017
期刊：
2017 IEEE 56th Annual Conference on Decision and Control (CDC)
影响因子：
--
作者：
Kaushik Mallik;S. Soudjani;Anne;R. Majumdar
通讯作者：
R. Majumdar
影响因子：
3
作者：
Omar Hussien;A. Ames;P. Tabuada
通讯作者：
P. Tabuada
DOI：
10.1016/j.ic.2009.05.007
发表时间：
2007
期刊：
52nd IEEE Conference on Decision and Control
影响因子：
--
作者：
L. D. Alfaro;Pritam Roy
通讯作者：
Pritam Roy
影响因子：
6.8
作者：
Reissig, Gunther;Weber, Alexander;Rungger, Matthias
通讯作者：
Rungger, Matthias
具有模式计数约束的大型系统集合的控制综合
DOI：
10.1145/2883817.2883831
发表时间：
2016
期刊：
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control
影响因子：
--
作者：
Petter Nilsson;N. Ozay
通讯作者：
N. Ozay