Full Trace Equivalence Methods Between Specifications of Concurrent Systems

摘要

The present invention relates to a method for checking complete trace equivalence between the specifications of two parallel systems only when the size of the action set is one. In order to achieve the present invention, by generating a characteristic polynomial for the starting state of each specification of two parallel systems, and comparing each of the feature functions to be the same, it is possible to check whether the two specifications are completely trace equivalents. It is. As described above, in the present invention, an efficient equivalence test is performed by using a method of representing a polynomial function through two arrays. Therefore, the present invention checks the full trace equivalence between two specifications within a square time when the size of the action set used in a given system specification is one.