Modeling and analysis of the behavior of successive reactive programs

Finite state transducers extend the finite state automata to model functions on strings or lists. They may be used also as simple models of sequential reactive programs. These programs operate in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data such program performs a sequence of actions. When certain control points are achieved a program outputs the current results of computation as a response. It is significant that different sequences of actions may yield the same result. Therefore, the basic actions of a program may be viewed as generating elements of some appropriate semigroup, and the result of computation may be regarded as the composition of actions performed by the program. This paper offers an alternative technique for the analysis of finite state transducers over semigroups. To check the equivalence of transducers $\pi_1$ and $\pi_2$ we associate with them a Labeled Transition Systems $\Gamma_{\pi_1,\pi_2}$. Each path in this LTS represents all possible runs of $\pi_1$ and $\pi_2$ on the same input word. Every node of $\Gamma_{\pi_1,\pi_2}$ keeps track of the states of $\pi_1$ and $\pi_2$ achieved at reading some input word and the deficiency of the output words computed so far. If both transducers reach their final states and the deficiency of their outputs is nonzero then this indicates that $\pi_1$ and $\pi_2$ produce different images for the same word, and, hence, they are not equivalent. The nodes of $\Gamma_{\pi_1,\pi_2}$ that capture this effect are called rejecting nodes. Thus, the equivalence checking of $\pi_1$ and $\pi_2$ is reduced to checking the reachability of rejecting nodes in LTS $\Gamma_{\pi_1,\pi_2}$. We show that one needs to analyze only a bounded fragment of $\Gamma_{\pi_1,\pi_2}$ to certify (un)reachability of rejecting nodes. The size of this fragment is polynomial of the size of $\pi_1$ and $\pi_2$ if both transducers are deterministic, and single-exponential if they are k-bounded. The same approach is applicable for checking k-valuedness of transducers over semigroups.