doc-src/TutorialI/CTL/CTL.thy
author nipkow
Thu Oct 12 18:38:23 2000 +0200 (2000-10-12)
changeset 10212 33fe2d701ddd
parent 10210 e8aa81362f41
child 10217 e61e7e1eacaf
permissions -rw-r--r--
*** empty log message ***
     1 (*<*)theory CTL = Base:;(*>*)
     2 
     3 subsection{*Computation tree logic---CTL*};
     4 
     5 text{*\label{sec:CTL}
     6 The semantics of PDL only needs transitive reflexive closure.
     7 Let us now be a bit more adventurous and introduce a new temporal operator
     8 that goes beyond transitive reflexive closure. We extend the datatype
     9 @{text formula} by a new constructor
    10 *};
    11 (*<*)
    12 datatype formula = Atom atom
    13                   | Neg formula
    14                   | And formula formula
    15                   | AX formula
    16                   | EF formula(*>*)
    17                   | AF formula;
    18 
    19 text{*\noindent
    20 which stands for "always in the future":
    21 on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
    22 in HOL: it is simply a function from @{typ nat} to @{typ state}.
    23 *};
    24 
    25 constdefs Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set"
    26          "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}";
    27 
    28 text{*\noindent
    29 This definition allows a very succinct statement of the semantics of @{term AF}:
    30 \footnote{Do not be mislead: neither datatypes nor recursive functions can be
    31 extended by new constructors or equations. This is just a trick of the
    32 presentation. In reality one has to define a new datatype and a new function.}
    33 *};
    34 (*<*)
    35 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80);
    36 
    37 primrec
    38 "s \<Turnstile> Atom a  =  (a \<in> L s)"
    39 "s \<Turnstile> Neg f   = (~(s \<Turnstile> f))"
    40 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
    41 "s \<Turnstile> AX f    = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
    42 "s \<Turnstile> EF f    = (\<exists>t. (s,t) \<in> M^* \<and> t \<Turnstile> f)"
    43 (*>*)
    44 "s \<Turnstile> AF f    = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)";
    45 
    46 text{*\noindent
    47 Model checking @{term AF} involves a function which
    48 is just complicated enough to warrant a separate definition:
    49 *};
    50 
    51 constdefs af :: "state set \<Rightarrow> state set \<Rightarrow> state set"
    52          "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}";
    53 
    54 text{*\noindent
    55 Now we define @{term "mc(AF f)"} as the least set @{term T} that contains
    56 @{term"mc f"} and all states all of whose direct successors are in @{term T}:
    57 *};
    58 (*<*)
    59 consts mc :: "formula \<Rightarrow> state set";
    60 primrec
    61 "mc(Atom a)  = {s. a \<in> L s}"
    62 "mc(Neg f)   = -mc f"
    63 "mc(And f g) = mc f \<inter> mc g"
    64 "mc(AX f)    = {s. \<forall>t. (s,t) \<in> M  \<longrightarrow> t \<in> mc f}"
    65 "mc(EF f)    = lfp(\<lambda>T. mc f \<union> M^-1 ^^ T)"(*>*)
    66 "mc(AF f)    = lfp(af(mc f))";
    67 
    68 text{*\noindent
    69 Because @{term af} is monotone in its second argument (and also its first, but
    70 that is irrelevant) @{term"af A"} has a least fixpoint:
    71 *};
    72 
    73 lemma mono_af: "mono(af A)";
    74 apply(simp add: mono_def af_def);
    75 apply blast;
    76 done
    77 (*<*)
    78 lemma mono_ef: "mono(\<lambda>T. A \<union> M^-1 ^^ T)";
    79 apply(rule monoI);
    80 by(blast);
    81 
    82 lemma EF_lemma:
    83   "lfp(\<lambda>T. A \<union> M^-1 ^^ T) = {s. \<exists>t. (s,t) \<in> M^* \<and> t \<in> A}";
    84 apply(rule equalityI);
    85  apply(rule subsetI);
    86  apply(simp);
    87  apply(erule lfp_induct);
    88   apply(rule mono_ef);
    89  apply(simp);
    90  apply(blast intro: r_into_rtrancl rtrancl_trans);
    91 apply(rule subsetI);
    92 apply(simp, clarify);
    93 apply(erule converse_rtrancl_induct);
    94  apply(rule ssubst[OF lfp_unfold[OF mono_ef]]);
    95  apply(blast);
    96 apply(rule ssubst[OF lfp_unfold[OF mono_ef]]);
    97 by(blast);
    98 (*>*)
    99 text{*
   100 All we need to prove now is that @{term mc} and @{text"\<Turnstile>"}
   101 agree for @{term AF}, i.e.\ that @{prop"mc(AF f) = {s. s \<Turnstile>
   102 AF f}"}. This time we prove the two containments separately, starting
   103 with the easy one:
   104 *};
   105 
   106 theorem AF_lemma1:
   107   "lfp(af A) \<subseteq> {s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A}";
   108 
   109 txt{*\noindent
   110 The proof is again pointwise. Fixpoint induction on the premise @{prop"s \<in> lfp(af A)"} followed
   111 by simplification and clarification
   112 *};
   113 
   114 apply(rule subsetI);
   115 apply(erule lfp_induct[OF _ mono_af]);
   116 apply(clarsimp simp add: af_def Paths_def);
   117 (*ML"Pretty.setmargin 70";
   118 pr(latex xsymbols symbols);*)
   119 txt{*\noindent
   120 leads to the following somewhat involved proof state
   121 \begin{isabelle}
   122 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ \isadigit{0}\ {\isasymin}\ A\ {\isasymor}\isanewline
   123 \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ \isadigit{0}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
   124 \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymand}\isanewline
   125 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymforall}p{\isachardot}\ t\ {\isacharequal}\ p\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
   126 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
   127 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
   128 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
   129 \end{isabelle}
   130 Now we eliminate the disjunction. The case @{prop"p 0 \<in> A"} is trivial:
   131 *};
   132 
   133 apply(erule disjE);
   134  apply(blast);
   135 
   136 txt{*\noindent
   137 In the other case we set @{term t} to @{term"p 1"} and simplify matters:
   138 *};
   139 
   140 apply(erule_tac x = "p 1" in allE);
   141 apply(clarsimp);
   142 (*ML"Pretty.setmargin 70";
   143 pr(latex xsymbols symbols);*)
   144 
   145 txt{*
   146 \begin{isabelle}
   147 \ \isadigit{1}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\ p\ \isadigit{1}\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharsemicolon}\isanewline
   148 \ \ \ \ \ \ \ \ \ \ \ {\isasymforall}pa{\isachardot}\ p\ \isadigit{1}\ {\isacharequal}\ pa\ \isadigit{0}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}pa\ i{\isacharcomma}\ pa\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}\ {\isasymlongrightarrow}\isanewline
   149 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
   150 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A
   151 \end{isabelle}
   152 It merely remains to set @{term pa} to @{term"\<lambda>i. p(i+1)"}, i.e.\ @{term p} without its
   153 first element. The rest is practically automatic:
   154 *};
   155 
   156 apply(erule_tac x = "\<lambda>i. p(i+1)" in allE);
   157 apply simp;
   158 apply blast;
   159 done;
   160 
   161 text{*
   162 The opposite containment is proved by contradiction: if some state
   163 @{term s} is not in @{term"lfp(af A)"}, then we can construct an
   164 infinite @{term A}-avoiding path starting from @{term s}. The reason is
   165 that by unfolding @{term lfp} we find that if @{term s} is not in
   166 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
   167 direct successor of @{term s} that is again not in @{term"lfp(af
   168 A)"}. Iterating this argument yields the promised infinite
   169 @{term A}-avoiding path. Let us formalize this sketch.
   170 
   171 The one-step argument in the above sketch
   172 *};
   173 
   174 lemma not_in_lfp_afD:
   175  "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
   176 apply(erule swap);
   177 apply(rule ssubst[OF lfp_unfold[OF mono_af]]);
   178 apply(simp add:af_def);
   179 done;
   180 
   181 text{*\noindent
   182 is proved by a variant of contraposition (@{thm[source]swap}:
   183 @{thm swap[no_vars]}), i.e.\ assuming the negation of the conclusion
   184 and proving @{term"s : lfp(af A)"}. Unfolding @{term lfp} once and
   185 simplifying with the definition of @{term af} finishes the proof.
   186 
   187 Now we iterate this process. The following construction of the desired
   188 path is parameterized by a predicate @{term P} that should hold along the path:
   189 *};
   190 
   191 consts path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)";
   192 primrec
   193 "path s P 0 = s"
   194 "path s P (Suc n) = (SOME t. (path s P n,t) \<in> M \<and> P t)";
   195 
   196 text{*\noindent
   197 Element @{term"n+1"} on this path is some arbitrary successor
   198 @{term t} of element @{term n} such that @{term"P t"} holds.  Remember that @{text"SOME t. R t"}
   199 is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec-SOME}). Of
   200 course, such a @{term t} may in general not exist, but that is of no
   201 concern to us since we will only use @{term path} in such cases where a
   202 suitable @{term t} does exist.
   203 
   204 Let us show that if each state @{term s} that satisfies @{term P}
   205 has a successor that again satisfies @{term P}, then there exists an infinite @{term P}-path:
   206 *};
   207 
   208 lemma infinity_lemma:
   209   "\<lbrakk> P s; \<forall>s. P s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> P t) \<rbrakk> \<Longrightarrow>
   210    \<exists>p\<in>Paths s. \<forall>i. P(p i)";
   211 
   212 txt{*\noindent
   213 First we rephrase the conclusion slightly because we need to prove both the path property
   214 and the fact that @{term P} holds simultaneously:
   215 *};
   216 
   217 apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> P(p i))");
   218 
   219 txt{*\noindent
   220 From this proposition the original goal follows easily:
   221 *};
   222 
   223  apply(simp add:Paths_def, blast);
   224 
   225 txt{*\noindent
   226 The new subgoal is proved by providing the witness @{term "path s P"} for @{term p}:
   227 *};
   228 
   229 apply(rule_tac x = "path s P" in exI);
   230 apply(clarsimp);
   231 (*ML"Pretty.setmargin 70";
   232 pr(latex xsymbols symbols);*)
   233 
   234 txt{*\noindent
   235 After simplification and clarification the subgoal has the following compact form
   236 \begin{isabelle}
   237 \ \isadigit{1}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
   238 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ P\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
   239 \ \ \ \ \ \ \ \ \ \ \ \ P\ {\isacharparenleft}path\ s\ P\ i{\isacharparenright}
   240 \end{isabelle}
   241 and invites a proof by induction on @{term i}:
   242 *};
   243 
   244 apply(induct_tac i);
   245  apply(simp);
   246 (*ML"Pretty.setmargin 70";
   247 pr(latex xsymbols symbols);*)
   248 
   249 txt{*\noindent
   250 After simplification the base case boils down to
   251 \begin{isabelle}
   252 \ \isadigit{1}{\isachardot}\ {\isasymlbrakk}P\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ P\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}{\isasymrbrakk}\isanewline
   253 \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ P\ t{\isacharparenright}\ {\isasymin}\ M
   254 \end{isabelle}
   255 The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
   256 holds. However, we first have to show that such a @{term t} actually exists! This reasoning
   257 is embodied in the theorem @{thm[source]someI2_ex}:
   258 @{thm[display,eta_contract=false]someI2_ex}
   259 When we apply this theorem as an introduction rule, @{text"?P x"} becomes
   260 @{prop"(s, x) : M & P x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove
   261 two subgoals: @{prop"EX a. (s, a) : M & P a"}, which follows from the assumptions, and
   262 @{prop"(s, x) : M & P x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that
   263 @{text fast} can prove the base case quickly:
   264 *};
   265 
   266  apply(fast intro:someI2_ex);
   267 
   268 txt{*\noindent
   269 What is worth noting here is that we have used @{text fast} rather than
   270 @{text blast}.  The reason is that @{text blast} would fail because it cannot
   271 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
   272 subgoal is nontrivial because of the nested schematic variables. For
   273 efficiency reasons @{text blast} does not even attempt such unifications.
   274 Although @{text fast} can in principle cope with complicated unification
   275 problems, in practice the number of unifiers arising is often prohibitive and
   276 the offending rule may need to be applied explicitly rather than
   277 automatically. This is what happens in the step case.
   278 
   279 The induction step is similar, but more involved, because now we face nested
   280 occurrences of @{text SOME}. As a result, @{text fast} is no longer able to
   281 solve the subgoal and we apply @{thm[source]someI2_ex} by hand.  We merely
   282 show the proof commands but do not describe the details:
   283 *};
   284 
   285 apply(simp);
   286 apply(rule someI2_ex);
   287  apply(blast);
   288 apply(rule someI2_ex);
   289  apply(blast);
   290 apply(blast);
   291 done;
   292 
   293 text{*
   294 Function @{term path} has fulfilled its purpose now and can be forgotten
   295 about. It was merely defined to provide the witness in the proof of the
   296 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know
   297 that we could have given the witness without having to define a new function:
   298 the term
   299 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)"}
   300 is extensionally equal to @{term"path s P"},
   301 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}, whose defining
   302 equations we omit.
   303 *};
   304 (*<*)
   305 lemma infinity_lemma:
   306 "\<lbrakk> P s; \<forall> s. P s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> P t) \<rbrakk> \<Longrightarrow>
   307  \<exists> p\<in>Paths s. \<forall> i. P(p i)";
   308 apply(subgoal_tac
   309  "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> P(p i))");
   310  apply(simp add:Paths_def);
   311  apply(blast);
   312 apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> P u)" in exI);
   313 apply(simp);
   314 apply(intro strip);
   315 apply(induct_tac i);
   316  apply(simp);
   317  apply(fast intro:someI2_ex);
   318 apply(simp);
   319 apply(rule someI2_ex);
   320  apply(blast);
   321 apply(rule someI2_ex);
   322  apply(blast);
   323 by(blast);
   324 (*>*)
   325 
   326 text{*
   327 At last we can prove the opposite direction of @{thm[source]AF_lemma1}:
   328 *};
   329 
   330 theorem AF_lemma2:
   331 "{s. \<forall> p \<in> Paths s. \<exists> i. p i \<in> A} \<subseteq> lfp(af A)";
   332 
   333 txt{*\noindent
   334 The proof is again pointwise and then by contraposition (@{thm[source]contrapos2} is the rule
   335 @{thm contrapos2}):
   336 *};
   337 
   338 apply(rule subsetI);
   339 apply(erule contrapos2);
   340 apply simp;
   341 (*pr(latex xsymbols symbols);*)
   342 
   343 txt{*
   344 \begin{isabelle}
   345 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
   346 \end{isabelle}
   347 Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second
   348 premise of @{thm[source]infinity_lemma} and the original subgoal:
   349 *};
   350 
   351 apply(drule infinity_lemma);
   352 (*pr(latex xsymbols symbols);*)
   353 
   354 txt{*
   355 \begin{isabelle}
   356 \ \isadigit{1}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymforall}s{\isachardot}\ s\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}\isanewline
   357 \ \isadigit{2}{\isachardot}\ {\isasymAnd}s{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\isanewline
   358 \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A
   359 \end{isabelle}
   360 Both are solved automatically:
   361 *};
   362 
   363  apply(auto dest:not_in_lfp_afD);
   364 done;
   365 
   366 text{*
   367 The main theorem is proved as for PDL, except that we also derive the necessary equality
   368 @{text"lfp(af A) = ..."} by combining @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2}
   369 on the spot:
   370 *}
   371 
   372 theorem "mc f = {s. s \<Turnstile> f}";
   373 apply(induct_tac f);
   374 apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]);
   375 done
   376 
   377 text{*
   378 The above language is not quite CTL. The latter also includes an
   379 until-operator, which is the subject of the following exercise.
   380 It is not definable in terms of the other operators!
   381 \begin{exercise}
   382 Extend the datatype of formulae by the binary until operator @{term"EU f g"} with semantics
   383 ``there exist a path where @{term f} is true until @{term g} becomes true''
   384 @{text[display]"s \<Turnstile> EU f g = (\<exists>p\<in>Paths s. \<exists>j. p j \<Turnstile> g \<and> (\<exists>i < j. p i \<Turnstile> f))"}
   385 and model checking algorithm
   386 @{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M^-1 ^^ T))"}
   387 Prove the equivalence between semantics and model checking, i.e.\ that
   388 @{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"}
   389 %For readability you may want to annotate {term EU} with its customary syntax
   390 %{text[display]"| EU formula formula    E[_ U _]"}
   391 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
   392 \end{exercise}
   393 For more CTL exercises see, for example \cite{Huth-Ryan-book}.
   394 \bigskip
   395 
   396 Let us close this section with a few words about the executability of our model checkers.
   397 It is clear that if all sets are finite, they can be represented as lists and the usual
   398 set operations are easily implemented. Only @{term lfp} requires a little thought.
   399 Fortunately the HOL library proves that in the case of finite sets and a monotone @{term F},
   400 @{term"lfp F"} can be computed by iterated application of @{term F} to @{term"{}"} until
   401 a fixpoint is reached. It is actually possible to generate executable functional programs
   402 from HOL definitions, but that is beyond the scope of the tutorial.
   403 *}
   404 (*<*)end(*>*)