[譯]時間自動機：語義，算法和工具

本文原題是《Timed Automata Semantics, Algorithms and Tools》，本人碩士畢業設計與此相關，研究了好久，現在自行翻譯出來。轉載請注明版權。

時間自動機：語義，算法和工具

Johan Bengtsson和Wang Yi

 

Uppsala大學

Email：{johanb,yi}@it.uu.se

（譯者：祝威http://bitzhuwei.cnblogs.com）

摘要：本文是時間自動機的教程，重點介紹了它作為驗證工具的語義和算法。本文給出了時間自動機的具體語義、抽象語義、決策問題及其算法（主要是轉換規則、區域和帶這些概念）。DBM（Difference Bound Matrices）是常用的基於時間自動機理論的驗證工具使用的數據結構。本文詳細講解其原理。最后，本文以Uppaal為例，介紹這一款時間自動機驗證工具的基本原理和使用方法。

1. 簡介

時間自動機是一套對實時系統進行建模和驗證的理論。這一理論是Alur和Dill的傑出工作成果。很多驗證工具（例如Uppaal）就是基於時間自動機理論制作的。本文就將介紹這些工具所依賴的時間自動機的語義和算法。

時間自動機就是帶有時鍾集的有限自動機。時鍾集是有限個時鍾的集合，每個時鍾都是一個取值范圍為0或正數的變量。時間自動機狀態之間的轉換要滿足時鍾約束才可能發生。時間自動機的狀態可以附加上“位置不變性”的屬性，這也是一個時鍾約束，用來保證狀態不會保持在原地不動。這種自動機稱為“時間安全自動機”，本文默認討論的都是這種自動機。

后文組織方式如下：下一節講述時間自動機的語法和語義，以及和自動化驗證相關的決策問題。本文中，可判定性和不可判定性被視為計算模型的基本屬性。第3節介紹基於區域和帶的抽象語義。第4節介紹DBM的數據結構。第5節介紹驗證工具UPPAAL。最后，在附錄中給出DBM相關算法的偽代碼。

2. 時間自動機群

時間自動機是附帶了若干實值變量的有限自動機（由有限個結點或位置和有限個邊組成的圖）。時間自動機是時序系統的抽象模型。變量模擬邏輯時鍾，時鍾從零開始，同步地增長。邊上的時鍾約束（例如guard）限制了自動機的跳轉行為。只有時鍾值滿足guard時，guard所在的邊才能發生跳轉。跳轉時可以將時鍾重置為零。

下面的Figure 1時間自動機和位置不變性是一個時間自動機的例子。時序性質由兩個時鍾x和y實現。時鍾x用於控制loop結點的自循環。當x為1時，loop就可能發生一次自循環。時鍾y控制整個自動機的完整運行。自動機可能在10<=y<=20的任何時間點離開start結點，也可以在40<=y<=50的任何時間點從loop到達end結點。

Figure 1時間自動機和位置不變性

Timed Büchi Automata

Guard只規定了在某些時間范圍內可以發生跳轉，但不是強制發生跳轉。（必要不充分條件）

時間安全自動機（略）

2.1 正規語法

表示實值變量或時鍾(clock)的有限集合，其元素用等表示。

表示動作的有限集合，其元素用等表示。

原子時鍾約束：形如或的式子，其中且

時鍾約束(Clock Constraint)：原子時鍾約束的合式公式。用於充當轉換條件。用等表示。

表示時鍾約束的集合。

定義1 （時間自動機Timed Automaton）

一個時間自動機Α是一個四元組，其中

－ 是位置（或稱為狀態）的有限集合

－ 是初始位置

－ 是邊的集合

－ 是從不變性到位置的映射

若，可記作，即存在從位置到的轉換。

在Uppaal里，位置不變性規定為x<=n或x<n的形式。

並發和交互

（略）

2.2 操作語義

時間自動機的語義是一個狀態轉換系統。狀態由當前位置和所有時鍾的當前值組成。

狀態轉換包括兩種類型，即延時轉換和動作轉換。為了表述時間自動機的操作語義，引入時鍾映射的概念。時鍾映射是從到非負實數的映射，用表示。用代表所映射的時鍾值滿足，即動作轉換是可能發生的。用代表，其中。用代表范圍內的時鍾值置為零，外的時鍾值由確定()。

