CTL Model Checking

Fixed-point Theory

Complete Lattice

Complete lattice is a partially-ordered set which has join ($\cup$) and meet ($\cap$) operators. The former generates the least lower bound and the latter the greatest upper bound. The state space of a Kripke model forms a complete lattice under containment, i.e. $(2^S, \subseteq)$ is a complete lattice.

Monotonic Function

$F$ is monotonic if $\forall a < b$, $F(a) < F(b)$.

Tarski's Theorem

A monotonic function over a complete lattice has the least and the greatest fixed point.

Kleene's Theorem

The mentioned fixed points can be calculated this way. Assume $F$ is a monotonic function and $\cup$-continuous (increments), the least fixed point must be reached (this chain converges): $$\emptyset \subseteq F(\emptyset) \subseteq F(F(\emptyset)) \subseteq \ldots$$

Instead, if $F$ is $\cap$-continuous (decrements), the greatest fixed point is obtained by, $$S \supseteq F(S) \supseteq F(F(S)) \supseteq \ldots$$

Formula Rewriting

All CTL formulae can be rewritten in terms of $\neg, \wedge, \mathbf{EX}, \mathbf{EU}, \mathbf{EG}$ only.

• $\mathbf{AG}\phi = \neg \mathbf{EF} \neg \phi$
• $\mathbf{EF}\phi = \mathbf{E}(\top \mathbf{U} \phi)$
• $\mathbf{A}(\phi_1 \mathbf{U} \phi_2 ) = \neg \mathbf{E}(\neg \phi_2 \mathbf{U} (\neg \phi_1 \wedge \neg \phi_2 )) \wedge \neg \mathbf{EG}\neg \phi_2$
• $\mathbf{AX} \phi = \neg \mathbf{EX} \neg \phi$

Although irrelevant at this context, but it is worthy to note that $\mathbf{EG}\phi = \mathbf{E}(\bot \mathbf{R} \phi)$, this is to say $\phi$ is never released (has to be true forever).

Tableaux Rules

• $\mathbf{EF}\phi = \phi \vee \mathbf{EXEF}\phi$
• $\mathbf{EG}\phi = \phi \wedge \mathbf{EXEG}\phi$
• $\mathbf{E}(\phi \mathbf{U} \psi) = \psi \vee (\phi \wedge \mathbf{EXE}(\phi \mathbf{U} \psi))$

Pre-Image

