Symbolic model checking of finite precision timed automata
文献类型：期刊论文
| 作者 | Yan, RJ; Li, GY; Tang, ZS |
| 刊名 | Theoretical aspects of computing - ictac 2005
 |
| 出版日期 | 2005 |
| 卷号 | 3722页码:272-287 |
| 关键词 | Finite precision timed automata Model checking Symbolic methods |
| ISSN号 | 0302-9743 |
| 通讯作者 | Yan, rj(yrj@ios.ac.cn) |
| 英文摘要 | This paper introduces the notion of finite precision timed automata (fptas) and proposes a data structure to represent its symbolic states. to reduce the state space, fptas only record the integer values of clock variables together with the order of their most recent resets. we provide constraints under which the reachability checking of a timed automaton can be reduced to that of the corresponding fpta, and then present an algorithm for reachability analysis. finally, the paper reports some preliminary experimental results, and analyzes the advantages and disadvantages of the new data structure. |
| WOS关键词 | VERIFICATION ; ALGORITHMS |
| WOS研究方向 | Computer Science |
| WOS类目 | Computer Science, Theory & Methods |
| 语种 | 英语 |
| WOS记录号 | WOS:000233420900018 |
| 出版者 | SPRINGER-VERLAG BERLIN |
| URI标识 | http://www.irgrid.ac.cn/handle/1471x/2377127 |
| 专题 | 中国科学院大学 |
| 通讯作者 | Yan, RJ |
| 作者单位 | 1.Chinese Acad Sci, Comp Sci Lab, Inst Software, Beijing 100080, Peoples R China 2.Chinese Acad Sci, Grad Sch, Beijing 100039, Peoples R China |
| 推荐引用方式 GB/T 7714 | Yan, RJ,Li, GY,Tang, ZS. Symbolic model checking of finite precision timed automata[J]. Theoretical aspects of computing - ictac 2005,2005,3722:272-287. |
| APA | Yan, RJ,Li, GY,&Tang, ZS.(2005).Symbolic model checking of finite precision timed automata.Theoretical aspects of computing - ictac 2005,3722,272-287. |
| MLA | Yan, RJ,et al."Symbolic model checking of finite precision timed automata".Theoretical aspects of computing - ictac 2005 3722(2005):272-287. |
入库方式： iSwitch采集
来源：中国科学院大学
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。