Method and system for reducing the computation tree to include only model behaviors defined succinctly by a user via regular expressions as being of interest

A computer program storage device readable by machine, tangibly embodying a program of instructions executable by the machine to perform method steps for pruning a computation-tree defining a set of model behaviors of a state machine to a subset of the model behaviors, thereby reducing a complexity of the computation-tree and allowing analysis thereof by a computer in a shorter calculation time than would be possible for the complete computation-tree, said method comprising the steps of:

• (a) obtaining as input:
• i) a Finite State Machine, and
• ii) a Regular Expression defining a set of behaviors that are of interest to the user,
• (b) using the Regular Expression to construct:
• iii) a finite automaton accepting all prefixes of words accepted by the Regular Expression, and
• iv) a Boolean expression that realizes a property that the state is part of some path of a behavior defined by the Regular Expression and evaluates to a first logic state for each of said words that are allowable according to the Regular Expression and evaluates to a second logic state otherwise, and
• (c) exploring a state space of a product machine comprising the Finite State Machine and the constructed finite automaton such that for each state of the product machine there exists a corresponding Finite State Machine component and a corresponding finite automaton component, and for each explored state of the product machine, if the finite automaton component of a currently explored state of the product machine does not satisfy the Boolean Expression, then:
• (d) pruning the currently explored state from the computation tree so as to abort further exploration from the currently explored state.

A computer program product comprising a computer useable medium having computer readable program code embodied therein for pruning a computation-tree defining a set of model behaviors of a state machine to a subset of the model behaviors, thereby reducing a complexity of the computation-tree and allowing analysis thereof by a computer in a shorter calculation time than would be possible for the complete computation-tree, said computer program product comprising:

• computer readable program code for causing the computer to obtain as input:
• i) a Finite State Machine, and
• ii) a Regular Expression defining a set of behaviors that are of interest to the user,
• computer readable program code for causing the computer to use the Regular Expression to construct:
• i) a finite automaton accepting all prefixes of words accepted by the Regular Expression, and
• ii) a Boolean expression that realizes a property that the state is part of some path of a behavior defined by the Regular Expression and evaluates to a first logic state for each of said words that are allowable according to the Regular Expression and evaluates to a second logic state otherwise, and
• computer readable program code for causing the computer to explore a state space of a product machine age comprising the Finite State Machine and the constructed finite automaton such that for each state of the product machine there exists a corresponding Finite State Machine component and a corresponding finite automaton component, and for each explored state of the product machine, if the finite automaton component of a currently explored state of the product machine does not satisfy the Boolean Expression, pruning the currently explored state from the computation tree so as to abort further exploration from the currently explored state.

A system for pruning a computation-tree defining a set of model behaviors of a state machine to a subset of the model behaviors, thereby reducing a complexity of the computation-tree and allowing analysis thereof by a computer in a shorter calculation time than would be possible for the complete computation-tree, said system comprising:

• an input device for obtaining as input:
• i) a Finite State Machine, and
• ii) a Regular Expression defining a set of behaviors that are of interest to the user,
• an finite automaton constructor coupled to the input device for using the Regular Expression to construct a finite automaton accepting all prefixes of words accepted by the Regular Expression,
• a Boolean expression constructor coupled to the input device for using the Regular Expression to construct a Boolean expression that realizes a property that the state is part of some path of a behavior defined by the Regular Expression and evaluates to a first logic state for each of said words that are allowable according to the Regular Expression and evaluates to a second logic state otherwise,
• a state space explorer for exploring a state space of a product machine comprising the Finite State Machine and the constructed finite automaton such that for each state of the product machine there exists a corresponding Finite State Machine component and a corresponding finite automaton component, and
• a pruning unit coupled to the state space explorer and, for each explored currently state of the product machine, responsive to the finite automaton component of the currently explored state of the product machine not satisfying the Boolean Expression, for pruning the currently explored state from the computation tree so as to abort further exploration from the currently explored state.