復雜環境下基于價格時間自動機飛機著陸調度*

姬莉霞，張 晗

（鄭州大學軟件技術學院，河南鄭州 450002）

0 引言

如何對到港飛機進行高效合理的排序是管制員的主要職責，管制員根據飛行數據、經驗和直觀判斷，確定飛機著陸次序和時間。現有調度策略一般在滿足相鄰飛機尾流間隔和其他空管規則的限制下，根據先到先服務（first come first serve，FCFS）原則制定每架飛機的著陸時間。此方法存在很大局限性:首先，管制員在短時間內做出決定，很難詳細考慮各種方案的利弊，可能會造成不必要的沖突和延誤;其次，從經濟效益考慮，調度方案的不科學性將導致著陸總成本的無謂增加。

飛機著陸調度問題在近20年來得到各國研究機構和空管部門的廣泛研究［1～4］，主要內容為確定著陸飛機隊列的順序、時間和跑道指派，以達到減小延誤、提高系統容量和增強飛行安全的目的。本文在研究相關文獻的基礎上，主要從三方面著手研究:1）在每架飛機著陸時間窗范圍內安排著陸時間;2）滿足相鄰飛機最小尾流間隔;3）根據機型、環境因素、到達時間等參數安排跑道和著陸時間。采用時間自動［5］（timed automata，TA）機及其擴展分支價格時間自動［6］（priced timed automata，PTA）機作為形式化方法。

1 問題描述與概念模型的建立

假設某機場具有m條不同方向的跑道，交通流量為Δt時間內有n架飛機著陸，集合E={i|1≤i≤n}代表飛機以最佳巡航速度預計到達序列，即飛機最佳著陸時間序列，集合W={［i，j］|1≤i≤2，1≤j≤n}為飛機著陸時間窗，集合S={j|1≤j≤n}為調度后飛機的實際降落時間序列。本文采用的調度結果是得到與E（i）一一對應的S（j），并滿足以下約束:

1）飛機在其時間窗內降落

2）同一跑道上連續降落的飛機滿足安全尾流間隔。以i?j為飛機j尾隨i降落在相同跑道;常量C表示基準尾流間隔;集合T={［i］|1≤i≤n}為飛機相應的尾流間隔系數;e為綜合環境影響參數，主要包括風力風向、跑道方向、雨雪霧等，這些因素皆能對安全尾流間隔造成影響，從而直接影響后續飛機著陸時間和額外成本

3）著陸時飛機如果能夠逆風飛行，不僅可以使狀態更穩定，而且著陸后可以更快地在跑道上停止，從而減少所需跑道的長度和安全尾流間隔，因此，盡可能為到港飛機安排逆風的跑道。用R={i|1≤i≤m}為跑道的角度，變量d為風向，兩者采用相反的原始坐標和相同的增加方向

飛機著陸調度的目標通常為容量最大或總延誤最小，本文兼顧兩者，采用額外總成本最優作為目標。假設第i架飛機單位時間內因為提前降落而加速飛行產生的額外費用為F（i），單位時間內延遲降落盤旋產生的費用為Y（i），則額外消耗最優成本問題的概念性數學模型為

2 形式化模型的建立

2．1 時間自動機和價格時間自動機

時間自動機被廣泛應用于各類擁有觸發事件和時間約束的復雜實時系統，在模型驗證方面得到了非常廣泛的應用［7］。

定義1:一個時間自動機是一個八元組TA=（L，l0，C，A，E，I，V，T）:L為有限位置集合;l0∈L為開始位置集合;C為有限時鐘集合;A為有限動作集合;E?L×Ф（C）×A×2C×L為邊的集合，邊一般伴隨有動作、衛士條件和復位時鐘集合;I:L→Ф（C）為位置的不變式;V為有窮變量集合;T:L×A→L為轉換函數。

價格時間自動機是在時間自動機的基礎上擴展價格元素的模型，它是建模和解決成本最優問題的形式化方法。

定義2:一個價格時間自動機是一個九元組PTA=（L，l0，C，A，E，I，V，P，T），其中，L，l0，C，A，E，I，V，T與TA中意義相同，P:L∪E→N0表示給位置和邊分配價格元素。

