轉(zhuǎn)換系統(tǒng)行為近似等價性的研究.pdf

1、在形式化方法研究領域，轉(zhuǎn)換系統(tǒng)是描述軟件或硬件系統(tǒng)行為的一種重要形式化模型。近年來，針對實時系統(tǒng)、控制系統(tǒng)及最優(yōu)化問題等實際系統(tǒng)的建模需要，學術(shù)界提出了諸多帶有量化信息的轉(zhuǎn)換系統(tǒng)。對于這些系統(tǒng)而言，傳統(tǒng)的互模擬概念不適合描述系統(tǒng)間的行為等價性。為了克服這一缺陷，研究者們提出了眾多近似等價概念并開展了較深入的理論和應用研究。本文將就帶有量化信息的轉(zhuǎn)換系統(tǒng)的近似等價理論開展研究，全文工作分為理論研究與應用研究兩部分。理論研究方面的主要工作包

2、括如下方面：
　　 (1)近似互模擬與距離函數(shù)是定義系統(tǒng)近似等價的兩種主要方法，在度量化的轉(zhuǎn)換系統(tǒng)的框架下，應明生教授和Breugel采用這兩種方法分別提出了λ-互模擬和行為擬度量。本文研究了兩者之間的關系，否定了Breugel的猜想，建立了λ-互模擬誘導出的λ-行為擬度量的不動點特征。
　　 (2)在量化轉(zhuǎn)換系統(tǒng)框架下，本文將折扣的思想引入近似互模擬的定義中，提出了(η，α)-互模擬概念，其中參量η表示狀態(tài)之間的近似程

3、度，α是一個折扣因子。本文給出了(η，α)-互模擬的一些基本性質(zhì)，研究了(η，α)-互模擬與Girard和Pappas提出的δ-近似互模擬之間的關系，建立了(η，α)-互模擬的分層刻畫，并探討了(η，α)-互模擬誘導出的距離函數(shù)的相關性質(zhì)。在量化轉(zhuǎn)換系統(tǒng)框架下，de Alfaro等人提出了分岔距離用于描述系統(tǒng)的行為近似等價性。本文討論了(η，α)-互模擬與分岔距離之間的關系，利用(η，α)-互模擬給出任意折扣下分岔距離的互模擬刻畫，從而

4、將Girard和Pappas關于無折扣分岔距離的互模擬刻畫的結(jié)果推廣到一般情形。本文還證明了，在非死鎖和有限分岔的量化轉(zhuǎn)換系統(tǒng)中，(η，α)-互模擬也可以由分岔距離刻畫。這些結(jié)論揭示了(η，α)-互模擬與分岔距離之間的內(nèi)在聯(lián)系。
　　 (3)交替轉(zhuǎn)換系統(tǒng)是一種刻畫開放式系統(tǒng)的重要形式化模型。針對一類特殊的交替轉(zhuǎn)換系統(tǒng)，Pola和Tabuada定義了交替近似互模擬的概念用于刻畫帶擾動控制系統(tǒng)與其有限抽象之間的關系。本文將這個概念推

5、廣到一般的交替轉(zhuǎn)換系統(tǒng)中，探討了交替近似互模擬的基本性質(zhì)，并提出了一種近似互模擬模態(tài)特征表述方式，基于交替時序邏輯給出了交替近似互模擬的邏輯特征，從而建立了交替轉(zhuǎn)換系統(tǒng)間行為近似等價性與其所滿足的邏輯性質(zhì)之間的內(nèi)在聯(lián)系。
　　 應用研究方面的工作側(cè)重解決帶擾動線性控制系統(tǒng)的形式化設計中遇到的若干問題?？刂葡到y(tǒng)的形式化設計旨在利用形式化的方法構(gòu)造控制系統(tǒng)的反饋控制器使得控制系統(tǒng)在該控制器作用下滿足給定的規(guī)范。最近幾年，學術(shù)界已經(jīng)就

