Patent ID: 7092858

Claim:
A method of determining an output sequence of states in a finite state machine from an at least one input start state to an at least one input goal state, performed by a data processing system having a memory, comprising the steps of: determining an overapproximated path through the finite state machine, from an at least one first start state to an at least one first goal state, using a formal method, wherein the formal method is applied to a matrix comprised of state sets, the matrix being organized by time-steps along a first dimension and by partitions of state bits along a second dimension; determining a formally constrained underapproximated path that lies along the overapproximated path, the constrained path being of at least one time-step and comprising at least one state of the finite state machine; combining the constrained underapproximated path with the output sequence of states such that an updated output sequence of states and an updated at least one first start state are determined; ending a search, if the updated output sequence of states comprises at least one state of the at least one input start state and the at least one input goal state, but otherwise repeating the above steps.