https://scholars.lib.ntu.edu.tw/handle/123456789/497109
標題: | Efficient Verification of Timed Automata with BDD-Like Data-Structures. | 作者: | FARN WANG | 關鍵字: | BDD; Data-structures; Model-checking; Timed automata; Verification | 公開日期: | 2003 | 起(迄)頁: | 189-205 | 來源出版物: | Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings | 摘要: | We investigate the efficiency of BDD-like data-structures for timed automata verification. We find that the efficiency is highly sensitive to the variable designs and canonical form definitions. We explore the two issues in details and propose to use CRD (Clock-Restriction Diagram) for timed automata state-space representation. We compare two canonical forms for zones, develop a procedure for quick zone-containment detection, and discuss the effect of variable-ordering of CRD. We implement our idea in our tool red 4.1 and carry out experiments to compare with other tools and red's previous version in both forward and backward analysis. © Springer-Verlag Berlin Heidelberg 2003. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-35248884302&doi=10.1007%2f3-540-36384-x_17&partnerID=40&md5=1d8cf1e2c22bfb8d3f45bd49e0b04f1d | ISSN: | 03029743 | DOI: | 10.1007/3-540-36384-X_17 | SDG/關鍵字: | Automata theory; Boolean functions; Data structures; Efficiency; State space methods; Verification; BDD; Canonical form; Forward-and-backward; State space representation; Timed Automata; Variable order; Model checking |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。