Theory CTL

(*<*)theory CTL imports Base begin(*>*)

subsection‹Computation Tree Logic --- CTL›

text‹\label{sec:CTL}
\index{CTL|(}%
The semantics of PDL only needs reflexive transitive closure.
Let us be adventurous and introduce a more expressive temporal operator.
We extend the datatype
‹formula› by a new constructor
›
(*<*)
datatype formula = Atom "atom"
                  | Neg formula
                  | And formula formula
                  | AX formula
                  | EF formula(*>*)
                  | AF formula

text‹\noindent
which stands for ``\emph{A}lways in the \emph{F}uture'':
on all infinite paths, at some point the formula holds.
Formalizing the notion of an infinite path is easy
in HOL: it is simply a function from typ‹nat› to typ‹state›.
›

definition Paths :: "state ⇒ (nat ⇒ state)set" where
"Paths s ≡ {p. s = p 0 ∧ (∀i. (p i, p(i+1)) ∈ M)}"

text‹\noindent
This definition allows a succinct statement of the semantics of const‹AF›:
\footnote{Do not be misled: neither datatypes nor recursive functions can be
extended by new constructors or equations. This is just a trick of the
presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define
a new datatype and a new function.}
›
(*<*)
primrec valid :: "state ⇒ formula ⇒ bool" ("(_ ⊨ _)" [80,80] 80) where
"s ⊨ Atom a  =  (a ∈ L s)" |
"s ⊨ Neg f   = (~(s ⊨ f))" |
"s ⊨ And f g = (s ⊨ f ∧ s ⊨ g)" |
"s ⊨ AX f    = (∀t. (s,t) ∈ M ⟶ t ⊨ f)" |
"s ⊨ EF f    = (∃t. (s,t) ∈ M* ∧ t ⊨ f)" |
(*>*)
"s ⊨ AF f    = (∀p ∈ Paths s. ∃i. p i ⊨ f)"

text‹\noindent
Model checking const‹AF› involves a function which
is just complicated enough to warrant a separate definition:
›

definition af :: "state set ⇒ state set ⇒ state set" where
"af A T ≡ A ∪ {s. ∀t. (s, t) ∈ M ⟶ t ∈ T}"

text‹\noindent
Now we define term‹mc(AF f)› as the least set term‹T› that includes
term‹mc f› and all states all of whose direct successors are in term‹T›:
›
(*<*)
primrec mc :: "formula ⇒ state set" where
"mc(Atom a)  = {s. a ∈ L s}" |
"mc(Neg f)   = -mc f" |
"mc(And f g) = mc f ∩ mc g" |
"mc(AX f)    = {s. ∀t. (s,t) ∈ M  ⟶ t ∈ mc f}" |
"mc(EF f)    = lfp(λT. mc f ∪ M¯ `` T)"|(*>*)
"mc(AF f)    = lfp(af(mc f))"

text‹\noindent
Because const‹af› is monotone in its second argument (and also its first, but
that is irrelevant), term‹af A› has a least fixed point:
›

lemma mono_af: "mono(af A)"
apply(simp add: mono_def af_def)
apply blast
done
(*<*)
lemma mono_ef: "mono(λT. A ∪ M¯ `` T)"
apply(rule monoI)
by(blast)

lemma EF_lemma:
  "lfp(λT. A ∪ M¯ `` T) = {s. ∃t. (s,t) ∈ M* ∧ t ∈ A}"
apply(rule equalityI)
 apply(rule subsetI)
 apply(simp)
 apply(erule lfp_induct_set)
  apply(rule mono_ef)
 apply(simp)
 apply(blast intro: rtrancl_trans)
apply(rule subsetI)
apply(simp, clarify)
apply(erule converse_rtrancl_induct)
 apply(subst lfp_unfold[OF mono_ef])
 apply(blast)
apply(subst lfp_unfold[OF mono_ef])
by(blast)
(*>*)
text‹
All we need to prove now is  prop‹mc(AF f) = {s. s ⊨ AF f}›, which states
that term‹mc› and ‹⊨› agree for const‹AF›\@.
This time we prove the two inclusions separately, starting
with the easy one:
›

theorem AF_lemma1: "lfp(af A) ⊆ {s. ∀p ∈ Paths s. ∃i. p i ∈ A}"

txt‹\noindent
In contrast to the analogous proof for const‹EF›, and just
for a change, we do not use fixed point induction.  Park-induction,
named after David Park, is weaker but sufficient for this proof:
\begin{center}
@{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound})
\end{center}
The instance of the premise prop‹f S ⊆ S› is proved pointwise,
a decision that \isa{auto} takes for us:
›
apply(rule lfp_lowerbound)
apply(auto simp add: af_def Paths_def)

