满足线性时序逻辑规范的混合障碍证书方法
系统与控制
2020-11-24 v1 形式语言与自动机理论
系统与控制
动力系统
摘要
在这项工作中，我们通过近期的混合动力系统形式化方法，表述了物理装置上（语法上 co-safe）线性时序逻辑规范的满足问题。为解决该问题，我们向此类混合系统框架引入了所谓事件性(eventuality)性质的扩展，其恰当地匹配了该时序逻辑规范满足的条件。事件性性质可通过障碍证书建立，我们针对所考虑的混系统框架推导了相应证书。利用混合障碍证书，我们提出了原问题的一种解法。仿真验证了所提方法的有效性。
引用
@article{arxiv.2011.11464,
title = {A hybrid barrier certificate approach to satisfy linear temporal logic specifications},
author = {Andrea Bisoffi and Dimos V. Dimarogonas},
journal= {arXiv preprint arXiv:2011.11464},
year = {2020}
}