《互動式Petri網及其兼容性研究》是依託同濟大學，由劉關俊擔任項目負責人的青年科學基金項目。
基本介紹
- 中文名：互動式Petri網及其兼容性研究
- 項目類別：青年科學基金項目
- 項目負責人：劉關俊
- 依託單位：同濟大學
中文摘要,結題摘要,
中文摘要
Web服務組合與跨組織工作流在學術界與工業界得到廣泛研究與套用，它們在邏輯層可以抽象為一組子系統通過訊息的傳送與接收進行互動協同。提出互動式Petri網（IPN）以模擬這些系統。基於IPN可達性，定義0、1、2、3級兼容性以刻畫子系統間不同的協同能力。給出IPN的平凡拓展網，證明IPN的3級兼容性等價於其平凡拓展網的活和有界性,但其判定是co-NP-難的。從子系統執行邏輯、訊息庫所的輸出以及事件的外部使能條件等三個維度，將IPN分為16個具有不同結構特徵的子類，其目的是針對不同類別研究其基於網結構的兼容性判定與控制。對其中一些子類已給出判定其兼容性、活性的充要條件。在已有工作基礎上繼續研究：IPN的0、1、2級兼容性問題的複雜度，以及與平凡拓展網的性質（如活性、可重複性等）之間的關係；基於網結構判定其他子類兼容性的充要條件；兼容性的控制問題；基於理論成果開發IPN分析軟體。
結題摘要
本項目面向互動式系統，研究了其行為建模與性質分析。主要研究成果有：（1）給出了互動式Petri網模型，用於模擬多主體間的異步互動；兼容性保證主體間互動時即不會出現死鎖，也無活鎖，並且每個系統事件都有機會發生；而弱兼容性只需要求前兩點；（2）證明了互動式Petri網的（弱）兼容性判定問題是PSPACE完全的；針對一些特殊的子類，給出了相關兼容性問題求解的複雜度；（3）提出了T-組件的概念，給出了基於T-組件的判定（弱）兼容性的充要條件，給出了判定算法；（4）定義了一類Petri網（S3PWR）用於模擬多主體間資源共享與分配，提出了結構循環等待的概念，給出了基於結構循環等待的判定死鎖的充分必要條件；同時，理論上證明了這類網系統活性判定問題是PN-難的；（5）發現了外部事件與安全策略對於面向安全的互動式系統的互動式行為的影響，發現經典的語言等價、互模擬等價的概念不能直接用於刻畫面向安全的互動式系統的行為，提出了安全互模擬的概念以表征安全的互動式行為；（6）對Web服務組合、網路攻擊也開展了部分研究，提出了基於邏輯Petri網的建模與分析方法。這些研究為互動式系統的建模與行為正確性分析驗證提供了有力的支持。
