Boundedness of adaptive nets is decidable

Boundedness is a relevant property for adaptive systems: creation, composition and destruction of components at runtime introduce different infiniteness dimensions. In this paper we show the decidability of the boundedness for adaptive nets, a subclass of nested nets enhanced with subprocess composition.     

Soundness-preserving reduction rules for reset workflow nets

The application of reduction rules to any Petri net may assist in its analysis as its reduced version may be significantly smaller while still retaining the original net’s essential properties. Reset nets extend Petri nets with the concept of a reset arc, allowing one to remove all tokens from a certain place. Such nets have a natural application in business process modelling where possible cancellation of activities need to be modelled explicitly and in workflow management where such process models with cancellation behaviours should be enacted correctly. As cancelling the entire workflow or even cancelling certain activities in a workflow has serious implications during execution (for instance, a workflow can deadlock because of cancellation), such workflows should be thoroughly tested before deployment. However, verification of large workflows with cancellation behaviour is time consuming and can become intractable due to the state space explosion problem. One way of speeding up verification of workflows based on reset nets is to apply reduction rules. Even though reduction rules exist for Petri nets and some of its subclasses and extensions, there are no documented reduction rules for reset nets. This paper systematically presents such reduction rules. Because we want to apply the results to the workflow domain, this paper focusses on reset workflow nets (RWF-nets), i.e. a subclass tailored to the modelling of workflows. The approach has been implemented in the context of the workflow system YAWL.     

基于Petri网的工作流模型简化

计算状态空间可达图是验证工作流正确性的主要方法,状态空间爆炸是这类方法的主要困难.文章对线性时态逻辑LTL-x描述的正确性提出了一种基于Petri网图形化简的验证方法,证明了所提出化简规则的完备性,并以实例说明了所提方法的有效性.     

The relationship between workflow graphs and free-choice workflow nets

Workflow graphs represent the main control-flow constructs of industrial process modeling languages such as BPMN, EPC and UML activity diagrams, whereas free-choice workflow nets are a well understood class of Petri nets that possesses many efficient analysis techniques. In this paper, we provide new results on the translation between workflow graphs and free-choice workflow nets.We distinguish workflow graphs with and without inclusive Or-logic. For workflow graphs without inclusive logic, we show that workflow graphs and free-choice workflow nets are essentially the same thing. More precisely, each workflow graph and each free-choice workflow net can be brought into an equivalent normal form such that the normal forms are, in some sense, isomorphic. This result gives rise to a translation from arbitrary free-choice workflow nets to workflow graphs.For workflow graphs with inclusive logic, we provide various techniques to replace inclusive Or-joins by subgraphs without inclusive logic, thus giving rise to translations from workflow graphs to free-choice nets. Additionally, we characterize the applicability of these replacements. Finally, we also display a simple workflow graph with an inclusive Or-join, which, in some sense, cannot be replaced. This shows a limitation of translating inclusive logic into free-choice nets and illustrates also a difficulty of translating inclusive logic into general Petri nets.     

A method of workflow scheduling based on colored Petri nets

Effective methods of workflow scheduling can improve the performance of workflow systems. Based on the study of existing scheduling methods, a method of workflow scheduling, called phased method, is proposed. This method is based on colored Petri nets. Activities of workflows are divided into several groups to be scheduled in different phases using this method. Details of the method are discussed. Experimental results show that the proposed method can deal with the uncertainties and the dynamic circumstances very well and a satisfactory balance can be achieved between static global optimization and dynamic local optimization.     

A valuation-based analysis of conflict-free Petri nets

We propose a novel valuation-based approach for analyzing conflict-free Petri nets. The basic idea is to associate a natural number, called the valuation, to each marking in the Petri net. If the set of markings of zero valuation is forward closed, then the valuation along any Petri net computation is nonincreasing, and in many cases, has the tendency to move towards zero valuation. Using the valuation-based method, we demonstrate a number of problems for conflict-free Petri nets to be decidable.     

基于Petri网的稿件处理工作流模型

稿件处理流程是一个部分自动执行的业务过程。通过对稿件处理工作流实际应用环境的分析,提出了一个相对完整的基于Petri网的工作流模型,并给出了该模型的完整性验证。     

Verification of workflow nets with transition conditions

Workflow management is concerned with automated support for business processes.Workflow management systems are driven by process models specifying the tasks that need to be executed,the order in which they can be executed,which resources are authorised to perform which tasks,and data that is required for,and produced by,these tasks.As workflow instances may run over a sustained period of time,it is important that workflow specifications be checked before they are deployed.Workflow verification is usually concerned with control-flow dependencies only;however,transition conditions based on data may further restrict possible choices between tasks.In this paper we extend workflow nets where transitions have concrete conditions associated with them,called WTC-nets.We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies,are actually possible when considering the conditions based on data.Thus,we are able to more accurately determine at design time whether a workflow net with transition conditions is sound.     

基于Petri网的工作流层次模型及结构分析

在对工作流网络理论研究的前提下,结合企业业务流程建模的应用特点,提出了几种将工作流网络分层的思想,并着重介绍了将继承特性用于Petri网建模的方法。     

The finiteness of synchronous,tabled picture languages is decidable

