DocumentCode
2346934
Title
Property Checking for 1-Place-Unbounded Petri Nets
Author
Wang, Yunhe ; Jiang, Bo ; Jiao, Li
Author_Institution
State Key Lab. of Comput. Sci., Grad. Univ. of Chinese Acad. of Sci., Beijing, China
fYear
2010
fDate
25-27 Aug. 2010
Firstpage
117
Lastpage
125
Abstract
The reachability tree for an unbounded net system is infinite. By using ω symbol to represent infinitely many markings, coverability tree can provide a finite form. However, with too much information lost, it can not check properties such as reachability, deadlock freedom, liveness, etc. In this paper, an improved reachability tree (IRT for short) is constructed to enrich the ω representation for 1-place-unbounded nets. Based on the tree containing exactly all the reachable markings, an algorithm is proposed to check liveness of the system.
Keywords
Petri nets; reachability analysis; trees (mathematics); 1-place-unbounded Petri nets; coverability tree; property checking; reachability tree; Construction industry; Laboratories; Manganese; Petri nets; Software; Solids; System recovery; Petri nets; improved reachability tree; liveness; reachability; unboundedness;
fLanguage
English
Publisher
ieee
Conference_Titel
Theoretical Aspects of Software Engineering (TASE), 2010 4th IEEE International Symposium on
Conference_Location
Taipei
Print_ISBN
978-1-4244-7847-7
Type
conf
DOI
10.1109/TASE.2010.9
Filename
5587721
Link To Document