Based On The Number Of New Models Of Timed Automata

Timed automata is in the application of real-time system and model checking. It appears many algorithms and tools in practice of verification. On the other hand, various models based on timed automata has been suggested such as timed tree automata and signal automata.The theory of timed tree automata is far from perfect now. The classes of languages and their relationship have been discussed. The paper proposes a condition of timed tree automata recognizing language. We prove the correctness of our conclusion. If a language can not satisfy the condition, it mustn't be accepted by a timed tree automata. It is a potential way to approving a language being a non timed tree regular language.Signal automata is a model rather fit than timed automata for a class of real-time system. But now, it is no algorithm available. This paper prove the relationship of behavior equivalence between timed automata and signal automata, then we proposed a bisimulation algorithm under discrete step. So, the question of system verification based on signal automata is deduced to the same question based on timed automata. There are many much software and tools for the latter. So, it has operability of solving the former.In the engineering of gene network, formal method is used for forecast the behavior of controlling biologic gene network by artificial gene network. The model based on finite state automata has flaws such as poor ability of describing time constraint. In this paper, we suggests a model of gene network based on timed automata , then we gives a way for computing the pathway of network.