Specifying CTL Syntax in Isabelle/HOL

• Basic CTL (Computation Tree Logic) expresses properties on states in branching trees of computation.

• CTL formulae are constructed from atomic propositions \(p\) and the following connectives: \[\varphi ::= \mathsf{true}~|~p~|~\varphi \land \varphi~|~\neg \varphi~|~AX\varphi~|~EX\varphi~|~A\,\varphi\ \mathcal{U}\ \varphi~|~E\,\varphi\ \mathcal{U}\ \varphi\]

Understanding CTL Constructs

• The temporal quantifiers break down along two axes: \(A\) vs. \(E\):

• \(A\)-quantifiers quantify over all paths forward from the current state

• \(E\)-quantifiers quantify over some such path

• \(X\) vs. \(\mathcal{U}\) for temporal specification

• where \(X\) specifies the state immediately following the current state

• \(\mathcal{U}\) asserts that some property holds at all points along a path until the first point at which some other property holds.

Adding Past-time

• The derived operators \(AF\), \(EF\), \(AG\), and \(EG\) are also often used:

  \[\begin{array}{l} AF\ \varphi \triangleq A\ \mathsf{true}\ \mathcal{U}\ \varphi \quad \quad EF\ \varphi \triangleq E\ \mathsf{true}\ \mathcal{U}\ \varphi \quad \quad\\ AG\ \varphi \triangleq \neg EF\ \neg\varphi\quad \quad EG\ \varphi \triangleq \neg AF\ \neg\varphi \end{array}\]

• Intuitively,

• \(AF\ \varphi\) (likewise \(EF\)) expresses the property that along all (some) paths, eventually (at some point now or in the future) \(\varphi\) will hold,

• \(AG\ \varphi\) (likewise \(EG\)) expresses the property that along all (some) paths \(\varphi\) will always hold.

Adding Past-time

• Our formulation of past-time CTL treats past-time operators is symmetric to future-time operators: \[\varphi ::= \ldots~|~A\,\varphi\ \mathcal{B}\ \varphi~|~E\,\varphi\ \mathcal{B}\ \varphi\]

Semantics of CTL

• Formally, the satisfaction of a CTL formula is defined with respect to a transition system \(\mathcal{G}\) (i.e. directed graph) and a state \(q\) in that transition system.

• We write \(\mathsf{Paths}(\mathcal{G}, q)\) to denote the set of (linear, non-branching) paths forward from \(q\) in \(\mathcal{G}\),

  • where a path from \(q\) is simply a sequence of states \(q_0\ q_1\ ...\) such that \(q_0 = q\) and for all \(i\), \((q_i, q_{i+1})\) is a valid transition (edge) in \(\mathcal{G}\).

  • We write \(\lambda_i\) to indicate the \(i_{th}\) element of a path \(\lambda\).

Semantic Rules of CTL (1)

The CTL satisfaction relation \(\mathcal{G}, q \models \varphi\) is defined as follows:

• \(\mathcal{G}, q \models \mathsf{true}\)

• \(\mathcal{G}, q \models p\) if \(p\) holds at \(q\)

• \(\mathcal{G}, q \models \varphi \land \psi\) if \(\mathcal{G}, q \models \varphi\) and \(\mathcal{G}, q \models \psi\)

• \(\mathcal{G}, q \models \neg\varphi\) if it is not the case that \(\mathcal{G}, q \models \varphi\)

Semantic Rules of CTL (2)

The CTL satisfaction relation \(\mathcal{G}, q \models \varphi\) is defined as follows:

• \(\mathcal{G}, q \models AX\varphi\) if \(\forall \lambda \in \mathsf{Paths}(\mathcal{G}, q).\ \mathcal{G}, \lambda_1 \models \varphi\)

• \(\mathcal{G}, q \models EX\varphi\) if \(\exists \lambda \in \mathsf{Paths}(\mathcal{G}, q).\ \mathcal{G}, \lambda_1 \models \varphi\)

• \(\mathcal{G}, q \models A\,\varphi\ \mathcal{U}\ \psi\) if \(\forall \lambda \in \mathsf{Paths}(\mathcal{G}, q).\ \exists i.\ \mathcal{G}, \lambda_i \models \psi\) and \(\forall j<i.\ \mathcal{G}, \lambda_j \models \varphi\)

• \(\mathcal{G}, q \models E\,\varphi\ \mathcal{U}\ \psi\) if \(\exists \lambda \in \mathsf{Paths}(\mathcal{G}, q).\ \exists i.\ \mathcal{G}, \lambda_i \models \psi\) and \(\forall j<i.\ \mathcal{G}, \lambda_j \models \varphi\)