一類非線性混合自動機的離散化驗證

施楓

摘要：混合系統是同時包含有相互作用的連續性子系統和離散性子系統的一類動態系統?；旌献詣訖C是目前混合系統驗證研究中最常用的一種形式化模型。由于混合自動機連續變量的復雜性以及連續變量和離散變量的相互作用性，對混合自動機的可達集的計算一直是一個復雜而難以解決的問題。該文提出了在連續時間下針對一類非線性混合自動機的離散化驗證算法，通過求出混合自動機每次發生離散遷移之后，在新的控制模式下的可達集的區域近似極值來解決該文所研究的問題。實驗結果表明，該文提出的算法可以有效地對連續時間下的一類非線性混合自動機所代表的混合系統的部分性質進行驗證。

關鍵詞：混合自動機；離散化驗證；計算樹邏輯；連續變量；形式化驗證