Article collection "Mathematical Problems of Cybernetics" №10, Moscow, 2001
On the equivalence checking problem for sequential programs on balanced homogeneous invertible frames
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.