多個并發的PTA可以構成價格時間自動機網絡，每個PTA都有自身的狀態，它們之間共享時鐘變量和全局數據變量，并通過邊上的動作同步協作，通過共享全局變量進行傳值通信。格局用于描述價格時間自動機網絡中所有PTA的運行狀態。

定義3:假設有n個價格時間自動機PTA1，…，PTAn，由這n個價格時間自動機構成的網絡為價格時間自動機的積，記為PTAN≡PTA1‖PTA2…‖PTAn，它的一個格局表示為一個三元組c=〈l，r，v〉，其中

2．2 調度主體的PTA模型

飛機著陸問題牽涉的最重要對象是飛機，取樣n架飛機，抽象得到如圖1所示的價格時間自動機模型Aircraft。在模型中，位置Approach表示飛機進入管制臺雷達視線范圍，位置 Early，Ontime，Delay分別為飛機提前［W（1，i），E（i）］、準時E（i）和延后［E（i），W（2，i）］，在轉換約束下，這3個位置僅有1個可能處于活動狀態。位置Early產生的額外成本為引擎加速飛行造成，計算方法為該位置的價格與其處于活動狀態的時間的積。位置Ontime為緊迫位置，也就是當其轉換條件滿足時毫無延遲的發生，在此位置不產生額外成本。位置Delay產生的額外成本為盤旋等待著陸產生的消耗，計算方法為該位置的價格與該位置處于活動狀態的時間的積。緊迫位置Urg保證在臨近時間窗結束時，暫時不考慮成本因素，優先降落。位置Special表示在綜合環境影響參數高于安全著陸閾值時，收到廣播信號poor，此時飛機等待著陸或備降信號。

圖1 飛機的價格時間自動機模型示意圖Fig 1 Diagram of PTA model of aircraft

2．3 交互實體的PTA模型

在著陸過程中，與飛機交互作用的實體應具備以下特征:擁有唯一的身份標識以區別于其他實體;擁有一定的物理或者虛擬屬性，狀態可以被改變或者可以被感知;具有通信能力。如果將各個交互實體看作對象，那么相同屬性的實體可以被抽象為類，從飛機著陸過程中，可以抽象出控制臺、管制員、雷達、跑道、環境等類，為弱化系統內部交互，將雷達和管制員并入控制臺類，則各實體的PTA模型示意如圖2所示。

圖2 交互實體的價格時間自動機模型示意圖Fig 2 Diagram of PTA models of interacting entities

跑道（runway）模型的位置Idle和Use分別表示跑道空閑和使用，跑道的選擇通過邊ready的價格參數來確定，優先為飛機安排空閑逆風跑道，跑道選定后判斷風力是否為積極影響，并據此影響尾流間隔。環境屬性只能被感知而不能被改變，其模型 Enviorment的固有屬性es，ew，er，es，ef和wdir分別表示當前風力參數、降雨參數、冰雪參數、霧靄參數、其他環境系數以及當前風向，當綜合環境影響參數超出安全著陸閾值時，通過控制器發出廣播信號poor?？刂破髂Ｐ?Control主要通過信道 approach，ready，land，done以及廣播信道poor與飛機、環境和跑道協同交互。

3 最優成本可達性問題

最優成本可達性問題就是找到一個到達給定目標位置的最小花費［2，8］。由于時鐘被定義為非負整數，價格轉換系統可以是無限的，與價格符號狀態［9］相關的成本也可能是無限的。在探索過程中，如果沿不同的路徑到達相同的狀態的成本不同，則丟棄更昂貴的狀態。類似于時間自動機，PTA的價格符號狀態通過時鐘域的簡單約束來表示，成本通過價格時鐘域［9］上的仿射平面給出。

在PTA驗證工具UPPAAL CORA中，最優成本的可達性分析使用如下所示標準分支界定算法，算法可以使用不同的搜索策略，目前有廣度優先、（隨機）深度優先、最佳深度優先、最佳優先和用戶啟發式等。

Cost記錄當前已知最優成本，列表Passed和Waiting分別記錄已搜索過的和待搜索的符號狀態，算法迭代搜索直至沒有狀態需要搜索。在While循環中，根據分支策略選擇未搜索狀態S，如果S被已搜索狀態主導或者其成本不可能更低，則跳過此狀態;否則，如果S是目標狀態，則得到最優成本;如果S不是目標狀態，則將其所有后繼加入Waiting序列并進行下一次迭代。

