Query Checking for Linear Temporal Logic

Abstract

The query-checking problem for temporal logic may be formulated as follows. Given a Kripke structure M and a temporal-logic query of form $\phi \left[ {\texttt {var}}\right]$, which may be thought of as a temporal formula with a missing propositional subformula ${\texttt {var}}$, find the most precise propositional formula f that, when substituted for ${\texttt {var}}$ in $\phi \left[ {\texttt {var}}\right]$, ensures M satisfies the resulting temporal property. Query checking has been used for system comprehension, specification reconstruction, and other related applications in the formal analysis of systems.

In this paper we present an automaton-based methodology for query checking over linear temporal logic (LTL). While this problem is known to be hard in the general case, we show that by exploiting several key observations about the interplay between the input model M and the query $\phi \left[ {\texttt {var}}\right]$, we can produce results for many problems of interest. In support of this claim, we report on preliminary experimental data for an implementation of our technique.

1 Introduction

Temporal logics [9] are widely used to specify desired properties of system behavior. Such logics permit the description of how systems should execute over time; tools such as model checkers [4, 8] can then be used automatically to determine whether or not certain types of system possess given temporal properties.

The practical utility of model checking and other temporal-logic-based verification technologies relies on the ability of users to define correctly the properties they are interested in. To assist users in this regard, researchers have looked into various forms of automated temporal-property reconstruction [1, 11, 17, 18] as a means of helping users to devise temporal specifications from given system specifications. Users may then use these as specifications for the system (useful when systems subsequently have new functionality added, as the new system can be checked against the old specification to ensure backward compatibility); they may also review them as a means of gaining insight into the behavior of a system that may not have been formally specified or verified. One of the most influential lines of work in this area is so-called temporal logic query checking [6], which aims to solve the following general problem: given a system, and a temporal formula with a missing (propositional) subformula, “solve” for the missing subformula. As originally formulated by Chan [6], the temporal logic in question was a subset of the branching-time temporal logic CTL [10], for which he gave efficient algorithms for computing most-precise missing formulas. Others have considered different variants of this problem, by considering multiple missing subformulas, for instance, or different logics [5, 7, 15].

In this paper we consider the problem of query checking for linear temporal logic (LTL) [10]. LTL differs from branching-time logics in that one specifies properties of executions, rather than states in a system, and it is often viewed as an easier formalism to master for this reason. It is also the basis for specification languages, such as FORSPEC [2], used in digital hardware design. In the current work we show how automaton-based model-checking techniques may be adapted to yield a solution to the query-checking problem that, while computationally complex in the worst case, exploits structure in the space of possible query solutions to yield better performance. To this end, after reporting on related work and developing needed mathematical preliminaries, we present our technique and report on a preliminary implementation that we are developing.

2 Related Work

Temporal-logic query checking was initially defined and explored by William Chan [6], who considered the problem in the context of the branching-time temporal logic CTL [10]. Chan initially considered a subset of CTL and showed that queries in this subset, which allows the universal path quantifier and places restrictions on the modal operators, can be solved in linear time. This work was subsequently extended to more expressive branching-time logics via alternating-tree automaton constructions [5] and three-valued model checking [15]; this last paper also describes several applications of the technique in areas such as invariant inference and test generation. Other work has studied the problem for classes of infinite-state systems [21].

In contrast to branching time, linear-time query checking has remained relatively unstudied. Chokler et al. [7] consider several variants of LTL query checking and prove complexity results for these problems; however, no implementation or experimental results were reported.

Other researchers have considered the problem of so-called specification mining, in which temporal properties are inferred not from system models, but from execution behavior, using techniques from data mining and machine learning. Such properties hold of the data from which they are generated, but not necessarily of all system behaviors. Emblematic of this work is the dynamic-invariant generation work of Ernst et al. [11], which uses program instrumentation to obtain state information as a program executes and then data mining to identify possible invariants. Other work in this vein couples data mining of execution data with retesting to attempt to remove invalid invariants in the case of Simulink models [1]. Other work has considered the mining of general LTL formulas from run-time data [16].

3 LTL, Kripke Structures and Büchi Automata

This section defines the syntax of LTL and reviews the notions of Kripke structure, Büchi automata, and model checking in LTL. In what follows, we fix a finite non-empty set $\mathcal {A}$ of atomic propositions.

3.1 LTL and Kripke Structures

The syntax of LTL formulas is given by the following grammar.

$$\begin{aligned} \phi := a \in \mathcal {A} \mid \lnot \phi \mid \phi \vee \phi \mid {{\mathrm{\mathbf {X}}}}\phi \mid \phi {{\mathrm{\mathbf {U}}}}\phi \end{aligned}$$

In addition to the propositional constructs a, $\lnot$ and $\vee$, LTL formulas also include the modal operators ${{\mathrm{\mathbf {X}}}}$, or “next state”, and ${{\mathrm{\mathbf {U}}}}$, or “until”. The derived propositional operations $\wedge , \rightarrow$, etc. are defined in the usual manner; we also write ${\texttt {tt}}$ as an abbreviation for $a \vee \lnot a$ for a designated $a \in \mathcal {A}$ and ${\texttt {ff}}$ for $\lnot {\texttt {tt}}$. We additionally use the following derived temporal operators in the sequel.