In CTL model checking, the calculating unit is a set of states that satisfy some formula $\phi$, noted as denotation $[\phi]$. Pre-Image maps the image (in the range) back to the domain (its pre-image). It is thus defined, $$\mathsf{PreImage}([\phi]) = \{s | \exists (s, s') \in R \wedge s' \in [\phi]\}$$

$\mathsf{PreImage}$ is a monotonic function over the complete lattice $(2^S, \subseteq)$, thus Kleene's theorem applies. Pre-Image matches the idea of $\mathbf{EX}$, i.e. $[\mathbf{EX}\phi]$ is the pre-image of $[\phi]$.

Fixed points for CTL Model Checking

According to tableaux rules, $\mathbf{EG}$, $\mathbf{EF}$, $\mathbf{EU}$s are written in the form of fixed points ($\nu$: greatest, $\mu$: least.).

• $[\mathbf{EG}\phi] = \nu Z. ([\phi] \cap [\mathbf{EX}Z])$
• $[\mathbf{EF}\phi] = \mu Z. ([\phi] \cup [\mathbf{EX}Z])$
• $[\mathbf{E}(\phi \mathbf{U} \psi)] = \mu Z. ([\psi] \cup ([\phi] \cap [\mathbf{EX}Z]))$

So given a CTL formula $\phi$, after rewriting, we apply the set operations for negations (complement the set) and disjunctions (union), and fixed points for temporal formulas. We say $M \models \phi$ iff $I \subseteq [\phi]$.

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.

Conflict-Driven Backtracking and Clause-Learning

See appendix for credits.

Conflict-Driven backtracking is a huge advancement to the classical chronological backtracking applied to the DPLL algorithm. It solves the Boolean formulas with about $10^7$ variables.

State of the art

The idea was to learn from error. When we see a conflict, we find the cause (building a conflict set), and we go back to the decision point where we could do it differently if we have had known this conflict set. It seems hard to catch for a machine. However, it is operable through the following algorithm. This is the most advanced modern approach in many SAT solvers.

Deciphering the myth

Data structure: stack partitioned into decision levels. Each level comprises of a decision literal and its implied literals (unit-propagated). Every implied literal is tagged with the clause causing its unit propagation (aka. antecedent clause).

One level in the stack can be depicted by an implication graph, where there are nodes and edges. A node without edges means a decision literal , because an edge is are marked with the antecedent clause of the literal. E.g.,

Fig. 1 An Implication Graph (Shown on Right)

Building the conflict set

It has two steps,

1. C := conflicting clause
2. repeat {
      C <- resolve C with the antecedent clause of the last
      unit-propagated literal in C
}
until { C verifies some termination criteria }

Well, we wonder what this "resolve" mean, it is a disjunction but removing $A_i \vee \neg A_i$ since they become true. Resolution is a rule saying two input clauses entails the output clause (aka. resolvent). For a detailed discussion, see Resolution (logic). By performing this, the unit propagation is undone. What about some termination criteria? Here comes the magic.

1st UIP

It means First Unique Implication Point, this is the state-of-the-art strategy. It is the first point where we find only one literal of current decision level in C. For instance (built from the same example above),

Fig. 2 Conflict set construction

Upon this, we build the conflict set: $\{ \neg A_{10} , \neg A_{11} , A_4 \}$, and "learn" (add) a new clause $c_{10} := A_{10} ∨ A_{11} ∨ \neg A_4$. Now that we reached the conflict, also we know these $\neg A_{10}$, $\neg A_{11}$ can not survive with $A_4$, so we backtrack to $\neg A_{11}$, and right there we assign $\neg A_4$. Yes, we cut off all paths to $A_4$ from that point on. We would never fall into this conflict set again (we learned from the error).

Drawbacks and a solution

We saved all these learned clauses, on a larger scale ($10^7+$), we can reach an exhaustion of space. The solution is to keep only the active ones, i.e. the ones showed up (on the edges of implication graph) in the current decision level.

Fig. 3 The breath-taking jump

---

Appendix

The following is a copy of original copyright notice of slides where the images here were taken.

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.

Region Automata and Zone Automata

As a sequel of a previous article on timed automaton (link), here we introduce its computational models.

1. Region

Why region automata? Timed automata have infinite state space (time be divided into infinite pieces), region automata give a finite partition of timed automata such that the computation becomes possible.

Intuition A region is a set of equivalent states. The partition divides the state space into different equivalent classes (regions).

Temporal constraint given by this grammar $\phi := x > c | x < c | x = c | \phi \wedge \phi$, $c$ must be an integer constant (to ensure non-zenoness)

Equivalent class The set of states which satisfies the same set of temporal constraints.

Region equivalence states are equivalent due to being in the same region, they are either within the integer grid, on the $x=c$ or $y=c$ axes, or above/below the diagonal of the integer grid. (see Figure 1.)

Fig 1. Regions as equivalent classes

Remind that largest constant relevant $c$ is actually the ceiling of $x_i$, i.e. $c = \lceil x_i \rceil$. Figure 2 is an example of partitions (regions) of the state space of a timed automaton. Not only are those shadowed areas regions, but also segments of lines (they usually are a result of clock resetting).

Fig 2. Regions on a 2-clock timed automaton

A further example Figure 3 shows the region representation of a simple timed automaton. Location $F$ is shadowed since it may loop forever, a bad design (livelock).

Fig 3. Timed automaton represented in regions

Time-abstract bisimulation If $w \simeq v$, $w,v \in l$, 1) after action $a$, $w'$ is in the region of location $l'$, so is $v'$; 2) $\forall d \exists d' . w+d \simeq v+d'$. They are respectively the transition on action and the transition on delay.

Region equivalence relation is a time-abstract bisimulation ($\simeq$).

Region reset The clock for all equivalent states is reset, hence the operation projects the whole region onto the clock axis (i.e. a line of shadow).

2. Zone

Why zone automata? Regions are still too many, we can force them collapse into unions of regions, where the unions are convex, i.e. no angles are larger than 180 degrees.

Zone Zones are so-called symbolic state (conjunction of regions). Formally, $Z = (s, \varphi)$, that is to start from a location (state) $s$ in a timed automaton, we make a conjunction of regions specified by temporal constraint $\varphi$.

Zone automaton A transition system for zones. Formally, $Z = (Q, Q^0, \Sigma, R)$, set of zones, initial zone, set of transition labels, transition relation.

Symbolic transition It may involve operations such as intersection (conjuncts), delay (stretches diagonally as x,y propagate in time simultaneously), reset (projects a shadow on the time axis). For a zone $Z = (s, \varphi)$, the transition is denoted as $\mathsf{succ}(\varphi, e)$, where $e$ is the label of switch. When $e$ is executed, $Z$ propagates by time till the time constraint $\varphi$ is met. The action is thus invoked. Proceed with a reset if it is needed.

Fig 4. Transitions on Zone Automaton

Figure 4 showed a symbolic transition from location n to m, i.e. $(n, 1 \leqslant x \leqslant 4, 1 \leqslant y \leqslant 3) \rightarrow (m, x>3,y=0)$

References

1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012, link

Appendix