定義2 （操作語義Operational Semantics）

一個時間自動機的語義被定義為一個轉換系統，時間自動機的狀態為二元組<l，u>，轉換則定義為：

① if 且，

② if ，，，且

2.3 驗證問題

操作語義是時間自動機驗證的基礎。下文基於轉換系統來闡述可判定性問題。（略）

定義3 （語句Run）

在操作語義的基礎上，我們可以定義一個時間自動機的時間語言，其中，若對於存在時序序列使得如下的序列成立：

，其中

那么我們稱是的一條語句。

定義4 （相似Bisimulation）

（略）

可達性分析

定義5 （可達性）

（略）

3. 符號語義和驗證

時鍾是實值的，所以狀態轉換系統有無數個情況，這不能用於自動化驗證。為解決這個問題，提出下面的區域、帶和符號語義的概念。

3.1 區域，帶和符號語義

區域等價是時間自動機屬性判定的基礎。

定義6 （區域等價Region Equivalence）

（略）

Figure 2有兩個時鍾的系統區域圖

（略）

時間自動機的狀態空間的更高效的表述方法是用“帶圖”。“帶”表示符號狀態。構造帶圖的方法和算法在第4節有介紹。Figure 3時間自動機和它的帶圖展示了一個示例。這個帶圖只有8個狀態，而它的區域圖卻有超過50個狀態。

Figure 3時間自動機和它的帶圖

一個帶就是一個時鍾約束。嚴格的說，是這個所有滿足這個時鍾約束的解的集合。帶可以用DBM表示，這方面的研究很成熟。以后D既可以表示時鍾約束，也可以表示帶，那么就可以表示帶的集合了。

時間自動機的符號狀態是一個二元組<l,D>。<l,D>實際上是時間自動機的某些狀態的集合，其中l是位置，D是帶。符號轉換描述的就是這些狀態集之間的所有可能發生的轉換。

定義7 （符號轉換Symbolic Transition）

第4節會詳細講述這些操作。其中的D^↑寫作了up(D),r(D)寫作了reset(D,r:=0)。帶的運算結果仍然是帶（矩陣的運算結果仍然是矩陣）。帶可以像代數式那樣化簡（canonical），而且化簡的最終形式是唯一的。這是符號語義緩解狀態空間爆炸的關鍵結構。

符號語義和操作語義有着對應關系。就是說，若<l,D>à<l’,D’>，那么對於所有的u’屬於D’，一定存在u∈D，使得<l,u>-><l’,u’>。符號語義可以說是對定義2的本質的描述。

定理1 （符號語義的完整性和存在性）

設時間自動機初始狀態為<l₀,u₀>

完整性的意思是，若初始的符號狀態能夠到達最終的符號狀態，那么最終的符號狀態中包含的所有具體狀態都應該是可到達的。存在性的意思是，若一個具體狀態是可達的，那么就存在一個符號轉換關系把這個狀態包含進去。

不幸的是，符號狀態轉換是無限的，所以時間自動機的帶圖可能是無限的。考慮下面的示例Figure 4產生無限帶圖的時間自動機，時鍾y無限的增長，從而繪出了無限的帶圖。

Figure 4產生無限帶圖的時間自動機

解決方式是用類似擴展操作的技術，把含有任意大常量的帶轉化為一個類型的帶。直覺上看，就是一旦時鍾值超過某個常量，它具體是多少就無關緊要了。

3.2 不含差約束的帶的正規化

差約束是形如x-y<=n的guard。最初的時間自動機理論不允許差約束作為guard，只允許x<=n的形式。這是無斜角的自動機。這類自動機的帶用k正規化操作即可。Uppaal就是這么做的。

定義8 （K正規化k-Normalization）

設D為帶，k為時鍾上限，那么D上的k正規化操作的語義如下：

Norm_k(D)可以通過對D的最簡式執行以下兩個操作來實現。

1. 去掉所有m>k(x)的x<=m，x-y<=m的約束；

2. 把所有m>k(x)的x>=m和x-y>=m分別替換為x>=k(x)和x-y>=k(x)。

