混成系統研究綜述

摘 要：混成系統是一類既包含連續動態行為又包含離散動態行為的系統，這類系統在實際應用中顯得越來越重要，對這類系統需要探索新的模型和研究方法。從建模、分析與驗證三個方面綜述了混成系統的研究現狀和需要進一步研究的課題。

關鍵詞：混成系統; 建模; 分析; 驗證

中圖分類號：TP13文獻標志碼：A 文章編號：1001-3695(2008)08-2255-05

Survey on hybrid system

LI Lang1，2， LI Ren-fa1， LI Ken-li1， YAO Feng-juan1

( 1.College of Computer Communication， Hunan University， Changsha 410082 ， China; 2.Dept. of Computer， Hengyang Normal University， Hengyang Hunan 421001， China)

Abstract:The hybrid systems contain both the discrete events and the continuous dynamic events. These systems are beco-ming more and more important and call for new modeling and analysis approach. This paper reviewed status of the hybrid system from modeling， analysis and verification of the three aspects and the need for further researches.

Key words：hybrid system; modeling; analysis; verification

0 引言

混成系統一般由離散分離組件和連續組件并行或串行組成，組件之間的行為由計算模型進行控制。大多數復雜控制系統都包含了由連續變量所描述的物理層的動態演化過程和以符號操作與離散監控決策為特征的高層協調優化過程，因此混成系統在工業控制和國防等領域大量存在。同時，現代計算機技術的高速發展和普及應用，為系統的模型化、優化控制和決策問題提供了強有力的技術支持。關于混成系統的多學科研究在過去二十多年來發展迅速，已成為當今計算機科學與控制學科的前沿研究熱點。

第一篇混成系統的研究文獻出現于1966年^[1]，Witsen 研究了一類具有混成狀態的連續時間動態系統的優化問題。1979年，Cellier提出了將系統分為離散、連續和接口三個部分的混成系統結構的概念^[2]；1989年，Golli等人將連續部分與接口相結合^[3]。20世紀90年代，混成系統的研究進入快速發展時期，隨著這方面的巨大應用需求，近年來成為研究的熱點。國際上每年都有不少關于混成系統的專門會議如International Hybrid Systems Workshop、International Workshop on Hybrid and Real-time Systems、 Hybrid System: Computation and Control等；許多國際著名刊物如IEEE Trans actons on Automatic Control、ACM Transactions on Modeling and Computer Simulation、Procee-dings of IEEE等近年來也相繼出專輯介紹混成系統的理論與應用現狀。

世界上許多大學和研究機構都成立了關于混成系統理論與應用的研究小組，并各具自己的研究特色。國外比較著名的有美國的Pennsylvania大學、California大學、Berkeley大學、Stanford大學、MIT、 Yale大學等。國外知名的混成系統研究學者有偏重于控制學科方面的如PanosAntsaklis、Roger Brockett、 Peter Caines等，以及偏重于計算機科學方面的如R.Alur、Tom Henzinger和Nancy Lynch等。

國內對混成系統的研究相對國外要晚一點，但也取得了很多理論和應用上的成果，且得到計算機、控制和數學方面的深入研究。國內研究混成系統的大學和研究機構主要有清華大學、東北大學、中國科學院自動化所、浙江大學、上海交通大學、東南大學、北京航空航天大學、北京工業大學等；湖南大學計算機與通信學院的嵌入式與網絡實驗室在混成理論的應用方面也做了一些工作，如混成理論在網絡擁塞控制中的應用、實際混成系統的驗證平臺設計與開發。近年來在《中國科學》《自動化學報》《控制與決策》《控制理論與應用》《計算機學報》《軟件學報》《計算機研究與發展》等權威雜志上均有混成系統方面的文章，但國內對混成系統的研究主要偏重于控制科學方面。

1997年召開了第五屆國際混成系統的研討會(HSCC1997)，與會學者們認為混成系統研究的基本問題可以分為三個方面:a)如何對混成系統建模；b)如何驗證系統的行為滿足程序和性能的規范要求；c)如何從實際的物理系統及仿真模型中提取性能指標要求，并設計控制與決策使得系統滿足給定的性能指標。

