离散时间动力系统的余Buchi障碍证书
形式语言与自动机理论
2026-01-22 v2 系统与控制
系统与控制
摘要
障碍证书为动力系统可达集提供函数上近似，并对系统的安全演化提供归纳保证。在自动机理论验证中，一个关键查询是判定系统是否有限次访问给定状态谓词，这通常源于传统Buchi接受条件的补。本文提出一种障碍证书方法以回答此类查询，通过发展余Buchi障碍证书（CBBCs）的概念，将经典障碍证书推广以确保系统轨迹访问给定谓词固定次数。我们的CBBC概念受限于LTL可实现性的有界综合范式启发，其中LTL规约经泛余Buchi自动机转换为安全自动机，并将最终状态访问次数的界作为超参数给出。我们在验证中对CBBC的应用类似：固定一个界并搜索合适的障碍证书，若找不到合适函数则增大界。随后我们使用这些CBBC针对余Buchi自动机指定的性质验证系统，并通过若干案例研究展示其有效性。
引用
@article{arxiv.2311.07695,
title = {Co-Buchi Barrier Certificates for Discrete-time Dynamical Systems},
author = {Vishnu Murali and Ashutosh Trivedi and Majid Zamani},
journal= {arXiv preprint arXiv:2311.07695},
year = {2026}
}