Automata-theoretic verification of systems

Improved design testing apparatus for making a determination whether a design performs a task, the design testing apparatus being of the type which includes means for making the determination by testing a model automaton including variables and the improvement comprising:

• a processor operable to create a directed graph of dependency relations of the variables;
• means for using the directed graph to make a reduced version of the model automaton, wherein said means for using the directed graph comprises means for reducing the size of the directed graph to form a reduced version of the directed graph;
• and
• means for freeing a set of variables each said freed variable thereby being treated as a primary input for said reduced model automaton.

A method for testing a design to determine whether the design defines a task, the method comprising:

• constructing a model automaton, the model automaton being of the type that includes variables;
• creating a directed graph of dependency relations of the variables;
• using the directed graph to make a reduced version of the model automaton,
• wherein said step of using comprises the step of reducing the size of the directed graph to form a reduced version of the directed graph,
• wherein said step of reducing comprises the step of resizing variables having a value upon which the reduced version of the model automaton does not depend;
• and
• determining whether the design defines the task using the reduced version of the model automaton.

A method for testing a design to determine whether the design defines a task, the method comprising:

• constructing a model automaton, the model automaton being of the type that includes variables;
• creating a directed graph of dependency relations of the variables;
• using the directed graph to make a reduced version of the model automaton, wherein said step of using comprises the step of reducing the size of the directed graph to form a reduced version of the directed graph;
• freeing a set of variables, each said freed variable thereby being treated as a primary input for said reduced model automaton;
• and
• determining whether the design defines the task using the reduced version of the model automaton.

A method for testing a model of a design to determine whether the design defines a task, the model being of the type that includes variables, the method comprising:

• creating a directed graph of dependency relations of the variables;
• using the directed graph to make a reduced version of the model, wherein said means for using the directed graph includes means for reducing the size of the directed graph to form a reduced version of the directed graph, wherein said means for reducing includes means for resizing variables having a value upon which the performance of the reduced version of the model does not depend;
• and
• determining whether the reduced version of the model performs the task.

A method for testing a model of a design to determine whether the design defines a task, the model being of the type that includes variables, the method comprising:

• creating a directed graph of dependency relations of the variables;
• using the directed graph to make a reduced version of the model, wherein said means for using the directed graph includes means for reducing the size of the directed graph to form a reduced version of the directed graph;
• freeing a set of variables, each said freed variable thereby being treated as a primary input for said reduced model;
• and
• determining whether the reduced version of the model performs the task.