在2006年嵌入式系統國際會議（HSCC2006）上，谷德權（John Koo）教授又再一次對上述觀點作了進一步的闡述，即混成系統的建模、形式化分析與驗證技術。隨著實時與混成系統在工業及國防等領域得到越來越廣泛的應用，混成系統中的數理邏輯、計算模型與方法、自動推理工具、采用形式化分析和驗證技術(特別是模型檢測技術)等均為重要研究方向。特別地，用形式化方法對實時混成系統的軟件系統設計和綜合的正確性進行驗證，保證這些系統的可靠性成為近年來計算機科學與控制論領域的一個研究熱點。

本文以混成系統的建模、分析與驗證為主線，綜述混成系統目前研究的主要進展、成果以及存在的問題和研究難點，并對某些問題結合筆者的研究和工作實踐提出一些看法和探討。

1 混成系統的建模

為了保證混成系統可靠性、可達性、可控性，特別是對于某些安全關鍵系統，通過數學工具在某種意義上能夠準確地預測系統將來行為的建模技術顯得非常重要。只有對系統行為模型進行準確的數學刻畫，才能對其可達性、穩定性等性能進行準確分析，所以混成系統的建模需要正確、統一地描述連續與離散動態特性及其相互關系。最有效的方法之一就是將連續與離散系統的模型描述有機結合起來，充分利用現有模型的特長，這就需要將連續動態系統的模型嵌入到離散行為描述中去，或者將離散行為描述嵌入到連續動態的模型中去。另外，還有不少學者嘗試建立一種統一的混成系統模型。

目前對混成系統進行建模和描述，最主要的方法有兩種，即基于DEDS的建模方法(將連續動態系統的模型嵌入到離散行為描述中)和基于CVDS 的建模方法(將離散行為描述嵌入到連續動態的模型中)。

早期O. Maler等人提出的相位轉換系統(phase transitionsystems)模型、1993年R. Alur等人首次提出的能同時作為混成系統的系統刻畫語言來表示混成系統實現的混成自動機(hybrid automata)^[4，5]、Bail等人在20世紀90年代初首次提出的更適合于異步并發系統的建模和分析的混成Petri網的形式結構模型，均是基于DEDS建模方法。然而相位轉換系統、混成自動機和混成Petri網模型總體上都是基于狀態轉換的思想，在處理復雜問題時，可能遇到狀態爆炸的情況，這將使其后面的分析工作無法進行下去。

Ilya Kolmanovsky等人提出的用多個控制器按切換方式控制一個連續對象的基于邏輯轉換的切換系統模型、Morari 提出的通過連續與離散特性相互依賴的物理規律、邏輯法則和操作約束共同描述系統的混成邏輯動態系統模型(MLD模型)、R.Alur將線性系統與有限自動機結合的混成控制模型，均為基于CVDS的建模方法的模型。然而，上述模型多是針對具體問題加以研究， 模型的通用性不好。

除上述兩大類建模方法外， 還有如下一些建模方法:Bra-nicky提出了針對混成系統分析設計的模型框架建立的一種統一混成系統模型^[6]；Mosterman等人則將能量的觀點引入Bond Graph中，將事件的發生視為能量的變化，結合離散事件的理想開關、控制節點及相應的有限自動機來描述系統中復雜的多模態行為^[7]；Tavernini提出用數字估計方法預測混成系統軌跡的收斂性的微分自動機模型；Grossman提出的多agent混成系統模型；Park將線性跳變系統與有限自動機結合作為混成系統的模型；Le Yi-wang等人提出了一個新的混成控制系統的模型和結構;De.Schutter將一類混成系統的問題歸結為擴展的線性補集問題，然后采用整數規劃的方式進行處理。

在混成系統眾多模型中，盡管所采用的建模方法不盡相同，但混成系統的現有模型多是針對具體問題加以研究， 而將離散事件理論與成熟的連續系統理論相結合的通用模型卻很少。同時，對于許多實際混成系統為大規模的復雜系統，目前建模方法在模塊化方面考慮不多。

混成系統是一門交叉學科，所解決的問題復雜多樣，因此就需要人們在模型的通用性方面進一步深入研究。發展形式化的描述工具，刻畫混成系統行為本質是目前研究的主要問題，并期待在將來有所突破。

2 混成系統的分析與設計

