基于概率時間自動機的異構多agent自適應運行時驗證

穆勇安 劉瑋 高勝 葉幸瑜 王紫昊

摘 要：多agent自適應系統在運行過程中需要根據環境進行自適應調整。異構agent能夠提高agent的使用效率和降低系統的構建成本，但存在復雜的協作問題，因此提出一種基于概率時間自動機的異構多agent自適應系統運行時驗證方法。該方法通過形式化描述異構agent的功能特征并融合環境中的隨機因素構建概率時間自動機模型模擬自適應系統的運行過程，針對異構agent之間的協作邏輯制定安全約束條件以確保系統運行中狀態遷移流程的安全性。通過模型檢查結合運行時定量驗證方法進行實驗驗證，在智能泊車系統案例中應用該方法。實驗結果表明，agent之間協作邏輯的正確性可以有效保證系統運行時的穩定性，且相較于不使用運行時定量驗證的初始系統在相同時間內正常運行的時間提升了21%左右。

關鍵詞：自適應系統； 異構agent； 概率時間自動機； agent協作； 運行時定量驗證

中圖分類號：TP311.5?? 文獻標志碼：A?? 文章編號：1001-3695（2023）12-032-3728-08

doi：10.19734/j.issn.1001-3695.2023.04.0158

Runtime verification of heterogeneous multiagent selfadaptive based on probabilistic timed automata

Abstract：The multiagent selfadaptive system requires adaptive adjustments based on the dynamic environment during its runtime. Heterogeneous agents can enhance the efficiency of agent utilization and reduce system construction costs， but also present complex collaboration issues. Therefore， this paper proposed a runtime verification method for heterogeneous multiagent selfadaptive systems based on probabilistic timed automata. The approach constructed a probabilistic timed automaton model by formally describing the functional characteristics of heterogeneous agents and integrating random factors in the environment to simulate the operation process of the selfadaptive system. Regarding the collaboration logic among heterogeneous agents， it established security constraints to ensure the security of state transition processes during system operation. It combined model checking with runtime quantitative verification methods to conduct experiment and applied it in the case of an intelligent unmanned parking system. Experimental results show that the correctness of the cooperation logic between agents can effectively ensure the stability of the system at runtime， and compared with the initial system without runtime quantitative verification， the uptime of the system is increased by about 21% at the same time.

Key words：selfadaptive system（SAS）; heterogeneous agent; probabilistic timed automata; agent cooperative; runtime quantitative verification

0 引言

自適應系統（SAS）可以監控環境及其自身的變化，通過規范和修改自身行為或結構，以達到持續性地滿足用戶需求的目的[1]。將自適應系統中的功能實體抽象和封裝為多agent，能有效提高自適應系統的自適應能力[2]。自適應能力是指agent根據收集到的環境數據自主作出系統決策的能力，自適應能力的高低是影響agent能否根據環境條件變化作出正確決策的關鍵因素。決策的正確與否會對SAS的運行過程產生重大影響。例如，SAS的不正當決策使系統狀態遷移錯誤，則會導致系統運行死鎖等重大后果。因此，在復雜環境下的自適應驗證問題已成為開發可靠的SAS[3]亟待解決的問題之一。

為了提高SAS決策的可靠性，最初采用系統測試的方法[4，5]。該方法通過各項測試設備與接口來判定SAS的功能是否合格，但這類測試方法無法預測和枚舉動態環境下SAS運行時可能產生的多種系統行為，無法反映系統在動態環境下的運行情況。Weyns在SAS的形式化描述方法上進行了研究調查[6]，并指出形式化描述方法能夠準確指定和驗證SAS可能產生的多種行為，以提供SAS所需的服務質量保證（quality of service，QoS）[7～10]。模型檢查技術是形式化描述方法的具體應用，是將SAS形式化描述為可驗證的系統模型，并驗證其各項屬性是否滿足給定的公式規范[11]，但系統模型的狀態數量會影響驗證過程，只能應用于有限狀態的小型系統。為了使模型檢查技術能夠應用到更復雜的大型SAS中，在模型檢查的基礎上引入數學分析和邏輯形式主義的形式化規范方法以輔助解決大規模復雜或無限狀態系統的驗證問題[12，13]。該方法通過符號表達式等價驗證的方法減少模型的路徑重復和狀態數量以降低對驗證效率的影響。文獻[14]提出了一個在無界多agent系統中驗證系統行為的框架，并給出了基于反抽象技術構建抽象模型的驗證方法，但該方法建立在agent所處環境狀態不會出現變化的情況下，無法驗證在不確定性環境下系統agent的自適應需求規劃。劉瑋等人[15]通過概率規劃來定量刻畫agent行為在隨機環境下的不確定性并關聯上下文狀態以獲得最優的自適應需求規劃。文獻[16～18]就SAS的安全性、可達性和穩定性的驗證問題進行了研究，為SAS的驗證提供了更多角度。

然而，上述方法通常應用于SAS設計或維護等離線階段，無法處理在實際運行過程中出現的不確定因素。如果SAS在運行過程中出現需求和硬件設備故障等重大變化，可能會導致SAS的QoS下降，嚴重時甚至造成系統功能不可用的情況。因此，SAS的驗證要適應環境、需求的動態變化以保障SAS運行時的安全穩定。

在運行時使用形式化方法驅動SAS的驗證可以作為解決上述問題的可行方案[19]。運行時、量化的驗證技術是基于形式化驅動SAS重構的一種數學方法。該方法通過構建SAS及其環境的隨機模型，在運行時監測更新模型并通過對模型的形式分析來引導系統控制回路進行決策。文獻[20，21]將運行時定量驗證（runtime quantitative verification，RQV）的概念引入到了自適應系統驗證領域中，并分別在遠程醫療服務系統[22]和云計算基礎設施[23]等場景中進行應用。Mason等人[24]使用抽象策略定義系統中agent行為空間的區域，結合RQV來識別滿足約束的行為策略。Gadelha等人[25]提出使用場景作為運行時實體來驗證SAS的方法，該方法通過監測系統運行軌跡和場景之間的轉移概率來構成系統行為規范，再通過RQV判斷出違反規范的系統行為。

