基于權重區間的模態接口自動機

黃潤華 張晉津 張君瑤

摘? 要： Gerald Lüttgen和Walter Vogler將接口自動機的輸入輸出行為引入到模態轉換系統的模態邏輯中，從而可以隱式允許輸入表達，稱為模態接口自動機。但他們的工作并沒有考慮量化信息，而實際應用中這類量化信息是必要的。本文通過將權重與轉換關系相關聯，來表達量化信息，建立了加權模態接口自動機，并重新定義了帶有權重區間的精化關系。在這個框架中，我們研究了合取、析取和并發等系統算子，并證明了精化關系是關于這些算子的同余關系。

關鍵詞： 模態接口自動機； 量化信息； 精化關系； 系統算子

中圖分類號：TP301? ? ? ? ? 文獻標識碼：A? ? ?文章編號：1006-8228（2023）05-20-05

Modal interface automata with weight intervals

Huang Runhua1，2， Zhang Jinjin1，2， Zhang Junyao1，2

（1. College of Information Engineering， Nanjing Audit University， Nanjing， Jiangsu 211815， China;

2. Jiangsu Key Laboratory of Public Project Audit）

Abstract： Gerald Lüttgen and Walter Vogler introduced the input and output behavior of interface automata into the modal logic of the modal transformation system so that the input expressions can be implicitly allowed， which is called a modal interface automaton. However， their work does not consider the quantitative information， which is necessary in practical applications. In this paper， by associating weights with transformation relations to express quantitative information， we establish a weighted modal interface automaton and define a new refinement relation with weight intervals. In this framework， we study the system operators such as conjunction， disjunction and concurrency， and prove that the refinement relation is a congruence relation on these operators.

Key words： modal interface automata; quantitative information; refinement relationship; system operator

0 引言

De Alfaro和Henzinger T提出了接口自動機（Interface Automata）來解決軟件和系統工程之間的組件組合問題[1]。Larsen的模態轉換系統（Modal Transformation System）通過一系列改進將規范轉化為實現，并且提供必須轉換和可能轉換的兩種轉換關系[2]。在文獻[3]中，Gerald Lüttgen和Walter Vogler將接口自動機嵌入模態轉換系統，提出了模態接口自動機（Modal Interface Automaton），它既能滿足輸入的一致性，又可以表達強制性輸出，他們還修復了文獻[4]中的缺陷，即精化關系不是關于并行運算具有同余性的。

近年來，一些接口理論[5-7]也研究了接口自動機和模態轉換系統的結合，還有一些學者對模態接口自動機做了一些改進，比如Bujtor F和Vogler W在模態接口自動機中添加了時態邏輯，稱為時態MIA，時態MIA允許對各種操作和邏輯連接進行異構規范[8]。但還沒發現有學者對模態接口自動機進行量化信息的研究，而在實際系統中，存在著資源的消耗比如價格，燃料，時間等。在定量系統方面的研究也有很多，比如在自動機的定量研究中，Droste M和GastinP引入了一種帶權重的邏輯關系，并分析了加權有限自動機的行為恰好是加權一元二階邏輯中可定義序列的條件[9]。Line Juhl和Kim G. Larsen提出了一種新的模態轉換系統擴展，稱為加權模態轉換系統[10]，它允許表達其預期實現的必須和可能行為，并給出了如何計算一組有限確定性規范的最大公共精化問題的算法。

本文提出了一種加權模態接口自動機（Weighted Modal Interface Automata），作為模態接口自動機的擴展。它用一系列權重區間來修飾每個轉換關系，這些區間可以描述資源約束，如時間、資源、價格、燃料等消耗。我們還重新定義了加權模態接口自動機的精化關系，并且定義了三個系統操作符：合取、析取和并發。同時，我們給出精化關系是關于這些算子的同余性的定理。

本文第1節介紹加權模態接口自動機及相關概念，定義新的精化關系。在此基礎上，第2節引入第一個系統算子——合取操作，并給出精化關系在合取操作上的同余性定理。第3節定義了另外兩種系統算子——析取和并發，也給出精化關系在這兩種系統算子上的同余性定理。最后第4節總結全文并指出未來研究方向。

1 加權模態接口自動機

1.1 基本定義

