Constructing the Reaching Region Graph for Timed Automata with PVS
Huaikou Miao, Qingguo Xu · 2006
Summary 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.