On the equivalence checking problem for a model of programs related with muti-tape automata.
On the equivalence checking problem for a model of programs related with muti-tape automata.
Authors
Abstract
We study the equivalence-checking problem for a formal model of computer programs which is used for the purpose of verification. In this model programs are viewed as deterministic finite automata operating on Kripke structures defined in the framework of dynamic logics. When a transition relation in such structures is Euclidean, a result of a program execution does not depends on the order in which basic statements are applied to data states. The models of programs with commuting statements has a direct relationship to multi-tape finite automata. We consider the case when evaluation functions which specify truth-values of basic predicates in programs are monotonic. This corresponds to multi-tape automata operating on binary words of the type $0^*1^*$. The main theorem states that the equivalence-checking problem in the model of programs with commuting and monotonic statements is decidable in polynomial time.
Keywords
Edition
Proceedings of the 9-th International Conference on Implementation and Application of Automata (CIAA'04), July 22-24, 2004), Kingston, Ontario, Canada, Lecture Notes in Computer Science, 2005, vol. 3317, pp. 293-305.
Research Group
All publications during 2005
All publications