https://scholars.lib.ntu.edu.tw/handle/123456789/497109
Title: | Efficient Verification of Timed Automata with BDD-Like Data-Structures. | Authors: | FARN WANG | Keywords: | BDD; Data-structures; Model-checking; Timed automata; Verification | Issue Date: | 2003 | Start page/Pages: | 189-205 | Source: | Verification, Model Checking, and Abstract Interpretation, 4th International Conference, VMCAI 2003, New York, NY, USA, January 9-11, 2002, Proceedings | Abstract: | 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/Keyword: | 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 |
Appears in Collections: | 電機工程學系 |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.