2．1 穩定性分析

穩定性分析是混成系統一個最根本的問題，如果模型不穩定，就沒有意義。現有的混成系統穩定性分析結果主要是針對切換系統的。許多研究者認為非線性系統問題可以通過切換方式變成線性系統問題。切換系統穩定性的一個顯著特點是其子系統的穩定性不等于整個系統的穩定性，即每個子系統是穩定的，但組合起來的大系統可能不穩定；同樣，盡管每個子系統是不穩定的，但是可以通過某種切換規則或切換策略使整個系統穩定。即使切換系統每個子系統都是線性定常系統，其整體也不是線性系統，屬于非線性系統。文獻[8]構造了一種切換線性定常系統，結果表明該切換線性定常系統能夠產生合盆混沌吸引子，而混沌現象正是非線性系統的特性之一。

對于自治切換系統

x·(u)=f(x(u)，p(u))≡fp(u)(x(u))(1)

其中：p(u)∈{1，…，M}分段右連續。其穩定性問題可歸結為三類^[9]: a)對于任意的切換序列，系統是否穩定; b)對于給定的某類切換序列，系統是否穩定; c)構造使系統穩定的切換序列，即鎮定問題。

眾多學者對切換系統穩定性問題進行了研究并取得了一定的成果，其主要內容如下：

a)統一李雅普諾夫(Lgapunov)函數法。該函數法與傳統的李雅普諾夫直接法基本是一致的。主要思想是:對于切換系統，若各子系統存在統一李雅普諾夫函數，那么系統對于任意的切換序列都穩定。問題的關鍵在于統一李雅普諾夫函數是否存在以及如何構造。對于切換線性定常系統

x·= Ax(2)

其中：A在子系統{A1，A2，…，An}間切換，各狀態變量值在切換時刻不發生跳變。 文獻[10]證明了對于切換系統（式(2)），若子系統x·= Aix (i=1，2， …，N)都漸近穩定，且各子系統的狀態矩陣可以兩兩互換，即i，j≤N 有AiAj=AjAi成立，則整個切換系統是漸近穩定的。文獻[10]進一步給出了統一李雅普諾夫函數的一種構造方法。

文獻[11]利用李代數對統一李雅普諾夫函數法進行了研究，主要思想是將統一李雅普諾夫函數的存在性問題轉換為切換系統李代數的可解性問題。當式(1)的子系統為線性系統時，文獻[11]中證明了若式(1)對應的李代數是可解的，則系統存在統一的李雅普諾夫函數，且對于任意切換序列都是全局一致指數穩定的；子系統為非線性系統時，進一步證明了若式(1)對應的李代數是可解的，則系統對于任意切換序列是局部一致指數穩定的。

b)多李雅普諾夫函數法。M. S. Branicky從切換系統的特點出發提出了多李雅普諾夫函數法^[12]。其主要思想是為切換系統定義一組類李雅普諾夫函數{Vi， i = 1，…，M}，然后判定切換系統的穩定性。 對于式(1)，假設各子系統切換時狀態不發生跳變，平衡點為切換序列是否穩定；多李雅普諾夫函數法研究系統對于一類切換序列是否穩定。當式(1)只有一個子系統時，多李雅普諾夫函數法退化為常見的李雅普諾夫直接法；當各子系統李雅普諾夫函數相同時，可視做統一李雅普諾夫函數法。M. S.Branicky進一步拓展了多李雅普諾夫函數法，使之適用于各子系統平衡點不同的情形。文獻[13]研究了當子系統切換時狀態發生跳變系統的穩定性。文獻[14]放寬了多李雅普諾夫函數法的前提假設，不要求fi(x)是全局Lipschiz連續的。文獻[15]在李雅普諾夫穩定性的基礎上更進一步論證了切換系統的漸近穩定性及指數穩定性。