txt‹
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
In this remaining case, we set term‹t› to term‹p(1::nat)›.
The rest is automatic, which is surprising because it involves
finding the instantiation term‹λi::nat. p(i+1)›
for ‹∀p›.
›

apply(erule_tac x = "p 1" in allE)
apply(auto)
done


text‹
The opposite inclusion is proved by contradiction: if some state
term‹s› is not in term‹lfp(af A)›, then we can construct an
infinite term‹A›-avoiding path starting from~term‹s›. The reason is
that by unfolding const‹lfp› we find that if term‹s› is not in
term‹lfp(af A)›, then term‹s› is not in term‹A› and there is a
direct successor of term‹s› that is again not in \mbox{term‹lfp(af
A)›}. Iterating this argument yields the promised infinite
term‹A›-avoiding path. Let us formalize this sketch.

The one-step argument in the sketch above
is proved by a variant of contraposition:
›

lemma not_in_lfp_afD:
 "s ∉ lfp(af A) ⟹ s ∉ A ∧ (∃ t. (s,t) ∈ M ∧ t ∉ lfp(af A))"
apply(erule contrapos_np)
apply(subst lfp_unfold[OF mono_af])
apply(simp add: af_def)
done

text‹\noindent
We assume the negation of the conclusion and prove term‹s ∈ lfp(af A)›.
Unfolding const‹lfp› once and
simplifying with the definition of const‹af› finishes the proof.

Now we iterate this process. The following construction of the desired
path is parameterized by a predicate term‹Q› that should hold along the path:
›

primrec path :: "state ⇒ (state ⇒ bool) ⇒ (nat ⇒ state)" where
"path s Q 0 = s" |
"path s Q (Suc n) = (SOME t. (path s Q n,t) ∈ M ∧ Q t)"

text‹\noindent
Element term‹n+1::nat› on this path is some arbitrary successor
term‹t› of element term‹n› such that term‹Q t› holds.  Remember that ‹SOME t. R t›
is some arbitrary but fixed term‹t› such that prop‹R t› holds (see \S\ref{sec:SOME}). Of
course, such a term‹t› need not exist, but that is of no
concern to us since we will only use const‹path› when a
suitable term‹t› does exist.

Let us show that if each state term‹s› that satisfies term‹Q›
has a successor that again satisfies term‹Q›, then there exists an infinite term‹Q›-path:
›

lemma infinity_lemma:
  "⟦ Q s; ∀s. Q s ⟶ (∃ t. (s,t) ∈ M ∧ Q t) ⟧ ⟹
   ∃p∈Paths s. ∀i. Q(p i)"

txt‹\noindent
First we rephrase the conclusion slightly because we need to prove simultaneously
both the path property and the fact that term‹Q› holds:
›

apply(subgoal_tac
  "∃p. s = p 0 ∧ (∀i::nat. (p i, p(i+1)) ∈ M ∧ Q(p i))")

txt‹\noindent
From this proposition the original goal follows easily:
›

 apply(simp add: Paths_def, blast)

txt‹\noindent
The new subgoal is proved by providing the witness term‹path s Q› for term‹p›:
›

apply(rule_tac x = "path s Q" in exI)
apply(clarsimp)

txt‹\noindent
After simplification and clarification, the subgoal has the following form:
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
It invites a proof by induction on term‹i›:
›

apply(induct_tac i)
 apply(simp)

