On-the-fly Construct Büchi Automata for LTL formulae

The previous post introduced the declarative construction, which is exponential. For instance, the LGBA for $p \mathbf{U} q$ has 8 states. However, on-the-fly construction can build Büchi automata for linear size. Surely, distinct automata can express the same language (further, the LTL formula).

Negative Normal Form

First we write LTL formulas into their NNF equivalence, which is composed by $\vee, \wedge, \mathbf{X}, \mathbf{U}, \mathbf{R}$ only. Negations are pushed down to literals. Here we quote some rules,

• $\neg \mathbf{X} \phi \Rightarrow \mathbf{X} \neg \phi$
• $\neg ( \phi \mathbf{U} \psi ) \Rightarrow (\neg \phi \mathbf{R} \neg \psi) $
• $\neg ( \phi \mathbf{R} \psi ) \Rightarrow (\neg \phi \mathbf{U} \neg \psi) $

Tableaux Expansion

• $\phi \mathbf{U} \psi \Rightarrow \psi \vee (\phi \wedge \mathbf{X}(\phi \mathbf{U} \psi)) $
• $\phi \mathbf{R} \psi \Rightarrow \psi \wedge (\phi \vee \mathbf{X}(\phi \mathbf{R} \psi)) $

Disjunctive Normal Form

With all formulas converted to the following form, each disjunct is a state.

$$\bigvee_i \bigg( \bigwedge_j I_{ij} \wedge \bigwedge_k \mathbf{X}\psi_{ik} \bigg)$$

Note $\bigwedge_j I_{ij}$ represents the labels, and $\bigwedge_k \mathbf{X}\psi_{ik}$ shows the transition. When the $\mathbf{X}$-formula is not present, we write $\mathbf{X} \top$.

Cover

A cover of a set of LTL formulas $\Psi= \{ \psi_1, \ldots, \psi_k \}$ calculates the set of initial states of Büchi automaton that represents $\bigwedge_i \psi_i$. A state is denoted as $\langle \lambda, \chi, \sigma \rangle$, which are the set of labels, the next formula, the set of subformulas of satisfied in $s$.

$$\mathsf{Cover}(\Psi) := \mathsf{Expand}(\Psi, \langle \emptyset, \emptyset, \emptyset \rangle)$$

Expand

We quote its definition. Assume $s=\langle \lambda, \chi, \sigma \rangle$, $l$ is a propositional literal, $\mathsf{Expand}(\Psi, s)=$

\begin{align*} \begin{cases} s & \Psi = \emptyset \\ \emptyset & \bot \in \Psi \\ \mathsf{Expand}(\Psi \backslash \top , s) & \top \in \Psi \\ \mathsf{Expand}(\Psi \backslash \{l\}, \langle \lambda \cup \{l\}, \chi, \sigma \cup \{l\} \rangle) & l \in \Psi \\ \mathsf{Expand}(\Psi \backslash \{\mathbf{X}\psi\}, \langle \lambda , \chi \cup \{ \psi \}, \sigma \cup \{\mathbf{X}\psi\} \rangle) & \mathbf{X}\psi \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_1, \psi_2\} \backslash \{\psi_1 \wedge \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \wedge \psi_2\} \rangle) & \psi_1 \wedge \psi_2 \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_1\} \backslash \{\psi_1 \vee \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \vee \psi_2\} \rangle) \cup \\ \mathsf{Expand}(\Psi \cup \{\psi_2\} \backslash \{\psi_1 \vee \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \vee \psi_2\} \rangle) & \psi_1 \vee \psi_2 \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_1\} \backslash \{\psi_1 \mathbf{U} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi \cup \{\psi_1 \mathbf{U} \psi_2\}, \sigma \cup \{\psi_1 \mathbf{U} \psi_2\} \rangle) \cup \\ \mathsf{Expand}(\Psi \cup \{\psi_2\} \backslash \{\psi_1 \mathbf{U} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \mathbf{U} \psi_2\} \rangle) & \psi_1 \mathbf{U} \psi_2 \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_2\} \backslash \{\psi_1 \mathbf{R} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi \cup \{\psi_1 \mathbf{R} \psi_2\}, \sigma \cup \{\psi_1 \mathbf{U} \psi_2\} \rangle) \cup \\ \mathsf{Expand}(\Psi \cup \{\psi_1, \psi_2\} \backslash \{\psi_1 \mathbf{R} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \mathbf{R} \psi_2\} \rangle) & \psi_1 \mathbf{R} \psi_2 \in \Psi \end{cases} \end{align*}

Construct $A_\phi$

