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 states. In this paper, we propose a symbolic querychecking algorithm that finds exactly state query. We argue our approach generalizes previous specialized techniques, and generality allows us find new interesting applications, such finding stable Our is linear in size space cost model checking, has been implemented on top checker NuSMV, using latter black box. show effectiveness by comparing it, gene network example, naive which all possible checked separately.