隨著SAS的應用場景越來越復雜、功能目標越來越多，這使SAS需要向協作和分布式方向發展以具有更好的并發性和容錯性等良好特性[26]。因此，多agent系統（multiagent system，MAS）及其協作模式和分布式優化技術引起了研究者的關注。針對MAS的可協作性，將agent根據功能與特征進行區分，將特征、功能不同的agent稱為異構agent[27]。而現有應用RQV的研究所描述的自適應系統都是基于同構多agent系統，并沒有考慮到存在異構多agent的自適應系統，同時其缺乏對異構agent之間協作邏輯的形式化描述。若要對異構多agent自適應系統進行驗證，就要解決異構agent的形式化建模和協作邏輯描述問題。

文獻[14]同樣是將需要驗證的對象實體形式化描述為具有隨機過程的模型并結合定量驗證以驗證系統的各項需求指標。文獻[14]將具有隨機行為的agent構建為馬爾可夫決策過程（Markov decision processes，MDP），并結合交替時間邏輯（alternatingtime logic， ATL）建立agent的檢查指標，但驗證的對象實體與本文不同且不考慮不同類型agent之間存在協作問題的情況。Gadelha等人以文本或者圖形形式表示場景以描述SAS的一組事件序列，再用場景之間的轉換概率表達SAS的行為規范并應用模型檢查技術驗證可達性屬性是否成立；與本文邏輯基本一致，但其驗證的SAS需求存在一定的局限性，無法表達SAS的全部行為事件且需要大量的場景數據來支持驗證結果的正確性。文獻[28]將基于模型檢查的形式化概率框架應用到了基于機器學習的系統框架中，通過MDP建模非確定行為并基于獎勵屬性生成最優策略；但其提出的模型框架是基于單agent的，不涉及異構agent和協作問題，構建的概率模型主要針對機器學習中的再訓練模塊，能夠表達的功能行為有限。Weyns等人[29]基于自適應反饋控制循環MAPEK構建驗證模型，使用一組正確性屬性驗證的模型來表示MAPEK的四個主要階段[30]；該方法結合具體場景下的SAS構建的系統模型同時包含系統的功能行為和MAPEK的四個主要階段，可以在運行時直接部署和執行；但相比本文而言，其驗證的模型并不涉及多agent的概念，并且不適用存在協同工作問題的多反饋循環系統。

總體來說，本文工作針對隨機環境下的多agent自適應系統構建其概率模型，聚焦于異構agent之間的協作問題并提出形式化解決方案，結合模型檢查和RQV技術在運行時部署執行驗證模型以確保系統的安全性和穩定性。本文從概率時間自動機（probabilistic timed automata，PTA）和動態環境下的異構多agent自適應系統出發，結合RQV提出了基于概率時間自動機的異構多agent自適應運行時驗證方法（PTAbased heterogeneous multiagent selfadaptation runtime verification，PMARV）。首先根據系統中的異構agent構建相應的PTA模型，組合PTA模型將SAS描述為可驗證的概率時間自動機網絡模型（probabilistic timed automata network，PTAN），由此可以得到SAS的可驗證概率模型；根據SAS中異構agent的協作邏輯問題，制定合理的安全約束條件并將其形式化描述為PTA模型支持的模型語言，再融入到SAS的概率模型中；在運行時部署融合安全約束條件的SAS概率模型到相應的模型檢查工具中，驗證系統運行過程中狀態遷移流程的安全性；將SAS的功能行為形式化為時間時序邏輯公式，用于量化系統的任務目標作為驗證的評估標準；通過模型檢查和運行時定量驗證分析模型，并在發生違反需求情況時生成重新配置計劃。

以智能無人停車系統（intelligent unmanned parking system，IUPS）作為研究背景和實驗場景，其在此前的工作中已有應用[31]。該系統中主要有兩類智能機器人，一類是用于裝載并跨層運輸車輛的升降機器人lift，另一類是自動泊車機器人AGV。

本文的主要貢獻有：

a）提出了一種基于概率時間自動機的異構多agent自適應運行時驗證方法（PTAbased heterogeneous multiagent selfadaptation runtime verification，PMARV）。通過該方法，可以將異構agent分別形式化描述為單個PTA模型，其組合起來的模型網絡PTAN便可模擬整個多agent自適應系統。

b）將異構agent之間的協作邏輯融入到SAS概率模型中，提出了一種異構agent之間協作交互的形式化描述方法。該方法將協作邏輯轉換為模型語言加入到SAS概率模型中，通過制定安全約束驗證系統運行過程的安全性，實驗證明其能夠有效保障系統運行的穩定性。

c）將運行時定量驗證技術擴展運用至異構多agent系統中，并量化系統的功能行為作為驗證的指標。實驗對比原始系統和運用了運行時定量驗證的系統在運行過程中的正確率，結果證明運行時定量驗證可以有效提高系統運行的可靠性。

1 模型基礎與時序計算邏輯

1.1 時間自動機模型

時間自動機是帶有時鐘集的有限自動機[32]，設X是一個有限的時鐘集合，其中x∈R∩[0，+∞]，表示記錄時間的時鐘變量。為時鐘變量賦值的動作定義為時鐘變量到非負實數集的映射，記為X→R，R≥0。設C為一個由布爾變量組合的時鐘約束，若一個時鐘變量x的值滿足其時鐘約束C，則該時鐘約束C的結果為true，記為C==true，可以定義為以下幾種形式：

a）x≤n。

b）n≤x。

c）x1+n1≤x2+n2。

d）C。

e）C∩C。

其中：x1，x2，…，xi∈X;n1，n2都是自然數。如果C中存在的所有x都使C==true，則令C表示為時鐘變量集X上的時鐘約束集。

定義1 時間自動機。一個時間自動機可以定義為一個六元組TA=（S，s0，E，I，X，V）。其中：S是時間自動機中所有狀態的非空集合；s0∈S是TA中所有初始狀態的集合；ES×C×Act×2C×S是一個狀態變遷的集合，Act是動作a的集合；I：S→C是一個狀態集合與時鐘變量集合的映射，表示狀態的約束；X是一個有限的時鐘變量集合；V是數據變量的集合。

