Comparing generic state machines

Abstract

This paper presents a technique for comparing generic state machines (i.e., machines where the size of manipulated data is not yet specified). The machine behavior is modeled using transfer formulas, a special kind of first order logic formulas. The technique is a mix of theorem proving methods with an automata comparison algorithm, in which first order logic terms are used to represent the values of the inputs, states and outputs of the machines.