Notes on Model Checking

This is my notes on model checking based on Müller-Olm et al.’s Model Checking A Tutorial Introduction.

Basic Concepts

A model checker is a procedure that decides whether a given structure $M$ is a model of a logical formula $\phi$, i.e., whether $M$ satisfies $\phi$, abbreviated $M \models \phi$. Typically, $M$ is a finite automata-like structure, $\phi$ is drawn from a temporal or modal logic, and specifies the desirable property.

Models

Several approaches:

  • Kripke structures, notes are annotated with atomic propositions
  • Labeled transition systems (LTS), arcs are annotated with actions
  • Kripke transition systems (KTS), which combines Kripke structure and LTS
Kripke Structures

Definition: A Kripke structure over a set of atomic propositions $AP$ is a triple $(S, R, I)$, where $S$ is a set of states; $R \in S \times S$ is a transition relation; and $I: S \to 2^{AP}$ is an interpretation.

We assume $AP$ always contains propositions $true$ and $false$ and for any states $s$, $true \in I(s)$ and $false \notin I(s)$. A Kripke structure is total if $R$ is total; otherwise is partial. Usually, for model-checking purpose $S$ and $AP$ are finite.

Labeled Transition Systems

Definition: A LTS is a triple $T = (S, Act, \to)$, where $S$ is a set of states, $Act$ is a set of actions, and $\to \in S \times Act \times S$ is a transition relation.

$s \overset{a}{\to} s’$ is a transition from $s$ to $s’$ labeled by action $a$ and $s’$ is an $a$-successor of $s$. $S$ and $Act$ are usually finite.

Kripke Transition Systems

Definition: a KTS over a set of atomic propositions $AP$ is a a structure $T = (S, Act, \to, I)$, where $S$ is a set of states, $Act$ is a set of actions, $\to \in S \times Act \times S$ is a transition relation, and $I: S \to 2^{AP}$ is an interpretation. We assume $AP$ and $Act$ are disjoint.

KTS generalizes both Kripke structures and LTS: a Kripke structure is a KTS with an empty set of actions; a LTS is a KTS with a trivial interpretation $I$.

Logics

Two variants of temporal logics: linear-time and branching-time. Linea-time logics concerns properties of paths.

Propositional linear-time logic (PLTL)

PLTL formulas are interpreted over paths in a Kripke structure $K$ over $AP$. A finite path is a finite, non-empty sequence of states $s = \langle s_0, \cdots, s_{n-1} \rangle $, where $(s_i, s_{i+1}) \in R$ forall $0 \leq i < n-1$. $n$ is the length of a path, denoted by $|s|$. An infinite path is an infinite sequence $\langle s_0, s_1, \cdots \rangle$; the length of infinite path is $\infty$. For $0 \leq i < |s|$, $s_i$ denotes the $i$-th state, and $s^{i}$ denotes $\langle s_i, s_{i+1}, \cdots \rangle$. A path is called maximal if it cannot be extended.

The formulae are constructed as follows, where $p$ ranges over the set $AP$.

$$ \phi ::= p ~|~ \neg \phi ~|~ \phi_1 \vee \phi_2 ~|~ \texttt{X}(\phi) ~|~ \texttt{U}(\phi, \psi) ~|~ \texttt{F}(\phi) ~|~ \texttt{G}(\phi) $$

The semantics of PLTL are list as follows:

  • $s \models p$ iff $p \in I(s_0)$
Hennessy-Milner Logics
Fixpoints in Complete Lattices
Computational Tree Logic

Model Checking

Global vs Local Model-Checking
Overview of Approaches
Semantic Approach
Automata-Theoretic Appraoch
Tableau Appraoch