在Figure 4產生無限帶圖的時間自動機中的帶圖的正規化的結果如下Figure 5正規化的帶圖所示。其中的時鍾上限是時間自動機中出現的最大時鍾常量。

注意到，對於有限個時鍾，給定它們的時鍾上限，那么只存在有限個正規化的帶。就是說，通過正規化我們可以把無限的帶圖轉化為有限的帶圖。

Figure 5正規化的帶圖

定義9 （正規跳轉）

無斜角的時間自動機，正規跳轉滿足完整性、存在性和有限性。

定理2 無斜角的時間自動機

設時間自動機有初始狀態<l0,u0>，最大時鍾常量上限由函數k決定，且不含差約束。那么：

不幸的是，對於包含差約束的時間自動機，不滿足完整性。本文用下面的示例說明。考慮如下Figure 6計數器示例所示的自動機。最后一個節點是不可達的。因為在S2結點，時鍾帶是（x-y>2且x>2）;而S2到S3的guard是（x<z+1且z<y+1），這等價於（x-z<1且z-y<1且x-y<2）。很明顯S2永遠不能滿足guard，最后一個轉換就不可能發生。

Figure 6計數器示例

但是，x時鍾的最大常量是1，y是2，S2的帶（x-y>2且x>2）經過正規化就是（x-y>1且x>1），這樣就能夠滿足S2到S3的guard了。這樣一來，基於正規化的符號可達性分析就出錯了。

帶的最簡式在下面的列出。隱含的所有時鍾都為非負數沒有列出。

Figure 7計數器示例的帶

注意到，正規化前后的S0和S1是相同的，問題是S2前后帶與guard的交集一個是空的一個是非空的。

3.3 含有差約束的時間自動機的正規化

含有差約束的正規化是很有用的。

定義10 （使用差約束的正規化Normalization Using Difference Constraints）

優化定義的k正規化操作的語義可表示為：

優化的區域等價要符合時鍾上限k函數和guard集G。正規化操作也是。

因為k等價運算得到的區域是有限的，G中的guard也是有限的，所以優化的k正規化操作得到的區域也是有限多個。這就是說，給定帶D，norm_k,G(D)操作僅包含有限個等價區域。只不過這個區域不是凸的。這個區域可以由有限個凸的區域的並集組成。下一節將詳細介紹算法。

定義11 （優化的k正規化跳轉）

設時間自動機有初始狀態<l0,u0>，最大時鍾常量上限由函數k決定，guards中的差約束集合用G表示。則滿足完整性、存在性和有限性：

3.4 符號可達性分析

模型檢測關心兩種類型的屬性：liveness和safety。檢測liveness的算法是環路檢測，非常耗時。時序系統主要是由safety檢測，相關算法是遍歷時間自動機的狀態空間。

算法1 可達性分析

可達性分析用於檢測狀態的性質。核心思想分兩步，首先計算出時間自動機的狀態空間，然后搜索狀態空間中符合條件或與之矛盾的狀態。第一步可以提前處理，也可以在搜索過程中實時處理。后者更有優勢，因為只需要處理那些需要驗證的狀態就可以了。但是有時候這並不管用，還是要處理所有的狀態空間。

我們將講解Uppaal的核心驗證引擎。Uppaal是基於符號語義和帶圖進行可達性分析的一種工具。

設有時間自動機A，初始狀態<l0,D0>和最終狀態<lf, φf>，時鍾上限k由A和φf中的最大常量定義，G表示A和φf中的差約束的集合。算法1可用於檢測初始狀態能否到達這樣的狀態：其位置為lf，其時鍾值滿足φf。它實時計算A的帶圖，搜索其中位置為lf且帶和φf有交集的符號狀態。

算法1工作在有限的狀態空間，所以一定會終止；另一方面，它的返回值也一定是正確的，這在之前的定義11中得到了論證。

算法1也提示出了，時間自動機的模型驗證器要解決的關鍵問題，例如狀態、帶的表示和運算。另外還需要帶的判空和相互包含的判定，以及壓縮存儲、狀態空間壓縮和近似計算等技術。

