| property checking for 1-place-unbounded petri nets | |
| Wang Yunhe; Jiang Bo; Jiao Li | |
| 2010 | |
| 会议名称 | 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010 |
| 会议录名称 | Proceedings - 2010 4th International Symposium on Theoretical Aspects of Software Engineering, TASE 2010 |
| 页码 | 117-125 |
| 会议日期 | August 25, |
| 会议地点 | Taipei, Taiwan |
| 收录类别 | EI |
| 出版地 | United States |
| ISBN | 9780770000000 |
| 部门归属 | (1) State Key Laboratory of Computer Science, Institute of Software, Graduate University of Chinese Academy of Sciences, Beijing, China |
| 摘要 | 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. |
| 关键词 | Graph Theory Petri Nets Software Engineering |
| 主办者 | National Taiwan University; Res. Cent. Inf. Technol. Innov., Acad. Sin.; National Science Council; Ministry of Education; IEEE Computer Society |
| 内容类型 | 会议论文 |
| URI标识 | http://ir.iscas.ac.cn/handle/311060/8862 |
| 专题 | 基础软件与系统重点实验室 |
| 推荐引用方式 GB/T 7714 | Wang Yunhe,Jiang Bo,Jiao Li. property checking for 1-place-unbounded petri nets[C]. United States,2010:117-125. |
| 条目包含的文件 | ||||||
| 文件名称/大小 | 文献类型 | 版本类型 | 开放类型 | 使用许可 | ||
| 05587721.pdf（432KB） | 开放获取 | -- | 请求全文 | |||
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论