Using time reachability tree logic to specifying and verifying temporal behavior of workflow-net

Chyun Chyi Chen, Yueh Min Huang

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Workflow management has been a hot issue in both academic and industrial research. Deadline assignment is of great significance in workflow management. In order to avoid deadline violation, this paper presents an approach to the schedulability analysis of workflow system modeled in p-time Petri nets by separating timing properties from other behavior properties. The analysis of behavioral properties is conducted based on the reachability graph of the underlying p-Time Petri net, whereas timing constraints are checked in term of absolute and relative firing domains. Our technique is based on a concept called clock-stamped state class (CS-class) and temporal logic. With the reachability graph generated based on CS-class, we can directly compute the end-to-end time delay in workflow execution. We have identified a class of well-structured p-time Petri nets such that their reachability can be easy analyzed and temporal behavior can be easy analyzed by time reachability tree logical.

Original languageEnglish
Title of host publicationComputers and Information Processing Technologies I
PublisherTrans Tech Publications Ltd
Number of pages7
ISBN (Print)9783038351399
Publication statusPublished - 2014

Publication series

NameApplied Mechanics and Materials
ISSN (Print)1660-9336
ISSN (Electronic)1662-7482

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'Using time reachability tree logic to specifying and verifying temporal behavior of workflow-net'. Together they form a unique fingerprint.

Cite this