Mathematical Backgrounds of Informatics and Programming

Efficient equivalence-checking algorithms for propositional Mealy programs over balanced frames

V. V. Podymov

Lomonosov Moscow State University, Moscow, Russia

Abstract: We propose and investigate propositional Mealy programs (PMPs), a model that is a slight syntactic generalization of the discrete processor model studied by V. M. Glushkov and A. A. Letichevsky. PMPs employ a “modernized” semantics based on notions used in the model of propositional sequential programs proposed by V. A. Zakharov (PSPZs). A technique for constructing efficient equivalence checking algorithms for PMPs is proposed, adapting a known technique for PSPZs based on analysis of a graph of consistent program computations. Efficient PMP equivalence-checking algorithms based on the proposed technique are obtained for some kinds of applied semantics.

Keywords: equivalence problem, equivalence checking, program models, discrete processors, propositional sequential programs.

UDC: 519.681:519.71

DOI: 10.17223/20710410/70/5