楊弘博，呂 鵬，殷 翔*，李少遠(yuǎn)

(1.上海交通大學(xué)電子信息與電氣工程學(xué)院，上海201100；2.上海交通大學(xué)自動(dòng)化研究所，上海200030)

離散事件動(dòng)態(tài)系統(tǒng)(discrete-event dynamic system,DEDS)被廣泛應(yīng)用在邏輯任務(wù)和離散對象的建模上[1-3].為了約束DEDS，使其適應(yīng)復(fù)雜任務(wù)的要求，Ramadge等[4]提出了監(jiān)控理論(supervisory control theory,SCT).SCT是一種可證明的DEDS控制器綜合形式化方法，本質(zhì)上通過邏輯反饋使得受控DEDS的邏輯正確.此后SCT得到了廣泛發(fā)展，如Lin等[5]和Rudie等[6]研究了DEDS的可觀測性，Ushio等[7]和Yin等[8]研究了具有非確定輸出函數(shù)的米利自動(dòng)機(jī)監(jiān)控問題.隨著研究的不斷深入，SCT在工業(yè)[9]、交通運(yùn)輸[10]和醫(yī)療行業(yè)[11]等眾多領(lǐng)域得到了廣泛的應(yīng)用.

對DEDS的表征進(jìn)行控制有著重要的現(xiàn)實(shí)意義.其中“表征”定義在系統(tǒng)事件上，是事件的函數(shù).它既可以是真實(shí)的輸出，也可以是虛擬的屬性，稱之為系統(tǒng)的“輸出”.比如在故障檢測問題中，輸出可以建模表達(dá)相關(guān)儀表的讀數(shù).然而DEDS的事件主要用于刻畫系統(tǒng)的內(nèi)部行為，且現(xiàn)有SCT主要也研究系統(tǒng)內(nèi)部行為本身是否符合某些事件序列組成的規(guī)約，無法按照由事件的函數(shù)組成的規(guī)約實(shí)現(xiàn)控制.所以，為了研究離散事件動(dòng)態(tài)系統(tǒng)表征的行為，同時(shí)對經(jīng)典監(jiān)控理論做出進(jìn)一步的抽象，需要在系統(tǒng)的輸出層面上定義一種新的問題，即對系統(tǒng)輸出進(jìn)行控制，而非對系統(tǒng)內(nèi)部的原始行為進(jìn)行控制，稱這種控制問題為DEDS的輸出調(diào)節(jié)(output regulation,OR).

目前OR在現(xiàn)代控制理論中已經(jīng)被廣泛研究[12-14]，但關(guān)于DEDS的文獻(xiàn)中尚沒有涉及這類問題.在已有的SCT文章中，控制目標(biāo)都是基于系統(tǒng)內(nèi)部行為設(shè)計(jì)的，而非基于輸出行為.例如文獻(xiàn)[7]中，盡管引入了輸出，但考慮的是將事件和輸出組合成擴(kuò)展的系統(tǒng)行為.因此文獻(xiàn)[7]中的輸出仍和事件停留在同一層次，同樣值得注意的是, 在SCT中人們研究了DEDS的可觀測性[5-6]，并提出了部分可觀的監(jiān)督控制(partial observed supervisory control,POSC).但POSC和這里提出的OR有所不同.對于前者而言，由于受到傳感器感知精度等因素的制約，監(jiān)控器獲得的信息不完全，但規(guī)約的定義仍是基于系統(tǒng)的原始行為；相較之下，后者則是希望受控系統(tǒng)在信息層面滿足某種特性，其規(guī)約定義在系統(tǒng)事件的輸出上，對于監(jiān)控器沒有特別的限制.

本文將研究系統(tǒng)的OR問題并著重討論輸出的安全性問題，從系統(tǒng)行為和表征的同步關(guān)系入手，給出OR監(jiān)控器的設(shè)計(jì)方法.接著證明上述方法構(gòu)造的監(jiān)控器可以完成OR的控制任務(wù)且是最小約束的.最后本文將舉例說明OR問題在實(shí)際場景中的建模以及監(jiān)控器構(gòu)造算法的有效性.

