Article collection "Mathematical Problems of Cybernetics" №7, Moscow, 1998
Fast equivalence checking algorithms for sequential programs on balanced frames
This paper deals with equivalence checking problem for sequential imperative programs. The semantics of such programs is defined by means of interpretation (models) of Propositional Dynamic Logic (PDL). In fact, 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. The paper presents a novel uniform technique for reducing equivalence checking problem for sequential programs on balanced frames to the well known word problem in semigroups. Using this technique we show that equivalence checking problem for sequential programs with partially commutative statements is decidable in polynomial time.