c)其他相關問題。對于李雅普諾夫直接判別法，一個具有挑戰性的問題是李雅普諾夫函數如何構造。遺憾的是，目前尚無統一的方法。對于切換線性系統，目前主要的做法是將李雅普諾夫穩定性的判別轉換為LMI問題的求解，文獻[16]對此進行了研究。LMI法的優點是可利用軟件包(如MATLAB工具箱)求得可靠的數值解，借助LMI判定切換系統的穩定性是一個值得注意的研究方向。對于切換系統，一個有意義的問題是:如果切換系統是穩定的，那么系統是否存在統一李雅普諾夫函數，這就是所謂逆李雅普諾夫原理。文獻[17，18]對此進行了研究。在文獻[19]中提出了對采用切換PI控制器的線性系統的穩定性判別方法，具體做法是將非線性積分環節孤立出來，轉換為Lurie系統，利用POPOV絕對穩定性判據進行判別。文獻[20]討論了切換線性定常系統產生極限環的現象，并采用Poincaré映射來判別極限環的穩定性。

2.2 系統設計

混成系統設計的目的是使受控對象按照期望的方式運行，混成系統設計從設計方法學的角度看，大致有自上而下、自下而上或兩者結合的方法。基于精化的思想是典型的自上而下的方法，而經典控制中的分析方法多是自下而上的方法。將兩者有機結合在復雜的混成系統，特別是連續動態和離散動態耦合明顯的混成系統設計中就顯得格外重要。

在混成系統中，連續變量、離散變量和事件變量可能同時存在，這就使得混成系統的設計不僅表現為數值反饋的設計，而且表現為離散事件層的邏輯控制設計。如果能夠歸結出下層數值回路的等價離散事件模型，就可以在離散事件域進行控制器的設計綜合。形式化建模方法上的形式化設計技術是一項有影響力的設計技術。首先建立對系統行為和模型的嚴格描述；其次嚴格描述系統的需求；然后嚴格設計系統變量，逐步細化以滿足給定的需求規范。

混成系統研究的另一焦點是優化控制問題。文獻[21]針對切換自治系統研究了在切換序列給定、切換時刻狀態不跳變的情況下，如何選擇切換時刻使性能指標極小，從而實現最優切換控制； 文獻[22]研究了切換線性系統由一個狀態切換至另一狀態時，如何在切換次數最少的情況下實現目標； 文獻[23]討論了切換線性系統的廣義線性二次最優控制問題，即始末時刻固定，尋找最優的連續輸入及切換序列使性能指標極小的控制問題。

其他一些對混成系統進行分析的方法主要集中在幾類實際應用的需求上。數學規劃領域中的最優化技術，如整數規劃，已經在化學混成加工中解決了一些問題。離散事件系統方法，如極大代數方法，已經在混成系統的分析和設計中得到了應用，主要在魯棒制造系統中用于綜合任務調度、行動規劃和控制。最優控制方法可以用來解決一些制造問題，設計一個控制策略來對工作質量和完成時間作一個最優的安排，而這樣的問題已經可以用公式來表達并且得到了解決。在這種情況下，這種公式綜合了連續由時間驅動的動態部分和離散由事件驅動的動態部分。

3 混成系統的驗證

混成系統的驗證就是檢測系統所期望的一些屬性是否能得到滿足。工業界對混成系統控制方案的安全性驗證有著非常迫切的需求，使得計算機領域中的形式驗證方法在混成控制系統中得到應用。近年來，國際上有多個研究組從事混成系統形式驗證的研究并取得了一些成果，開發出了一些針對具體系統的協同驗證平臺。歐洲在1998年正式啟動混成系統驗證計劃（VHS），其中包括法國VERIMAG工作組、德國Dortmund大學和歐洲其他各國科學家；美國的Stanford大學、Carnegie Mellon大學和Cornell大學也從事此類研究?，F在已有的一些成果從不同角度研究驗證問題，提供了不同的驗證工具，給出了多個工業驗證的實際案例。

混成系統中包含連續變量動態系統和離散事件動態系統，系統中連續變量和離散事件之間存在著相互作用，也就是說混成系統在各個具有不同動態規律的模式間切換，模式的切換由不同類型的離散事件觸發，如狀態事件(狀態變量越過指定的閾值)、定時器事件和外部輸入事件等?；斐上到y中離散事件和連續動態行為間相互作用的特性使得系統開發的復雜性增加，開發結果的正確性也難以保證。尤其對于如航天、電力和化工等系統，對系統安全性的要求非常高，系統的錯誤運行將造成重大損失。形式驗證技術的目的在于檢驗混成系統是否在任何環境下都能保證安全運行。因此，混成系統形式驗證問題的研究有著重要的科學價值和工程意義。