我們首先擴展模態接口自動機的概念，為其每個轉換關系添加一個權重區間，這個權重區間表示對資源成本的量化限制，即一個行為（轉換）上附加一個權重區間，表示該行為（轉換）消耗的資源應在此區間范圍內[11，12]。類似于文獻[10]的方法，我們將該權重區用一個集合表示，并且可以在實現中將其細化為特定值。對于任意的[m，n∈Z∪-∞，+∞]，如果[m≤n，]則[m，n={a∈Z：m≤a≤n}]（即[m]與[n]之間的閉區間）稱為權重區間。本文使用[I]表示所有此類非空區間的集合，用[W]、[V]等符號表示權重區間，用[W*]、[V*]等符號表示權重區間的集合。

定義1 一個加權模態接口自動機（WMIA）是一個六元組[M=Q，I，O，→，?，δ]，其中：

⑴ [Q]是一個狀態集合；

⑵ [I，O]分別是輸入和輸出字母表，二者不相交且不含內部動作[τ]；

⑶ [→?Q×（I∪O）×（Q＼?））]表示必須轉換關系；

⑷ [??Q×（I∪O∪{τ}）×Q）]表示可能轉換關系；

⑸ [δ]是一個由[→∪?]到權重區間集[I]的函數。

我們用[A]表示[I∪O]，并將[A]和[A∪{τ}]中的元素分別表示為[a，b，c，d…]和[α， β， γ…]等。為了表述方便，在加權模態接口自動機中，我們規定：