從狀態s到s′的轉換，記為（s，C，a，U，s′）∈E，該式表示當處于狀態s時，只要滿足時鐘約束C，時間自動機TA就可以執行動作a，U中的時鐘變量將被重新賦值，使狀態由s轉移到s′的同時不違反I（s′）的時鐘約束。若時鐘約束I（s）持續被滿足，TA也可以停留在狀態s。

模型檢查是解決SAS驗證問題的主要方法之一，其基本思想是以系統行為建立數學模型，然后基于模型進行形式化分析[33]。時間自動機是一種用于真實系統建模和驗證的理論[34，35]，可將SAS的系統行為與結構特征建模為時間自動機模型進行驗證分析。然而，SAS需要根據環境的動態變化作出適應調整，其行為受不確定因素影響具有非確定性特征。因此，SAS的驗證模型也需要具備分析不確定性因素的能力。而概率時間自動機是一種具有不確定性和隨機性的形式化模型[36]，可以用于描述、分析帶有隨機因素實時系統行為，其定義在時間自動機的基礎上進行了擴充。內外環境中的不確定性是SAS不可避免的因素，為了更加有效地驗證SAS的安全性，將這種隨機性融入驗證工作中是及其必要的。假設SAS行為的某些特定方面可以用概率的形式描述，則可以將這類行為建模為一個隨機過程進行驗證，例如將來自系統環境中的不確定性抽象為概率形式，構建成一個概率時間自動機模型進行驗證分析。若系統中agent的某一種狀態存在多條轉移路徑時，可以將不同路線抽象為不同的隨機因素影響后的系統狀態變化路線，使其依照概率進行狀態轉移。

定義2 概率時間自動機。一個概率時間自動機可以定義為一個六元組PTA=（S，s0，T，I，X，V）。其中S，s0，I，X和V與定義1中的意義相同。TS×C×Act×P（2C×S）是一個概率狀態變遷的集合；P（U，s′）：T→（0，1]是當前狀態轉移到下一狀態的概率。

概率狀態的遷移可以記為（s，C，a，P）∈T，表示當處于狀態s時，只要滿足時鐘約束C，概率時間自動機PTA就可以執行動作a，U中的時鐘變量將被重新賦值，使狀態以P（U，s′）的概率從s轉移到s′，與此同時不違反I（s′）的時鐘約束。與TA模型相同，若時鐘約束I（s）持續被滿足，PTA也可以停留在狀態s。

定義3 概率時間自動機網絡。一個概率時間自動機網絡可以定義為一個四元組PTAN=（（PTA），VG，Cl，Ch），其中：（PTA）=（PTA0，PTA1，PTA2，…，PTAn）是一組互相平行、互相關聯的概率時間自動機；VG是全局變量的集合；Cl是全局時鐘的集合；Ch是同步信道的集合。

存在異構多agent的SAS能夠適應更加復雜的應用場景，如何構建異構多agent的SAS模型則成為了其驗證問題的難點。根據定義1與2，本文將SAS中的異構agent分別建立為TA模型并將其面臨的不確定性因素抽象為概率形式，擴展TA模型為PTA模型。由定義3可知，多個PTA模型可以組合成一個PTAN模型。多個同構或異構的agent共同組成了復雜SAS，則由多agent的PTA模型組成的PTAN模型便為SAS的可驗證系統模型。

1.2 時間時序計算樹邏輯

在得到SAS的系統建模后，需要對系統模型進行分析驗證。時間時序邏輯（timed computation tree logic，TCTL）是一組時間性質規約，可以用于形式化表示需要驗證的系統屬性。其公式描述如表1所示。

表1中公式的語義定義為，字母A和E用于量化路徑。A表示給定的屬性應該適用于樹的所有路徑，而E表示應該至少有一個樹的路徑包含該屬性。符號[]和〈〉用于量化路徑中的狀態。[]表示路徑上的所有狀態都應滿足該屬性，而〈〉表示執行中至少有一個狀態滿足該屬性。E〈〉和A[]是一組對偶屬性，即E〈〉滿足當且僅當A[]不滿足。這種類型的屬性通常被歸類為安全屬性，即意味著系統在特定危險不會發生的意義上是安全的。

通過TCTL構建SAS的模型屬性檢查，可以對系統結構屬性進行初步的安全驗證，而SAS中不確定的內外環境因素可以通過對TCTL添加概率性質的描述，得到TCTL的概率擴展形式PTCTL（probabilistic timed computation tree logic）。采用PTCTL描述PTA系統模型的性質，典型的例子有：

a）P<0.9[F<20 s send n]；

b）Trigger→P<0.000 1[G≤20deploy]；

c）Pmax=？[sent U fail]。

例a）的含義是在20 s內發送n條message的概率小于0.9；例b）的含義為安全氣囊在觸發后20 ms內未能展開的概率嚴格小于0.000 1，上述兩種公式通過驗證后能夠得到一個布爾值，該值的含義為模型某些行為發生的概率是否高于或低于給定的界限；例c）的含義是在消息傳輸完成之前發生故障的最大概率是多少，該公式在進行驗證后得到的是一個概率值，該值表示某些行為的實際概率。

PTCTL的語法公式如下。

狀態公式：

：：=true|a|χ|∧||PΔp[ψ]|RrΔq（1）

路徑公式：

ψ：：=U≤k|U（2）

其中：a∈AP是原子命題，AP是原子命題集合；χ∈C（X）是一個時鐘約束；Δ∈{<，≤，≥，>}是一個關系運算符；p∈Q∩[0，1];q∈Q≥0;r是一個獎勵結構;k∈N。該計算樹邏輯在TCTL的基礎上擴展出了概率算子（P）和獎勵算子（R），PΔp[ψ]表示路徑公式為真的概率滿足概率界限P，RrΔq[ρ]表示獎勵結構r上的獎勵函數ρ的期望值滿足其界限。

2 基于概率時間自動機的多agent建模

2.1 PMARV框架

