Patent ID: 8108195

Claim:
An apparatus comprising: one or more processors coupled to tangible memory for storing program code, wherein the one or more processors are utilized to determine whether a computing system satisfies a temporal logic property by exploring the underlying state space; a translator to translate an input model to be checked to include an already failed indicator AF for each state of said input model; and a satisfiability solver to check said translated input model, 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 wherein: AF(S i ) is said indicator for a current state S i , and BAD(S i ) is a Boolean predicate representing the bad states, S 0 is a state at cycle 0, AF(S 0 ) is a Boolean predicate which given a state S 0 determines whether either the temporal logic property does not hold in said state S 0 or if there is a state from a previous cycle for which the temporal logic property does not hold, Bad(S 0 ) is a Boolean predicate which checks given a state S 0 whether the temporal logic property does not hold in S 0 , S i−1 is a state reached in i−1 cycles, AF(S i−1 ) is a Boolean predicate which checks given a state S i−1 whether either the temporal logic property does not hold in state S 0 or there is a state from a previous cycle for which the property does not hold, i is the index of the current cycle.