$$\begin{aligned} {{\mathrm{\mathbf {F}}}}\phi\triangleq & {} {\texttt {tt}}{{\mathrm{\mathbf {U}}}}\phi \\ {{\mathrm{\mathbf {G}}}}\phi\triangleq & {} \lnot ({{\mathrm{\mathbf {F}}}}\lnot \phi )\\ \phi _1 {{\mathrm{\mathbf {R}}}}\phi _2\triangleq & {} \lnot ((\lnot \phi _1) {{\mathrm{\mathbf {U}}}}(\lnot \phi _2)) \end{aligned}$$

${{\mathrm{\mathbf {F}}}}$ and ${{\mathrm{\mathbf {G}}}}$ are the “eventually” and “always” operators, while ${{\mathrm{\mathbf {R}}}}$ is sometimes called the “release” operator. We write $\varPhi$ for the set of LTL formulas.

The semantics of LTL is given as a relation $\models \, \subseteq (2^\mathcal {A})^\omega \times \varPhi$. Intuitively, $\pi \models \phi$ holds if $\pi \in (2^\mathcal {A})^\omega$, which is an infinite sequence of subsets of $\mathcal {A}$, makes $\phi$ true. In what follows, if $\pi = A_0A_1\ldots$ then we write $\pi [i] \in 2^\mathcal {A}$ for $A_i \subseteq \mathcal {A}$ and $\pi [i..] \in (2^\mathcal {A})^\omega$ for the suffix $A_iA_{i+1}\ldots$. The relation $\models$ may now be defined as follows.

• $\pi \models a \;\;(a \in \mathcal {A})$ iff $a \in \pi [0]$.

• $\pi \models \lnot \phi$ iff $\pi \not \models \phi$.

• $\pi \models \phi _1 \vee \phi _2$ iff $\pi \models \phi _1$ or $\pi \models \phi _2$.

• $\pi \models {{\mathrm{\mathbf {X}}}}\phi$ iff $\pi [1..] \models \phi$.

• $\pi \models \phi _1 {{\mathrm{\mathbf {U}}}}\phi _2$ iff there is a $j \ge 0$ such that $\pi [j..] \models \phi _1$ and for all $0 \le i < j$, $\pi [i..] \models \phi _2$.

We often write $\llbracket \phi \rrbracket \triangleq \left\{ \pi \in (2^\mathcal {A})^\omega \mid \pi \models \phi \right\}$ for the set of sequences satisfying $\phi$.

LTL formulas are often used to specify properties of systems modeled as Kripke Structures.

Definition 1

A Kripke Structure is a quadruple $\left( S, R, L, i \right)$ where:

• S is a non-empty set of states;

• $R \subseteq S \times S$ is the transition relation;

• $L \in S \rightarrow 2^\mathcal {A}$ is the labeling function; and

• $i \in S$ is the initial state.

A Kripke structure encodes the behavior of a system, with S representing system states and the transition relation recording the possible execution steps that are possible when a system is in a given state: when the system is in state s it can evolve in one step to state $s'$ iff $\left( s,s' \right) \in R$. The labeling function indicates which atomic propositions are true in any given state; if $a \in L(s)$ then a is deemed true s, while if $a \not \in L(s)$ it is false. State i is the initial state. In what follows we require Kripke structures to be left-total: for every $s \in S$ it must be the case that there is an $s' \in S$ such that $\left( s,s' \right) \in R$. We also call a Kripke structure finite-state if its state set is finite. Semantically, left-total Kripke structure $K = \left( S,R,L,i \right)$ gives rise to a subset $\llbracket K \rrbracket$ of $(2^\mathcal {A})^\omega$ as follows.

• Infinite sequence $s_0s_1\ldots \in S^\omega$ is an execution of K if $s_0 = i$ and $\left( s_i, s_{i+1} \right) \in R$ for all $i \ge 0$.

• K generates $\pi = A_0A_1\ldots$ iff there is an execution $s_0s_1\ldots$ of K such that $A_i = L(s_i)$.

• $\llbracket K \rrbracket = \left\{ \pi \in (2^\mathcal {A})^\omega \mid K \text { generates } \pi \right\}$.

We then write $K \models \phi$, where K is a Kripke structure and $\phi$ is an LTL formula, iff $\llbracket K \rrbracket \subseteq \llbracket \phi \rrbracket$.

3.2 Büchi Automata and LTL Model Checking

The LTL model-checking problem may be formulated as follows.  

Given: :

Kripke structure K, LTL formula $\phi$

Determine: :

Does $K \models \phi$?

 

When K is finite-state the model-checking problem is decidable in time proportional to |K|, where |K| is the size of Kripke structure K. A common approach for LTL model checking relies on the use of Büchi automata. This section defines these automata and explains their use in LTL model checking.

Büchi automata. Büchi automata are used to recognize so-called $\omega$-regular languages, which are sets of infinite-length sequences of alphabet symbols.

Definition 2

A Büchi automaton is a quintuple $\left( Q, \varSigma , \delta , q_I, F \right)$, where:

• Q is a finite, non-empty set of states;

• $\varSigma$ is a finite, non-empty set of alphabet symbols;

• $\delta \subseteq Q \times \varSigma \times Q$ is the transition relation;

• $q_I$ is the initial state; and

• $F \subseteq Q$ is the set of accepting states.

Let B be a Büchi automaton $\left( Q, \varSigma , \delta , q_i, F \right)$. We define the language, $L(B) \subseteq \varSigma ^\omega$, of B as follows.

