Paper Info
Title
Improvements for the Symbolic Verification of Timed Automata
Abstract
Based on the equivalence relation for location based reachability between continuous and integer semantics of closed timed automata, Beyer et al. have implemented the verifier Rabbit, with the uniform representation of reachable configurations. However, the growth of maximal constant of clock variables will decline the performance of Rabbit. The paper proposes an improved symbolic method, using binary decision diagrams (BDDs) to store the symbolic representation of discretized states, for the verification of timed systems. Compared with Rabbit, experiments demonstrate that besides the memory reduction, our implementation is also less sensitive to the size of clock domain.
Year
DOI
Venue
2007
10.1007/978-3-540-73196-2_13
FORTE
Keywords
Field
DocType
symbolic representation,binary decision diagram,verifier rabbit,uniform representation,symbolic verification,equivalence relation,clock variable,improved symbolic method,discretized state,clock domain,timed automata,integer semantics,symbolic method,verification
Integer,Equivalence relation,Computer science,Automaton,Binary decision diagram,Reachability,Theoretical computer science,Timed automaton,Symbolic method,Symbolic trajectory evaluation
Conference
Volume
ISSN
Citations 
4574
0302-9743
0
PageRank 
References 
Authors
0.34
17
4
Name
Order
Citations
PageRank
Rongjie Yan19917.81
Guangyuan Li2567.19
Wenliang Zhang300.34
Yunquan Peng400.34