GOAL針對交替式自動機與時序邏輯翻譯的支援

Abstract

「交替」是非確定性的一種延伸，賦予了自動機更便利的狀態接合表達能力。儘管交替式自動機與非確定性自動機一樣，表述力侷限在ω正規語言，但善用交替的性質，我們能以更少的狀態建構出表達語言交集與聯集的自動機。將狀態接合的能力應用在邏輯接合，以時序邏輯表述的命題可更容易地轉譯成交替式自動機。然而，若是要將交替式自動機轉換成非確定性自動機，去除交替性將使狀態數量產生指數性成長。研究已經顯示我們可以直接檢查交替式自動機辨識的語言是否為空，而不需要事先去除自動機的交替性。因此，我們可以同時利用交替式自動機在大小與建置難易度方面的優點，並且在不犧牲空間與時間的前提下進行模型檢查。 這篇論文闡述我們對可操作ω自動機與時序邏輯公式的圖像化工具GOAL進行的擴充。GOAL已經實作了交替式自動機，不過支援交替式自動機的函式仍舊有限。我們針對交替式自動機的擴充將包含空集問題與宇集問題的檢查、建構Büchi與co-Büchi自動機的補集、以及從LTL與LDL公式轉譯至交替式自動機的演算法。我們亦實作了以反鏈為基礎的非確定性自動機的宇集問題檢查。我們還將GOAL表述自動機初始狀態的能力擴充到可以支援多個起始狀態，這將讓我們更方便呈現語言的聯集，而此擴充也已經植入GOAL既有的演算法。最後，我們引入符號型交替式自動機，以便使用者更方便地建構出定點運算以檢查時序邏輯公式的滿足性。