Institutional Repository
| property checking for 1-place-unbounded petri nets | |
| Wang Yunhe; Jiang Bo; Jiao Li | |
| 2010 | |
| Conference Name | 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010 |
| Source | Proceedings - 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010 |
| Pages | 117-125 |
| Conference Date | August 25, |
| Conference Place | Taipei, Taiwan |
| Indexed Type | EI |
| Publish Place | United States |
| ISBN | 9780770000000 |
| Department | (1) State Key Laboratory of Computer Science, Institute of Software, Graduate University of Chinese Academy of Sciences, Beijing, China |
| English 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. © 2010 IEEE. |
| Keyword | Graph Theory Petri Nets Software Engineering |
| Sponsorship | National Taiwan University; Res. Cent. Inf. Technol. Innov., Acad. Sin.; National Science Council; Ministry of Education; IEEE Computer Society |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/8862 |
| Collection | 基础软件与系统重点实验室 |
| Recommended Citation GB/T 7714 | Wang Yunhe,Jiang Bo,Jiao Li. property checking for 1-place-unbounded petri nets[C]. United States,2010:117-125. |
| Files in This Item: | ||||||
| File Name/Size | DocType | Version | Access | License | ||
| 05587721.pdf（432KB） | 开放获取 | -- | Application Full Text | |||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment