自动机理论邂逅障碍证书：非线性系统的时序逻辑验证
形式语言与自动机理论
2014-03-17 v1 计算机科学中的逻辑
摘要
我们考虑在连续状态空间上演化的（可能是非线性的）动力系统的时序逻辑验证。我们的方法结合了基于自动机的验证和所谓障碍证书的使用。基于自动机的验证允许将验证任务分解为连续状态空间上的一组有限的更简单约束。这些约束的满足性反过来可以通过适当构造的障碍证书来（可能是保守地）证明。因此，我们的方法结合基于优化的障碍证书搜索，允许针对时序逻辑属性对动力系统进行计算验证，同时避免了文献中常见的对动力学的显式抽象。
引用
@article{arxiv.1403.3524,
title = {Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems},
author = {Tichakorn Wongpiromsarn and Ufuk Topcu and Andrew Lamperski},
journal= {arXiv preprint arXiv:1403.3524},
year = {2014}
}