Name
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/TASE.2010.9 | TASE |
Keywords | Field | DocType |
finite form,deadlock freedom,coverability tree,petri nets,trees (mathematics),improved reachability tree,ability tree,unboundedness,reach ability tree,liveness,reachability tree,reachability,reach ability,property checking,1-place-unbounded net,reachable marking,1-place-unbounded petri nets,reachability analysis,petri net,construction industry,solids,manganese | Petri net,Model checking,Computer science,System recovery,Deadlock,Reachability,Theoretical computer science,Construction industry,Software,Liveness | Conference |
ISBN | Citations | PageRank |
978-1-4244-7847-7 | 2 | 0.41 |
References | Authors | |
6 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yunhe Wang | 1 | 8 | 2.11 |
| Bo Jiang | 2 | 59 | 11.86 |
| Li Jiao | 3 | 3 | 3.50 |