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
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;
Conference_Titel :
Theoretical Aspects of Software Engineering (TASE), 2010 4th IEEE International Symposium on
Conference_Location :
Taipei
Print_ISBN :
978-1-4244-7847-7
DOI :
10.1109/TASE.2010.9