系統從某一初始狀態集合出發，在一定時間內可能到達的所有狀態的集合稱為系統的可達集?；斐上到y的形式驗證技術是對系統模型進行可達性分析，即分析在給定的初始條件集合下，系統的可達集是否都在目標狀態集合內?；斐上到y的形式驗證技術是對仿真技術的拓展。仿真技術是從某一個初始狀態出發，一次只能檢驗系統的一條路徑，即使進行了數千次仿真仍然可能錯過一些重要的安全因素?；斐上到y的形式驗證技術是通過窮舉算法對系統進行可達分析:在一次運行中，給定初始狀態和輸入信號的集合后，模型檢查系統的每一種可能行為來證明所有的可達狀態是否滿足預定的規范，從而為控制程序的可靠性提供了科學分析。

混成系統的驗證方法主要有如下兩種：

a)定理證明，將系統的安全要求規范用定理表示，用形式化的推理方法對系統屬性進行證明。定理證明方法通過一些公理或推理規則來證明系統具有某些性質，其推理方法主要有自然推演、歸結、Hoare邏輯以及時序演算（如Manna-Pnueli命題線性時序邏輯PLTL^[24]）等；常見演繹推理工具包括機器定理證明器或檢驗器ACL2、HOL、TLV、Coq等^{[25，26]}。定理證明的優點是既可以驗證有窮狀態系統，又可以使用歸納方法來處理無限狀態問題，但不足之處在于不能完全自動化，對于多維復雜系統需要人工干預，效率較低。因此該方法難以被工業界所接受。

b）模型檢驗，在整個狀態空間中搜索，對系統所有可能的運行路徑進行收斂近似或過近似，以檢查系統是否滿足安全規范的要求。收斂近似和過近似方法是模型檢驗的兩種主要方法。收斂近似力求盡可能真實地表達可達集，它采用后向可達性分析，一般從非安全狀態集合出發，后向計算可達集。目前，收斂近似采用的計算技術主要有基于穩態Hamilton-Jacobi方程方法、基于生存理論的方法、可以表達和分析任意形狀的非線性混成系統的基于水平集表達和Hamilton-Jacobi方程粘性解的方法。收斂近似方法雖能處理無須限制可達集形狀的連續部分，但是算法賴以計算的網格節點數隨系統維數呈指數增長，故僅限于低維系統驗證。目前許多驗證工具在實際應用中最多就只能驗證到六維。過近似驗證方法確保計算所得可達集是實際可達集的擴大。對于安全性驗證問題，過近似方法從初始狀態集合出發，前向計算可達集，檢查可達集是否在給定安全狀態集合內。可達集的表示方法和對連續動態類型的限制是過近似方法中的兩個關鍵問題?？蛇_集的表示方法主要有超矩形、多面體和橢圓體。超矩形容易表示且超矩形面的數量與連續空間維數呈線性關系，但要實現足夠精確的表示可達集，則需要增加大量的柵格；多面體對凸集有很好的近似，然而多面體面和頂點的數量隨著連續空間維數的增長而大量增加，導致其不適用于高維系統；橢圓體雖與連續空間維數呈二次關系，但橢圓體的相交部分和合并部分卻非橢圓體。由此可見，過近似方法是可達集表示的復雜度、多面體數量和可達集的近似精確度之間的折中。目前大部分過近似方法難以處理非線性，而將連續動態行為限制為線性的。模型檢驗方法的優點是可以實現自動化，且驗證速度快、效率高；并且如果一個性質不滿足，它能給出這個性質不滿足的理由，據此可對系統描述進行改進。該方法因此被工業界和學術界廣泛關注，但某些情況下不能保證驗證的可決策性。在混成系統的模型檢驗方法中，關鍵問題是如何計算在某一初始狀態集合下系統連續部分的可達集。