4 仿真分析

某機場由3條跑道組成，交通需求平均88架/h，表1給出某時間段的一組數據。以該機場為例，在 UPPAAL CORA中，將系統模型實體化，追蹤模擬系統運行狀況，得到多種運行軌跡。

表1 部分到港飛機數據Tab 1 Datas of partial inbound aircraft

圖3給出單條跑道極限容量下1 h內對40架飛機仿真調度示意。不同長度的黑色線段代表不同類型的飛機;E0表示最優著陸時間序列，存在嚴重沖突;S1表示忽略環境影響時現有FCFS調度結果，各飛機的著陸時間被勻化，一旦延遲發生，將不可避免的造成后續延遲累加，平均延時約191 s;S2表示與S1對應的基于PTA的調度結果，平均延時約156 s;S1＇表示風向隨機波動、環境影響參數在安全著陸范圍內隨機波動情況下現有FCFS調度結果，平均延時約221 s;S2＇表示與S1＇對應的基于PTA的調度結果，平均延時約169 s。

表2給出該機場24 h對2113架飛機仿真優化調度成本、延誤和容量等分析結果。在不考慮和考慮環境影響2種情況下，平均延誤減小幅度分別為30．22%和32．70%;跑道容量增幅分別為5．28%和6．71%;因加速、盤旋、環境等造成額外成本減幅分別為32．92%和34．28%。從該結果可以看出:在以最優成本為目標的PTA方法中，平均延時和額外成本有較大幅度下降，跑道容量也有一定的提升空間，在考慮環境影響因素情況下效果尤為顯著。

圖3 單跑道調度結果示意圖Fig 3 Scheduling result diagram of a single runway

表2 24 h仿真調度結果分析Tab 2 Simulation scheduling results analysis in 24 h

5 結束語

針對目前飛機著陸調度方法的不足，以著陸消耗成本為目標，考慮環境因素的影響，給出了飛機著陸調度需要滿足的限制條件和最優成本問題的數學描述。使用價格時間自動機作為形式化建模方法，對飛機、跑道、控制器、環境等交互實體進行建模，使用UPPAAL CORA對模型實體進行模擬分析和求解最優成本的可達性，并對某機場飛機著陸調度數據進行仿真實驗和分析。為復雜環境下安全高效地進行飛機著陸調度提供了科學的建議。

［1］ Alur R，Trivedi A．Relating average and discounted costs for quantitative analysis of timed systems［C］∥The 11th ACM International Conference on Embedded Software，New York，2011．

［2］ Behrmann G，Larsen G K G，Rasmussen J I．Priced timed automata:Algorithms and applications［C］∥International Symposium Formal Methods for Components and Objects（FMCO），Berlin，Heidelberg:Springer-Vedag，2004．

［3］ Chen Shuang，Xia Xuezhi．Researches on optimal scheduling model for aircraft landing problem［C］∥2009 WASE International Conference on Information Engineering:IEEE Computer Society，2009:418-421．

［4］ 余 江，劉曉明，蒲 云．飛機著陸調度問題的MPS優化算法研究［J］．系統工程理論與實踐，2004（3）:119-133．

［5］ Alur R，Dill D L．A theory of timed automata［J］．Theoretical Computer Science，1994，126:183-235．

［6］ Behrmann G，Felmker A，Hune T，et al．Minimum-cost reachability for priced timed automata［C］∥Lecture Notes in Computer Science，Berlin，Heidelberg:Springer-Verlag，2001．

［7］ 周清雷，姬莉霞，王艷梅．基于UPPAAL的實時系統模型驗證［J］．計算機應用，2004，24（9）:129-131．

［8］ Behrmann G，Larsen K，Rasmussen J．Optimal scheduling using priced timed automata［C］∥ACM SIGMETRICS Perfoin’lance E-valuation Review，New York:ACM，2005．

［9］ Larsen K，Behrmann G，Brinksma E，et al．As cheap as possible:Efficient cost-optimal reachability for priced timed automata［C］∥Proc of Computer Aided Verification，2011:493-508．