On the equivalence problem for programs with mode switching

Abstract

We study a formal model of imperative sequential programs and focus on the equivalence problem for some class of programs with mode switching whose runs can be divided into two stages. In the first stage a program selects an appropriate mode of computation. Several modes may be tried (switched) in turn before making the ultimate choice. Every time when the next mode is put to a test, the program brings data to some predefined state. In the second stage of the run, once a definite mode is fixed, the final result of computation is produced. We develop a new technique for simulating the behavior of such programs by means of finite automata and demonstrate that the equivalence problem for programs with mode switching is decidable within a polynomial space. By revealing a close relationships between the equivalence problem for this class of programs and the intersection emptiness problem for deterministic finite automata we show that the the former is PSPACE-complete. © Springer-Verlag Berlin Heidelberg 2006.