總之，由于離散變化和連續變化分析方法不同，且這兩種變化間的相互影響復雜，驗證一個混成系統的正確性是比較困難的。大多數情況下這種系統的模型檢測問題是不可判定的，故混成系統的算法驗證主要集中在線性混成系統的模型檢查(如R.Alur等人討論了線性混成系統的符號模型檢查，T. A. Henzinger等人對線性混成系統的一些重要子類如多速率混成系統、矩形混成系統等的可達性判定問題進行了討論)，對線性系統的模型檢查也僅僅是限于低維的。而用定理表示系統的安全要求規范、用形式化的推理方法對系統屬性進行證明的定理證明方法雖然不局限于有限狀態系統，但是需要人工干預，難以形成自動化的驗證工具。

目前應用模型檢驗方法的驗證工具主要有UPPAL、KRONOS、HyTech、HyperTech、d/dt、CheckMate、Verdict、Cospan/Formal Check(Bell)、MURPHY(Stanford)、SPIN(Bell)、SMV(CMU)、VIS(Berkeley)等^[27、28]。從驗證工具對系統連續動態行為限制的角度分析，UPPAL與KRONOS適用于賦時自動機；Hytech適用于線性混成自動機；VeriShift適用于連續動態行為用線性微分包含描述的混成系統；d/dt適用于連續動態行為用線性微分方程x′=ax+bu描述的混成系統；CheckMate與Verdict可用于非線性連續動態系統，但可處理的非線性類型有限；HyperTech (HyTech的升級)由于采用區間代數算法，可用于非線性連續動態系統。

雖然混成系統形式驗證技術的研究已取得了一些初步成果，在汽車控制、過程控制和機器人技術等領域中有多個實例得到驗證。例如Bruce應用CheckMate對化工過程控制系統和汽車中的電子節流閥控制系統進行了驗證；Tomlin應用水平集和Hamilton-Jacobi方程粘性解的方法成功驗證了飛機自動著陸系統；Eugene應用工具d/dt驗證了自動高速公路系統中的車輛防撞系統。但目前各種驗證工具都是針對某些具體問題和系統提出來的，沒有一個通用解決方法體系，需解決的問題主要有^[29]：

a)由于可達集計算的復雜性，導致時間和內存的大量消耗，現有的驗證技術和工具僅適用于小規模的系統，連續變量空間維數一般不超過六維。

b)現有的驗證工具在得出系統可能不滿足安全規范后，不能指出系統不安全的原因和系統的控制策略以及參數設計應該如何修改。

c)混成系統的形式驗證只對一些特定的系統才有確定性結果，大多數系統的驗證不可決策，給實際應用帶來困難。

如何建立可達性可決策的混成系統模型是迫切需要解決的問題，是今后研究者主要的努力方向之一。

4 結束語

混成系統理論及應用的研究取得了一定的進展， 但混成系統仍有許多問題亟待解決， 主要包括以下幾個方面^[30~43]:

a)混成系統的現有模型多是針對具體問題加以研究，從通用的角度進行建模， 將離散事件理論與成熟的連續系統理論相結合將可能是一條有效的途徑。但也有許多工作有待解決，往往會出現理論上的通用模型實際應用并不可行，但可以從現有對具體問題的混成經典模型出發，考慮輸入和輸出不同，建立通用某一類的混成模型。

b)非線性系統的混成理論與應用研究在實際應用中存在著大量的非線性問題，如何把線性理論擴展應用到非線性中去解決實際問題，是人們目前需要研究的一個非常重要的方向。

c)如何回避對實際系統過度抽象后容易出現的Zeno現象，以及對Zeno現象發生后的處理方法。

d)混成系統的研究工作集中在對系統可達集的準確或近似計算方面， 但由于混成系統的復雜性，多數情況下難以給出顯式解。 如何計算系統可達集以及如何簡化算法， 也是一個重要的研究方向。

e)混成系統能控性和穩定性的研究對于系統綜合設計和優化控制具有重要意義， 但要獲得一般性結果卻存在著困難。 在探索簡化復雜性一般方法的同時， 也可針對具體問題按照分散集約的方式獲得相關結果。

f)混成計算的進一步研究與深入應用，用計算機或嵌入式設備來處理的問題最終將歸結到計算問題。如何設計更好的算法，以及對非線性問題如何處理是研究的重點與難點。

g)混成控制系統復雜的組織結構和信息耦合關系決定了混成控制系統問題的求解需要混合的求解方法。如何融合多學科的理論、方法和數學工具是待解問題。