1 問題定義

1.1 離散事件動(dòng)態(tài)系統(tǒng)建模

考慮以五元組定義的離散事件動(dòng)態(tài)系統(tǒng)

G=(X,Σ,f,Γ,x0),

(1)

1.2 監(jiān)督控制

P(ε)=ε,

(2)

ε∈L(S/G),

[sσ∈L(S/G)]?[sσ∈L(G)]∧[s∈

L(S/G)]∧[σ∈S(P(s))].

(3)

監(jiān)督控制問題通常都會(huì)考慮兩個(gè)問題，即存在性問題(existence problem)和綜合問題(synthesis problem).給定一個(gè)語言集合K,前者要求找到L(S/G)=K嚴(yán)格成立的條件；而后者要求構(gòu)造出一個(gè)監(jiān)控器，使得受控系統(tǒng)的行為滿足L(S/G)?K.在實(shí)際應(yīng)用中，由于受到各種場景約束，要使L(S/G)=K嚴(yán)格成立往往并不容易甚至不可實(shí)現(xiàn)，因此研究可以解決綜合問題的監(jiān)控器構(gòu)造算法更有實(shí)際意義.標(biāo)準(zhǔn)監(jiān)控問題(standard supervisory control problem，SSCP)的數(shù)學(xué)定義如下：

問題1(SSCP) 令G為系統(tǒng)自動(dòng)機(jī)，Σc和Σo分別代表可控事件和可觀事件集合.令規(guī)約K?L(G)是系統(tǒng)語言的非空子集，設(shè)計(jì)監(jiān)控器S:P(L(G))→Γ,使得

1)S是“安全”的，即L(S/G)?K；

2)S是“最小約束”的，即對于任何S′使得L(S′/G)?K,有L(S/G)?L(S′/G).

1.3 OR

本文用原子命題表示事件的輸出，為了描述OR問題，定義事件的輸出函數(shù)如下：M:Σ→Δ∪{ε},其中Δ表示原子命題的集合，ε代表空命題.為了定義事件序列的輸出函數(shù), 對上式進(jìn)行拓展如下：M:Σ*→(Δ∪{ε})*,定義如式(4)所示，其中δ為一個(gè)輸出符號.

(4)

接著對于給定的語言L,記M(L)為語言輸出的集合：

M(L)={M(s):?s∈L}.

(5)

式(4)形式上類似于自然映射函數(shù)的擴(kuò)展.事實(shí)上，輸出函數(shù)和自然映射函數(shù)可以理解為對系統(tǒng)事件的兩個(gè)觀察角度.前者可以認(rèn)為是從系統(tǒng)使用者角度觀察，涉及到OR問題的控制目標(biāo)；而后者則是來自系統(tǒng)內(nèi)部的觀測，監(jiān)控器看到的就是這部分信息.通過將規(guī)約定義在系統(tǒng)輸出上，DEDS的OR問題的數(shù)學(xué)定義如下：

1)S是“輸出安全”的，即M(L(S/G))?K；

2)S是“最小約束”的，即對于任何S′使得M(L(S′/G))?K,有L(S/G)?L(S′/G).

2 輸出調(diào)節(jié)監(jiān)控器的設(shè)計(jì)

經(jīng)過多年的研究，標(biāo)準(zhǔn)監(jiān)控問題已經(jīng)有了成熟的解法[15]，特別是提出了在部分可觀情形下對于多種性質(zhì)的通用解決方式[16].因此，考慮將OR問題轉(zhuǎn)化為SSCP，進(jìn)而構(gòu)造解決OR問題的監(jiān)控器.下面介紹的監(jiān)控器構(gòu)造方法將會(huì)在第3節(jié)中給出證明.

