施楓

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

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