雖然混成系統不成熟的理論體系將使混成系統的研究充滿困難，但是深厚的工程背景需求會使混成系統的研究充滿活力。現在有些學者又開始提出復雜系統的概念，這是一個包含多個混成系統的大系統，問題的復雜性比混成系統更大，建模、分析與驗證起來更困難。因此，對混成系統理論和應用上的突破必將對復雜系統有重大的理論和應用意義。混成系統模型描述、混成系統的分析與設計、混成系統的驗證與仿真是當前研究的主要方向。

致謝：本文得到了國內實時混成專家周巢塵院士的具體指導，并得到其許多寶貴的建設性意見，在此特別表示感謝。

參考文獻：

[1]WITSENHAUSEN S. A class of hybrid-state continuous-time dynamic systems[J]. IEEE Trans onAutomatic Control，1966， 11(2):161-167.

[2]CELLIER F E. Combined continuous/discrete system simulation by use of digital computer: techniques and tools[D] . Zurich， Switzerland: Swiss Federal Institute of Technology ，1979.

[3]GOLLI A， VARAIYA P. Hybrid dynamical systems[C]// Proc of the 28th IEEE Conference on Decision and Control. 1989:2708-2712.

[4]ALUR R， COURCOUBETIS C， HENIGER T A， et al. Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems[C]//Proc of Hybrid Systems Workshop. Berlin: Springer-Verlag， 1993:209-229.

[5]ALUR R， DILL D L. The theory of timed automata[J] . TheoreticalComputer Science， 1994，126(2):183-235.

[6]BRANICKY M S， BORKAR V S， MITTER S K. A unified framework for hybrid control: model and optimal control theory[J].IEEE Trans on Automatic Control， 1998，43(1):31-45.

[7]MOSTERMAN P J， BISWAS G. Principles for modeling， verification， and the simulation of hybrid dynamic systems[C]//Proc of the 5th International Conference on Hybrid Systems. 1997: 21-27.

[8]LU Jin-hu， YU Xing-huo， CHEN Guan-rong. Merged basins of attraction : a switching piecewise linear control approach[J]. IEEE Trans on Circuits and Systems I: Fundamental Theory and Applications， 2003， 50(2):198-207.

[9]LIBERZON D， MORSE A S. Basic problems in stability and design of switched systems[J]. Control Systems Magazine，1999，19(5):59-70.

[10]NARENDRA K S ， BALAKRISHNAN J. A common Lyapunovfunction for stable LTI systems with commuting A-matrices[J]. IEEE Trans on Automatic Control，1994，39(12):2469-2471.

[11]LIBERZON D， HESPANHA J P ， MORSE A S. Stability of switched linear systems:a Liealgebraic condition [J].Systems Control Letters， 1999，37:117-122.

[12]BRANICKY M S. Multiple Lyapunov functions and other analysis tools for switched and hybrid systems[J]. IEEE Trans on Automa-tic Control，1998，43(4):86-200.

[13]YE Hui， MICHEL A N， HOU Ling. Stability analysis of systems with impulse effects[J]. IEEE Trans on Automatic Control， 1998，43 (12):1719-1723.

[14]PETTERSSON S， LENNARTSON B. Stability and robustness for hybrid systems[C]//Proc of the 35th IEEE Conference on Decision and Control. 1996: 1202-1207.

[15]MICHEL A N. Recent trends in the stability analysis of hybrid dynamical systems[J]. IEEE Trans on Circuit and Systems ， 1999，45(1):20-134.

[16]JOHANSSON M， RANTZER A. Computation of piecewise quadratic Lyapunov functions for hybrid systems[J]. IEEE Trans on Automatic Control， 1998，43(4):555-559.

[17]MICHEL A N， HU Bo. Toward a stability theory of general hybrid dynamical systems[J] . Automatica， 1999，35(3):371-384.

[18]DAYAWANSA W P， MARTIN C F. A converse Lyapunov theorem for a class of dynamical systems which undergo switching[J]. IEEE Trans on Automatic Control， 1999， 44(4): 751-760.

[19]HISKEN I A. Stability of limit cycles in hybrid systems[C]// Proc of the 34th Annual Hawaii International Conference on System Sciences. Washington DC: IEEE Computer Society， 2001:756-761.