本文先對需要驗證的SAS進行建模，再通過模型驗證平臺進行驗證。由于大型SAS所包含的任務目標和agent類型多且復雜，還涉及到異構agent之間的協作通信，所以如何對異構多agent系統進行建模是一個尤為重要的步驟。本文方法基于概率時間自動機模型，因此采用的模型驗證平臺為UPPAAL[37]，它可以對表現出概率行為的系統進行建模和分析，其圖形化的交互界面使模型狀態直觀清晰。基于概率時間自動機的SAS運行時驗證方法框架如圖1所示。

PMARV的步驟為：a）根據多agent自適應系統中的功能業務區分出異構agent，提取每個agent關鍵狀態以及引起狀態轉換的事件來表示SAS功能行為，得到SAS中每個agent的狀態轉移圖并為其構造相應的時間自動機模型；b）將可能的隨機因素轉換為SAS中agent各狀態之間的轉移概率以模擬內外環境對SAS的不確定性影響；c）根據agent狀態轉移圖與轉移概率，將全部agent的時間自動機模型擴展為具有不確定性因素的概率時間自動機模型；d）在模型驗證平臺中使用其支持的模型語言描述agent的概率時間自動機模型并結合PTCTL公式對agent功能行為進行形式化描述；e）在模型驗證平臺中對載入的全部agent模型進行分析驗證，將得到的驗證結果用于SAS在不確定環境下的決策，從而獲得滿足SAS服務質量的規劃。

每一類模型檢查器在對模型進行驗證前都需要將抽象的時間自動機模型描述為其所支持的模型語言，不同的模型檢查器使用不同的模型描述語言。UPPAAL可以將不同的模型建模在同一環境下，且多個模型間可通過guard、synchronisation和update等功能進行同時跳轉和模型間的交互協作，因此可以將不同功能的異構agent在同一環境下分別建模，通過guard（守衛）進行agent間的約束交互，通過synchronisation（同步）進行協同狀態變遷，通過update（更新）進行agent的數據更新，從而滿足多agent自適應系統的整體功能。

2.2 異構agent及其協作邏輯建模

復雜SAS中存在多種功能類型的異構agent，異構agent之間需要通過協作、通信等方式完成任務目標。本節將闡述PMARV中步驟a）～c）的方法細節，具體到如何對異構agent的協作邏輯以及合作方式進行形式化描述。

2.2.1 agent協作邏輯

在復雜SAS中需要有不同類型的agent完成不同的任務目標，一個任務目標也可能需要多個agent共同參與。假設一個任務目標需要A和B兩個agent先后合作完成，則A在執行自己的任務時要和B進行交互通信，確保B的狀態可以執行交接后的任務，在任務交接時進行安全檢查，使系統時刻處于安全可靠的狀態下，反之B對A也有同樣的協作邏輯。而agent之間需要進行多少次協作通信以及協作時需要滿足什么樣的安全條件則由具體的任務目標決定，將這種agent在環境中進行的有一定持續時間的任務活動稱為狀態，而agent等待、交互或檢查是一種特殊的狀態，本文稱其為協作邏輯。

定義4 agent協作邏輯。agent的協作邏輯L是一個七元組L=（S，s0，A，F，g，γ，P）。其中：S是時間自動機中所有狀態的非空集合；s0∈S是初始狀態的集合；A∈Ｓ×Ｓ是所有狀態遷移的集合；F是agent相關邏輯表達式的集合；g：A→F表示每次狀態遷移需要滿足的條件，主要用于agent之間的安全檢查；γ是對環境變量的賦值；P：A→（0，1]是狀態轉移的概率。

agent的協作邏輯表示其狀態轉移邏輯，根據系統目標的需求，一個agent可能需要多個協作邏輯，即其可能參與多個任務目標的實現。同構agent之間擁有相同的協作邏輯，不同的協作邏輯則決定了agent之間存在功能結構的差異。本文將agent之間的交互通信行為稱為交互事件，交互事件由單個agent發起，可能有多個同構或異構的agent接收此事件。在交互事件中可以包含環境變量的更新，狀態屬性變量的調整以及轉移條件的檢查等多種交互。在2.2.2與2.2.3節中將會針對agent之間的交互事件與異構多agent的協作方式進行具體描述。

2.2.2 交互事件建模

事件是多個agent之間的交互協作，在概率時間自動機模型中，可以采用廣播通道的方式表示agent之間的事件。對于系統整體而言，有全局廣播通道向多個agent發出交互信息；對于局部單個agent之間的交互，有單一廣播通道用于其交流協作，不同的廣播方式有不同的適應場景，這將在下文中進一步闡述。根據應用場景下agent之間的通信協作方式，可以將交互事件分為更新事件和約束事件。設Eu為更新事件的集合，Ec為約束事件的集合。更新事件Eu的發起者一般為單個agent，接收者為單個或多個agent，會根據廣播消息更新自己狀態的相關變量。在更新事件的廣播信息發出或接收時，agent自身狀態可以保持不變，也可以在發出或接收后進行狀態轉移。約束事件Ec一般由一個約束發起方和一個受約束方組成，約束發起方使受約束方的狀態在滿足一定約束條件前，不進行狀態轉移或在受約束方的約束條件達成后一定進行狀態轉移，在此期間通常會伴隨受約束方的Eu事件進行。

設si，sj∈S，u∈Eu，u！和u？分別表示更新事件的發出和接收。當agent發出或者接收更新事件時，如圖2左側update event部分表示，agent在狀態si發出更新事件u！，消息發出后agent可能仍然保持在狀態si，或者進行狀態轉移至sj。接收更新事件同理，由于消息傳遞是瞬間完成的，所以事件發起或結束的agent狀態si需要將自動機狀態屬性設置為committed，表示不消耗系統時間，這也表示消息傳遞是一種瞬時的過程。

在約束事件進行的過程中，通常伴隨著更新事件的發出和接收，agent狀態屬性變量也因此產生變化。設agent之間的約束條件為R，則Ec∈Eu×C，設si，sj∈S，c！和c？表示約束事件的發出和接收。如圖2右側constraint event部分所示，agent在狀態sj發出約束事件c！，在狀態sm接收約束事件c？并判斷自身狀態是否滿足約束條件R。用條件三元運算符表示約束條件的判定，τ與τ表示判定的結果，結果為τ時狀態一直保持在sm，直到約束判定結果為τ時，被約束的狀態一定轉移到sn。發出約束事件的狀態需要將自動機狀態屬性設置為committed，表示不消耗系統時間。接收消息的狀態由于約束條件的達成會存在一定的時間需求，所以不需要設定自動機狀態屬性。

