New ideas on symbolic manipulations of finite state machines

Formal verification of finite state machines (FSM) using symbolic manipulations is addressed. It is shown that the use of symbolic manipulations algorithms for the traversal of a FSM can be sublinear in the number of state and input patterns for some classes of machines. A symbolic manipulation algorithm can be directly used as a method for the transformation of a FSM which preserves the observable behavior. It is also shown that a backward traversal of a FSM can also be performed using symbolic techniques