New ideas on symbolic manipulations of finite state machines
Christian Berthet, Olivier Coudert, J.C. Madre · 2002
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.>