On the Computation of the Set of Reachable States of Hybrid Models

In this paper, we present a method to compute symbolically, the set of configurations reachable from the initial configuration of an Extended Finite State Machine. Our representation allows variables of arbitrary type (boolean, arithmetic etc.) to be freely mixed. We define a class of EFSMs called direct sum machines and show how the reachable set of configurations for this class can be computed. In the computation, we use a hybrid model to represent sets of configurations. Sets of states formed by boolean variables are represented by BDDs and sets of states formed by arithmetic variables are represented as polyhedral regions. This method can be adapted to perform validation, verification, test generation etc. for sequential machines. We describe an implementation of this approach and the results of applying it to some design examples.