基於混合自動機的多台自駕車系統相容性驗證框架

Abstract

多台自駕車系統（autonomous multi-vehicle systems）越來越常被部署於去中心化的交通環境中，在此情境下，每輛車輛皆需獨立進行決策，確保行車安全與運行效率遂至關重要。然而，現有的大多數驗證技術仍多依賴特定場景，缺乏嚴謹的保證，特別是在車輛間行為相容性的檢查上。本文針對這一缺口，提出一套形式化驗證框架，能系統性檢查給定的道路條件下，各自獨立開發的車輛其行為是否相容。 本框架根據混合自動機（hybrid automata）來建模車輛的連續動態與離散決策邏輯，並藉由修改原始定義，成功產生一種新穎的自動機形式，既支援組合式驗證，也與現有混合系統驗證工具相容。透過車輛模型的組合，我們能夠針對整合後的系統模型，驗證安全性及活性（liveness）等性質是否滿足，進而得到系統層級的嚴謹分析。 為驗證框架的實用性，我們將其應用於一個涉及異質規劃與決策控制器的變換車道場景。利用 Flow* 此驗證工具，我們展示了該方法可偵測行為不相容之處，並識別出可安全執行協同操作的初始狀態。實驗結果凸顯了形式驗證在提升自主多車輛系統可靠性方面的潛力。

Autonomous multi-vehicle systems (MVSs) are increasingly deployed in decentralized traffic environments, where each vehicle makes decisions independently. While ensuring safety and efficiency in such settings is critical, most existing validation techniques remain scenario-specific and lack rigorous guarantees, particularly regarding inter-vehicle compatibility. This thesis addresses this gap by developing a formal verification framework that systematically checks whether the behaviors of independently developed vehicles are compatible under shared road conditions.

The proposed framework adopts hybrid automata to model both the continuous dynamics and discrete decision logic of individual vehicles. We introduce a novel automaton formalism that facilitates compositional verification and is compatible with existing hybrid-system verification tools. By composing vehicle models and verifying global safety and liveness properties, our approach enables rigorous system-level analysis.

To demonstrate the practicality of the framework, we apply it to a lane-changing scenario involving heterogeneous planning-and-decision controllers. Using the Flow* tool, we show that our method can detect compatibility violations and identify safe initial states for coordinated maneuvers. The results highlight the potential of formal verification methods in advancing the reliability of autonomous MVSs.