6.5.2 Predicates and CTL model checking

In this section, you will find a short introduction into the syntax and semantics of CTL (Computational Tree Logic), and a description of the state predicates used in INA .

Subsections

• State predicates
• Model checking
• Syntax of CTL
• Semantics of CTL
• Equivalences and further notes

State predicates

During the computation of minimal paths (see chapter 6.5.3 on page ff), the reachability analysis (see under ``bad'' predicate on page in chapter 6.5.4), and the model checking (see on page ff in chapter 6.5.4), INA works with state predicates.

A predicate is a disjunction of conjunctions of possibly negated atoms (disjunctive normal form). An atom consists of a statement of the form

$low \leq value \leq upp$ (where $0\leq low\leq upp\leq \infty$)

As an example for the state predicates used in INA , value=number of tokens on a place; an atom $p_1:\;low=1,\;upp=2;$ is then satisfied by all states in which place p₁ contains one or two tokens. For clocked transitions, restrictions of the clock positioning can be formulated in the same way.

When a predicate is requested at the predicate input file prompt, you can switch to the terminal mode by pressing <esc> . If so, enter the first conjunction of atoms: After entering a place number, the lower and upper bounds are asked for (lower bound, upper bound). With <o> , you can enter unbounded above. You can negate the atom or not (negate the atom?), and then enter another state number, or quit the current conjunction with <Q> . When working with time allocation, further state atoms can be defined with respect to time restrictions.

If you answer the question next conjunction with <Y> , you get to the definition of the next conjunction of (possibly negated) atoms.

Predicates are saved in files with the extension .pdc.

In chapter 6.5.4 on page ff, you find a set of functions with which certain predicates can be generated automatically. In the atomic mode described there, simpler atoms, which represent the alternative whether a place is marked or not, can also be used as predicates.

Model checking

Testing the validity of CTL-formulae in the initial state is called model checking. Thereby, witnesses for existence-quantified sub-formulae, and counter examples for all-quantified sub-formulae can be determined and displayed. On the computation procedure and the entering of formulae, see chapter 6.5.4 on page ; on the implementation, see [Hel96].

Model checking is based on the structure M=[S,R,P] of a labelled state transition graph where

• S is an finite state set
• R is a binary relation on S ( $R\subseteq S\times S$), which describes the possible state transitions. This relation is assumed to be total: for every state s, there exists a state $s'\in S$ with $(s,s')\in R$.
• P is a mapping from the state set onto the power set of the predicates.

  For a given state, this mapping yields the set of predicates which are satisfied in it.

Syntax of CTL

The syntax of CTL-formulae is defined inductively:

• Each predicate p is a CTL-formula.
• If f₁ and f₂ are formulae, then so are
  • $\neg f_1$, $(f_1 \wedge f_2)$ and $(f_1 \vee f_2)$
    (logical connectors)
    
  • $EX\,f_1$, $EF\,f_1$, $EG\,f_1$, $AX\,f_1$, $AF\,f_1$, $AG\,f_1$, $E[f_1\,U\,f_2]$, $A[f_1\,U\,f2]$, $E[f_1\,B\,f_2]$, $A[f_1\,B\,f2]$
    (temporal-logical quantors)

Semantics of CTL

A path is an infinite sequence of states $(s_0,s_1,\ldots)$, so that $(s_i,s_{i+1})\in R$ holds for all i.

The relation $M,s_0\models f$ means that the CTL-formula f is satisfied in the state s₀ within the given structure M.

We use the following inductive definition of $\models$:

• $M,s_0\models p$ iff $p\in P(s_0)$
• $M,s_0\models \neg f$ iff not $M,s_0\models f$
• $M,s_0\models (f_1 \wedge f_2)$ iff $M,s_0\models f_1$ and $M,s_0\models f_2$
• $M,s_0\models EX\, f$ iff for a state s' with $(s_0,s')\in R$, $M,s'\models f$

  There exists an immediate post-state in which f is satisfied.

• $M,s_0\models A[f_1\,U\,f_2]$ iff for all paths $(s_0,s_1,\ldots)$, there exists an $i\geq 0$ with $M,s_i\models f_2$, and $M,s_j\models f_1$ holds for all $0\leq j < i$

  Along all paths, f₁ is satisfied until a state is reached which satisfies f₂.

• $M,s_0\models E[f_1\,U\,f_2]$ iff for a path $(s_0,s_1,\ldots)$, there exists an $i\geq 0$ with $M,s_i\models f_2$, and $M,s_j\models f_1$ holds for all $0\leq j < i$

  There exists a path, along which f₁ is satisfied until a state is reached which satisfies f₂

• $M,s_0\models A[f_1\,B\,f_2]$ iff for all paths $(s_0,s_1,\ldots)$, there exists an $i\geq 0$ with $M,s_i\models f_2$, and $M,s_j\models f_1$ holds for a $0\leq j < i$ On all paths, f₁ is satisfied at least once, before a state is reached, which satisfies f₂
• $M,s_0\models E[f_1\,B\,f_2]$ iff for at least one path $(s_0,s_1,\ldots)$, there exists an $i\geq 0$ with $M,s_i\models f_2$, and $M,s_j\models f_1$ holds for a $0\leq j < i$ There exists a path along which f₁ is satisfied at least once, before a state is reached which satisfies f₂

The entering of CTL-formulae is described in chapter 6.5.4 on page ff.

Equivalences and further notes

Among others, the following equivalences hold:

• $AX(f)\equiv \neg EX(\neg f)$

  f is satisfied in all post-states

• $AF(f)\equiv A[True\,U\,f]$ f is satisfied on every path in the future
• $EF(f)\equiv E[True\,U\,f]$

  There exists a path which leads to a state in which f is satisfied

• $AG(f)\equiv \neg EF(\neg f)$

  f is satisfied in every state on all paths

• $EG(f)\equiv \neg AF(\neg f)$ There exists a path where f is satisfied in every state

The semi-formal significance of the individual quantors is underlined by the symbols used: E stands for ``exists'', A for ``always'', X for ``next'', U for ``until'', B for ``before'', F for ``forward'', and G for ``globally''.