考慮輸出規(guī)約K和動(dòng)態(tài)系統(tǒng)G=(XG,ΣG,fG,ΓG,x0,G),如果原系統(tǒng)G不滿足M(L(G))?K,就需要構(gòu)造一個(gè)監(jiān)控器S,使得受控系統(tǒng)S/G在規(guī)約K下是輸出安全的，即M(L(S/G))?K.將規(guī)約K用自動(dòng)機(jī)的形式表達(dá)，記為規(guī)約自動(dòng)機(jī)H=(XH,Δ∪{ε},fH,ΓH,x0,H),s.t.L(H)=K.算法1將基于自動(dòng)機(jī)G,H構(gòu)造一個(gè)在其狀態(tài)中嵌入了“輸出安全”性質(zhì)的自動(dòng)機(jī)Gs,進(jìn)而得到作用于系統(tǒng)事件本身的新規(guī)約K′.

為了捕捉自動(dòng)機(jī)中符合輸出安全性質(zhì)的事件序列，算法需要使用新的組合運(yùn)算.與傳統(tǒng)的并行組合(parallel composition)運(yùn)算類似，這種新運(yùn)算也是基于自動(dòng)機(jī)的同步關(guān)系，但研究的對象變成了同一系統(tǒng)的行為及其輸出.相較于并行組合，新運(yùn)算有兩個(gè)特點(diǎn)：一是兩個(gè)自動(dòng)機(jī)的事件集不同，確切地說，第二個(gè)自動(dòng)機(jī)H的事件集是第一個(gè)自動(dòng)機(jī)G的輸出集合；二是運(yùn)算只完全遍歷第一個(gè)自動(dòng)機(jī)G,另一個(gè)自動(dòng)機(jī)H跟隨它運(yùn)行.即在遍歷G時(shí)若發(fā)生事件e,那么H將轉(zhuǎn)移至發(fā)生M(e)之后的狀態(tài).結(jié)合這些特點(diǎn)，稱這種運(yùn)算為“基于映射的并行組合(mapping-based parallel composition,MBPC)”.

定義1(MBPC)定義關(guān)于自動(dòng)機(jī)的二元運(yùn)算，記作‖M.考慮將離散動(dòng)態(tài)系統(tǒng)建模成自動(dòng)機(jī)G=(XG,ΣG,fG,ΓG,x0,G)；將規(guī)約K用自動(dòng)機(jī)的形式表達(dá)，記為規(guī)約自動(dòng)機(jī)H=(XH,Δ∪{ε},fH,ΓH,x0,H),s.t.L(H)=K.它們的MBPC定義為

G‖MH=(XMP,ΣMP,fMP,ΓMP,x0,MP)，

(6)

其中XMP?XG×XH為自動(dòng)機(jī)G‖MH的狀態(tài)集合；組合系統(tǒng)G‖MH的事件集合ΣMP=ΣG,與G的事件集合保持一致；組合系統(tǒng)的轉(zhuǎn)移函數(shù)fMP定義為

fMP((x1,x2),e)=

(7)

因此當(dāng)組合系統(tǒng)處于狀態(tài)xMP=(x1,x2)時(shí)，可能發(fā)生的事件集合為ΓMP(xMP)=ΓG(x1)；組合系統(tǒng)的初始狀態(tài)x0,MP=(x0,G,x0,H)∈XM.

在傳統(tǒng)的并行組合中，兩個(gè)系統(tǒng)除了在公共的狀態(tài)下運(yùn)行外，還能在各自獨(dú)有的狀態(tài)集合中運(yùn)行.考慮自動(dòng)機(jī)G的運(yùn)行情況，定義1將[e?ΓG(x1)]∧[M(e)∈ΓH(x2)]涉及的情形列入了“其他”情況.定義1通過系統(tǒng)的行為和表征之間的同步關(guān)系，利用規(guī)約對系統(tǒng)事件本身進(jìn)行了標(biāo)記.基于MBPC運(yùn)算和規(guī)約的轉(zhuǎn)化，下面提出一種OR監(jiān)控器的設(shè)計(jì)算法.

算法1：規(guī)約轉(zhuǎn)化

輸入：

輸出函數(shù)M:Σ→Δ∪{ε}

系統(tǒng)自動(dòng)機(jī)G=(XG,ΣG,fG,ΓG,x0,G)

規(guī)約自動(dòng)機(jī)H=(XH,Δ∪{ε},fH,ΓH,x0,H)