• Given $\omega$-word $w = \alpha _0\alpha _1\ldots \in \varSigma ^\omega$, define a run of B on w to be a sequence $q_0q_1\ldots \in Q^\omega$ such that $q_0 = q_I$ and $\left( q_i, \alpha _i, q_{i+1} \right) \in \delta$ for all $i \ge 0$.

• A run $q_0q_1\ldots \in Q^\omega$ of B on w is accepting iff for all $i \ge 0$ there exists $j \ge i$ such that $q_j \in F$.

• $L(B) = \left\{ w \in \varSigma ^\omega \mid B \text { has an accepting run on } w \right\}$.

The subsets $W \subseteq \varSigma ^\omega$ such that $W = L(B)$ for some Büchi automaton B coincide with the so-called $\omega$-regular languages. This class of languages is closed with respect to complementation and intersection; both of these operations can be realized as constructions on Büchi automata. In addition, checking for emptiness of the language of B is decidable in time proportional to the size of B. Algorithmically, this can be done by computing the strongly connected components of B and determining if there is one such component reachable from the start state, containing an accepting state, and having at least one edge from a state in the component to another state in the component. This ensures the existence of at least one accepting run in B, and hence the non-emptiness of L(B).

LTL model checking using Büchi automata. Büchi automata may be used as a basis for model checking of finite-state Kripke structures against LTL formulas [19]. Recall the model-checking problem in this case: given finite-state Kripke structure K and LTL formula $\phi$, determine whether or not $K \models \phi$. This problem may be solved algorithmically using Büchi automata as follows.

• From K, construct Büchi automaton $B_K$ such that $L(B_K) = \llbracket K \rrbracket$.

• From $\phi$, construct Büchi automaton $B_{\lnot \phi }$ such that $L(B_{\lnot \phi }) = \llbracket \lnot \phi \rrbracket$.

• Construct the Büchi automaton $B_{K,\lnot \phi }$ such that $L(B_{K,\lnot \phi }) = L(B_K) \cap L(B_{\lnot \phi })$ and check if $L(B_{K,\lnot \phi }) = \emptyset$. This is true iff $K \models \phi$.

Note that both $B_K$ and $B_{\lnot \phi }$ must have alphabet sets $\varSigma = 2^\mathcal {A}$. Specifically, transitions in both of these Büchi automata are labeled by subsets of $\mathcal {A}$.

For $K = \left( S,R,L,i \right)$, the construction $B_K$ is straightforward: define $B_K = \left( S,2^\mathcal {A},\delta _K,i,S \right)$, where

$$ \delta _K = \left\{ \left( s,A,s' \right) \mid \left( s,s' \right) \in R \text { and } A = L(s) \right\} .$$

The construction of $B_\phi$ for LTL formula $\phi$ is more complex, and a number of approaches may be found in the literature [3, 12,13,14]. The best techniques yield automata that are $O(3^{|\phi |})$, where $|\phi |$ is the size of formula $\phi$.

We close this section by giving an alternative formulation of Büchi automata whose alphabets are $2^\mathcal {A}$. The edges in these automata are labeled by propositional formulas constructed from $\mathcal {A}$, rather than subsets of $\mathcal {A}$; the interpretation of such an edge $q \mathop {\longrightarrow }\limits ^{\gamma } q'$ is that $q \mathop {\longrightarrow }\limits ^{A} q'$ for every A satisfying $\gamma$. These notions are formalized as follows.

• Define the set of propositional formulas $\varGamma$ over $\mathcal {A}$ by the following grammar.

  $$ \gamma \,{:}{:}\!\!= a \in \mathcal {A} \mid \lnot \gamma \mid \gamma \vee \gamma $$

  Note that $\varGamma \subsetneq \varPhi$. We use the usual encodings of ${\texttt {tt}}$, $\wedge$, etc.

• If $A \subseteq \mathcal {A}$ and $\gamma \in \varGamma$ then define $A \models \gamma$ as follows.

  • $A \models a$ iff $a \in A$

  • $A \models \lnot \gamma$ iff $A \not \models \gamma$

  • $A \models \gamma _1 \vee \gamma _2$ iff $A \models \gamma _1$ or $A \models \gamma _2$.

  We write $\llbracket \gamma \rrbracket$ for $\left\{ A \subseteq \mathcal {A} \mid A \models \gamma \right\}$. Note that $A \models \gamma$ iff $\pi \models \gamma$ for all $\pi$ such that $\pi [0] = A$.

We sometimes use $A \subseteq \mathcal {A}$ as short-hand for the formula $(\bigwedge _{a \in A} a) \wedge (\bigwedge _{a \not \in A} \lnot a)$. Note that $\llbracket A \rrbracket = \{A\}$ in this case.

Definition 3

Given $\mathcal {A}$, a Büchi propositional automaton is a tuple $\left( Q, \delta , q_I, F \right)$, where:

• Q is a finite non-empty set of states, with $q_I \in Q$ and $F \subseteq Q$.

• $\delta \subseteq (Q \times \varGamma \times Q)$ is the transition relation.

Based on our interpretation of sets $A \subseteq \mathcal {A}$ as propositions it is easy to see that every Büchi automaton is also a Büchi propositional automaton. An arbitrary Büchi propositional automaton $B = \left( Q, \delta , q_I, F \right)$ may also be translated into a traditional Büchi automaton $B' = \left( Q, 2^\mathcal {A}, \delta ', q_I, F \right)$ by defining