4. DBM: 算法和數據結構

前文講解了符號化的可達性分析中的關鍵點。回憶一下，zone（帶）是用時鍾區間（clock assignment）定義的。我們還沒有闡述zone是如何計算的。下面將對zone的表達（數據結構）、zone的操作（算法）和驗證（檢驗是否具有某屬性）進行講解。最后附上相關操作的偽代碼。

5.1 DBM基礎

在時鍾集C上的時鍾約束是原子約束的合式公式。原子約束是x~m或者x-y~n的形式，其中x，y是時鍾集C的元素，~屬於{≤，＜，=，＞，≥}，m，n屬於自然數。用時鍾區間D表示的zone是滿足D的時鍾值的集合。（符合時鍾約束的x，y。。。的值的所有情況）zone最重要的性質（或者說搞出zone這個東西來的理由）是zone可以用矩陣來表示，就是DBM（Difference Bound Matrices）。所以下面就講述DBM的結構和性質。

為方便數學表達，我們引入“零時鍾”。零時鍾就是無論何時其值都為0。設C0=C∪{零時鍾}，那么任意zone都可以寫作x-y<=n的形式。（n是整數）

顯然，用|C0|2個形如x-y<=n的原子約束就可以表達zone。所以就用|C0|×|C0|的矩陣表示zone，矩陣的一個元素對應一個原子約束，這個原子約束表達了兩個時鍾的差異，所以叫做差界矩陣。后文中一律用Dij表示DBM的（i，j）處的元素。（DBM表示zone，或者說D）

下面是構造DBM的方法。

首先，將C0的時鍾按0，...，n排序，讓零時鍾的序號為0,。矩陣的一行表示一個時鍾。計算規則如下：

對於形如Xi – Xj<=n的約束，讓Dij=（n，<=）

對於Xi – Xj未定義的Dij，讓Dij=（∞，<=）無窮大在數據結構里用一個特殊值表示。

對特殊情況：0 – Xi <= 0和Xi – Xi <= 0進行設置

示例：例如一個zone，表示為D= x – 0 < 20且y – 0 <= 20且 y – x <= 10且x – y <= -10且0 – z < 5。這個zone轉化為矩陣如下：

DBM的元素有兩種操作：比較和相加。我們規定如下：

若n1 < n2，則（n，<=1） < （n1，<=） < （n2，<=2）。

（n，<） < （n，<=）

b1 + ∞ = ∞

（m，<=） + （n，<=） = （m+n，<=）

（m，<） + （n，<=） = （m+n，<）

最簡（Canonical）DBM

通常，會有無限個zone本質上相同，但他們只有一個最簡的形式。

為求出最簡化的DBM，我們把用權重圖表示zone，其中C0的元素用結點表示，原子約束用邊表示。形如x-y<=n被轉化為從y結點到x結點的邊，用（n，<=）標記，這意思是說從y到x的距離最大是n。

Figure 8示例矩陣的圖解和閉包形式

分析一下（過程略），可知界限最緊最強的等價D表示可以通過圖解中兩個結點的最短路徑算法得到！（好厲害的結論，Floyd-Warshall算法就可以）由於這個算法比較耗時，所以我們要求DBM的保存和操作結果的保存都用最簡化的形式。

最小約束系統

一個zone可能包含冗余的約束。例如D=x-y<2, y-z<5, x-z<7。其中x-z<7顯然可以從前兩個推理出來。去掉冗余約束是必要的。最小約束矩陣可以用稀疏矩陣表示，這就緩解了狀態空間爆炸的問題。最小約束系統已經被很徹底的研究過了。下面我們總結一下前人的成果就好。

（總結略）在附錄的算法4里有偽代碼。看代碼就行了。

好了，我們能夠得到DBM的最簡形式了。減輕了包袱，下面開始處理DBM的計算問題。

5.2 DBM基本操作

本節講述除了zone標准化之外的所有基本操作。這些操作會用在時間自動機的模型驗證，前向、后向分析。下一節再講zone標准化（normalization）。

為描述簡單，本節討論的zone都是相容的（不為空的），最簡化的。

DBM的操作分為兩類：

