Lazy symbolic model checking

A computer software product having one or more recordable medium having executable instructions stored thereon which, when executed by a processing device, causes the processing device to:

• identify in a transition relation partition a first internal variable of a state predicate of a pre-image calculation;
• identify in the transition relation partition a second internal variable not of the state predicate;
• and
• conjoin a first next state relation for the first internal variable but not for the second internal variable to a pre-image including the state predicate.

A method comprising:

• identifying a next internal variable in a state predicate of a pre-image calculation;
• building a transition relation including a first next state relation for the identified internal variable;
• and
• conjoining the first next state relation for the identified internal variable to a pre-image including the state predicate.

A method comprising:

• identifying in a transition relation partition a first internal variable of a state predicate;
• identifying in the transition relation partition a second internal variable not of the state predicate;
• and
• conjoining a first next state relation for the first internal variable but not for the second internal variable to a pre-image including the state predicate.

A computer software product having one or more recordable medium having executable instructions stored thereon which, when executed by a processing device, causes the processing device to:

• access a next state relation N and a set of next variables W′ that contains a set of next internal variables Ws′;
• and
• compute a pre-image Pre(S(W)) of a state predicate S(W) involving a set of variables W according to a logical relation equivalent to or including
• Pre(S(W))=∃W′·[ANDfor all v′ in Ws′(v′=N(v)) AND S(W′)].

A verification system comprising:

• means for identifying a next internal variable in a state predicate of a pre-image calculation;
• means for building a transition relation including a first next state relation for the identified internal variable;
• and
• means for conjoining the first next state relation for the identified internal variable to a pre-image including the state predicate.

A verification system comprising:

• means for identifying in a transition relation partition a first internal variable of a state predicate;
• means for identifying in the transition relation partition a second internal variable not of the state predicate;
• and
• means for conjoining a first next state relation for the first internal variable but not for the second internal variable to a pre-image including the state predicate.

A verification system comprising:

• a recordable medium to store executable instructions;
• a processing device to execute executable instruction;
• and
• a plurality of executable instructions to cause the processing device to:
• identify a next internal variable in a state predicate of a pre-image calculation;
• build a next state relation for a first transition relation partition to include the identified internal variable;
• and
• conjoin the first next state relation of the identified internal variable to a pre-image including the state predicate.

A verification system comprising:

• a recordable medium to store executable instructions;
• a processing device to execute executable instruction;
• and
• a plurality of executable instructions to cause the processing device to:
• identify in a transition relation partition a first internal variable of a state predicate of a pre-image calculation;
• identify in the transition relation partition a second internal variable not of the state predicate;
• and
• conjoin a first next state relation for the first internal variable but not for the second internal variable to a pre-image including the state predicate.