TLQSolver: A Temporal Logic Query Checker

摘要

Query checking was proposed by Chan [2] to speed up design understanding by discovering properties not known a priori. A temporal logic query is an expression containing a symbol? x, referred to as the placeholder, which may be replaced by any propositional formula to yield a CTL formula, e.g., AG~?_x, (AG(?_x Λ p). A propositional formula ψ is a solution to a query ψ in state s if substituting ψ for the placeholder in ψ is a formula that holds in state s. A query ψ is positive [2] if when ψ_1 is a solution to ψ and ψ_1 => ψ_2, then ψ_2 is also a solution. For example, if p Λ q is a solution to ψ, then so is p. For positive queries, we seek to compute a set of strongest propositional formulas that make them true. For example, consider evaluating the query AG?_x, i.e., "what are the invariants of the system", on a model in Figure 1(a), ignoring the variable m. (p V q) Λ r is the strongest invariant: all others, e.g., p V q or r, are implied by it. Thus, it is the solution to this query. In turn, if we are interested in finding the strongest property that holds in all states following those in which-q holds, we form the query AG(-q => AX?_x) which, for the model in Figure 1(a), evaluates to q Λ r. Chan also showed [2] that a query is positive iff the placeholder appears under an even number of negations.