[20]JOTA G， GOODWIN C. Switching control: some stability results[C]//Proc of the 36th IEEE Conference on Decision and Control. San Diego:[s.n.]， 1997:2209-2210.

[21]XU Xu-ping， ANTSAKIS J. Optimal control of switched autonomous systems[C]//Proc of the 41st IEEE Conference on Decision and Control. Las Vegas: [s.n.]， 2002: 4401-4406.

[22]RIEDINGER P， ZANNE C， KRATZ F. Time optimal control of hybrid systems[C]// Proc of American Control Conference. San Diego: [s.n.] 1997:2466-2470.

[23]XU Xu-ping， ANTSAKIS P J. An approach of solving general switched linear quadratic optimal control problems[C]//Proc of the 40th IEEE Conference on Decision and Control. Orlando:[s.n.]， 2001: 2478-2483.

[24]MANNA Z，PNUELI A. Temporal verification of reactive systems safety[M]. New York: Springer-Verlag， 1995.

[25]PELED D A.Software reliability methods[M]. Berlin: Springer， 2001.

[26]INAN M K， KURSHAN R P. Verification of digital and hybrid systems[M]. Berlin: Springer，2000.

[27]BERARD B， BIDOIT M， FINKEL A， et al. Systems and software verification: model-checking techniques and tools[M]. Berlin: Springer，2001.

[28]HENZINGER T A， HO P H.HyTech: a model checker for hybrid systems[C]//Proc of the 9th International Conference on Computer Aided Verification. London: Springer-Verlag， 1997:460-463.

[29]方敏，張雅順，李輝. 混成系統的形式驗證方法[J].系統仿真學報，2006，18（10）:2921-2928.

[30]A SCHAFT van der， SCHUMACHERH. An introduction to hybrid dynamical systems[M]. Berlin: Springer-Verlag，2000.

[31]GOOS G，HARTMANIS J L， van EEUWEN J. Hybrid systems: computation and control [C]//Lecture Notes in Computer Science. Berlin: Springer-Verlag，2000.

[32]DJ BENEDETTO M D， SANGIOVANNI A. Hybrid systems: computation and control[C]//Lecture Notes in Computer Science， vol 2034. Berlin: Springer-Verlag， 2001.

[33] ANTSAKLIS P J ， LEMMON M D. Special issue on hybrid systems[J]. Discrete Event DynamicalSystems: Theory andApplications， 1998，8(2):92-131.

[34]HENZINGER T A， SASTRYS. Hybrid systems: computation and control-Lecture Notes in ComputerScience， vol 1386. Berlin: Sprin-ger-Verlag，1998.

[35]VAANDRAGERF W， van SCHUPPEN J H van.Hybrid systems computation and control[C]//Lecture Notes in Computer Science， vol 2289. Berlin: Springer-Verlag，1999.

[36]TOMLIN C J， GREENSTREET M R. Hybridsystems: computation and control[C]//Lecture Notes in Computer Science， vol 2289 . Berlin: Springer-Verlag，2002.

[37]鄭大鐘， 趙千川. 離散事件動態系統[M]. 北京: 清華大學出版社， 2000.

[38]HOARE C A R， RAVN A P. A calculus of durations[J]. Information Processing Letters， 1991， 40(5):269-276.

[39]ZHOU Chao-chen， RAVN A P， HANSEN M R. An extended duration calculus for hybrid real-time systems[C]//Proc of Theory of Hybrid Systems Workshop. Springer-Verlag，1993:36-59.

[40]SASTRY S， MEYER G， TOMLIN C， et al. Hybrid control in air traffic management systems[C]//Proc of the 34th IEEE Conference on Decision and Control.1995:1478-1483.

[41]NERODE A， KOHN W. Models for hybrid systems: automata， topo-logies， controllability and observability[C]//Proc of Theory of Hybrid Systems Workshop. London: Springer-Verlag， 1993:317-356.

[42]PNUELI A. Hybrid systems: the computer science view[C]// Proc of DIMACS Workshop on Verification and Control of Hybrid Systems. New York: Springer-Verlag， 1995.

[43]鄭剛，譚民，宋永華.混雜系統的研究進展[J].控制與決策，2004，19(1):7-16.

注：本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文