To search, Click below search items.


All Published Papers Search Service


Constructing the Reaching Region Graph for Timed Automata with PVS


Huaikou Miao, Qingguo Xu


Vol. 6  No. 7  pp. 175-181


Based on our existing works, this paper firstly gives clock region equivalence PVS specification, and then constructs the reachable region graph for a given Timed Automaton (TA) via characterizing some kinds of clock regions, finally analyses the reachable states using the region graph. These works can conveniently analysis some real-time system in the form of TA model. A case study is investigated and the results are satisfying. As a by-product, an error is detected in the region-equivalence definition which is extensively referred in many papers.


Timed Automata, Clock region, Region equivalence, Reachability analysis, PVS