2.2.3 異構多agent建模

復雜場景下的SAS由多個agent組成，根據系統不同的功能需求，可以將agent分為多種結構，完成相同功能目標的agent有相同的協作邏輯。在模型中，將agent的協作邏輯用一個概率時間自動機模型表達，一個agent對應一個PTA模型，該agent的每次聲明實現則對應該PTA模型的實例化。

設AG為一個SAS中全部agent的集合，每個agk∈AG，agk表示協作邏輯為k的agent，k∈N。設對應agk的概率時間自動機元組為PTAk=（S，s0，T，I，X，V），其中時間自動機的狀態、初始狀態、有向邊和狀態轉移的概率分別對應agent協作邏輯中的狀態、初始狀態、狀態轉移和狀態轉移概率；agent協作邏輯中相關邏輯表達式及時間變量和的賦值則對應時間自動機中的X和V。協作邏輯中的g根據語義轉換為狀態不變式、狀態轉移中的觸發條件和動作，其對應時間自動機中的I；時間自動機每個狀態轉移中的賦值對應協作邏輯中的γ函數賦值。

對于由單個agent或多個同構agent組成的系統模型，該系統擁有一個統一的系統目標，對應agent擁有同一個協作邏輯，在這種情況下agent協作邏輯的狀態遷移基本是順序隨時間推移進行的，不存在與其他agent的交互事件和復雜的隨機因素。對于由異構agent組成的系統模型，可以確定系統中至少包含兩個及以上的功能目標，需要由不同結構的agent完成，其構建的PTA模型可組成一個PTAN模型。多個agent共同實現系統目標的方式可分為兩類。一類是agent之間先后交替順序完成任務目標，如圖3所示，任務目標task1、task2分別由agent1和agent2順序完成。agent1行為模式從si開始，在完成活動task1后向agent2的狀態sj發起交互事件；agent2在狀態sj接收到事件后再完成目標task2。另一類是單個agent發起，多個agent協作完成系統任務目標task3，如圖4所示。agent1和agent2分別在初始狀態si和sm進入活動處理系統任務目標task3，agent1是發起方，agent2是協作方，兩者都需要彼此的參與來完成任務目標。

多agent自適應系統的主要功能行為是通過其系統內不同的agent完成的，可以說不同特征、不同功能的多個agent之間協作、適應實現多種任務目標就形成了一個系統，即多agent自適應系統。因此，為系統中的每個agent都構建其PTA模型，將這些PTA模型根據任務目標組合起來，即可得到一個表示整個系統功能行為的PTAN模型。在模型檢查工具載入PTAN模型，結合RQV量化系統的任務目標，即可在運行時模擬系統的運行過程并得出任務目標的驗證結果。

通過上述agent的建模方法，可以對復雜的異構多agent自適應系統進行形式化建模。通過構建agent之間的協作邏輯，可以初步確定系統中agent協作方式，具體到agent之間執行任務的先后順序、所處狀態、何時開始執行任務，以及是否需要其他agent滿足一定的先決條件等。確定協作方式是為后續協作邏輯的形式化描述做準備。2.2.2節交互事件建模將agent之間的交互方式概括為了兩類，2.2.3節異構agent建模將不同類型的agent參與執行任務的方式概括為了兩類，并且都給出了PTA模型語言的描述表達，因此可以將其融入SAS的PTAN模型中，且不存在模型語言沖突的情況，解決了異構多agent的協作問題和形式化問題。通過模擬運行融入協作邏輯后的PTAN模型，即可對系統協作邏輯的安全性和RQV對系統可靠性的提升效果進行分析和驗證。

2.3 IUPS的多agent模型構建

本節以IUPS為例，對上述方法進行實例化。本文從IUPS中提取lift和AGV的關鍵狀態，lift的關鍵狀態如表2所示，AGV的關鍵狀態如表3所示。

在此前的工作中[28]已經將IUPS環境因素的不確定性轉換為轉移概率并采用貝葉斯方法進行計算。根據lift的故障集W=｛W1，W2，…，Wn｝和癥狀集E=｛E1，E2，…，Em｝構建出圖5所示的雙層貝葉斯網絡。使用貝葉斯方法是為了計算出與agent狀態相對應的故障概率值，即計算故障狀態節點的后驗概率P（Wi|E）。

為了描述系統產生的不確定行為以及關鍵狀態之間發生的轉移，在模型中采用不同的符號對行為、狀態以及概率進行描述。根據對PTAN的描述，系統中存在lift和AGV兩種不同功能的agent，其PTA模型可以組成一個概率時間自動機網絡模型PTAN。定義IUPS的系統模型為一個四元組IUPS=（（PTA），VG，Cl，Ch），其中：概率時間自動機集合PTA包含系統中的lift和AGV兩種PTA模型；VG、Cl與Ch分別是lift和AGV涉及的全局變量集合、全局時鐘集合和交互通信的通道集合。對于概率時間自動機模型，這里以lift為例說明，lift的PTA模型為一個六元組lift=（S，s0，T，I，X，V），其中：

a）非空狀態集合S。模型中的狀態來源于系統運行狀態，S包含兩類狀態S=｛Ni，Fi｝，狀態Ni與系統正常運行狀態一一對應，狀態Fi表示系統運行中發生的故障情況，用于表達不確定性。s0表示系統初始狀態。

b）概率狀態變遷集合T。描述了從lift狀態s轉移到狀態s′需要滿足的約束條件和轉移的概率，概率集合P中包含兩類轉移概率，pi表示系統正常運行情況下的轉移概率，qi表示系統出現故障的轉移概率，而概率0用于表示該條轉移路徑無法通過。

c）數據變量集合V。用于標記lift與AGV的狀態節點屬性，因此V是兩類agent中狀態節點屬性變量的集合。

