REACTIVE SYSTEM SAFETY VERIFICATION DEVICE, METHOD, PROGRAM, AND RECORDING MEDIUM CONTAINING THE PROGRAM

摘要

A reactive system safety verification device in which a set of axioms is a set including as elements only a commutative law and an associative law. The device includes a translation section (8) for generating a first equation-equipped tree automaton receiving a set of terms under the set of axioms, a simulation section (9) for generating a second equation-equipped tree automaton receiving a set of terms deriving from the set of terms and the set of terms, and a set calculation section (10) for generating a fourth equation-equipped tree automaton by combining the second equation-equipped tree automaton and a third equation-equipped tree automaton receiving a set of terms to be inspected and judging whether the set received by the fourth equation-equipped automaton is an empty set.