In the present paper, synchronous, tabled chain code picture systems based on Lindenmayer systems (sT0L system) are studied with respect to the finiteness of their picture languages. The finiteness is proved to be decidable. Additionally, a method is given for deciding whether or not an sT0L system generates a finite picture language.     

Agent-based workflow management systems (WfMSs)

Workflow management systems (WfMSs) based on agent technology can cope with the rapidly evolving business environment better than most other systems as they are more flexible and open. In this paper we describe a possible architecture of such a system by means of our prototype WfMS called JBees. The combination of collaborating agents and the Coloured Petri Net (CPN)-formalism in JBees enables a flexible and adaptive system with the possibility of simulation, analysis, and monitoring of the process execution in order to identify potential inconsistencies and to provide appropriate information to the workflow administrator for the purpose of the process improvement.     

On the relationship between workflow models and document types

The best practice in information system development is to model the business processes that have to be supported and the database of the information system separately. This is inefficient because they are closely related. Therefore we present a framework in which it is possible to derive one from the other. To this end we introduce a special class of Petri nets, called Jackson nets, to model the business processes, and a document type, called Jackson types, to model the database. We show that there is a one-to-one correspondence between Jackson nets and Jackson types. We illustrate the use of the framework by an example.     

Classification and evaluation of timed running schemas for workflow based on process mining

The system running logs of a workflow contain much information about the behavior and logical structure between activities. In this paper, a mining approach is proposed to discover the structural and temporal model for a workflow from its timed running logs. The mining results are represented in the formalized form of Petri nets extended with two timing factors that allows validation or verification the actual behaviors, especially the temporal constraints between activities. According to the reachability graph of the extended Petri net model mined, all running schemas of a workflow can be generated, which defines the temporal constraints between running activities. By calculating the earliest and latest start time of each activity, the earliest starting and latest existing time of each state in the running schema can be determined. Based on the temporal relations between the timing factors of each running state, the running schemas can be classified into six classes. The effects of the six classes of running schemas on the implementation of the whole workflow are evaluated so as to obtain the best one that can ensure the workflow is finished in the shortest time. The standards for the ideal, reliable and favorable running schemas and their existence conditions are discussed, which can be used to evaluate the running logs and control the future running of a workflow.     

基于Petri网的工作流模型的分析

通过模型分析发现所描述的过程定义中的设计错误,以便对业务过程重构提供正确的指导和科学的依据。首先将信牌驱模型转化为Petri网,接着将Petri网进行必要化简,最后对化简后的Petri网进行死锁等分析。     

DFL: A dataflow language based on Petri nets and nested relational calculus

In this paper we propose DFL—a formal, graphical workflow language for dataflows, i.e., workflows where large amounts of complex data are manipulated, and the structure of the manipulated data is reflected in the structure of the workflow. It is a common extension of (1) Petri nets, which are responsible for the organization of the processing tasks, and (2) nested relational calculus, which is a database query language over complex objects, and is responsible for handling collections of data items (in particular, for iteration) and for the typing system. We demonstrate that dataflows constructed in a hierarchical manner, according to a set of refinement rules we propose, are semi-sound, i.e., initiated with a single token (which may represent a complex scientific data collection) in the input node, terminate with a single token in the output node (which represents the output data collection). In particular they never leave any “debris data” behind and an output is always eventually computed regardless of how the computation proceeds.     

aH算法:工作流挖掘中一种能挖掘隐含任务的扩展a算法

正确发现流程实际运作情况对工作流管理有着重要的意义。工作流挖掘抽取系统日志信息,挖掘流程的真实运作模型。其中挖掘隐含任务是工作流挖掘中待研究问题之一。基于a算法,提出了能挖掘隐含任务的挖掘算法aH。分析了隐含任务出现的可能情况,通过判断并行任务的位置关系,往工作流网中添加隐含任务;然后合并相同的隐含任务,去掉冗余隐含任务,以完善结果模型。实现了。算法原型,实验证实了方法的可行性及有效性,并分析了方法的不足之处。     

Decomposition of Petri nets

The problem of splitting any given Petri net into functional subnets is considered. The properties of functional subnets and sets that induce them are investigated. An algorithm of polynomial complexity is constructed for decomposition of nets.Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 131–140, September–October 2004.     

Compositional analysis of Petri nets

Foundations of compositional analysis of Petri nets are presented. This analysis consist of the determination of properties of a given Petri net from the properties of its functional subnets. Compositional analysis covers the investigation of behavioral and structural properties of Petri nets with the help of matrix methods that use fundamental equations and invariants. The exponential acceleration of computations as a function of the dimensionality of a net is obtained. __________ Translated from Kibernetika i Sistemnyi Analiz, No. 1, pp. 143–154, January–February 2006.     

工作流模型正确性验证过程中的模型简化问题

将工作流概念映射到Petri网后得到的工作流网的合理性验证过程比较复杂,容易出现状态空间爆炸的问题,需要对工作流模型进行简化。文章将工作流模型的简化过程分为两个步骤,首先将工作流模型转化为经典Petri网,再对经典Petri网进行简化。对于自由选择网可以采用自由选择语义的规约方法进行简化,而对于非自由选择网可以结合自由选择语义的规约方法和标准的Petri网简化方法进行简化。