Paper Info
Title
A Refined Algorithm for Reachability Analysis of Updatable Timed Automata
Abstract
Timed automata (TAs) are a widely-used model for formally analyzing real-time systems. Updatable Timed Automata (UTAs), extended from TAs, provide a more flexible way to adjust the value of clock during location switches. The reachability problem of some subclasses of UTAs is decidable. When considering an efficient implementation of these subclasses, the algorithm that is usually used is based on the notion of zones, implemented by Difference Bound Matrices (DBMs). However, similar to that of TAs, the zone-based algorithm is not sound when considering diagonal constraints on clocks, illustrated by a well-known counterexample. This paper proposes a sound zone-based algorithm by introducing extended DBM (EDBM). It refines the standard forward reachability analysis (FRA) algorithm. The correctness of the algorithm is proven and experimental results are given to show the efficiency of the implementation.
Year
DOI
Venue
2015
10.1109/QRS-C.2015.47
QRS Companion
Keywords
Field
DocType
updatable timed automata, reachability algorithm, EDBM, diagonal constraint
Diagonal,Computer science,Correctness,Automaton,Algorithm,Reachability,Decidability,Timed automaton,Reachability problem,Counterexample
Conference
Citations 
PageRank 
References 
2
0.38
8
Authors
4
Name
Order
Citations
PageRank
Bingbing Fang120.38
Guoqiang Li28528.36
Ling Fang331.40
Jianwen Xiang411323.36