Reachability and recurrence in extended finite state machines: Modular vector addition systems

Abstract

In this paper, a formal model of Extended Finite State Machines (EFSMs) is proposed and an approach to their analysis is suggested. The state of an EFSM is captured by its configuration. A class of EFSMs, called Modular Vector Addition Systems (MVAS), is defined and analyzed. Modular Vector Addition Systems cover a significant subset of models used in communication protocols and behavioral synthesis of hardware. For this class of EFSMs, an algorithm to compute the set of configurations reachable from an initial configuration is presented. This algorithm may also be used to compute the set of recurrent configurations. Knowledge of these sets is useful in verification, testing, and optimization of EFSM models. A compact representation of these sets and a simple test for membership for such representations are also presented.