黃潤華 張晉津 張君瑤

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

關(guān)鍵詞： 模態(tài)接口自動機(jī)； 量化信息； 精化關(guān)系； 系統(tǒng)算子

中圖分類號：TP301? ? ? ? ? 文獻(xiàn)標(biāo)識碼：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提出了接口自動機(jī)（Interface Automata）來解決軟件和系統(tǒng)工程之間的組件組合問題[1]。Larsen的模態(tài)轉(zhuǎn)換系統(tǒng)（Modal Transformation System）通過一系列改進(jìn)將規(guī)范轉(zhuǎn)化為實(shí)現(xiàn)，并且提供必須轉(zhuǎn)換和可能轉(zhuǎn)換的兩種轉(zhuǎn)換關(guān)系[2]。在文獻(xiàn)[3]中，Gerald Lüttgen和Walter Vogler將接口自動機(jī)嵌入模態(tài)轉(zhuǎn)換系統(tǒng)，提出了模態(tài)接口自動機(jī)（Modal Interface Automaton），它既能滿足輸入的一致性，又可以表達(dá)強(qiáng)制性輸出，他們還修復(fù)了文獻(xiàn)[4]中的缺陷，即精化關(guān)系不是關(guān)于并行運(yùn)算具有同余性的。

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

本文提出了一種加權(quán)模態(tài)接口自動機(jī)（Weighted Modal Interface Automata），作為模態(tài)接口自動機(jī)的擴(kuò)展。它用一系列權(quán)重區(qū)間來修飾每個(gè)轉(zhuǎn)換關(guān)系，這些區(qū)間可以描述資源約束，如時(shí)間、資源、價(jià)格、燃料等消耗。我們還重新定義了加權(quán)模態(tài)接口自動機(jī)的精化關(guān)系，并且定義了三個(gè)系統(tǒng)操作符：合取、析取和并發(fā)。同時(shí)，我們給出精化關(guān)系是關(guān)于這些算子的同余性的定理。

本文第1節(jié)介紹加權(quán)模態(tài)接口自動機(jī)及相關(guān)概念，定義新的精化關(guān)系。在此基礎(chǔ)上，第2節(jié)引入第一個(gè)系統(tǒng)算子——合取操作，并給出精化關(guān)系在合取操作上的同余性定理。第3節(jié)定義了另外兩種系統(tǒng)算子——析取和并發(fā)，也給出精化關(guān)系在這兩種系統(tǒng)算子上的同余性定理。最后第4節(jié)總結(jié)全文并指出未來研究方向。

1 加權(quán)模態(tài)接口自動機(jī)

1.1 基本定義

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

定義1 一個(gè)加權(quán)模態(tài)接口自動機(jī)（WMIA）是一個(gè)六元組[M=Q，I，O，→，?，δ]，其中：

⑴ [Q]是一個(gè)狀態(tài)集合；

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

⑶ [→?Q×（I∪O）×（Q＼?））]表示必須轉(zhuǎn)換關(guān)系；

⑷ [??Q×（I∪O∪{τ}）×Q）]表示可能轉(zhuǎn)換關(guān)系；

⑸ [δ]是一個(gè)由[→∪?]到權(quán)重區(qū)間集[I]的函數(shù)。

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

● 如果[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*]是權(quán)重區(qū)間集合，如果對于任意的[W∈W*]，都存在[V∈V*]使得[W?V]，我們記作[W*≤V*]；

● 令[W*]和[V*]是權(quán)重區(qū)間集合，我們定義：

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

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

可能轉(zhuǎn)換[?]的相關(guān)標(biāo)記可以類似定義。

為了滿足一致性，我們規(guī)定（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）的要求既加入了權(quán)重區(qū)間，又不改變文獻(xiàn)[3]中關(guān)于模態(tài)接口自動機(jī)中的輸入一致性。具體而言，（b）表示如果模態(tài)接口自動機(jī)中的一個(gè)狀態(tài)可以進(jìn)行一個(gè)可能轉(zhuǎn)換到達(dá)一個(gè)后繼狀態(tài)，那么這個(gè)狀態(tài)就可以進(jìn)行必須轉(zhuǎn)換，這能夠保證模態(tài)接口自動機(jī)可以接受所有規(guī)定的輸入；（c）表示對于一個(gè)相同的輸入而言，必須轉(zhuǎn)換能夠到達(dá)相同的后繼狀態(tài)集合。

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

1.2 精化關(guān)系

為了描述規(guī)范間和實(shí)現(xiàn)與規(guī)范間的精化關(guān)系，引入以下定義。我們現(xiàn)在可以定義WMIA的精化關(guān)系，這是MIA上精化關(guān)系的自然擴(kuò)展。從現(xiàn)在起，當(dāng)使用術(shù)語精化關(guān)系時(shí)，我們總是指下面定義的兩個(gè)WMIA之間的模態(tài)精化關(guān)系。

定義2（WMIA精化關(guān)系） 假設(shè)[P=P，I，O，→，?，δ]和[Q=Q，I，O，→，?，δ]是兩個(gè)具有相同輸入輸出集合的WMIA，則[R?P×Q]是一個(gè)[WMIA]精化關(guān)系當(dāng)且僅當(dāng)對于任意的[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]精化關(guān)系[R]使得[p，q∈R]，則稱[p] WMIA-精化了[q]，寫作[p?WMIAq]。進(jìn)一步，如果[p?WMIAq]且[q?WMIAp]，我們稱[p]和[q]是互精化的，記作[p=WMIAq]。