We define $L(B) = L(B')$. The traditional tableau-based constructions for converting LTL formulas into Büchi automata may easily be adapted to generate Büchi propositional automata with the property that for every pair of automaton states $q, q'$ there is exactly one $\gamma$ such that $\left( q,\gamma ,q' \right) \in \delta$.

Finally, we give a construction for Büchi propositional automaton $B_{12}$ with $L(B_{12}) = L(B_1) \cap L(B_2)$ for the special case of Büchi propositional automata $B_1$ and $B_2$, with every state in $B_1$ accepting.

Theorem 1

Let $B_1 = \left( Q_1, \delta _1, q_1, Q_1 \right)$ and $B_2 = \left( Q_2, \delta _2, q_2, F_2 \right)$ be Büchi propositional automata. Then $L(B_{12}) = L(B_1) \cap L(B_2)$, where

$$B_{12} = \left( Q_1 \times Q_2, \delta _{12}, \left( q_1, q_2 \right) , Q_1 \times F_2 \right) $$

and $\left( \left( q_1, q_2 \right) , \gamma _1 \wedge \gamma _2, \left( q_1',q_2' \right) \right) \in \delta _{12}$ iff $\left( q_1, \gamma _1, q_1' \right) \in \delta _1$ and $\left( q_2, \gamma _2, q_2' \right) \in \delta _2$.

4 The LTL Query Checking Problem

In LTL query checking we are interested in Kripke structures and LTL formula queries, which are formulas containing a missing propositional subformula. The goal in LTL query checking is to construct solutions for the missing subformula. This section defines the problem precisely and proves results that will be used later in our algorithmic solution.

LTL queries correspond to LTL formulas with a missing propositional subformula, which we denote ${\texttt {var}}$. It should be noted that ${\texttt {var}}$ stands for an unknown proposition over $\mathcal {A}$; it is not a propositional variable. The syntax of queries is as follows.

$$\begin{aligned} \phi := {\texttt {var}}\mid a \in \mathcal {A} \mid \lnot \phi \mid \phi \vee \phi \mid {{\mathrm{\mathbf {X}}}}\phi \mid \phi {{\mathrm{\mathbf {U}}}}\phi \end{aligned}$$

In this paper we only consider the case of a single propositional unknown, although the definitions can naturally be extended to multiple such unknowns. We often write $\phi [{\texttt {var}}]$ for LTL query with unknown ${\texttt {var}}$, and $\phi [\phi ']$ for the LTL formula obtained by replacing all occurrences of ${\texttt {var}}$ by LTL formula $\phi '$. We also say that an occurrence of ${\texttt {var}}$ within $\phi [{\texttt {var}}]$ is positive if it appears within an even number of instances of $\lnot$, and negative otherwise. If all occurrences of ${\texttt {var}}$ in $\phi [{\texttt {var}}]$ are positive we say ${\texttt {var}}$ is positive in $\phi [{\texttt {var}}]$; if all are negative we say ${\texttt {var}}$ is negative in $\phi [{\texttt {var}}]$; if there are both positive and negative occurrences of ${\texttt {var}}$ in $\phi [{\texttt {var}}]$ then ${\texttt {var}}$ is mixed in $\phi [{\texttt {var}}]$.

The query-checking problem may now be formulated as follows.  

Given: :

Finite-state Kripke structure K, LTL query $\phi [{\texttt {var}}]$

Compute: :

All $\gamma \in \varGamma$ (i.e. all propositional formulas over $\mathcal {A}$) with $K \models \phi [\gamma ]$.

 

If $\gamma$ is such that $K \models \phi [\gamma ]$, then we call $\gamma$ a solution for K and $\phi [{\texttt {var}}]$, and in this case we say that $\phi [{\texttt {var}}]$ is solvable for K. Computing all solutions for query checking problem K and $\phi [{\texttt {var}}]$ cannot be done explicitly, since the number of propositional formulas is infinite. However, if we define $\gamma _1 \equiv \gamma _2$ to hold if $\llbracket \gamma _1 \rrbracket = \llbracket \gamma _2 \rrbracket$, then it is clear that there are only finitely many distinct equivalence classes for $\varGamma$. We also say that $\gamma _1$ is at least as strong (weak) as $\gamma _2$ if $\llbracket \gamma _1 \rrbracket \subseteq \llbracket \gamma _2 \rrbracket$ ($\llbracket \gamma _2 \rrbracket \subseteq \llbracket \gamma _1 \rrbracket$). We now have the following.

Theorem 2

Let K be a finite-state Kripke structure and $\phi [{\texttt {var}}]$ an LTL query.

• 1. If ${\texttt {var}}$ is positive in $\phi [{\texttt {var}}]$ then there is a finite set (modulo $\equiv$) of strongest solutions for $\phi [\gamma ]$.

• 2. If ${\texttt {var}}$ is negative in $\phi [{\texttt {var}}]$ then there is a finite set (modulo $\equiv$) of weakest solutions to $\phi [\gamma ]$.

In some cases these sets of maximal solutions contain a single solution.

Definition 4

Let $\phi [{\texttt {var}}]$ be an LTL query. Then $\phi [{\texttt {var}}]$ is:

• conjunctively covariant iff for all $\gamma _1, \gamma _2$, $\phi [\gamma _1 \wedge \gamma _2] \equiv \phi [\gamma _1] \wedge \phi [\gamma _2]$; and

• conjunctively contravariant iff for all $\gamma _1, \gamma _2$, $\phi [\gamma _1 \vee \gamma _2] \equiv \phi [\gamma _1] \wedge \phi [\gamma _2]$.

Theorem 3

Let K be a finite-state Kripke structure, and let $\phi [{\texttt {var}}]$ be solvable for K. Then the following hold.

• 1. If ${\texttt {var}}$ is positive in $\phi [{\texttt {var}}]$ and $\phi [{\texttt {var}}]$ is conjunctively covariant, then there is a unique strongest solution (modulo $\equiv$) for $\phi [{\texttt {var}}]$.

• 2. If ${\texttt {var}}$ is negative in $\phi [{\texttt {var}}]$ and $\phi [{\texttt {var}}]$ is conjunctively contravariant, then there is a unique weakest solution (modulo $\equiv$) for $\phi [{\texttt {var}}]$.

As examples, note that ${{\mathrm{\mathbf {G}}}}{\texttt {var}}$ is conjunctively covariant and solvable for every K, and that ${\texttt {var}}$ is positive; it is guaranteed to have a unique strongest solution for any K. So does ${{\mathrm{\mathbf {G}}}}{{\mathrm{\mathbf {F}}}}{\texttt {var}}$. On the other hand, ${{\mathrm{\mathbf {G}}}}({\texttt {var}}\implies {{\mathrm{\mathbf {F}}}}\phi ')$ is conjunctively contravariant and solvable for every K, and ${\texttt {var}}$ appears negatively. Thus, every K has a unique weakest solution for this query.

5 Automaton-Based LTL Query Checking

In this section we show how LTL query checking can be formulated as a problem on Büchi propositional automata whose propositional labels may contain instances of ${\texttt {var}}$. In this paper we only consider LTL queries in which ${\texttt {var}}$ is either negative or positive; the mixed case will not be dealt with. The approach is based on LTL model checking in that we generate Büchi propositional automata from both a Kripke structure and the negation of an LTL query and compose them; we then search for solutions to ${\texttt {var}}$ that make the language of the composition automaton empty. To formalize these notions, we introduce the following definitions.

5.1 Propositional Queries

Definition 5

Let ${\texttt {var}}$ be an unknown proposition. Then propositional queries are generated by the following grammar.

$$\begin{aligned} \gamma {:}{:}= {\texttt {var}}\mid a \in \mathcal {A} \mid \lnot \gamma \mid \gamma \vee \gamma \end{aligned}$$

We write $\gamma [{\texttt {var}}]$ for a generic instance of a propositional template, and $\varGamma [{\texttt {var}}]$ for the set of all propositional templates involving ${\texttt {var}}$.

It is easy to see that propositional queries form a subset of LTL queries, and that notions of $\gamma [\gamma ']$, positive and negative occurrences of ${\texttt {var}}$, etc., carry over immediately. A shattering formula for query $\gamma [{\texttt {var}}]$ is a propositional formula $\gamma '$ with the property that $\llbracket \gamma [\gamma '] \rrbracket = \emptyset$; that is, $\gamma '$ “makes” $\gamma [{\texttt {var}}]$ unsatisfiable. We call $\gamma [{\texttt {var}}]$ shatterable if it has a shattering formula. The following is a consequence of the fact that the set of propositional formulas form a Boolean algebra.

Theorem 4

Let $\gamma [{\texttt {var}}]$ be shatterable.

• 1. If ${\texttt {var}}$ is positive in $\gamma [{\texttt {var}}]$ then there is a unique (modulo $\equiv$) weakest shattering formula for $\gamma [{\texttt {var}}]$.

• 2. If ${\texttt {var}}$ is negative in $\gamma [{\texttt {var}}]$ then there is a unique strongest (modulo $\equiv$) shattering formula for $\gamma [{\texttt {var}}]$.

Intuitively, if $\gamma [{\texttt {var}}]$ is shatterable and ${\texttt {var}}$ is positive, then $\gamma [{\texttt {var}}]$ can be rewritten as ${\texttt {var}}\wedge \gamma '$ for some propositional formula $\gamma '$ (i.e. $\gamma '$ contains no occurrences of ${\texttt {var}}$). In this case the weakest shattering formula for $\gamma [{\texttt {var}}]$ is $\lnot \gamma '$. A dual argument holds in the case that ${\texttt {var}}$ is negative in $\gamma [{\texttt {var}}]$.

5.2 Büchi Query Automata

Büchi query automata are propositional automata with propositional queries labeling transitions.

Definition 6

Let ${\texttt {var}}$ be a propositional unknown. A Büchi query automaton has form $\left( Q, \delta , q_I, F \right)$, with finite state set Q, initial state $q_I \in Q$, accepting states $F \subseteq Q$, and transition relation $\delta \subseteq Q \times \varGamma [{\texttt {var}}] \times Q$.

Intuitively, a Büchi query automaton is like an LTL query in that it contains a propositional unknown, ${\texttt {var}}$, that can be used to change the language accepted by the automaton. Specifically, if ${\texttt {var}}$ is set to a condition $\gamma '$ that shatters the edge label $\gamma [{\texttt {var}}]$, then any query-automaton edge of form $(q,\gamma [{\texttt {var}}],q')$ is no longer available for use in constructing runs of the automaton. Figure 1 illustrates this phenomenon. Thus, by varying ${\texttt {var}}$ we can thus affect the language accepted by the query automaton.

Fig. 1.

Shattering edges in a Büchi query automaton. Proposition $\gamma '$ shatters $\gamma [{\texttt {var}}]$, and consequently the edge $(q, \gamma [{\texttt {var}}], q')$ is removed.

Formally, if $B[{\texttt {var}}]$ is a Büchi query automaton then define $B[\gamma ]$ to be the Büchi propositional automaton obtained by replacing all occurrences of ${\texttt {var}}$ by $\gamma$ in any edge label within $B[{\texttt {var}}]$. We say that $\gamma$ shatters $B[{\texttt {var}}]$ if $L(B[\gamma ]) = \emptyset$, i.e. if $\gamma$ renders the language of $B[{\texttt {var}}]$ empty. Notions of positive and negative occurrences of ${\texttt {var}}$ in $B[{\texttt {var}}]$, etc., carry over in the obvious manner.

We now note the following correspondence between LTL queries and Büchi query automata.

Theorem 5

Let $\phi [{\texttt {var}}]$ be an LTL query. Then there exists a Büchi query automaton $B_\phi [{\texttt {var}}]$ such that the following hold.

• 1. For all $\gamma \in \varGamma$, $\llbracket \phi [\gamma ] \rrbracket = L(B_\phi [\gamma ])$.

• 2. If ${\texttt {var}}$ is positive in $\phi [{\texttt {var}}]$ then ${\texttt {var}}$ is positive in $B_\phi [{\texttt {var}}]$.

• 3. If ${\texttt {var}}$ is negative in $\phi [{\texttt {var}}]$ then ${\texttt {var}}$ is negative in $B_\phi [{\texttt {var}}]$.

The construction of $B_\phi [{\texttt {var}}]$ is a straightforward adaptation of the construction of Büchi propositional automata from LTL formulas $\phi$.

5.3 LTL Query Checking via Büchi Query Automata

We now explain our approach to LTL query checking. Given finite-state Kripke structure K and LTL query $\phi [{\texttt {var}}]$, we perform the following.

• 1. Construct Büchi (propositional) automaton $B_K$.

• 2. Construct Büchi query automaton $B_{\lnot \phi }[{\texttt {var}}]$.

• 3. Construct the product query automaton, $B_{K, \lnot \phi }[{\texttt {var}}]$.

• 4. Solve for shattering conditions for $B_{K, \lnot \phi }[{\texttt {var}}]$.

Because of Theorem 5 we know the following. If $\phi [{\texttt {var}}]$ is conjunctively covariant and ${\texttt {var}}$ is positive in $\phi [{\texttt {var}}]$, then ${\texttt {var}}$ is negative in $B_{K,\lnot \phi }[{\texttt {var}}]$, and the strongest solution for ${\texttt {var}}$ in $\phi [{\texttt {var}}]$ with respect to K coincides with the weakest shattering condition for $B_{K, \lnot \phi }[{\texttt {var}}]$. The dual result holds in case ${\texttt {var}}$ is negative in $\phi [{\texttt {var}}]$. Thus, solving for shattering conditions in $B_{K,\lnot \phi }[{\texttt {var}}]$ yields appropriate query solutions for K and $\phi [{\texttt {var}}]$.

6 Implementing an LTL Query Checker

Based on the developments given earlier in the paper, to develop a query checker for finite-state Kripke structures and LTL queries $\phi [{\texttt {var}}]$ it suffices to construct the product query automaton $B_{K,\lnot \phi }[{\texttt {var}}]$ and then search for $\gamma$ that shatter $B_{K,\lnot \phi }[{\texttt {var}}]$. In this section we highlight some of the algorithmic aspects of this strategy and report on preliminary results of a prototype implementation.

At the outset, we can note that there is one immediate algorithmic solution: enumerate $\gamma$ and test to see if $L(B[\gamma ]) = \emptyset$ by computing the strongly connected components of $B[\gamma ]$ and seeing if the start state can reach a successful component (i.e. one with an accepting state and at least one edge from the component back to itself). As there are $2^{2^{|\mathcal {A}|}}$ semantically distinct such $\gamma$, this procedure terminates; indeed, this is the basis of the approach outlined in [7]. The complexity of this approach is prohibitive, however, as a sample implementation of ours has shown: even Kripke structures with 10s of states and 10 atomic propositions failed to complete successfully. This is to be expected, given that there are $2^{2^{10}} \ge 1.75 \times 10^{308}$ semantically distinct propositions in this case.

Instead, the approach outlined below pursues two different strategies to reduce the computational effort associated with shattering. One involves exploiting the lattice structure of $2^{2^\mathcal {A}}$ to reduce the number of propositions that must be considered; the second combines this idea with a weakening of the problem to require the computation of a single shattering proposition, rather than all such propositions. The next sections provide further details regarding our approach.

6.1 Construct Büchi Automaton $B_{K}$

Given a Kripke structure K, constructing the corresponding Büchi automaton $B_{K}$ is done using the traditional method as described above. There is no query component to the model input, it should be noted.

6.2 Construct Büchi Query Automaton $B_{\lnot \phi }[{\texttt {var}}]$

The LTL3BA package performs translations from standard LTL formulas to Büchi propositional automata. For a given query $\phi [{\texttt {var}}]$ we convert the formula into a Büchi query automaton by treating ${\texttt {var}}$ as a normal atomic proposition. By default, LTL3BA attempts to remove non-determinism from the output Büchi query automaton, which can increase the number of edges in the automaton containing ${\texttt {var}}$ on their labels. We configure LTL3BA so that removal of non-determinism is not required in order to avoid this extra overhead.

6.3 Construct Product Query Automaton $B_{K, \lnot \phi }[{\texttt {var}}]$

As mentioned before, there is a well-known product construction for composing two Büchi automata into a single one accepting the intersection of the languages of the component automata. We adapt this composition operation to automaton $B_K$ and query automaton $B_{\lnot \phi }[{\texttt {var}}]$, yielding composite query automaton $B_{K,\lnot \phi }[{\texttt {var}}]$, as follows. States in $B_{\lnot \phi }[{\texttt {var}}]$ are pairs of states from $B_{K}$ and $B_{\lnot \phi }[{\texttt {var}}]$. Tuple $\left( \left( q_1, q_2 \right) , A \wedge \gamma [{\texttt {var}}], \left( q_1', q_2' \right) \right)$ is a transition in $B_{K,\lnot \phi }[{\texttt {var}}]$ iff $\left( q_1, A, q_1' \right)$ is a transition in $B_K$ and $\left( q_2, \gamma [{\texttt {var}}], q_2' \right)$ is a transition in $B_{\lnot \phi }[{\texttt {var}}]$. It should be noted that the transition label in this case, $A \wedge \gamma [{\texttt {var}}]$, has a special property: for any ${\texttt {var}}$, either $\llbracket A \wedge \gamma [{\texttt {var}}] \rrbracket = \{A\}$, or $\llbracket A \wedge \gamma [{\texttt {var}}] \rrbracket = \emptyset$. This is a consequence of the fact that our treatment of A as a proposition means that $\llbracket A \rrbracket = \{A\}$. The initial state of $B_{K,\lnot \phi }[{\texttt {var}}]$ is the pair consisting of the start states of $B_K$ and $B_{\lnot \phi }[{\texttt {var}}]$, respectively; states are accepting in $B_{K,\lnot \phi }[{\texttt {var}}]$ if and only if the state component coming from $B_{\lnot \phi }[{\texttt {var}}]$ is accepting.

6.4 Solve for Shattering Conditions of $B_{K, \lnot \phi }[{\texttt {var}}]$

Given $B_{K, \lnot \phi }[\gamma ]$, we now must find a proposition $\gamma$ such that $L(B_{K, \lnot \phi }[\gamma ]) = \emptyset$. One approach [7] is to enumerate all possible $\gamma$ and compute whether or not $L(B_{K, \lnot \phi }[\gamma ]) = \emptyset$ for each such $\gamma$. Because of the number of possible $\gamma$, this approach is infeasible for all but trivial $\mathcal {A}$.

Our approach instead focuses on determining when sets of edges in $B_{K, \lnot \phi }[{\texttt {var}}]$ can be shattered via a common proposition $\gamma$ in such a way that $L(B_{K, \lnot \phi )}[\gamma ])$ is empty. Our procedure may be summarized as follows.

• 1. Pre-process $B_{K, \lnot \phi }[{\texttt {var}}]$ to eliminate all strongly connected components that have no outgoing edges from the component and that do not contain any accepting states. Call the reduced query automaton $B'[{\texttt {var}}]$.

• 2. Identify all unique edge labels $S = \{\gamma _1[{\texttt {var}}], \ldots , \gamma _n[{\texttt {var}}]\}$ in $B'[{\texttt {var}}]$.

• 3. Process $\varGamma$ appropriately to determine how $B'[{\texttt {var}}]$ can be shattered.

We now expand on the last step of the above procedure. In this work our interest is only for LTL queries $\phi [{\texttt {var}}]$ in which ${\texttt {var}}$ appears only positively or only negatively; we do not consider queries in which ${\texttt {var}}$ is mixed. Based on the construction of $B_{K,\lnot {\texttt {var}}}[{\texttt {var}}]$ it follows that ${\texttt {var}}$ is either positive in all of the $\gamma _i[{\texttt {var}}]$ or negative in all of the $\gamma _i[{\texttt {var}}]$. In what follows we assume that ${\texttt {var}}$ is positive; the negative case is dual.

The first step in processing the $\gamma _i[{\texttt {var}}]$ (${\texttt {var}}$ is positive) is to determine if $\gamma _i[{\texttt {var}}]$ is shatterable, and if so, to compute its weakest shattering condition $\gamma _i'$. Propositional queries $\gamma _i[{\texttt {var}}]$ that are not shatterable are removed from future consideration, as they cannot contribute to shattering $B'[{\texttt {var}}]$. In what follows we assume that each $\gamma _i[{\texttt {var}}]$ is shatterable, with weakest shattering condition $\gamma _i'$.

The next step S is to search for subsets of S that, when all shattered, shatter $B'[{\texttt {var}}]$. More specifically, suppose $S' \subseteq S$ and $\gamma ''$ is such that $\gamma ''$ shatters each $\gamma '[{\texttt {var}}] \in S'$. In $B'[\gamma '']$ none of the edges labeled by elements of $S'$ would be present; if enough edges are eliminated, $L(B[\gamma '']) = \emptyset$, and $\gamma ''$ would shatter $B'[{\texttt {var}}]$. In this case we say that $S'$ shatters $B'[{\texttt {var}}]$. This search procedure is facilitated by the following observations.

• 1. If $S'$ shatters $B'[{\texttt {var}}]$ and $S' \subseteq S''$, $S''$ also shatters $B'[{\texttt {var}}]$.

• 2. If $S'$ does not shatter $B'[{\texttt {var}}]$ and $S'' \subseteq S'$, $S''$ does not shatter $B'[{\texttt {var}}]$.

These observations can be exploited to develop a modified breadth-first search (BFS) strategy for finding all minimal subsets of S that shatter $B'[{\texttt {var}}]$. The BFS algorithm maintains a work set, $W \subseteq 2^S$, of subsets of S that need processing. Initially, $W = \{\emptyset \}$. The algorithm then repeatedly does the following. It selects a minimum-sized $S' \in W$ and checks if $S'$ shatters $B[{\texttt {var}}]$. If it does, then it removes all supersets of $S'$ from W and adds $S'$ to the set of minimal shattering subsets of S. If it does not, then every superset of $S'$ that contains one more element than $S'$ is added to W. The procedure terminates when W is empty. Note that the approach does not add to W when $S'$ is found to be a shattering set; the correctness of this approach is based on the first observation above.

The BFS algorithm in the worst-case can still require examination of all subsets of S, so we also consider a different algorithm whose goal is to compute a single minimal shattering subset of S. This approach, which we call GREEDY_SET_SEARCH (GSS), first locates a (not necessarily minimal) shattering set using a depth-first search strategy as follows. The procedure maintains a set $R \subseteq S$ that is initially $\emptyset$. It then repeatedly checks to see if R shatters $B'[{\texttt {var}}]$; if so, it terminates, otherwise, it adds a new element from S into R. The observations above guarantee that the above procedure will terminate after at most |S| iterations. The second stage of the procedure then locates a minimal subset of the shattering set R returned by the first stage as follows. Each edge (except the last one added) is removed from R, and the set without this edge is checked for shattering. If the newly modified set $R'$, consisting of R with this single edge removed, shatters $B'[{\texttt {var}}]$ then the edge is permanently removed from R; otherwise, the edge is left in R. When this procedure terminates the resulting value of R is guaranteed to be a minimal shattering subset of S.

6.5 Implementation and Evaluation

We have developed prototype implementations of the BFS and GSS algorithms. Kripke structures are read in as directed graph data containing node labels, and LTL formulas are represented as simple strings. As stated previously, the LTL3BA routine was used to generate Büchi query automata from LTL queries.

For a proof-of-concept assessment of the techniques we use a modified version of NuSMV to extract the explicit Kripke structures from a sample .smv model files included in the NuSMV distribution. For each choice of model used, we considered property queries that were conceivably of interest based upon grounded properties known to be true of the systems already. These always took one of the following forms: ${{\mathrm{\mathbf {G}}}}a$, ${{\mathrm{\mathbf {G}}}}{{\mathrm{\mathbf {F}}}}a$ or ${{\mathrm{\mathbf {G}}}}\left( a \rightarrow {{\mathrm{\mathbf {F}}}}b\right)$. The models we considered in our evaluation are the following.

• Counter[k] - An implementation of a k-bit counter.

• Semaphore[k] - An implementation of a semaphore access control scheme for k different processes.

• Production cell - A production cell control model, first presented as an SMV model by Winter [20]. The original intent of this model concerned safety and liveness specifications.

Figure 2 contains relevant data about sizes of these models, and about the size of the Büchi query automata formed when composing the models with the query automaton $B_{\lnot {{\mathrm{\mathbf {G}}}}{\texttt {var}}}$. For our purposes, the following measures are relevant: (1) number of states, (2) number of transitions, (3) number of atomic propositions in the Kripke structure, (4) number of transition labels containing variable labels in the composite automaton, and (5) number of unique transition labels.

Fig. 2.

Statistics for Büchi product query automata when composed with ${{\mathrm{\mathbf {G}}}}({\texttt {var}})$.

Figure 3 contains performance data for both BFS and GSS. Algorithms were implemented in Java, and experiments were conducted on a single machine with a 3.5 GHz processor containing 32 GB of memory. Individual experiments were allowed to run for up to 2 h before being stopped and considered timed out. BFS yielded minimal success, as most datasets timed out. The GSS approach to find a single minimal shattering set proved much more effective.

Fig. 3.

Timing results for finding (a) all shattering sets via breadth first search, and (b) one minimal shattering set via GREEDY SET SEARCH. The number of total shattering queries that are made for each experiment are also reported. Query counts marked with a (*) are estimates based on our understanding of the models.

7 Conclusions and Directions for Future Research

In this paper we have considered the problem of query checking for Linear Temporal Logic (LTL). An LTL query checker takes a query, or LTL formula with a missing propositional subformula, together with a Kripke structure and computes a solution for the missing subformula. We have shown how this problem may be solved using automata-theoretic techniques that rely on the use of Büchi automata and the computation of so-called shattering conditions that make the languages of these automata empty. An implementation and preliminary performance data are also given.

As future work, we intend to fully develop the implementation and extend the experimental results we have so far. We also would like to extend the results to handle queries involving multiple missing subformulas, as well as ones in which the missing subformula can appear both positively and negatively. Finally, we would like to leverage relationships between different edge labels containing variables, such as in cases where one label implies another.