s.t.L(H)=K?M(L(G))

輸出：

新規(guī)約自動(dòng)機(jī)Hs及規(guī)約K′ s.t.K′=L(Hs)

步驟1 構(gòu)造一個(gè)標(biāo)記不安全輸出序列的自動(dòng)機(jī)Ha=(Xa,Δ∪{ε},fa,Γa,x0,a).在規(guī)約自動(dòng)機(jī)H的狀態(tài)集XH中加入狀態(tài)BAD,即Xa=XH∪{BAD},x0,a=x0,H.轉(zhuǎn)移函數(shù)fa定義為

(8)

步驟2 基于MBPC運(yùn)算，構(gòu)造Gs=G‖MHa；

步驟3 在Gs中刪除所有含有BAD分量的狀態(tài)(形如(xs,BAD))，并刪除所有指向這些狀態(tài)的轉(zhuǎn)移邊.記自動(dòng)機(jī)Gs的剩余部分為Hs,代表組合系統(tǒng)中滿足輸出安全要求的事件序列；

步驟4 返回轉(zhuǎn)化后的規(guī)約K′=L(Hs).

根據(jù)算法1的構(gòu)造過程，可以得到轉(zhuǎn)化后規(guī)約K′的數(shù)學(xué)描述如下：

K′={s∈L(G):M(s)∈K},

(9)

算法1通過指數(shù)復(fù)雜度的構(gòu)造，借助MBPC運(yùn)算將OR問題轉(zhuǎn)化為關(guān)于系統(tǒng)G和規(guī)約K′的SSCP.對事件序列的長度應(yīng)用數(shù)學(xué)歸納法容易證明算法1中的兩個(gè)自動(dòng)機(jī)Gs和Hs滿足以下性質(zhì)：

1)L(Gs)=L(G)；

2)L(Hs)?L(G).

基于算法1給出的規(guī)約轉(zhuǎn)化方法，解決OR問題的完整流程如算法2所示：

算法2：輸出調(diào)節(jié)

輸入：

輸出函數(shù)M:Σ→Δ∪{ε}

系統(tǒng)自動(dòng)機(jī)G=(XG,ΣG,fG,ΓG,x0,G)

規(guī)約自動(dòng)機(jī)H=(XH,Δ∪{ε},fH,ΓH,x0,H)

s.t.L(H)=K?M(L(G))

輸出：

最小約束輸出安全監(jiān)控器S*

步驟1 利用算法1推導(dǎo)規(guī)約自動(dòng)機(jī)Hs和規(guī)約K′；

步驟2 針對規(guī)約自動(dòng)機(jī)Hs和系統(tǒng)自動(dòng)機(jī)G應(yīng)用部分可觀監(jiān)控器的生成方法[16]得到最小約束輸出安全監(jiān)控器S*.

3 監(jiān)控器設(shè)計(jì)的正確性

上述算法給出了構(gòu)造OR監(jiān)控器的方法，完成了從OR問題到SSCP的轉(zhuǎn)化.本節(jié)將會(huì)證明監(jiān)控器構(gòu)造方法的正確性.

引理1給定系統(tǒng)自動(dòng)機(jī)G,以及轉(zhuǎn)化前后的規(guī)約K和K′,有

M(L(S/G))?K?L(S/G)?K′.

(10)

證明：(?)假設(shè)M(L(S/G))?K.根據(jù)輸出函數(shù)M的定義(式(5))，?s∈L(S/G),

M(s)∈M(L(S/G))?K,

因此s滿足

s∈L(G),M(s)∈K.

根據(jù)轉(zhuǎn)化后規(guī)約K′=s∈L(G):M(s)∈K(式(9))有s∈K′,進(jìn)而有

M(L(S/G))?K?L(S/G)?K′.

(11)

(?)假設(shè)L(S/G)?K′.?s∈L(S/G)?K′,由式(9)可知M(s)∈K,進(jìn)而有

M(L(S/G))?K?L(S/G)?K′.

(12)

