This paper studies the equivalence checking problem for sequential imperative programs. The semantics of such programs is defined by means of interpretation (models) of Propositional Dynamic Logic (PDL). The semantics of program statements is specified by PDL frames. A frame is called balanced if for every pair of finite sequence of program statements these sequences yield different results only if they have different length. A frame is called homogeneous if it is isomorphic to every its subframe induced by an arbitrary data state. A frame is called invertible if every program statement is invertible on in this frame. The paper presents a technique for building decision procedures for checking equivalence of programs operating on r.

program, semantics, Propositional Dynamic Logic, frame, equivalence checking problem, semigroup, decision procedure

Mathematical problems and theory of numerical methods