With the above operations defined, we construct the Büchi Automaton for an LTL formula. $A_\phi = (Q, Q_0 , \Sigma, L, T , FT)$, with $Q_0 = \mathsf{Cover}(\{\phi\})$, $Q$ is the smallest set such that $Q_0 \subseteq Q$, also if $\langle \lambda, \chi, \sigma \rangle \in Q$, then $\mathsf{Cover}(\{\chi\}) \in Q$, the labeling function $L(s) = \{a \in \Sigma | a \models \lambda \}$, transition relation $T = \{(s,s') | s = \langle \lambda, \chi, \sigma \rangle \wedge s' \in \mathsf{Cover}(\{\chi\}) \}$, the fairness conditions $FT = \{F_1, \ldots, F_n\}$, where $F_i = \{s \in Q | \phi_i \mathbf{U} \psi_i \notin \sigma \vee \psi_i \in \sigma \}$.

Examples

Here we present the Büchi Automata built from the stated method.

Fig 1. NBA of $\mathbf{FG}p$

Fig 2. NBA of $p \mathbf{U} q$

References

1. R. Sebastiani, Automata-theoretic LTL Model Checking, slides on Formal Methods, 2012
2. Wikipedia, Linear temporal logic to Buchi Automaton, http://en.wikipedia.org/wiki/Linear_temporal_logic_to_Büchi_automaton

Appendix

The following is a copy of original copyright notice of slides which this article is quoting.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Translate LTL formulae into Büchi Automata

LTL formulae are translated in Labelled Generalized Büchi Automata (LGBA), where labels are moved into states. See a previous post (link).

$\omega$-automaton, $\omega$-word, $\omega$-language

An $\omega$-automaton is an automaton which accepts infinite inputs. Büchi Automata are a typical example. An $\omega$-word is an accepting run on an $\omega$-automaton, the set of all $\omega$-words accepted (defined) by an $\omega$-automaton is called an $\omega$-language.

The alphabet of a language is denoted as $\Sigma$, the set of all $\omega$-words composed by symbols in $\Sigma$ is denoted as $\Sigma^{\omega}$. A language recognizable (accepted) by an automaton $A$ is written $L(A)$. Usually we only work in automata that have $L(A) \subset \Sigma^{\omega}$.

$\omega$-regular

Recall that regular languages can be recognized by NFAs/DFAs (equivalent). It can also be generated by regular grammar (left linear or right linear, but not mixed).

A language is called $\omega$-regular when it is represented as $$\bigcup_{i=1}^n U_i(V_i)^{\omega}$$

we require that $U_i$, $V_i$ be regular languages. $L$ is $\omega$-regular iff it can be recognized by Nondeterministic Büchi Automata. The $\omega$-regular languages are closed under complementation (useful for constructing $A_{\neg\phi}$).

Closures

The closure of an LTL formula is intended to calculate its components (including their negations). For instance, a closure set of $p\mathbf{U}q$ is $$\{p, q, p\mathbf{U}q, \mathbf{X}(p\mathbf{U}q), \neg p, \neg q, \neg (p\mathbf{U}q), \neg (\mathbf{X}(p\mathbf{U}q))\}$$

Atoms

An atom $A$ is called a maximal consistent subset of the closure set. First we remove negations. In order to be consistent (agree on assignments), we should have $p,q \in A$ when we have $p \wedge q \in A$. Similarly, when we have $p\mathbf{U}q \in A$, we require either $q \in A$ or $\{p \in A, \mathbf{X}(p\mathbf{U}q)\} \subset A$.

LTL to LGBA

$A_{\phi} = (Q, Q_0, \Sigma, L, T, FT)$, respectively, the set of states Q is the the set of all atoms of $\phi$, the set of initial states $Q_0$ are the atoms where $\phi$ is included, $\Sigma$ is the power set of all free variables in $\phi$, namely the alphabet, labeling function $L$ maps a state to the set of free variables appeared in that state, transition relation is built from $\mathbf{X}$-formulas, say $(\mathbf{X}\psi, \psi) \in T$, $FT$ is a set of fair conditions $\{F_1, \ldots, F_n \}$, where $$F_i = \{ s \text{ is an atom} | \psi \mathbf{U} \phi \in s \vee \phi \in s \}$$

The above is on the condition that $\psi \mathbf{U} \phi$ appears positively in $\phi$. (see Polarity)

Example

One can calculate the atoms of $p \mathbf{U} q$ and other parameters by the stated method, thus its Büchi automaton.

Fig 1. $A_{p \mathbf{U} q}$ constructed by definition

On-the-fly Construction

The above construction is called declarative construction, though an alternative is present, considering its volume, it is to be introduced in another post.

References

1. R. Sebastiani, Automata-theoretic LTL Model Checking, slides on Formal Methods, 2012
2. Wikipedia, ω-automaton, https://en.wikipedia.org/wiki/Ω-automaton
3. Wikipedia, Linear temporal logic to Buchi Automaton, http://en.wikipedia.org/wiki/Linear_temporal_logic_to_Büchi_automaton

Appendix

The following is a copy of original copyright notice of slides which this article is quoting.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

LTL Model Checking - The Automata Approach

Let $M$ be a Kripke model, and $\psi$ be an LTL formula. The model checking problem is whether $$M \models \psi$$

It is rephrased in the manner of Büchi automaton for automatic reasoning. We express both the model and the formula in Büchi automata ($A_M$, $A_\psi$), then the model checking problem is to check whether the language of $A_M$ is contained by the language of $A_\psi$, that is, $\mathcal{L}(A_M) \subseteq \mathcal{L}(A_{\psi})$. In other words, whatever $A_M$ expresses is well captured in $A_\psi$. Further, if we negate $\psi$, then the containment becomes emptiness checking. i.e. $$\mathcal{L}(A_M) \cap \mathcal{L}(A_{\neg\psi}) = \varnothing$$

Büchi Automata

Unlike NFA/DFAs, Büchi automata have infinite words (aka. $\omega$-words). The "final" states are a set of accepting states, where a loop exists. A run on automata is an infinite execution of automaton, e.g., say the alphabet is $\Sigma = \{a,b\}$, $F=\{b\}$, a legal run can be $\rho = abbbbbb\cdots$.

Like NFA, Non-deterministic Büchi automata (NBA) have transition relations $\delta : Q \rightarrow Q $ as partial ($Q$ is the set of states), while the deterministic one total. But the subset construction from NFA to DFA doesn't apply here.

Compute $A_M$

Given a Kripke model $M$, we add an initial state, and move labels from states to incoming edges, every state becomes an accepting state. The fair version is to change the accepting states only to fair states.

Labelled Generalized Büchi Automata

We need to move the labels of Büchi Automata into states. LGBA features a set of fair conditions $FT = \{F_1, ..., F_k \}$, an accepting run must concord with all fair conditions. Formally, $$\forall i . \mathsf{inf}(\rho) \cap F_i \neq \varnothing$$ where $\mathsf{inf}$ calculates the accepting states of the run $\rho$, $F_i \subseteq Q$. Further, an LGBA has a set of initial states rather than only one in BA.

Translate LTL formulas into LGBA

This part is relatively big and it will be introduced in another post.

Synchronous Product of NBAs

Compared to synchronous product of NFAs, NBAs' product employs a tag $(1,2)$ specifying on which NBA it is running. The synchronous product is used to calculate the language intersection, $$\mathcal{L}(A_1 \times A_2) = \mathcal{L} (A_1) \cap \mathcal{L} (A_2)$$

Initial state of the product, $I = I_1 \times I_2 \times \{ 1 \}$, accepting states $F = F_1 \times Q_2 \times \{ 1 \}$, transition relations are defined such that a run on track 1 ends at one of its accepting states $F_1$, then moves on to track 2 until meeting some state in $F_2$, then it switches back. The product has such initial states and finite states to ensure that an infinite run of the product automaton must infinitely run on both $A_1$ and $A_2$.

Complement Büchi automata

The complementation involves conversion to Rabin automaton. This is to construct $A_{\neg\phi}$.

Emptiness Checking - Double nested DFS algorithm

The problem can be addressed as searching an accepting cycle reachable from an initial state. Double nested DFS algorithm employs two Hash tables, two stacks and two nested DFS routines. The following is routine 1,

DFS1(NBA A) {
  stack S1=I; stack S2=∅;
  Hashtable T1=I; Hashtable T2=∅;
  while (S1!=∅) {
    v=top(S1);
    if ∃w s.t. w∈ δ(v) && T1(w)==0 {
      hash(w,T1);
      push(w,S1);
    } else {
      pop(S1);
      if v∈F DFS2(v,S2,T2,A);
    }
  }
  return EMPTY;
}

The following is routine 2,

DFS2(state f, stack S, Hashtable T, NBA A) {
  hash(f,T);
  push(f,S);
  while (S!=∅) {
    v=top(S);
    if f∈ δ(v) return NOT_EMPTY;
    if ∃w s.t. w∈ δ(v) && T(w)==0 {
      hash(w);
      push(w);
    } else pop(S);
  }
}

DFS1 starts with the initial state, hashes each state on the path when visiting it for the first time. It invokes DFS2 when no more moves are possible and the top of stack is an accepting state. DFS2 tries to search a loop starting from this accepting state and going back to itself. When such a loop is found, it means $A$ is not empty, and the path is a combination of stack 1 and stack 2.

References

1. R. Sebastiani, Automata-theoretic LTL Model Checking, slides on Formal Methods, 2012

Appendix

The following is a copy of original copyright notice of slides which this article is quoting.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.