Timed Automata New Recognition Model And The Automata Of The Long Span Area

In the use of classical u ?finite automata for system verification , the decision to abstract away from time properties is not adaptive when reasoning about systems that must interactive with physical processes. By adding time properties to classicl - finite automata, timed automata hold the behavior of the real time system, offer the solution to verification for finite control real time system and certain timing delay question. It is an effective tool to model and verify the concurrent real time systems, and is widely used in many fields such as temporal logic, Petri net, protocol verification and circuit verification. An important aspect of the theory of automata is the power of timed automata that recognizing timed languages with respect to recognizing conditions and the closure properties of timed language under boolean operations. Different recognizing conditions decide different recognizing models. Now only recognizing conditions including C1,C5, C3,E,l,L are discussed. This paper suggests and profoundly discusses timed automata model under other four types of classical recognizing conditions, i. e C2, C3, C4, C6, and new conditions obtained from the negation of C (i=l~6). The key step to real time verification in the use of timed automata is the construction of region automata. The disadvantages of classical region automata are: Limiting the clock constants to ratinal numbers is unreasonable; the divisions of clock region are too small to precisely correspond to the timed automata. This paper suggests a new region automata: wide-pan automata, which allows clock constants of real type and expands the time span of clock regions. Thus we can simplify the construction process, get a better time complexity and greatly promote the efficiency of verification.