｜利用全跨模與覆點擬陣設計自動化工廠的偵查法則

摘要：本文提出擬陣理論來設計自動化工廠的偵查器法則。傳統上，可程式控制器是用來控制自動化工廠的運作。當可程式控制器控制下的工廠出現不正常運作時，經過設計的偵查法則就可用來提供即時的警告訊息。所以如何設計出更好的法則來偵查出可程式控制器掌握下的不正常運作就成為研究上的一大挑戰。本文將可程式控制器與偵查器的數學模式視為擬陣理論裡的對偶關係。特別是可程式控制器的運作可用記號圖表達時，記號圖可視為擬陣理論裡的全跨模。由於全跨模的對偶擬陣為覆點擬陣，所以偵查器運作的數學模式可視為覆點擬陣。由於屬性方程式為隱性的偵查法則，故要實作的偵查法則可由覆點擬陣移除屬性方程式後產生。

Abstract: A matroid-theoretical approach has been proposed for designing the monitor rules of automated factory. In the traditional approach, Programmable Logic Controllers (PLCs) are used to control the operations of a given automated factory. Also monitor rules are designed to offer real-time alert messages once an abnormal operation under the PLCs occurs in the factory. Consequently how to design better rules for monitoring the unexpected operations under the PLCs becomes a research challenge. In this new approach, both the mathematical models of the PLCs and the monitor are treated as a dual relationship in matroid theory. Especially when the operational model under the PLCs is represented as marked graphs, the marked graphs naturally become a strict gammoid in matroid theory. Since the dual matroid of the strict gammoid is transversal matroid, the corresponding monitor model becomes a transversal matroid. Because the attribute equations are implicit and inherent monitor rules, the implemented monitor rules are generated from the transversal matroid after removing its attribute equations.

關鍵詞：自動化工廠、偵查法則、記號圖、全跨模、覆點擬陣、貪心的演算法

Keywords：Automated Factory, Monitor Rules, Marked Graph, Strict Gammoid, Transversal Matroid, Greedy Algorithm

前言
在自動化工廠（Automated Factory）裡，可程式控制器（Programmable Logic Controller, PLC）[2, 10]常用來監控設備的運作，而偵查器（Monitor）[1]則用來偵查可程式控制器是否正常運作。為了能正確的描述可程式控制器與偵查器的行為，兩者皆需要建立數學模式。通常記號圖（Marked Graph）[2]常用來做為可程式控制器的數學模式，而記號圖的不變量計算則用來做為偵查器的數學模式[1]。先前的研究已顯示記號圖與偵查法則（Monitor Rules）具有對偶關係[1]。

在本文中，擬陣理論（Matroid Theory）[8]裡的全跨模（Strict Gammoid）[6]與覆點擬陣（Transversal Matroid）[4, 8]則用來做為解決問題的工具，其設計理念可用圖一來代表。圖一的左邊代表自動化工廠從可程式控制器設計偵查法則的流程，而圖一的右邊代表其擬陣理論的設計流程。換言之，這是利用右邊的設計流程來取代左邊的設計流程。更詳細地說，這是先把記號圖視為有向圖（Digraph）裡從起點集（Initial Vertex Set）[8]至終點集（Final Vertex Set）[8]的徑接（Linking）問題。徑接是指不相交的路徑（Path），而從起點集跨到終點集的模式可用其可能的路徑集合來描述並稱為跨模（Gammoid）[9]。在擬陣理論裡，如果有向圖徑接的可能起點集為該圖全部點的所有部份集合，則稱為全跨模[8]。由於全跨模的對偶擬陣（Dual Matroid）是覆點擬陣，而全跨模的徑接則對應至覆點擬陣的匹配（Matching）[8]。所以在圖一右邊中，覆點擬陣的匹配可以用來設計偵查器的數學模式，而其匹配在扣除屬性方程式（Attribute Equations）[1]後則用來設計偵查法則。