Approximate Bisimulation and Its Applications for Polynomial Algebraic System Based on Symbolic and Numerical Calculation

摘要

In this paper, a concept of approximate bisimulation is proposed by symbolic computation for polynomial algebraic system and its approximate abstraction based on the common forms of their zeros. With using this idea for original system, on the one side, some extra nondeterministic branches are removed to achieve structure reduction. On the other hand, behavior reduction is achieved by choosing simple expression to replace its complex approximate equivalent expression. In addition, with symbolic and numerical hybrid computation, the error caused by approximate definition is computed and controlled. Based on our approach, the properties of deadlock and safety are proved to be maintainable. Finally, the results of the properties verification of simpler abstraction are used to determine the results of the same properties for original system. This method is applied to slow state explosion and decrease computing effort. The application of our framework is demonstrated on a program.