txt‹\noindent
After simplification, the base case boils down to
@{subgoals[display,indent=0,margin=70,goals_limit=1]}
The conclusion looks exceedingly trivial: after all, term‹t› is chosen such that prop‹(s,t)∈M›
holds. However, we first have to show that such a term‹t› actually exists! This reasoning
is embodied in the theorem @{thm[source]someI2_ex}:
@{thm[display,eta_contract=false]someI2_ex}
When we apply this theorem as an introduction rule, ‹?P x› becomes
prop‹(s, x) ∈ M ∧ Q x› and ‹?Q x› becomes prop‹(s,x) ∈ M› and we have to prove
two subgoals: prop‹∃a. (s, a) ∈ M ∧ Q a›, which follows from the assumptions, and
prop‹(s, x) ∈ M ∧ Q x ⟹ (s,x) ∈ M›, which is trivial. Thus it is not surprising that
‹fast› can prove the base case quickly:
›

 apply(fast intro: someI2_ex)

txt‹\noindent
What is worth noting here is that we have used \methdx{fast} rather than
‹blast›.  The reason is that ‹blast› would fail because it cannot
cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
subgoal is non-trivial because of the nested schematic variables. For
efficiency reasons ‹blast› does not even attempt such unifications.
Although ‹fast› can in principle cope with complicated unification
problems, in practice the number of unifiers arising is often prohibitive and
the offending rule may need to be applied explicitly rather than
automatically. This is what happens in the step case.

The induction step is similar, but more involved, because now we face nested
occurrences of ‹SOME›. As a result, ‹fast› is no longer able to
solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
show the proof commands but do not describe the details:
›

apply(simp)
apply(rule someI2_ex)
 apply(blast)
apply(rule someI2_ex)
 apply(blast)
apply(blast)
done

text‹
Function const‹path› has fulfilled its purpose now and can be forgotten.
It was merely defined to provide the witness in the proof of the
@{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
that we could have given the witness without having to define a new function:
the term
@{term[display]"rec_nat s (λn t. SOME u. (t,u)∈M ∧ Q u)"}
is extensionally equal to term‹path s Q›,
where term‹rec_nat› is the predefined primitive recursor on typ‹nat›.
›
(*<*)
lemma
"⟦ Q s; ∀ s. Q s ⟶ (∃ t. (s,t)∈M ∧ Q t) ⟧ ⟹
 ∃ p∈Paths s. ∀ i. Q(p i)"
apply(subgoal_tac
 "∃ p. s = p 0 ∧ (∀ i. (p i,p(Suc i))∈M ∧ Q(p i))")
 apply(simp add: Paths_def)
 apply(blast)
apply(rule_tac x = "rec_nat s (λn t. SOME u. (t,u)∈M ∧ Q u)" in exI)
apply(simp)
apply(intro strip)
apply(induct_tac i)
 apply(simp)
 apply(fast intro: someI2_ex)
apply(simp)
apply(rule someI2_ex)
 apply(blast)
apply(rule someI2_ex)
 apply(blast)
by(blast)
(*>*)

text‹
At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
›

theorem AF_lemma2: "{s. ∀p ∈ Paths s. ∃i. p i ∈ A} ⊆ lfp(af A)"

txt‹\noindent
The proof is again pointwise and then by contraposition:
›

apply(rule subsetI)
apply(erule contrapos_pp)
apply simp

txt‹
@{subgoals[display,indent=0,goals_limit=1]}
Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
premise of @{thm[source]infinity_lemma} and the original subgoal:
›

apply(drule infinity_lemma)

txt‹
@{subgoals[display,indent=0,margin=65]}
Both are solved automatically:
›

 apply(auto dest: not_in_lfp_afD)
done

text‹
If you find these proofs too complicated, we recommend that you read
\S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
simpler arguments.

The main theorem is proved as for PDL, except that we also derive the
necessary equality ‹lfp(af A) = ...› by combining
@{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot:
›

theorem "mc f = {s. s ⊨ f}"
apply(induct_tac f)
apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2])
done

text‹

The language defined above is not quite CTL\@. The latter also includes an
until-operator term‹EU f g› with semantics ``there \emph{E}xists a path
where term‹f› is true \emph{U}ntil term‹g› becomes true''.  We need
an auxiliary function:
›

primrec
until:: "state set ⇒ state set ⇒ state ⇒ state list ⇒ bool" where
"until A B s []    = (s ∈ B)" |
"until A B s (t#p) = (s ∈ A ∧ (s,t) ∈ M ∧ until A B t p)"
(*<*)definition
 eusem :: "state set ⇒ state set ⇒ state set" where
"eusem A B ≡ {s. ∃p. until A B s p}"(*>*)