綜合式(11)和(12)，M(L(S/G))?K?L(S/G)?K′.證畢.

定理1對于系統(tǒng)G和監(jiān)控器S*:Σ*→2Σc.S*是使G滿足安全性質(zhì)L(S*/G)?K′的最小約束的監(jiān)控器?S*是使G滿足輸出安全性質(zhì)M(L(S*/G))?K的最小約束監(jiān)控器.

證明首先證明安全性：根據(jù)引理1，L(S*/G)?K′是M(L(S*/G))?K的充要條件.已知S*是使G滿足安全性質(zhì)L(S*/G)?K′的監(jiān)控器，那么S*也是能使G滿足輸出安全性質(zhì)M(L(S*/G))?K的監(jiān)控器，反之亦然.

接著證明最小約束特性：考慮能夠使L(S*/G)?K′和M(L(S*/G))?K都成立的監(jiān)控器S*,在輸出安全的規(guī)約K下，S*對于系統(tǒng)G是最小約束的，當(dāng)且僅當(dāng)在安全性規(guī)約K′下，S*對于系統(tǒng)G是最小約束的.

(?)由反證法，假設(shè)在安全性規(guī)約K′下，S*對于系統(tǒng)G不是最小約束的，即存在一個(gè)不同的S′滿足L(S′/G)?K′,且

L(S*/G)?L(S′/G).

(13)

顯然式(13)與“在輸出安全的規(guī)約K下，S*對于系統(tǒng)G是最小約束的”相矛盾；

(?)由反證法，假設(shè)在輸出安全的規(guī)約K下，S*對于系統(tǒng)G不是最小約束的，即存在一個(gè)不同的S′滿足M(L(S′/G))?K′,且同樣可以得到式(13)，與“在安全性規(guī)約K′下，S*對于系統(tǒng)G是最小約束的”相矛盾.證畢.

4 實(shí)例研究

考慮一個(gè)檢查機(jī)器運(yùn)行狀態(tài)的檢查系統(tǒng)，本節(jié)將通過該實(shí)例來闡述本文算法的具體應(yīng)用過程和應(yīng)用場景.假設(shè)需要不定時(shí)使用一臺(tái)機(jī)器，在使用前為了知道機(jī)器的狀態(tài)是否正常，希望設(shè)計(jì)一個(gè)系統(tǒng)執(zhí)行以下檢查任務(wù)：打開機(jī)器時(shí)，系統(tǒng)提示機(jī)器已開機(jī)，然后給出簡短的狀態(tài)報(bào)告(如“狀態(tài)正?！被颉靶枰獧z修”)，隨后提示“狀態(tài)檢查完成”并結(jié)束檢查過程.

設(shè)這樣的一個(gè)檢查系統(tǒng)G的狀態(tài)集為X={x0,x1,x2,x3,x4,x5},事件集為Σ={a1,a2,b},為了敘述方便，不妨假設(shè)所有事件都是可控可觀的.當(dāng)檢查系統(tǒng)管理下的機(jī)器啟動(dòng)時(shí)，它處于“開機(jī)狀態(tài)”，同時(shí)檢查系統(tǒng)處于初始狀態(tài)x0.當(dāng)檢查系統(tǒng)處于x0時(shí)，期望系統(tǒng)通過事件b聲明機(jī)器已開機(jī)，并轉(zhuǎn)移到狀態(tài)x1,表明機(jī)器處于開機(jī)狀態(tài).隨后依據(jù)機(jī)器的檢查情況，輸出相應(yīng)的結(jié)果信息.如果系統(tǒng)輸出“狀態(tài)正?！保瑒t通過事件a1轉(zhuǎn)移到狀態(tài)x2；如果系統(tǒng)輸出“需要檢修”，則通過事件a2轉(zhuǎn)移到狀態(tài)x3.最后系統(tǒng)提示“狀態(tài)檢查完成”，通過事件b轉(zhuǎn)移到狀態(tài)x4并結(jié)束檢查.值得注意的是，系統(tǒng)在執(zhí)行檢查任務(wù)時(shí)，只有上面描述的事件序列可以認(rèn)為是正常的，由狀態(tài)x4接收.各狀態(tài)發(fā)生的其余事件都會(huì)轉(zhuǎn)移到狀態(tài)x5,表示檢查系統(tǒng)出錯(cuò)了.根據(jù)以上描述，系統(tǒng)可以建模為如圖1所示的有限狀態(tài)自動(dòng)機(jī).

