Starting Planning a Project in Isabelle

• Pick a topic

• Pick a result you wish to prove in Isabelle inthat topic

• What definitions do you need to state the result?

• What background theories do you need to have those definitions and associated theorems?

• Look for Libraries and entries in Archive of Formal Proofs

Problems with Libraries and Entries

• Definitions are not what you expected

  • Do they fit?

  • What wrappers (definitions and lemmas) will convert it to what you need?

  • What additional theory (definitions and theorems) do you need for your use?

• Should you build your own?

  • Plus: Better fit (maybe?)

  • Minus: More work (maybe?)

After Basics: Then What?

• Outline the proof

• What major Lemmas do you need?

  • Should your project be one of those instead?

• Outline (on paper) what you think the proof sketch is

• Get help from the class

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\in{AP}\) 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\]

Semantics of CTL - Transition System

More formally, the satisfaction of a CTL formula is defined with respect to:

• a transition system \((V,E)\) (i.e. verticies and edges of a directed graph) such that \(\forall u\in V. \exists v\in V. (u,v)\in E\)

• a predicate \(\mathcal{I}(p,v)\) where \(p\in AP\) and \(v\in V\) saying whether the proposition \(p\) is true in state/node/vertex \(v\) (where the set \(AP\) is the set of atomic propositions underlying the syntax of the CTL formulae).

• a specific state \(q\in V\) (where the CTL formula is claimed to hold).

  • \(u\) will be \(v\) when there is no place to go after \(u\)

Semantics of CTL - Paths

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

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

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

Semantic Rules of CTL (1)

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

• \((V,E), \mathcal{I}, q \models \mathsf{true}\)

• \((V,E), \mathcal{I}, q \models p\) if \(\mathcal{I}(p,q) = \mathrm{true}.\)

• \((V,E), \mathcal{I}, q \models \varphi \land \psi\) if \((V,E), \mathcal{I}, q \models \varphi\) and \((V,E), \mathcal{I}, q \models \psi\)

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

Semantic Rules of CTL (2)

Let \(AP\) be the set of atomic propositions underlying the CTL syntax. The CTL satisfaction relation \((V,E), \mathcal{I}, q \models \varphi\) is defined as follows:

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

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

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

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

Model Checker

• A model checker is a function / algorithm that inputs a model \(((V,E), \mathcal{I}, q)\) and a CTL formula \(\varphi\) and decides whether \((V,E), \mathcal{I}, q \models \varphi\).

• Will look at algorithm by E. A. Emerson, E. M. Clarke and A. P.Sistla described in “Automatic verification of finite-state concurrent systems using temporal logic specifications”

• Only outline given.

• Slides below quoted or paraphrased from this paper

Model Checker Background

• Alogrithm runs by recursion on the structure of CTL formula being checked.

• Assumes functions \(\texttt{arg1}\) and \(\texttt{arg2}\) giving the immediate leftmost subformula, and rightmost subformula (if it exists)

• Labels each state with all subformulae of the given formula that are modeled (satisfied) at that state.

Constructs used by Model Checker

• \(\texttt{labels}(s)\)) gives the set of subformulae true at \(s\).

• \(\texttt{labeled}(s,f) = \mathrm{true}\) if \(f\in\texttt{labels}(s)\).

• \(\texttt{add\_label} (s, f)\) adds formula \(f\) to the current label of state \(s\).

• \(\texttt{marked}(s)\) gives whether state \(s\) has been visited

• \(\texttt{ST}\) is a variable holding a stack of states making the current path for checking \(f\).

• \(\texttt{stacked}(s)\) indicates whether state \(s\) is currently on the stack \(\texttt{ST}\).

Code for label-graph

Model Checker search procedure au, \(s\) visited

• The recursive procedure \(\texttt{au}( f, s, b)\) performs the search for formula \(f\) from state \(s\)

• When \(\texttt{au}\) terminates, the boolean result parameter \(b\) will be set to \(\mathrm{true}\) iff \(s \models f\).

• \(\texttt{ST}\) holds the sequence of states previously visited while searching for \(f\).

  • Assume \(f=A\,f_1\ \mathcal{U}\ f_2\). Thus, \(\texttt{arg1}(f)=f_1\) and \(\texttt{arg2}(f)=f_2\).

  • For all \(u\in\texttt{ST}\) we have \(u\models f_1\) but \(u\not{\models} f_2\)

• If \(\texttt{marked}(s)\) and \(s\) is already labeled with \(f\), then set \(b\) to \(\mathrm{true}\) and return.

• If \(\texttt{marked}(s)\) but \(s\) is not labeled with \(f\), we found a cycle where for all states in cylce \(f_1\) holds but not \(f_2\) and hence not \(f\). Set \(b\) to \(\mathrm{false}\) and return.

Code for \(\texttt{au}( f, s, b)\) (\(s\) previously visited)

Model Checker search procedure au (\(s\) not visited)

• If not \(\texttt{marked}(s)\), mark \(s\) as visited.

• If \(f_2\) is true at \(s\), \(f\) is true at \(s\). Add \(f\) to the label at \(s\) and return true.

• If both \(f_1\) and \(f_2\) are false at \(s\), \(f\) is false at \(s\), so return false.

Code for \(\texttt{au}( f, s, b)\) (\(s\) not visited)

Code for \(\texttt{au}( f, s, b)\) (\(f_1\) holds, not \(f_2\))

• Check whether \(f\) holds at all successor states of \(s\)

• If \(f\) does not hold at successor state \(s_1\), \(f\) does not hold at \(s\)

  • remove \(s\) from stack \(\texttt{ST}\), return \(\textrm{false}\).

• If \(f\) holds at all successor states,

  • remove \(s\) from stack \(\texttt{ST}\), label \(s\) with \(f\), return \(\textrm{true}\).

Code for \(\texttt{au}( f, s, b)\) (\(s\) not visited)