出版社：Vilnius University, University of Latvia, Latvia University of Agriculture, Institute of Mathematics and Informatics of University of Latvia
摘要：Verifying correctness of real time systems, reachable states analysis method is amply developed and used. However, this method described in scientific literature cannot avoid the endless increase of reachable state space. This paper presents an equivalent nodes search algorithm enabling to reduce the number of nodes in the reachable states graph. The application of this algorithm allows transforming the graph of the infinite reachable states into the graph with the finite node numbers. An example illustrates the algorithm.
关键词：real time systems; continuous time models; verification; piece-linear aggregate ; formalism