屬性驗證：這類操作包括檢驗DBM相容性、zone之間的包含關系以及zone師父滿足給定的原子約束。

變形：這類操作包括根據guards、延時和時鍾重置來計算zone的最強后置條件和最弱前置條件。

1. 屬性驗證

1) Consistent（D）

最基本的操作。判斷DBM是否不為空（為空則表示這個帶不包含任何有意義的時鍾值）。例如，時鍾解的集合是否空集。這在狀態空間檢測中用來去掉不相容（即空）的狀態。（去掉那些不可能存在的狀態，減少狀態數）

把D₀₀設置為負就行了。

2) Relation（D,D’）

包含關系也是個重要的檢測。對所有的i,j屬於C₀，Dij <= D’ij是D包含於D’的充要條件。詳見算法5。

3) Satisfied（D，Xi – Xj <= m）

有時候會需要判斷一個zone是否滿足某約束。例如，在不修改D的前提下判斷D且Xi – Xj <= m是否相容。從consistent的定義我們知道zone是否相容取決於它是否包含負環。所以，Satisfied檢測就是把這個guard加到D上，看它是不是產生了負環。對於最簡化的DBM，只要檢測(m，<=)+Dji是否為負就可以了。

2. 變形

1) Up(D)

把那些由於時延被包括進D的時鍾區間的范圍都算進來，就是Up(D)。所以Up(D)={u+d|u∈D,d∈R+}。算法上的含義是，Up把所有時鍾的上限抹掉（DBM的Di0設置為∞）。由於所有時鍾具有同速率地走動的性質，任意兩個時鍾之間的差值都不會超過界限。（因為都是x – y <= n這種形式，所以x、y同步的增減都不會破壞這個關系）

Up和最強后置條件的關系我還不明白。資料上說Up就是計算最強后置條件的。

2) Down（D）

類似Up，Down（D）={u|u+d∈D,d∈R+}。算法上，把DBM的第一行（零時鍾所在行）都設置為（0，<=）。但這可能導致不產生不最簡的DBM，需要進一步處理。算法是：計算x時，將所有其他時鍾Yi置為0，檢查差別約束Yi-X,把其中最強約束最為新的界限。詳見算法7。

3) And（D，Xi – Yj <= b）

把一個約束加到zone上是最常見的操作。基本步驟是：若(b，<=) < Dij，則設置Dij為(b，<=)，然后調整新zone為最簡化的形式。調整方法使用O(n2)的特殊算法。特殊算法利用了只有Dij改變了這一事實和Floyd算法的性質，減少了運算量。詳見算法8。

4) Free（D，x）

去掉對給定時鍾的所有約束。就是說，x時鍾可以取任意正數。Free（D，x）={u[x=d]|u∈D，d∈R+}。用於狀態空間的后向檢查。詳見算法9。

5) Reset（D，x:=m）

在前向檢查中用於把時鍾置為特定的值。Reset（的，r:=m）={u[x=m]|u∈D}。若不要求最簡化的結果，只需設置Dx0=（m，<=），D0x=（-m，<=），並所有x行的邊界。但用類似做free的方法，可以得到最簡化的結果。詳見算法10。

6) Copy（D，x:=y）

用在前向狀態空間檢查。把y的值復制給x。定義Copy（D，x:=y）={u[x=u(y)]|u∈D}。實現方法很簡單，把Dxy和Dyx都置為（0，<=）,其他地方的x都換成y的值。詳見算法11。

7) Shift（D，x:=x+m）

把時鍾x增加或減少一個整數值。Shift（D，x:=x+m）={u[x=u(x)+m]|u∈D}。只需用x-m代替原來的x就行了。詳見算法12。

5.3 帶（Zone）的正規化

帶的正規化的目的是把含有任意大的常量的帶轉化為只含有不超過上限的常量的帶，從而將時間自動機的無限帶圖轉化為有限帶圖。

若時間自動機不含差約束，用normk(D)正規化即可。實際上只需做兩件事，一是把超過上限的<=差約束對應的約束刪除；二是把絕對值超過上限的>=差約束改到上限。對最簡化的DBM數據結構來說，就是若(m,<=) > (k(x),<=)，則去掉x-y<=m這個差約束；若(m,<=) < (-k(y),<)，則把x-y<=m改為x-y<-k(y)。

