On the computation of the set of reachable states of hybrid models
A. S. Krishnakumar, Kwang-Ting Tim Cheng · 1994
In this paper, we present a method to compute symbolically, the set of con gurations reachable from the initial con guration of an Extended Finite State Machine.Our representation allows variables of arbitrary type (boolean, arithmetic etc.) to be freely mixed.We de ne a class of EFSMs called direct sum machines and show h o w the reachable set of con gurations for this class can be computed.In the computation, we use a hybrid model to represent sets of con gurations.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, veri cation, test generation etc. for sequential machines.We describe an implementation of this approach and the results of applying it to some design examples. 31