圖1 機(jī)器運(yùn)行狀態(tài)檢查系統(tǒng)Fig.1An machine status checking system

前述的檢查系統(tǒng)需要確保在機(jī)器開機(jī)后依次輸出“初始狀態(tài)”、相應(yīng)的狀態(tài)報(bào)告和“狀態(tài)報(bào)告完成”.該任務(wù)可以用系統(tǒng)輸出的序列來描述.首先在事件集Σ={a1,a2,b}上定義輸出函數(shù)M,M(a1)=a′,M(a2)=a′,M(b)=b′.其中輸出符號b′表示檢查系統(tǒng)輸出指示流程進(jìn)度的信息，如“初始狀態(tài)”或“狀態(tài)報(bào)告完成”；輸出符號a′表示檢查系統(tǒng)輸出了相應(yīng)的狀態(tài)信息，如“狀態(tài)正?！被颉靶枰獧z修”.對于檢查任務(wù)的描述可以表示為對系統(tǒng)輸出的規(guī)約：K={ε,b′,b′a′,b′a′b′}.

因此，針對規(guī)約K,本研究希望為系統(tǒng)G設(shè)計(jì)一個(gè)滿足輸出安全性質(zhì)的最小約束監(jiān)控器S,即針對規(guī)約K和系統(tǒng)G定義OR問題.根據(jù)本文算法，給出該問題的求解過程.

如圖2(a)所示，首先將規(guī)約K描述為一個(gè)自動(dòng)機(jī)H,使得K=L(H).根據(jù)算法1，對標(biāo)記不安全輸出序列的自動(dòng)機(jī)Ha(圖2 (b))和系統(tǒng)自動(dòng)機(jī)G(圖1)應(yīng)用MBPC組合運(yùn)算，得到自動(dòng)機(jī)Gs(圖3(a)).最后，刪除所有被標(biāo)記的狀態(tài)以及指向這些狀態(tài)的轉(zhuǎn)移，得到自動(dòng)機(jī)Hs(圖3 (b))，其對應(yīng)的語言集合K′包含了所有滿足輸出安全性質(zhì)的事件序列.

圖2 算法1中步驟1涉及的自動(dòng)機(jī)Fig.2The involved automatons by applying step 1 of algorithm 1

圖3 隱含了控制前后系統(tǒng)行為信息的自動(dòng)機(jī)Gs和HsFig.3The automatons that embed system behaviors before and after supervisory

由于K′={ε,b,ba1,ba2,ba1b,ba2b},包含了系統(tǒng)G中所有滿足規(guī)約K的事件序列，從而驗(yàn)證了算法1的正確性.接著應(yīng)用算法2中的監(jiān)控器生成算法，即可得到滿足OR所需的監(jiān)控器S*.在本例中，S*與如圖3 (b)所示的自動(dòng)機(jī)Hs具有相同的結(jié)構(gòu).

5 結(jié) 論

為了方便實(shí)際應(yīng)用中對離散動(dòng)態(tài)系統(tǒng)表征的研究，本文在DEDS的理論框架下提出了OR問題的概念并給出了嚴(yán)格的數(shù)學(xué)描述.基于系統(tǒng)行為和輸出規(guī)約的同步關(guān)系，定義了一種新的組合運(yùn)算以求解OR問題，并在此基礎(chǔ)上實(shí)現(xiàn)了由OR問題向SSCP的轉(zhuǎn)化，通過求解SSCP實(shí)現(xiàn)了原OR問題的求解.最后，本文證明了OR監(jiān)控器設(shè)計(jì)算法的正確性，并通過機(jī)器狀態(tài)檢查系統(tǒng)的實(shí)例闡述了本文算法的具體應(yīng)用過程.