結合所使用的IUPS場景構建系統模型，可得到包含出現不確定情況的lift與AGV的PTA狀態轉移模型，以lift為例，其PTA狀態轉移模型如圖6所示。狀態Ni與系統運行過程的正常狀態，狀態F1對應不確定的故障狀態且有概率能轉移至正常運行狀態。對于N0，其作為系統的初始狀態，由p0的概率轉移至N1且由q0的概率轉移至F1，由于N1與F1作為N0的輸出狀態，所以存在q0=1-p0；對于F1，其表示系統出錯情況，在該狀態下，系統有概率p5轉移至正常狀態N1，也存在概率q5保持原狀以表示修復過程，有q5=1-p5。

3 實驗過程及分析

本文以IUPS智能泊車系統場景為例，將RQV應用于異構多agent系統中，確定該技術在此領域中的適用性，并比較使用該技術后對系統的改善。智能無人停車系統具有運行效率高、操作簡便等特點，是現代城市化的重要發展方向之一。深圳某機器人公司近年投入并建設的無人停車系統運用智能機器人運輸和停放車輛，實現了智能泊車的目標，并且部分項目已投入使用。本文實驗基于上述應用場景，構建了面向無人環境的智能泊車系統的多agent場景并進行了實驗，本實驗構建的模型包含兩類異構agent和一個獨立agent，異構agent為lift和AGV，獨立agent為controller，用于輔助實驗，方便對實驗系統進行調試。實驗使用的仿真工具為UPPAAL 4.1.19，其是由Aaborg大學和Appsala大學聯合開發的模型仿真驗證工具，支持對概率時間自動機的模擬與仿真，被用于很多案例研究。4.1.19版本支持SMC方法，能夠在具有隨機語義的復雜實時系統的模型上進行推理驗證[38]。

實驗1 IUPS異構agent協作邏輯驗證

為了驗證異構agent之間協作邏輯能否保障IUPS運行過程的穩定性，本實驗首先將IUPS構建為一個時間自動機網絡模型，該模型網絡由lift和AGV構建的時間自動機模型組成。在本實驗場景中，lift和AGV需要合作完成泊車的任務目標，通過表2、3所描述的關鍵狀態，可以為智能泊車系統制定安全驗證約束條件，如表4所示。將表中的約束條件形式化建模為agent協作邏輯中交互事件建模。將表中的前三條約束建模為agent之間約束事件交互模型，在滿足約束條件前agent狀態不能隨意變化。在系統運行過程中，agent間的約束事件會伴隨著agent自身狀態屬性的變化，將狀態屬性變化建模為更新事件交互模型。表4中的第4、5條約束建模為更新事件，但處于其約束事件約束下。

將上述約束條件加入到構建好的IUPS時間自動機網絡模型中，為確保該模型能夠正常模擬IUPS在無人環境下的自主運行，需要驗證模型的系統邏輯和時序邏輯正確性，驗證結果如表5所示。表中前兩行結果為lift與AGV的狀態可達性驗證，證明了lift與AGV的各個關鍵狀態在模型中均處于正常可達狀態。表中的屬性1～5與表4的序號相對應，是將安全約束條件構建為TCTL公式進行驗證。若驗證性質結果為滿足，說明安全約束條件成立，模型的運行過程是安全的，其狀態遷移過程被限制在安全范圍內，反之亦然，以此判斷安全約束條件的正確性。

在上述驗證之后，模擬一組lift和AGV協作完成一次泊車任務的系統trace以驗證模型運行的完整流程，如圖7所示。controller為輔助系統整體運行的agent，用于控制整個系統的開始與結束。圖中的數字0～5分別與表2、3中的序號相對應，代表lift和AGV處于相應的狀態。從圖7中可以看出，完成一次泊車任務，系統中兩類agent狀態轉移的路徑嚴格按照制定的安全約束進行。本trace只模擬了任務完成一次的路徑，lift和AGV完成任務目標后會回歸初始狀態并結束系統運行，到達圖中黑色矩形的位置；若系統繼續運行，則在完成一次任務后會進入系統預備過程，再重新回到系統開始運行的初始狀態，即圖中的黑色矩形會變為白色矩形，后續的系統trace與圖中保持一致。本實驗驗證了agent協作邏輯的正確性與其對系統運行的影響，結果表明為異構agent制定安全約束條件，也就是構建agent協作邏輯中的交互事件模型，可以有效保證系統各狀態遷移的正確性。

實驗2 IUPS正常狀態時長占比實驗

為了研究RQV對異構agent系統性能的改善，本實驗應用RQV的改進系統與不使用RQV的原始系統進行比較，并定義一段時間內系統正常運行的時間與該段時間的比值作為正確率以驗證使用RQV后對系統性能的提升[28]。正確率越高表示系統性能越好。本實驗在TA模型的基礎上加入概率形式的不確定因素，將時間自動機模型TA調整為概率時間自動機模型PTA并加入由實驗1驗證后的約束條件。將IUPS的任務目標轉換為相應的PTCTL公式并結合SMC統計方法在UPPAAL中進行屬性驗證。

將lift和AGV運行過程中采集到的錯誤數據作為癥狀集的先驗概率，取故障集的先驗概率為0.1。本文延用此前工作中lift和AGV的故障節點后驗概率，如表6所示。qi代表系統在正常運行狀態中發生故障的概率。qi的值越大，agent發生故障的概率越大。根據qi可知pi=1-qi，表示Ni轉移至Ni+1的概率值。對于以Fi為起點的自循環狀態，實驗統一取值為qi+4=0.1，因此Fi狀態轉移至Ni狀態的概率為pi+4=0.9。

IUPS系統包含lift和AGV兩類agent，先分別比較RQV對每類agent的性能提升，再比較RQV對整體系統性能的提升。因為對單個agent獨立進行實驗不涉及多個agent之間的協作，所以不需要加入安全約束。實驗分別以liftRQV和AGVRQV的形式表示使用了RQV的改進系統，以liftoriginal和AGVoriginal表示未使用RQV的原始系統。驗證單個agent時，定義一段時間內agent正常運行的時間與該段時間的比值作為正確率以對比agent的性能優劣。在UPPAAL中，每一個模擬時間對應現實的1 s。本實驗以500個模擬時間作為一個單位時間，得到兩類agent在10個單位時間內的實驗結果，分別如圖8、9所示。從圖中可以看出，在采用了RQV后兩類agent的正確率相比未使用RQV的原始系統有較大提升，lift的正確率有23%左右的提高，AGV有26%左右的提高。由于AGV所遇到的故障更多，其原系統在正確率上的波動較大，在使用了RQV后具有較為明顯的改善。lift運行過程中所遇到的不確定性相對較少，因此在整體正確率上也略高。

