A method to check liveness of WS3PR

Shouguang Wang, Miao Liu, Mengchu Zhou, Wenhui Wu

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


Petri nets are widely used to model flexible manufacturing systems (FMSs) because they can help analyze the properties and synthesize deadlock-free supervisory controllers of FMS. Weighted System of Simple Sequential Processes with Resources (WS3PR) is an important subclass of Petri nets that can well model many FMSs. This work first gives new algorithms to check liveness for a WS3PR net via its subnet trees and structure. Then the computation complexity for the proposed method is shown in this paper, to be polynomial under certain limitations. Finally, sufficient conditions for deciding liveness of a WS3PR are established. An example is used to illustrate the results.

Original languageEnglish (US)
Title of host publicationProceedings of the 33rd Chinese Control Conference, CCC 2014
EditorsShengyuan Xu, Qianchuan Zhao
PublisherIEEE Computer Society
Number of pages6
ISBN (Electronic)9789881563842
StatePublished - Sep 11 2014
EventProceedings of the 33rd Chinese Control Conference, CCC 2014 - Nanjing, China
Duration: Jul 28 2014Jul 30 2014

Publication series

NameProceedings of the 33rd Chinese Control Conference, CCC 2014
ISSN (Print)1934-1768
ISSN (Electronic)2161-2927


OtherProceedings of the 33rd Chinese Control Conference, CCC 2014

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Control and Systems Engineering
  • Applied Mathematics
  • Modeling and Simulation


  • Liveness
  • Petri net
  • deadlock
  • flexible manufacturing system


Dive into the research topics of 'A method to check liveness of WS3PR'. Together they form a unique fingerprint.

Cite this