The most of this post is heavily extracted from the RS's teaching slides, hence I don't claim the copyright. The character of this post is intended to be a note, with marginal and personal remarks. For those who need to respect the source, please refer the link in the references.

A Glimpse of Timed Automata

Terms

Timed Automaton Intuitively, an automaton with clocks, the transitions from state to state are constrained by time. Formally, $A = (L, L^0, \Sigma, X, I, E)$, respectively the set of locations (states), the set of initial locations, labels, clocks, invariants, the set of edges (transitions) $$E = \{ (s, a, \varphi, \lambda, s') | s,s' \in L, a \in \Sigma, \varphi \text{:clock constraints}, \lambda \subseteq X \}$$

Clock a stopwatch in this context, i.e. clocks are to measure the elapsed time, it can be reset.

Guard Boolean comparison between the clock and some integer value, serves as a constraint for the switch from one location to another

Action the label of transition, used to synchronize actions among several timed automata

Reset set the clock to time 0 and meanwhile the clock starts ticking again

Invariant a time constraint residing inside the state which must be respected when staying within such state, otherwise, it must move out.

Deadlock cases are, there are no more allowed moves (due to bad design of automata).

Example

We quote an automaton from this slide ^[1],

Figure 1. An Example Timed Automaton

• $s_i$'s are state labels
• two clocks present $x$, $y$
• after action $a$, it can only stay in $s_1$ for no more than $1$ time unit
• action $d$ can occur only when clock $y$ reads more than $2$ (due to the guard $y>2$)

References

1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012

Abstraction in Model Checking

Finite Transition System $M = (S, I, R, L)$, respectively the set of states, the set of initial states, the set of transition relations, labels. Simply put, a computational model, similar to Finite State Machine.

Which Computation? Well, model checking. $M \models \varphi$

Why abstraction? Too many states to compute and the abstraction reduces the number of states.

Why abstraction works? The existential-quantified properties (ECTL) are preserved after the abstraction ($M$ simulates $M'$, i.e., $M$ has whatever $M'$ has), that is, $M' \models \varphi \rightarrow M \models \varphi$. (But not vice versa!)

Now let's go to terms.

Abstraction function $h: S \rightarrow S'$

Simulation $M$ simulates $M'$ when each transition of $M'$ has a corresponding one in $M$. The simulation is the set of pairs of states $p \subseteq \{ (s,s') | s \in S, s' \in S' \}$ that records such behavior. It is the set denotation of the abstract function $h$.

Bisimulation The simulation applies on both sides. According to property preservation, $M \models \varphi \rightarrow M' \models \varphi$. As a consequence, $M \not \models \varphi \rightarrow M' \not \models \varphi$, otherwise we reach a contradiction.

$M$ simulates $M'$, plainly put, $M$ is an abstraction (simulation) from $M'$.

What about universal-quantified properties? (in LTL or ACTL) They are preserved when $M'$ simulates $M$. That is, $$M' \models \varphi \rightarrow M \models \varphi$$ Yes, same conclusion but different condition. Still, the reverse doesn't hold.

Exercise

Credit: ~rseba, disi.unitn.it

If we draw a relation $p = \{(S_{ij}, T_i) | \text{for all possible } i,j \}$, we see (with effort) that $p$ is a simulation from $M$ to $M'$ (i.e. $M'$ simulates $M$). Verify it by the rigorous definition, if $(S_{11}, T_1) \in p$, $(S_{11}, S_{12}) \in R_M$, $\exists (T_1, T_1) \in R_{M'}$ s.t. $(S_{12}, T_1) \in p$. So are the rest transition relations of $M$. Hence, the universal-quantified property preservation applies. e.g. if $\varphi$ is pure boolean, $$M' \models \mathbf{AG} \varphi \rightarrow M \models \mathbf{AG} \varphi$$

To note that the reverse doesn't hold. For instance, $(S_{13}, T_1) \in p$, $(T_1, T_1) \in R_{M'}$, $\forall j. \nexists (S_{13},S_{1j}) \in R_{M}$ s.t. $(S_{1j},T_1) \in p$.

Clarke-Emerson Theorem

The theorem gives CTL formula an iterative interpretation of their denotational semantics. \begin{align*} [\mathbf{EG} \phi] &= \nu z. ([\phi] \cap [\mathbf{EX} z]) \\ [\mathbf{E}(\phi \mathbf{U} \psi)] &= \mu z. ([\psi] \cup ([\phi] \cap [\mathbf{EX}z])) \\ [\mathbf{EF} \phi] &= \mu z. ([\phi] \cup [\mathbf{EX} z] \end{align*}

Appendix

• $[\mathbf{EX} \phi]$ is the existential pre-image of $[\phi]$.
• $\nu z. F z$ calculates the greatest fixed point.
• $\mu z. F z$ calculates the least fixed point.
• $\mathbf{EF} \phi = \mathbf{E}(\top \mathbf{U} \phi)$