在驗證了RQV對單個agent的提升后，需要驗證其對整體系統的提升，此時需要加入由實驗1驗證后的安全約束條件來保障系統運行。用sysRQV表示使用了RQV的改進系統，以sysoriginal表示未使用RQV的原始系統。以系統正確率作為驗證屬性構建PTCTL公式驗證模型。驗證結果如圖10所示，可以看出，使用RQV后整體系統正確率一直優于原始系統，提高幅度約為21%。

本文在智能無人泊車系統實驗場景的基礎上，首先對系統中多agent的協作邏輯進行安全驗證，通過制定安全約束，可以確保系統運行過程中狀態遷移的正確性與穩定性，但協作邏輯的安全驗證在面對功能較為復雜的SAS場景中存在一定的局限性。隨著SAS功能行為的增加，異構agent的數量也隨之增加，其中可能存在更多的交互事件和安全約束條件，且與驗證的成本成正相關。因此在大型復雜的SAS場景中，能否制定出簡潔高效的安全約束條件和交互邏輯是決定驗證成本與效率的重要因素。

本文通過多組比較實驗可以得到RQV在單個或多agent實驗中均比不使用RQV有較大的提升。實驗結果表明，本文PAARV方法在異構多agent系統中的可行性，且在使用該方法后對系統可靠性具有較大的提升。但實驗的效果與SAS場景中的實際數據有關，若實際數據不能良好反映SAS的實際情況，實驗結果的可靠性可能會受到一定影響。

4 結束語

本文提出了一種基于概率時間自動機模型的異構多agent自適應運行時驗證方法。首先針對復雜SAS的建模問題，將系統中不同功能結構的agent建模為時間自動機模型，再將內外環境中的隨機因素抽象為系統模型的轉移概率，使時間自動機模型擁有概率形式的隨機變化，從而轉換為概率時間自動機模型，這樣由多個PTA構成的PTAN可以模擬出隨機環境下SAS的運行過程。針對系統中存在異構agent的驗證問題，先形式化描述agent之間的協作邏輯，再制定相應的安全約束策略，在此基礎上確保系統運行邏輯保持在安全狀態下，從而驗證系統agent協作邏輯的正確性和可靠性。最后使用概率模型檢查技術對功能需求進行定量化的驗證，與原始系統進行了比較，證明了本文方法的有效性。

本文方法的不足在于，系統在運行過程中相比原始系統增加了運行時模型驗證的過程，而驗證分析需要額外的計算過程，且與模型的規模成正比，若agent數量較大，可能會導致驗證產生狀態空間擁擠，降低系統的決策效率，增加系統的運行成本；在系統運行過程中，若環境出現重大變化，模型結構可能會出現部分失效，此時系統模型需要重新設計更新，拉低驗證的效率。未來的研究內容會聚焦于上述問題，研究如何優化模型的狀態空間，提高驗證效率并應用于更大型以及復雜的SAS中；研究模型的更新方法，考慮引入人的因素，將人的影響加入到系統控制循環中，保持模型對內外環境的適應性，或者研究模型的動態更新方法，使系統能監測到環境重大變化導致的模型問題，自行更新修復模型，保證系統驗證結果的可靠性。

參考文獻：

[1]de Lemos R， Giese H， Müller H A，et al. Software engineering for selfadpaptive systems：a second research roadmap[M]//De Lemos R， Giese H， Müller H A， et al. Software Engineering for SelfAdaptive Systems Ⅱ.Berlin：Springer，2013：1-32.

[2]董孟高，毛新軍，郭毅，等.自適應agent的設計和實現[J].計算機科學與探索，2011，5（3）：238-246.（Dong Menggao， Mao Xinjun， Guo Yi， et al. Design and implementation of selfadaptive agent[J].Journal of Frontiers of Computer Science and Technology，2011，5（3）：238-246.）

[3]Betty H C C， Kerstin I E， Martin G，et al. Using models at runtime to address assurance for selfadaptive systems[M]//Bencomo N， France R， Cheng B H C， et al. Models@run.Time.Cham：Springer，2014：101-136.

[4]Xu Chang， Cheung S C， Ma Xiaoxing ， et al. Adam： identifying defects in contextaware adaptation[J].Journal of Systems & Software，2012，85（12）：2812-2828.

[5]Wang Zhimin， Elbaum S， Rosenblum D S. Automated generation of contextaware tests[C]//Proc of the 29th International Conference on Software Engineering.Piscataway，NJ：IEEE Press，2007：406-415.

[6]Weyns D， Iftikhar M U， de la lglesia D G，et al. A survey of formal methods in selfadaptive systems[C]//Proc of Computer Science and Software Engineering.New York：ACM Press，2012：67-79.

[7]Jeff M， Tom M. Towards specification， modelling and analysis of fault tolerance in self managed systems[C]//Proc of International Conference on Software Engineering.New York：ACM Press，2006：30-36.

[8]Zhang Ji， Cheng B H C. Modelbased development of dynamically adaptive software[C]//Proc of the 28th International Conference on Software Engineering.New York：ACM Press，2006：20-28.

[9]Vassev E， Hinchey M. ASSL：a software engineering approach to autonomic computing[J].Computer，2009，42（6）：90-93.

[10]Weyns D， Malek S， Andersson J. FORMS： unifying reference model for formal specification of distributed selfadaptive systems[J].ACM Trans on Autonomous and Adaptive Systems，2012，7（1）：1-61.

[11]Clarke E M， Lerda F. Model checking： software and beyond[J].Journal of Universal Computerence，2008，13（5）：639-649.

[12]Kong W， Ogata K， Seino T， et al. A lightweight integration of theorem proving and model checking for system verification[C]//Proc of the 12th AsiaPacific Software Engineering Conference.Piscataway，NJ：IEEE Press，2005：59-66.

