交互式Petri网及其兼容性研究

Web service and inter-organizational workflow are widely studied and applied in academic and industrial systems. These systems can be viewed as a collection of subsystems that interact with each other via a set of message channels. We define a subclass of Petri nets called Interactive Petri Nets (IPN) to model these systems, and classify compatiblity into four levels (i.e., L0-, L1-, L2-, L3-compatibility) to reflect different cooperating ability among subsystems. We have proven that the L3-compatibility is equavilent to the liveness and boundedness, but is co-NP-hard. From three aspects (i.e., execution logics, output of message channels, and external enabled condition of events) we present 16 subclasses of IPNs which have different structural characteristics. The purpose of this classification is to explore the conditions of deciding and controlling compatibility for each subclass based on its own structure. We have proposed sufficient and necessary conditions for the compatibility and liveness of some subclasses. Therefore, this project will continue to research IPNs and their compatibility mainly including: 1) the relationships between compatibility and other properties such as liveness and repetitiveness; 2) the net-structure-based conditions for the compatibility of other subclasses; 3) the control problem on compatibility; and 4) the tool of creating and analyzing IPNs.

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网的建模与分析方法。这些研究为交互式系统的建模与行为正确性分析验证提供了有力的支持。