受文獻(xiàn)[13]中關(guān)系定義的啟發(fā)，本文在WMIA允許輸入確定性的基礎(chǔ)上，添加了條件[W?V]來優(yōu)化精化關(guān)系的權(quán)重區(qū)間。因?yàn)橐粋€(gè)狀態(tài)進(jìn)行相同動作的轉(zhuǎn)換不一定只有一個(gè)后繼狀態(tài)，所以我們引入權(quán)重區(qū)間集合[W*]，[V*]的概念表示到達(dá)所有后繼所需權(quán)重的集合，并使用“[≤]”表示區(qū)間集合之間的包含關(guān)系。如果可以用[P]來模擬[Q]的必須轉(zhuǎn)換，并且可以[Q]來模擬[P]的可能轉(zhuǎn)換，我們稱[P]精化了[Q]。從直觀上講，如果[P]精化了[Q]，那么[Q]所消耗的資源量應(yīng)包含[P]所消耗的資源量。

2 三種系統(tǒng)算子——合取

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

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

（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]。

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

定義4（WMIA的合?。?給定一個(gè)合取積[PQ]，則其不一致狀態(tài)[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]中屬于不一致狀態(tài)[F]的狀態(tài)[p，q]，以確保[P∧Q]具有公共的輸入和輸出字母。我們定義[P∧Q]中的元素[p，q]為[p∧q]，其中所有的狀態(tài)都是已定義的且一致的。

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

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

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

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

3 三種系統(tǒng)算子——析取和并發(fā)

3.1 析取算子

在本節(jié)我們繼續(xù)在WMIA上定義第二種系統(tǒng)算子——析取算子，并討論它的性質(zhì)；特別是，對應(yīng)于合取操作，這個(gè)運(yùn)算符應(yīng)該對應(yīng)精化關(guān)系的最小的上界。

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

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

（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]也成立。

類似于合取，我們?nèi)W*]和[V*]的并集作為[p∨q]的權(quán)重區(qū)間，（May1）和（May2）的規(guī)則是為了保證WMIA的輸入確定性，即當(dāng)[α∈I]時(shí)，我們規(guī)定狀態(tài)[p]，[q]都可以做可能的[α]轉(zhuǎn)換。那么到目前為止，我們已經(jīng)為WMIA的析取算子增加了權(quán)重，并且應(yīng)滿足以下定理。

定理2 假設(shè)[P]、[Q]、[R]是WMIA，[p∈P]，[q∈Q]，[r∈R]。那么[p∨q?WMIAr]當(dāng)且僅當(dāng)[p?WMIAr]且[q?WMIAr]。

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

3.2 并發(fā)算子

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

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

（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--→τ]的情況下，我們需要權(quán)重間隔[W∩V]不能為空，否則它們不能交互。因此，對于[p1--→α，Wp'1]，[p2--→α，Vp'2]但[W∩V=?]的情況，我們認(rèn)為它是（May1）和（May2）在[α∈A1]且[α∈A2]時(shí)的特殊情況，這種情況下的[p1]和[p2]雖然是不能交互的，即不能產(chǎn)生內(nèi)部動作[τ]，但卻仍能進(jìn)行并發(fā)操作，因此我們以為此種情況不屬于不一致狀態(tài)?，F(xiàn)在我們刪除不一致狀態(tài)得到WMIA的定義。

定義7（WMIA的并發(fā)） 給定一個(gè)并發(fā)積[P1?P2]，對于[a∈A1∩A2]，那么[p1，p2]被認(rèn)為是一個(gè)錯誤狀態(tài)應(yīng)當(dāng)滿足下列幾種情況之一：

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

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

進(jìn)一步，我們定義并發(fā)積[P1?P2]的不一致狀態(tài)[E]為滿足以下條件之一的[p1，p2∈E]的最小集合：

（i） [p1，p2]是一個(gè)錯誤狀態(tài)；

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

[P1]和[P2]的并發(fā)操作[P1|P2]是通過刪除[P1?P2]中的所有的不一致狀態(tài)[E]得到的。其中的所有的不一致狀態(tài)包括轉(zhuǎn)換關(guān)系都需要刪除，并且所有必須轉(zhuǎn)換下的可能轉(zhuǎn)換也都要刪除。此時(shí)，如果[p1，p2∈P1|P2]，我們稱[p1]和[p2]是協(xié)調(diào)的，寫作[p1|p2]。

在WMIA的并發(fā)算子定義中，我們沒有考慮[τ]動作的必須轉(zhuǎn)換關(guān)系，因?yàn)樗c精化關(guān)系無關(guān)。類似于合取算子和析取算子的同余性定理，對于并發(fā)的同余性，我們也應(yīng)有以下定理。

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

⑴ [P1]和[P2]是可結(jié)合的；

⑵ 如果[p2]和[q1]是協(xié)調(diào)的，那么[p1]和[p2]也是協(xié)調(diào)的并且[p1|p2?WMIAq1|p2]。

4 結(jié)束語

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

在實(shí)際系統(tǒng)中，資源消耗并不局限于權(quán)重區(qū)間的包含關(guān)系，限于篇幅，本文也并未討論一般情況下的權(quán)重區(qū)間。在未來的工作中，我們將用近似等價(jià)理論來考慮一般情況下的權(quán)重區(qū)間，并進(jìn)一步給出相關(guān)操作語義，并探討這些算子關(guān)于近似等價(jià)關(guān)系的同余性問題。

參考文獻(xiàn)（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