[13]Todman T， Luk W. Verification of streaming designs by combining symbolic simulation and equivalence checking [C]//Proc of the 22nd International Conference on Field Programmable Logic & Applications.Piscataway，NJ：IEEE Press，2012：203-208.

[14]Lomuscio A R， Pirovano E. Parameterised verification of strategic properties in probabilistic multiagent systems[C]//Proc of the 19th International Conference on Autonomous Agents and Multiagent Systems.New York：ACM Press，2020：762-770.

[15]劉瑋，何成萬，馮在文.面向不確定性的自適應需求規劃算法研究[J].小型微型計算機系統，2014，35（2）：266-272.（Liu Wei， He Chengwan， Feng Zaiwen. Planning algorithms to address uncertainty in selfadaptive software requirements[J].Journal of Chinese Computer Systems，2014，35（2）：266-272.）

[16]Dobson S， Zambonelli F， Denazis S，et al. A survey of autonomic communications[J].ACM Trans on Autonomous & Adaptive Systems，2006，1（2）：223-259.

[17]Liu Yepang， Xu Chang， Cheung S C. AFChecker： effective model checking for contextaware adaptive applications[J].Journal of Systems & Software，2013，86（3）：854-867.

[18]Bartels B， Kleine M. A CSPbased framework for the specification， verification， and implementation of adaptive systems[C]//Proc of the 6th International Symposium on Software Engineering for Adaptive and SelfManaging Systems.New York：ACM Press，2011：158-167.

[19]趙天琪，趙海燕，張偉，等.基于模型的自適應方法綜述[J].軟件學報，2018，29（1）：23-41.（Zhao Tianqi， Zhao Haiyan， Zhang Wei， et al. Survey of modelbased selfadaptation methods[J].Journal of Software，2018，29（1）：23-41.）

[20]Calinescu R， Kwiatkowska M. Using quantitative analysis to implement autonomic IT systems[C]//Proc of the 31st International Conference on Software Engineering.Piscataway，NJ：IEEE Press，2009：100-110.

[21]Epifani I， Ghezzi C， Mirandola R，et al. Model evolution by runtime parameter adaptation[C]//Proc of the 31st International Conference on Software Engineering.Piscataway，NJ：IEEE Press，2009：16-24.

[22]Calinescu R， Rafiq Y， Johnson K，et al. Adaptive model learning for continual verification of nonfunctional properties[C]//Proc of the 5th ACM/SPEC International Conference on Performance Engineering.New York：ACM Press，2014：87-98.

[23]Johnson K， Calinescu R， Kikuchi S. An incremental verification framework for componentbased software systems[C]//Proc of the 16th International ACM Sigsoft Symposium on ComponentBased Software Engineering.New York：ACM Press，2013：33-42.

[24]Mason G， Calinescu R， Kudenko D， et al. Assurance in reinforcement learning using quantitative verification[J].Advances in Hybridization of Intelligent MethodsSmart Innovation， Systems and Technologies，2017，85：71-96.

[25]Gadelha R， Vieira L， Monteiro D，et al. Scen@rist： an approach for verifying selfadaptive systems using runtime scenarios[J].Software Quality Journal，2020，28（3）：1303-1345.

[26]洪學志.COBOT：一個面向協作的自適應系統軟件框架[D].南京：南京大學，2015.（Hong Xuezhi. COBOT：a software framework for collaborative selfadaptive systems[D].Nanjing：Nanjing University，2015.）

[27]李爽，劉瑋，吳坤，等.面向運行時協作的異構agent能力選擇與補償方法研究[J].煙臺大學學報：自然科學與工程版，2017，30（2）：6.（Li Shuang， Liu Wei， Wu Kun， et al. Runtimeoriented collaborative heterogeneous agents capability choosing and compensation[J].Journal of Yantai University：Natural Science and Engineering Edition，2017，30（2）：6.）

[28]Maria C， David G， Javier C，et al. A probabilistic model checking approach to selfadapting machine learning systems[C]//Proc of International Conference on Software Engineering and Formal Methods.Cham：Springer，2022：317-332.

[29]Weyns D， Iftikhar M U， Soderlund J. Do external feedback loops improve the design of selfadaptive systems？A controlled experiment[C]//Proc of the 8th International Symposium on? Software Engineering for Adaptive and SelfManaging Systems.Piscataway，NJ：IEEE Press，2013：3-12.

[30]Weyns D， Iftikhar U. ActivFORMS：a formally founded modelbased approach to engineer selfadaptive systems[J].ACM Trans on Software Engineering and Methodology，2023，32（1）：1-48.

[31]葉幸瑜，劉瑋，王寧，等.基于馬爾可夫模型的多agent自適應在線驗證[J].計算機應用研究，2021，38（5）：1477-1481.（Ye Xingyu， Liu Wei， Wang Ning， et al. Multiagent adaptive runtime verification based on Markov model[J].Application Research of Computers，2021，38（5）：1477-1481.）

[32]Desel J， Reisig W， Rozenberg G. Timed automata： semantics， algorithms and tools[M]//Desel J， Reisig W， Rozenberg G. Lecture Notes in Computer Science.Berlin：Springer，2004：87-124.

[33]Kwiatkowska M， Norman G， Parker D. Advances and challenges of probabilistic model checking[C]//Proc of the 48th Annual Allerton Conference on Communication，Control，and Computing.Piscataway，NJ：IEEE Press，2010：1691-1698.

[34]Alur R， Dill D. Automata for modeling realtime systems[C]//Proc of International Colloquium on Automata，Languages and Programming.Berlin：Springer，1990：322-335.

[35]Alur R， Dill D L. A theory of timed automata[J].Theoretical Computer Science，1994，126（2）：183-235.

[36]Norman G， Parker D， Sproston J. Model checking for probabilistic timed automata[J].Formal Methods in System Design，2013，43（2）：164-190.

[37]Behrmann G， David A， Larsen K G. A tutorial on UPPAAL[M]//Bernardo M， Corradini F. Formal Methods for the Design of RealTime Systems.Berlin：Springer，2004：200-236.

[38]David A， Larsen K G， Legay A，et al. Uppaal SMC tutorial[J].International Journal on Software Tools for Technology Transfer，2015，17（4）：397-415.