text‹\noindent
Expressing the semantics of term‹EU› is now straightforward:
@{prop[display]"s ⊨ EU f g = (∃p. until {t. t ⊨ f} {t. t ⊨ g} s p)"}
Note that term‹EU› is not definable in terms of the other operators!

Model checking term‹EU› is again a least fixed point construction:
@{text[display]"mc(EU f g) = lfp(λT. mc g ∪ mc f ∩ (M¯ `` T))"}

\begin{exercise}
Extend the datatype of formulae by the above until operator
and prove the equivalence between semantics and model checking, i.e.\ that
@{prop[display]"mc(EU f g) = {s. s ⊨ EU f g}"}
%For readability you may want to annotate {term EU} with its customary syntax
%{text[display]"| EU formula formula    E[_ U _]"}
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
\end{exercise}
For more CTL exercises see, for example, Huth and Ryan cite‹"Huth-Ryan-book"›.
›

(*<*)
definition eufix :: "state set ⇒ state set ⇒ state set ⇒ state set" where
"eufix A B T ≡ B ∪ A ∩ (M¯ `` T)"

lemma "lfp(eufix A B) ⊆ eusem A B"
apply(rule lfp_lowerbound)
apply(auto simp add: eusem_def eufix_def)
 apply(rule_tac x = "[]" in exI)
 apply simp
apply(rule_tac x = "xa#xb" in exI)
apply simp
done

lemma mono_eufix: "mono(eufix A B)"
apply(simp add: mono_def eufix_def)
apply blast
done

lemma "eusem A B ⊆ lfp(eufix A B)"
apply(clarsimp simp add: eusem_def)
apply(erule rev_mp)
apply(rule_tac x = x in spec)
apply(induct_tac p)
 apply(subst lfp_unfold[OF mono_eufix])
 apply(simp add: eufix_def)
apply(clarsimp)
apply(subst lfp_unfold[OF mono_eufix])
apply(simp add: eufix_def)
apply blast
done

(*
definition eusem :: "state set ⇒ state set ⇒ state set" where
"eusem A B ≡ {s. ∃p∈Paths s. ∃j. p j ∈ B ∧ (∀i < j. p i ∈ A)}"

axiomatization where
M_total: "∃t. (s,t) ∈ M"

consts apath :: "state ⇒ (nat ⇒ state)"
primrec
"apath s 0 = s"
"apath s (Suc i) = (SOME t. (apath s i,t) ∈ M)"

lemma [iff]: "apath s ∈ Paths s";
apply(simp add: Paths_def);
apply(blast intro: M_total[THEN someI_ex])
done

definition pcons :: "state ⇒ (nat ⇒ state) ⇒ (nat ⇒ state)" where
"pcons s p == λi. case i of 0 ⇒ s | Suc j ⇒ p j"

lemma pcons_PathI: "[| (s,t) : M; p ∈ Paths t |] ==> pcons s p ∈ Paths s";
by(simp add: Paths_def pcons_def split: nat.split);

lemma "lfp(eufix A B) ⊆ eusem A B"
apply(rule lfp_lowerbound)
apply(clarsimp simp add: eusem_def eufix_def);
apply(erule disjE);
 apply(rule_tac x = "apath x" in bexI);
  apply(rule_tac x = 0 in exI);
  apply simp;
 apply simp;
apply(clarify);
apply(rule_tac x = "pcons xb p" in bexI);
 apply(rule_tac x = "j+1" in exI);
 apply (simp add: pcons_def split: nat.split);
apply (simp add: pcons_PathI)
done
*)
(*>*)

text‹Let us close this section with a few words about the executability of
our model checkers.  It is clear that if all sets are finite, they can be
represented as lists and the usual set operations are easily
implemented. Only const‹lfp› requires a little thought.  Fortunately, theory
‹While_Combinator› in the Library~cite‹"HOL-Library"› provides a
theorem stating that in the case of finite sets and a monotone
function~term‹F›, the value of \mbox{term‹lfp F›} can be computed by
iterated application of term‹F› to~term‹{}› until a fixed point is
reached. It is actually possible to generate executable functional programs
from HOL definitions, but that is beyond the scope of the tutorial.%
\index{CTL|)}›
(*<*)end(*>*)