Patent Document ID: 8489380
Application ID: 13108008
Patent Flag: 1

Claim One:
1. A computer-implemented method executed on one or more processors for determining whether a computing system satisfies a temporal logic property by exploring the underlying state space, the method comprising: translating a target model for the computing system to include a state variable AF for one or more states of the target model, wherein AF(S) represents value of the state variable AF at state S; and solving, using said one or more processors, the translated version of the target model that satisfies predetermined constraints defined as: 
 AF( S 0 ) Bad( S 0 ) 
 AF( S i ) (AF( S i−1 ) BAD( S i )) i> 0 where: i is the index of the current cycle, AF(Si) is a Boolean predicate for the current state Si, which determines whether the temporal logic property does not hold in the current state Si or whether there is a state from a previous cycle i−1 for which the temporal logic property does not hold, and BAD(Si) is a Boolean predicate representing the failed states, which checks given a state Si, whether the temporal logic property does not hold in Si.