● 如果[p， a， p'∈→]并且[δp， a， p'=W]，則記作[pa，Wp']；

● 如果[p， a， p∈→]，我們寫作[pap']；如果[?p'， pap']，我們寫作[pa]；相反，如果不存在[p']，使得[p， a， p∈→]，則記作[p?a]；

● 如果[pa]，我們寫作[pa，W*P']，其中，[P'={p'：pap'}]，[W*={W：pa，Wp'，p'∈P'}]；

● 令[W*]和[V*]是權重區間集合，如果對于任意的[W∈W*]，都存在[V∈V*]使得[W?V]，我們記作[W*≤V*]；

● 令[W*]和[V*]是權重區間集合，我們定義：

[W*∩V*={W∩V| W∩V≠?， W∈W*， V∈V*}]，

[W*∪V*={W∪V| W∈W*， V∈V*}]。

可能轉換[?]的相關標記可以類似定義。

為了滿足一致性，我們規定（a）如果[pa，W*P']，則[?W∈W*，p'∈P']，都有[p--→a，Wp']；（b）[?i∈I]，如果[p--→i，Wp']則[?P'，pi，W*P']并且[W∈W*]，[p'∈P']；（c）[?i∈I]，如果[pi，W*P']并且[pi，W*P'']，則[P'=P'']。（b）和（c）的要求既加入了權重區間，又不改變文獻[3]中關于模態接口自動機中的輸入一致性。具體而言，（b）表示如果模態接口自動機中的一個狀態可以進行一個可能轉換到達一個后繼狀態，那么這個狀態就可以進行必須轉換，這能夠保證模態接口自動機可以接受所有規定的輸入；（c）表示對于一個相同的輸入而言，必須轉換能夠到達相同的后繼狀態集合。

因為轉換過程內部動作的不可觀測性，類似于文獻[10]，本文不區分內部動作[τ]并且不考慮[τ]的量化信息。與通常定義類似，引入以下標記：（i）如果[qτ*q']則記作[qεq']；（ii）對于[o∈O]，如果[qεq''oq']，記作[qoq']，其中這個公式中的輸出動作[o]不含內部動作[τ]。進一步，我們定義如果[α=τ]，則[α=ε]，否則[α=α]。

1.2 精化關系

為了描述規范間和實現與規范間的精化關系，引入以下定義。我們現在可以定義WMIA的精化關系，這是MIA上精化關系的自然擴展。從現在起，當使用術語精化關系時，我們總是指下面定義的兩個WMIA之間的模態精化關系。

定義2（WMIA精化關系） 假設[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是兩個具有相同輸入輸出集合的WMIA，則[R?P×Q]是一個[WMIA]精化關系當且僅當對于任意的[p，q?R]，有

⑴ 若[qa，V*Q']，則[?P'，pa，W*P'，W*≤V*]且[?p'∈P'，?q'∈Q'，p'，q'∈R]；

⑵ 若[p--→α，Wp']且[α∈O∪{τ}]，則[?q'，q==?α，Vq'，]

[W?V]，且[p'，q'∈R]。

如果存在[WMIA]精化關系[R]使得[p，q∈R]，則稱[p] WMIA-精化了[q]，寫作[p?WMIAq]。進一步，如果[p?WMIAq]且[q?WMIAp]，我們稱[p]和[q]是互精化的，記作[p=WMIAq]。

受文獻[13]中關系定義的啟發，本文在WMIA允許輸入確定性的基礎上，添加了條件[W?V]來優化精化關系的權重區間。因為一個狀態進行相同動作的轉換不一定只有一個后繼狀態，所以我們引入權重區間集合[W*]，[V*]的概念表示到達所有后繼所需權重的集合，并使用“[≤]”表示區間集合之間的包含關系。如果可以用[P]來模擬[Q]的必須轉換，并且可以[Q]來模擬[P]的可能轉換，我們稱[P]精化了[Q]。從直觀上講，如果[P]精化了[Q]，那么[Q]所消耗的資源量應包含[P]所消耗的資源量。

2 三種系統算子——合取

我們通過刪除與MIA類似的不一致狀態來定義WMIA的連接。區別在于，文獻[3]中只考慮了MIA中動作的匹配，而我們還需要考慮WMIA中權重間隔的匹配。我們使用區間集之間的交集[W*∩V*]來表示轉換關系所消耗的權重。因此，我們需要先引入合取積的定義。

定義3（WMIA的合取積） 假設[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是兩個具有相同輸入輸出集合的WMIA，我們定義合取積[PQ]為：[PQ=defP×Q∪P∪Q，I，O，→，?，T]。它繼承了[P]和[Q]的所有轉換關系，并且對于所有的[i∈I]，[o∈O]，[α∈O∪{τ}]有以下規則：

（IMust1） 如果[pi，W*PP']且[q?iQ]，

則[p，qi，W*P']；

（IMust2） 如果[qi，V*QQ']且[p?iP]，

則[p，qi，V*Q']；

（IMust3） 如果[pi，W*PP']且[qi，V*QQ']，

則[p，qi，T*P'×Q']，[T*=W*∩V*]；

（IMay1） 如果[p--→i，WPp']且[q--→iQ]，

則[p，q--→i，Wp']；

（IMay2） 如果[q--→i，VQq']且[p--→iP]，

則[p，q--→i，Vq']；

（IMay3） 如果[p--→i，WPp']且[q--→i，VQq']，

則[p，qi，Tp'，q']，[T=W∩V]；

（OMust1） 如果[po，W*PP']且[q==?o，VQ]，

則[p，qo，T*{p'，q'|p'∈P'，q==?o，VQq'}]，

[T*=W*∩V]；

（OMust2） 如果[qo，V*QQ']且[p==?o，WP]，

則[p，qo，T*{p'，q'|q'∈Q'，p==?o，WPp'}]，

[T*=W∩V*]；

（May1） 如果[p==?τPp']，

則[p，q--→τ（p'，q）]；

（May2） 如果[q==?τQq']，

則[p，q--→τp，q']；

（May3） 如果[p==?α，WPp']且[q==?α，VQq']，

則[p，q--→α，Tp'，q']，[T=W∩V]。

因此，當WMIA中的[p]和[q]同時滿足轉換關系時，我們只需要考慮權重。我們使用所需權重區間的公共區間來表示合取積[（p，q）]的權重區間。當[W*∩V*=?]時，我們將其添加到不一致狀態中。因此接下來我們由不一致狀態引入WMIA的合取操作的定義。

定義4（WMIA的合取） 給定一個合取積[PQ]，則其不一致狀態[F]定義為滿足下面要求的最小集合：

（F1）[po，W*P]，[q=?oQ]，[o∈O]， 則[p，q∈F]；

（F2）[qo，V*Q]，[p=?oP]，[o∈O]， 則[p，q∈F]；

（F3）[po，W*P]，[qo，V*Q]，[o∈O]，但[W*∩V*=?]，則[p，q∈F]；

（F4）[p，qa，T*F']，[F'?F]， 則[p，q∈F]；

合取操作[P∧Q]通過刪除所有合取積[PQ]中屬于不一致狀態[F]的狀態[p，q]，以確保[P∧Q]具有公共的輸入和輸出字母。我們定義[P∧Q]中的元素[p，q]為[p∧q]，其中所有的狀態都是已定義的且一致的。

定理1 假設[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是兩個具有相同輸入輸出集合的WMIA，[p∈P，q∈Q]，我們有以下結論：

（i） 如果[?WMIA R]，[r∈R]，則[r?WMIAp]且[r?WMIAq]當且僅當[p∧q]是已定義的；

（ii） 如果[p∧q]是已定義的并且對于所有的WMIA[ R]，[r∈R]，則[r?WMIAp]且[r?WMIAq]當且僅當[r?WMIAp∧q]。

上述定理表明，如果兩個規范[p]和[q]沒有共同的精化，那么它們在邏輯上是不一致的。此外，這個定理在（ii）中指出，WMIA的合取操作[∧]是關于精化關系[?WMIA]的最大的下界。因此，WMIA精化關系[?WMIA]與合取操作[∧]是具有同余性的。

3 三種系統算子——析取和并發

3.1 析取算子

在本節我們繼續在WMIA上定義第二種系統算子——析取算子，并討論它的性質；特別是，對應于合取操作，這個運算符應該對應精化關系的最小的上界。

定義5（WMIA的析取） 假設[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是兩個具有相同輸入輸出集合的WMIA，則析取算子[P∨Q]定義為

[P∨Q=def{p∨q|p∈P，q∈Q}∪P∪Q，I，O，→，?，T]其中[→]和[?]是滿足[→P?→]，[→Q?→]，[?P??]，[?Q??]的最小集合并且滿足下列轉換關系：

（Must）? 如果[pa，W*PP']且[qa，V*QQ']，

則[p∨qa，T*P'∪Q']，[T*=W*∪V*]；

（May1）? 如果[p--→α，WPp']，則[p∨q--→α，Wp']；

此外，如果[α∈I]，[q--→α，VQ]也成立；

（May2）? 如果[q--→α，VQq']， 則[p∨q--→α，Vq']；

此外，如果[α∈I]，[p--→α，WP]也成立。

類似于合取，我們取[W*]和[V*]的并集作為[p∨q]的權重區間，（May1）和（May2）的規則是為了保證WMIA的輸入確定性，即當[α∈I]時，我們規定狀態[p]，[q]都可以做可能的[α]轉換。那么到目前為止，我們已經為WMIA的析取算子增加了權重，并且應滿足以下定理。

定理2 假設[P]、[Q]、[R]是WMIA，[p∈P]，[q∈Q]，[r∈R]。那么[p∨q?WMIAr]當且僅當[p?WMIAr]且[q?WMIAr]。

通過這個定理我們可以看出WMIA的析取操作[∨]是關于精化關系[?WMIA]的最小上界，并且WMIA精化關系[?WMIA]與析取操作[∨]是具有同余性的。

3.2 并發算子

在本節中我們定義WMIA的第三種系統算子——并發算子，并發運算對于系統和規范的組成非常重要。我們在WMIA上提供了一個并行運算符。如同定義合取運算符一樣，這里采用的方法也是將所有的不一致狀態識別出來并刪除，并且在某些實現中不可避免地會出現錯誤的所有狀態也都被刪除。因此，同樣我們需要先定義WMIA的并發積。

定義6（WMIA的并發積） 若[P1]和[P2]是WMIA，[P1]的[I1∪O1]記為[A1]，[P2]的[I2∪O2]記為[A2]，如果[A1∩A2=（I1∩O2）∪（O1∩I2）]，則我們稱[P1]和[P2]是可結合的。對于這些可結合的WMIA，我們給出并發積[P1?P2]的定義為：[P1?P2=defP1×P2，I，O，→，?，T]，其中[I1∪I2＼O1∪O2]，[O1∪O2＼I1∪I2]，并且轉換關系[→]和[?]滿足以下條件：

（Must1）? 如果[p1a，W*P'1]且[a?A2]，

則[p1，p2a，W*P'1×{p2}]；

（Must2）? 如果[p2a，V*P'2]且[a?A1]，

則[p1，p2a，V*{p1}×P'2]；

（May1）? 如果[p1--→α，Wp'1]且[α?A2]，

則[p1，p2--→α，Wp'1，p2]；

（May2）? 如果[p2--→α，Vp'2]且[α?A1]，

則[p1，p2--→α，Vp1，p'2]；

（May3）? 如果[p1--→α，Wp'1]，[p2--→α，Vp'2]且[W∩V≠?]，

則[p1，p2--→τp'1，p'2]。

可以看出，在[p1，p2--→τ]的情況下，我們需要權重間隔[W∩V]不能為空，否則它們不能交互。因此，對于[p1--→α，Wp'1]，[p2--→α，Vp'2]但[W∩V=?]的情況，我們認為它是（May1）和（May2）在[α∈A1]且[α∈A2]時的特殊情況，這種情況下的[p1]和[p2]雖然是不能交互的，即不能產生內部動作[τ]，但卻仍能進行并發操作，因此我們以為此種情況不屬于不一致狀態。現在我們刪除不一致狀態得到WMIA的定義。

定義7（WMIA的并發） 給定一個并發積[P1?P2]，對于[a∈A1∩A2]，那么[p1，p2]被認為是一個錯誤狀態應當滿足下列幾種情況之一：

⑴ 如果[a∈O1]，[p1--→a]且[p2?a]；

⑵ 如果[a∈O2]，[p2--→a]且[p1?a]。

進一步，我們定義并發積[P1?P2]的不一致狀態[E]為滿足以下條件之一的[p1，p2∈E]的最小集合：

（i） [p1，p2]是一個錯誤狀態；

（ii） 對于[α∈O∪τ]，[p1，p2--→αp'1，p'2]，且[p'1，p'2∈E]。

[P1]和[P2]的并發操作[P1|P2]是通過刪除[P1?P2]中的所有的不一致狀態[E]得到的。其中的所有的不一致狀態包括轉換關系都需要刪除，并且所有必須轉換下的可能轉換也都要刪除。此時，如果[p1，p2∈P1|P2]，我們稱[p1]和[p2]是協調的，寫作[p1|p2]。

在WMIA的并發算子定義中，我們沒有考慮[τ]動作的必須轉換關系，因為它與精化關系無關。類似于合取算子和析取算子的同余性定理，對于并發的同余性，我們也應有以下定理。

定理3 令[P1]，[P2]和[Q1]是WMIA，[p1∈P1]，[p2∈P2]，[q1∈Q1]并且[p1?WMIAq1]。如果[P2]和[Q1]是可結合的，那么：

⑴ [P1]和[P2]是可結合的；

⑵ 如果[p2]和[q1]是協調的，那么[p1]和[p2]也是協調的并且[p1|p2?WMIAq1|p2]。

4 結束語

為了對轉換系統進行定量研究，本文提出了一種加權模態接口自動機，給出了加權模態接口自動機的定義和精化關系。并且針對合取、析取、并發等邏輯與操作算子給出了SOS語義，并探討了這些算子關于精化關系的同余性定理，由于篇幅的限制，我們并沒有給出證明過程，因此在未來的工作中，我們將給出這些證明過程以及加權模態接口自動機的邏輯特征。

在實際系統中，資源消耗并不局限于權重區間的包含關系，限于篇幅，本文也并未討論一般情況下的權重區間。在未來的工作中，我們將用近似等價理論來考慮一般情況下的權重區間，并進一步給出相關操作語義，并探討這些算子關于近似等價關系的同余性問題。

參考文獻（References）：

[1] Alfaro L D， Henzinger T A. Interface automata[J]. ACM

SIGSOFT Software Engineering Notes， 2001，26（5）：109-120

[2] Larsen K G， Legay A. Quantitative modal transition systems

[C]//International Workshop on Algebraic Development Techniques. Springer， Berlin， Heidelberg，2012：50-58

[3] G L ?uttgen， Vogler W. Modal Interface Automata. Logical

Methods in Computerence，2012，9（3）

[4] Bujtor F， Fendrich S， Lüttgen G， et al. Nondeterministic

modal interfaces[J]. Theoretical Computer Science，2016，642：24-53

[5] Raclet J B， Badouel E， Benveniste A， et al. A modal

interface theory for component-based design[J]. FundamentaInformaticae，2011，108（1-2）：119-149

[6] Bauer S S， Mayer P， Schroeder A， et al. On weak modal

compatibility， refinement， and the MIO Workbench[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer， Berlin， Heidelberg，2010：175-189

[7] Larsen K G，? Nyman U，? Wsowski A. Modal I/O automata

for interface and product line theories[C]//European Symposium on Programming.Springer，Berlin，Heidelberg，2007

[8] Bujtor F， Vogler W. ACTL for modal interface automata.

Theoretical ComputerScience，2017，693

[9] Manfred Droste， Paul Gastin， Manfred Droste， et al.

Weighted Automata andWeighted Logics. Handbook of Weighted Automata：175-211（2007）

[10] Juhl L， Larsen K G， Srba J. Modal Transition Systems

with Weight Intervals. TheJournal of Logic and Algebraic Programming，2012，81（4）：408-421

[11] Antonik A， Huth M， Larsen K， et al. 20 Years of Mixed

and Modal Specifications[J]. 2008

[12] K.G. Larsen， B. Thomsen， A modal process logic， in：

Proceedings of the 3rd Annual Symposium on Logic in Computer Science （LICS88）， IEEE Computer Society，1988：203-210

[13] Buchholz P. Bisimulation relations for weighted

automata.Theoretical ComputerScience，2008，393（1-3）：109-123