KIAM Main page Web Library  •  Publication Searh  Русский 
Publication

Article collection "Mathematical Problems of Cybernetics" №7, Moscow, 1998
Authors: Zakharov V.A.
Fast equivalence checking algorithms for sequential programs on balanced frames
Abstract:
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.
Keywords:
program, semantics, Propositional Dynamic Logic, frame, equivalence checking problem, semigroup, decision procedure, polynomial time
Publication language: russian, pages: 22 (p. 303-324)
Research direction:
Mathematical problems and theory of numerical methods
Source text: