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

Article collection "Mathematical Problems of Cybernetics" №10, Moscow, 2001
Authors: Zakharov V.A.
On the equivalence checking problem for sequential programs on balanced homogeneous invertible frames
Abstract:
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.
Keywords:
program, semantics, Propositional Dynamic Logic, frame, equivalence checking problem, semigroup, decision procedure
Publication language: russian,  pages: 12 (p. 155-166)
Research direction:
Mathematical problems and theory of numerical methods
Russian source text:
Export link to publication in format:   RIS    BibTex