Patent Document ID: 7835898
Application ID: 11285338
Patent Flag: 1

Claim One:
1. A method for finding bugs in a model implemented by a computer comprising: translating a model to be checked to include an already failed indicator AF for each state of said model, comprising using one of the following equations: A ′ = INIT ⁡ ( S 0 ) ⋀ ( ⋀ i = 1 k ⁢ ( TR ⁡ ( S i - 1 , S i ) ⋁ AF ⁡ ( S i - 1 ) ) ) ⋀ ( ⋁ i = 0 k ⁢ BAD ⁡ ( S i ) ) A ″ = INIT ⁡ ( S 0 ) ⋀ ( ⋀ i = 1 k ⁢ ( TR ⁡ ( S i - 1 , S i ) ⋁ AF ⁡ ( S i - 1 ) ) ) ⋀ ( AF ⁡ ( S k ) ) where INIT(S 0 ) is a Boolean predicate which checks if the state S 0 is one of the initial states and TR(S i-1 , S i ) is a transition relation from a previous state S i-1 to current state S i , solving said translated model for satisfiability in order to find said bugs, wherein said indicator AF is defined as one of the following: 
 AF ( S 0 ) Bad( S 0 ) 
 AF ( S i ) ( AF ( S i-1 ) BAD( S i )) i> 0 
 and 
 AF ( S 0 )→Bad( S 0 ) 
 AF ( S i )→( AF ( S i-1 ) BAD( S i )) i> 0 where AF(S i ) is said indicator for a current state S i , and BAD(S i ) is a Boolean predicate representing the bad states.