@inproceedings{90b3d8582f324473a9b200de0f9180a5,
title = "Incremental Synthesis of Safe Controller Guided by Learning-Enabled Barrier Certificates with Efficient LP Verification",
abstract = "Safe controller synthesis with formal guarantees is widely employed in safety-critical systems. However, existing controller synthesis methods are subject to significant limitations in scalability and efficiency. This paper presents a novel controller incremental synthesis framework guided by barrier certificates (BCs), thereby generating a safe controller with BC verification. To enhance verification efficiency, we construct a learning-enabled polynomial BC combined with efficient post-verification, which is transformed into smaller-scale linear Programming (LP) subproblems for feasibility determination. Furthermore, we have implemented a tool called ISafeC and evaluated its performance over a set of benchmark examples. The comparative experimental results demonstrate the effectiveness and efficiency of our approach.",
keywords = "Barrier certificate, Controller synthesis, Formal verification, Linear programming, Reinforcement learning",
author = "Niuniu Qi and Hanrui Zhao and Zhengfeng Yang and Xia Zeng and Mengxin Ren and Chao Peng and Zhiming Liu",
note = "Publisher Copyright: {\textcopyright} The Author(s) 2026.; 27th International Symposium on Formal Methods, FM 2026 ; Conference date: 18-05-2026 Through 22-05-2026",
year = "2026",
doi = "10.1007/978-3-032-26204-2\_22",
language = "英语",
isbn = "9783032262035",
series = "Lecture Notes in Computer Science",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "419--439",
editor = "Augusto Sampaio and Marielle Stoelinga",
booktitle = "Formal Methods - 27th International Symposium, FM 2026, Proceedings",
address = "德国",
}