6、無擾動控制系統(tǒng)的形式化設計展開了一系列研究。在這些工作中，為了降低控制系統(tǒng)的狀態(tài)空間的規(guī)模，研究者們通常構(gòu)造控制系統(tǒng)的有限抽象系統(tǒng)，進而通過構(gòu)造有限抽象系統(tǒng)的控制器得到原控制系統(tǒng)的控制器。本文試圖將這一技術(shù)路線推廣到帶擾動線性控制系統(tǒng)的形式化設計中，主要工作包括：
　　 (4)本文給出了一個控制策略算法用于構(gòu)造帶擾動線性控制系統(tǒng)的有限抽象的控制策略。在無擾動情形下，控制系統(tǒng)的有限抽象一般是經(jīng)典的轉(zhuǎn)換系統(tǒng)。文獻中給出了諸多算法用于

7、求解無擾動情形下控制系統(tǒng)的有限抽象的控制策略。然而，在帶擾動輸入的情形下，經(jīng)典的轉(zhuǎn)換系統(tǒng)無法刻畫可控輸入和擾動輸入之間的差別。為了克服這一缺陷，Pola和Tabuada采用交替轉(zhuǎn)換系統(tǒng)作為帶擾動控制系統(tǒng)與其有限抽象的形式化模型，這導致在無擾動情形下提出的各種算法不適用于求解帶擾動控制系統(tǒng)的有限抽象的控制策略。本文基于Kabanza等人提出的規(guī)劃算法給出了一個控制策略算法用于求解控制策略。具體而言，對給定的有限交替轉(zhuǎn)換系統(tǒng)和線性時序邏輯公

8、式，該算法可以用于尋找初始狀態(tài)和控制策略使得交替轉(zhuǎn)換系統(tǒng)可控滿足給定的線性時序邏輯公式。
　　 (5)本文證明了上述控制策略算法的正確性，并就一類時序邏輯公式證明了它的完備性。我們基于完全的Büchi自動機定義了完全公式概念，并證明對于完全公式而言，上述控制策略算法是完備的，即，給定有限交替轉(zhuǎn)換系統(tǒng)和完全的線性時序邏輯公式，如果存在初始狀態(tài)和控制策略使得交替轉(zhuǎn)換系統(tǒng)在該控制策略作用下從該初始狀態(tài)出發(fā)的所有軌跡均滿足給定的線性時序

9、邏輯公式，則上述控制策略算法必然可以找到所需的初始狀態(tài)和控制策略。
　　 (6)本文提出了一種基于有限抽象構(gòu)造帶擾動控制系統(tǒng)控制器的方法。在無擾動情形下，學術(shù)界先后分別基于互模擬和近似互模擬提出了兩種方法用于控制系統(tǒng)的形式化設計。這兩種方法采用了相近的技術(shù)路線，即，構(gòu)造與原系統(tǒng)互模擬(或近似互模擬)的有限抽象，進而通過構(gòu)造有限抽象的控制器得到原控制系統(tǒng)的控制器?；谂c原系統(tǒng)互模擬的有限抽象構(gòu)造的控制器可以確保控制系統(tǒng)在其作用下嚴

10、格滿足給定規(guī)范。然而，由于互模擬要求嚴格，與原系統(tǒng)互模擬的有限抽象較難構(gòu)造。Girard和Pappas退而求其次，提出了基于與原系統(tǒng)近似互模擬的有限抽象的控制器設計方法。這樣的有限抽象相對容易構(gòu)造，但該方法構(gòu)造的控制器僅能確?？刂葡到y(tǒng)近似滿足給定規(guī)范。我們基于本文交替近似互模擬邏輯特征的工作，針對帶擾動控制系統(tǒng)提出了另一種控制器形式化設計思路。本文方法的核心在于規(guī)范的轉(zhuǎn)換。我們提出了兩個規(guī)范轉(zhuǎn)換函數(shù)?；谵D(zhuǎn)換后的規(guī)范構(gòu)建有限抽象系統(tǒng)的控