The equivalence problem for programs with mode switching is PSPACE-complete.
Новости
The equivalence problem for programs with mode switching is PSPACE-complete.
Аннотация
We study a formal model of imperative sequential programs. In this model programs are viewed as deterministic finite automata whose semantics is defined on Kripke structures. We focus on the equivalence problem for some specific class of programs — 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 definitive mode is fixed, the final result of computation is produced. The effect of mode switching may be used for automatic generation of opaque predicates, i.e. boolean expressions whose behavior is known a priori. Such predicates provide a very simple and effective means for virus obfuscation; therefore the development of efficient algorithms for the analysis of programs with mode switching is an urgent task in view of designing virus detection tools. 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 relationship between the equivalence problem for this class of programs and the intersection emptiness problem for deterministic finite state automata we show that the former is PSPACE-complete.
Издание
Труды Института системного программирования РАН, том 11, 2006, стр. 109-128.
ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).
Для цитирования
Полный текст статьи в формате pdf
Вернуться к содержанию тома