若時間自動機的guard里含有差約束，就比較麻煩。設有時間自動機A，含有差約束的集合G，上限函數k。現在要對A的一個帶D進行正規化。根據定義10的正規化的語義，D和正規化的D的時鍾值同時滿足或不滿足G的所有差約束。這啟示我們導出如下的正規化核心算法。

1.收集A中滿足下列條件之一的所有差約束：

(1)g且D為空：這是g在D外的情況

(2)(非g)且D為空：這是g包含D的情況

設Gunsat=上述g和非g的集合。

2.不考慮差約束的存在，直接計算norm_k(D)

3.上一步得到的規范化的D逐一減去Gunsat的部分，即norm_k(D)且(非Gunsat)

第3步的目的在於確保規范化的D中不含那些D不滿足的差約束。算法14給出了k核心算法的偽代碼。算法中的Gd是時間自動機中出現的差約束的集合。

但norm_k(D)且(非Gunsat)仍然不是我們要求的正規化的帶。K核心算法沒有處理那種差約束分割了D的情況。就是說，可能存在一個g，使得g且D不為空同時(非g)且D也不為空。所以，我們要用算法15把D分割成若干部分，對分割出來的部分分別執行k核心算法。任意一個分割的Di都應該滿足：對於所有的g∈G，或者Di且g為空，或者Di且g為Di（即g包含Di）。最后把各個Di正規化的結果取並集，就是我們要求的norm_kG(D)

完整的計算流程就是算法16。

我們用上文中的計數器示例的S2的帶D：（x-y>2且x>2）來演示說明正規化過程。示例中的差約束是g1=x-z<1和g2=z-y<1。D既包含滿足g1的部分又包含滿足(非g1)的部分，所以在正規化之前要分割D，如下圖所示。

D(a)與g2交集為空，所以不需再分割。D(b)還要根據g2分割為滿足g2和非g2的部分，所以就分成了下面的形式。

這三個帶就要執行k核心算法了。

D(a)、D(b)、D(c)不滿足的差約束集合分別是Gunsat(a)={非g1,g2}，Gunsat(b)={g1,非g2}，Gunsat(a)={g1,g2}。分別對其進行kG正規化，得到：

由於正規化的D(A)、D(B)、D(C)與Gunsat都沒有交集，我們不需要減去對應的差約束了。最后強調一下，正規化的ABC和g1且g2都沒有交集，S2到S3的跳轉也沒有發生變化。（仍舊不能跳轉）

5.4 DBM的內存表示

（略）

5. Uppaal

Uppaal是時間自動機建模、仿真和驗證的工具箱。它用到了前文所述的數據結構和算法。它是由Uppsala大學和Aalborg大學共同開發的。

5.1 Uppaal建模

Uppaal建模的核心是時間自動機網絡。Uppaal已經擴展了建模和驗證能力。重點包括整型變量、立即管道和過期位置。

時間自動機網絡

（略）

6. 附錄

下面列出DBM常用運算的偽代碼。

算法2 Close(D)或Canonical(D)：計算D的最簡式

Figure 9計算D的最簡式

算法3 消去無零環帶圖的冗余約束

Figure 10 消去無零環帶圖的冗余約束

算法4 消去一般帶圖的冗余約束

Figure 11消去一般帶圖的冗余約束

算法5 判定兩個帶之間的包含關系

Figure 12判定兩個帶之間的包含關系

算法6 時間流逝

Figure 13時間流逝

算法7 時間倒流

Figure 14時間倒流

算法8 添加時間約束

Figure 15添加時間約束

算法9 取消整個時鍾的約束

Figure 16取消整個時鍾的約束

算法10 重置時鍾

Figure 17重置時鍾

算法11 復制時鍾

Figure 18復制時鍾

算法12 時鍾偏移

Figure 19時鍾偏移

算法13 k正規化

Figure 20k正規化

算法14 k核心正規化

Figure 21k核心正規化

算法15 帶的分割

Figure 22帶的分割

算法16 kG正規化

Figure 23kG正規化

算法17 添加上限

Figure 24添加上限