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(*>*)