Finding state solutions to temporal logic queries

Different analysis problems for state-transition models can be uniformly treated as instances of temporal logic query-checking, where solutions to the queries are restricted to states. In this paper, we propose a symbolic query-checking algorithm that finds exactly the state solutions to a query. We argue that our approach generalizes previous specialized techniques, and this generality allows us to find new and interesting applications, such as finding stable states. Our algorithm is linear in the size of the state space and in the cost of model checking, and has been implemented on top of the model checker NuSMV, using the latter as a black box. We show the effectiveness of our approach by comparing it, on a gene network example, to the naive algorithm in which all possible state solutions are checked separately.