Modeling and analysis of real-time cooperative systems using petri nets

Yu Yue Du, Chang Jun Jiang, Meng Chu Zhou

Research output: Contribution to journalArticlepeer-review

78 Scopus citations


The existing formal techniques are not suitable for elegantly modeling passing value indeterminacy and describing batch processing function in real-time cooperative systems. Moreover, the correct behavior of the systems depends on not only the logical correctness of the results obtained through running workflows but also the time of producing them before critical deadlines. For these purposes, this paper proposes an interorganizational logical workflow net (ILWN) for modeling and analyzing real-time cooperative systems based on time Petri nets, workflow techniques, and temporal logic. Through attaching logical expressions to some actions of an ILWN model, the size of the model is reduced. Thus, ILWNs can efficiently mitigate the state explosion problem to some extent. Also, this paper analyzes the soundness of a subclass of ILWNs: The or-restricted ILWNs. A rigorous analysis approach is given based on their static net structures only. The concepts and techniques proposed in this paper are illustrated with a seller-buyer example in electronic commerce.

Original languageEnglish (US)
Pages (from-to)643-654
Number of pages12
JournalIEEE Transactions on Systems, Man, and Cybernetics Part A:Systems and Humans
Issue number5
StatePublished - Sep 2007

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Human-Computer Interaction
  • Electrical and Electronic Engineering
  • Control and Systems Engineering
  • Computer Science Applications


  • Interorganizational workflow
  • Modeling
  • Real-time cooperative system
  • Temporal logic
  • Time Petri net (TPN)
  • Verification
  • Workflow analysis


Dive into the research topics of 'Modeling and analysis of real-time cooperative systems using petri nets'. Together they form a unique fingerprint.

Cite this