Finite state automata in the theory of algebraic program schemata

Algebraic program models considered in this paper generalize two models of programs introduced by A.A. Lyapunov and A.A. Letichevsky. The algebraic models are shown to approximate real-world programs via an intermediate formalization. The theory of program models focuses on the equivalence problem for program schemata. There are many results of decidability of this problem for various classes of algebraic program models. Most of these deciding algorithms derive from the equivalence checking algorithm for finite state automata. The aim of this paper is to reveal this relationship. An equivalent representation of schemes called matrix schemes is introduced. This representation is structurally closer to FSA, and it is proven that the equivalence problem in a subclass of program models represented as matrix models is reducible to one in FSA. The algorithm that checks an equivalence of FSA is studied and stated in terms of requirements applied to finite execution paths in automata. This results in a more general method which can be applied to other models, and necessary requirements models must satisfy for this method to be applicable are stated. Two models, namely the balanced semigroup model with left cancellation and the monotonous commutative model, are shown to have the equivalence problem decidable by the proposed method.