1 (*<*)theory CTL imports Base begin(*>*) |
|
2 |
|
3 subsection{*Computation Tree Logic --- CTL*}; |
|
4 |
|
5 text{*\label{sec:CTL} |
|
6 \index{CTL|(}% |
|
7 The semantics of PDL only needs reflexive transitive closure. |
|
8 Let us be adventurous and introduce a more expressive temporal operator. |
|
9 We extend the datatype |
|
10 @{text formula} by a new constructor |
|
11 *}; |
|
12 (*<*) |
|
13 datatype formula = Atom "atom" |
|
14 | Neg formula |
|
15 | And formula formula |
|
16 | AX formula |
|
17 | EF formula(*>*) |
|
18 | AF formula; |
|
19 |
|
20 text{*\noindent |
|
21 which stands for ``\emph{A}lways in the \emph{F}uture'': |
|
22 on all infinite paths, at some point the formula holds. |
|
23 Formalizing the notion of an infinite path is easy |
|
24 in HOL: it is simply a function from @{typ nat} to @{typ state}. |
|
25 *}; |
|
26 |
|
27 definition Paths :: "state \<Rightarrow> (nat \<Rightarrow> state)set" where |
|
28 "Paths s \<equiv> {p. s = p 0 \<and> (\<forall>i. (p i, p(i+1)) \<in> M)}" |
|
29 |
|
30 text{*\noindent |
|
31 This definition allows a succinct statement of the semantics of @{const AF}: |
|
32 \footnote{Do not be misled: neither datatypes nor recursive functions can be |
|
33 extended by new constructors or equations. This is just a trick of the |
|
34 presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define |
|
35 a new datatype and a new function.} |
|
36 *}; |
|
37 (*<*) |
|
38 primrec valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) where |
|
39 "s \<Turnstile> Atom a = (a \<in> L s)" | |
|
40 "s \<Turnstile> Neg f = (~(s \<Turnstile> f))" | |
|
41 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)" | |
|
42 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" | |
|
43 "s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)" | |
|
44 (*>*) |
|
45 "s \<Turnstile> AF f = (\<forall>p \<in> Paths s. \<exists>i. p i \<Turnstile> f)" |
|
46 |
|
47 text{*\noindent |
|
48 Model checking @{const AF} involves a function which |
|
49 is just complicated enough to warrant a separate definition: |
|
50 *}; |
|
51 |
|
52 definition af :: "state set \<Rightarrow> state set \<Rightarrow> state set" where |
|
53 "af A T \<equiv> A \<union> {s. \<forall>t. (s, t) \<in> M \<longrightarrow> t \<in> T}" |
|
54 |
|
55 text{*\noindent |
|
56 Now we define @{term "mc(AF f)"} as the least set @{term T} that includes |
|
57 @{term"mc f"} and all states all of whose direct successors are in @{term T}: |
|
58 *}; |
|
59 (*<*) |
|
60 primrec mc :: "formula \<Rightarrow> state set" where |
|
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\<inverse> `` T)"|(*>*) |
|
66 "mc(AF f) = lfp(af(mc f))"; |
|
67 |
|
68 text{*\noindent |
|
69 Because @{const af} is monotone in its second argument (and also its first, but |
|
70 that is irrelevant), @{term"af A"} has a least fixed point: |
|
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\<inverse> `` T)"; |
|
79 apply(rule monoI); |
|
80 by(blast); |
|
81 |
|
82 lemma EF_lemma: |
|
83 "lfp(\<lambda>T. A \<union> M\<inverse> `` T) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"; |
|
84 apply(rule equalityI); |
|
85 apply(rule subsetI); |
|
86 apply(simp); |
|
87 apply(erule lfp_induct_set); |
|
88 apply(rule mono_ef); |
|
89 apply(simp); |
|
90 apply(blast intro: rtrancl_trans); |
|
91 apply(rule subsetI); |
|
92 apply(simp, clarify); |
|
93 apply(erule converse_rtrancl_induct); |
|
94 apply(subst lfp_unfold[OF mono_ef]); |
|
95 apply(blast); |
|
96 apply(subst lfp_unfold[OF mono_ef]); |
|
97 by(blast); |
|
98 (*>*) |
|
99 text{* |
|
100 All we need to prove now is @{prop"mc(AF f) = {s. s \<Turnstile> AF f}"}, which states |
|
101 that @{term mc} and @{text"\<Turnstile>"} agree for @{const AF}\@. |
|
102 This time we prove the two inclusions separately, starting |
|
103 with the easy one: |
|
104 *}; |
|
105 |
|
106 theorem AF_lemma1: "lfp(af A) \<subseteq> {s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A}" |
|
107 |
|
108 txt{*\noindent |
|
109 In contrast to the analogous proof for @{const EF}, and just |
|
110 for a change, we do not use fixed point induction. Park-induction, |
|
111 named after David Park, is weaker but sufficient for this proof: |
|
112 \begin{center} |
|
113 @{thm lfp_lowerbound[of _ "S",no_vars]} \hfill (@{thm[source]lfp_lowerbound}) |
|
114 \end{center} |
|
115 The instance of the premise @{prop"f S \<subseteq> S"} is proved pointwise, |
|
116 a decision that \isa{auto} takes for us: |
|
117 *}; |
|
118 apply(rule lfp_lowerbound); |
|
119 apply(auto simp add: af_def Paths_def); |
|
120 |
|
121 txt{* |
|
122 @{subgoals[display,indent=0,margin=70,goals_limit=1]} |
|
123 In this remaining case, we set @{term t} to @{term"p(1::nat)"}. |
|
124 The rest is automatic, which is surprising because it involves |
|
125 finding the instantiation @{term"\<lambda>i::nat. p(i+1)"} |
|
126 for @{text"\<forall>p"}. |
|
127 *}; |
|
128 |
|
129 apply(erule_tac x = "p 1" in allE); |
|
130 apply(auto); |
|
131 done; |
|
132 |
|
133 |
|
134 text{* |
|
135 The opposite inclusion is proved by contradiction: if some state |
|
136 @{term s} is not in @{term"lfp(af A)"}, then we can construct an |
|
137 infinite @{term A}-avoiding path starting from~@{term s}. The reason is |
|
138 that by unfolding @{const lfp} we find that if @{term s} is not in |
|
139 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a |
|
140 direct successor of @{term s} that is again not in \mbox{@{term"lfp(af |
|
141 A)"}}. Iterating this argument yields the promised infinite |
|
142 @{term A}-avoiding path. Let us formalize this sketch. |
|
143 |
|
144 The one-step argument in the sketch above |
|
145 is proved by a variant of contraposition: |
|
146 *}; |
|
147 |
|
148 lemma not_in_lfp_afD: |
|
149 "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))"; |
|
150 apply(erule contrapos_np); |
|
151 apply(subst lfp_unfold[OF mono_af]); |
|
152 apply(simp add: af_def); |
|
153 done; |
|
154 |
|
155 text{*\noindent |
|
156 We assume the negation of the conclusion and prove @{term"s : lfp(af A)"}. |
|
157 Unfolding @{const lfp} once and |
|
158 simplifying with the definition of @{const af} finishes the proof. |
|
159 |
|
160 Now we iterate this process. The following construction of the desired |
|
161 path is parameterized by a predicate @{term Q} that should hold along the path: |
|
162 *}; |
|
163 |
|
164 primrec path :: "state \<Rightarrow> (state \<Rightarrow> bool) \<Rightarrow> (nat \<Rightarrow> state)" where |
|
165 "path s Q 0 = s" | |
|
166 "path s Q (Suc n) = (SOME t. (path s Q n,t) \<in> M \<and> Q t)" |
|
167 |
|
168 text{*\noindent |
|
169 Element @{term"n+1::nat"} on this path is some arbitrary successor |
|
170 @{term t} of element @{term n} such that @{term"Q t"} holds. Remember that @{text"SOME t. R t"} |
|
171 is some arbitrary but fixed @{term t} such that @{prop"R t"} holds (see \S\ref{sec:SOME}). Of |
|
172 course, such a @{term t} need not exist, but that is of no |
|
173 concern to us since we will only use @{const path} when a |
|
174 suitable @{term t} does exist. |
|
175 |
|
176 Let us show that if each state @{term s} that satisfies @{term Q} |
|
177 has a successor that again satisfies @{term Q}, then there exists an infinite @{term Q}-path: |
|
178 *}; |
|
179 |
|
180 lemma infinity_lemma: |
|
181 "\<lbrakk> Q s; \<forall>s. Q s \<longrightarrow> (\<exists> t. (s,t) \<in> M \<and> Q t) \<rbrakk> \<Longrightarrow> |
|
182 \<exists>p\<in>Paths s. \<forall>i. Q(p i)"; |
|
183 |
|
184 txt{*\noindent |
|
185 First we rephrase the conclusion slightly because we need to prove simultaneously |
|
186 both the path property and the fact that @{term Q} holds: |
|
187 *}; |
|
188 |
|
189 apply(subgoal_tac |
|
190 "\<exists>p. s = p 0 \<and> (\<forall>i::nat. (p i, p(i+1)) \<in> M \<and> Q(p i))"); |
|
191 |
|
192 txt{*\noindent |
|
193 From this proposition the original goal follows easily: |
|
194 *}; |
|
195 |
|
196 apply(simp add: Paths_def, blast); |
|
197 |
|
198 txt{*\noindent |
|
199 The new subgoal is proved by providing the witness @{term "path s Q"} for @{term p}: |
|
200 *}; |
|
201 |
|
202 apply(rule_tac x = "path s Q" in exI); |
|
203 apply(clarsimp); |
|
204 |
|
205 txt{*\noindent |
|
206 After simplification and clarification, the subgoal has the following form: |
|
207 @{subgoals[display,indent=0,margin=70,goals_limit=1]} |
|
208 It invites a proof by induction on @{term i}: |
|
209 *}; |
|
210 |
|
211 apply(induct_tac i); |
|
212 apply(simp); |
|
213 |
|
214 txt{*\noindent |
|
215 After simplification, the base case boils down to |
|
216 @{subgoals[display,indent=0,margin=70,goals_limit=1]} |
|
217 The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"} |
|
218 holds. However, we first have to show that such a @{term t} actually exists! This reasoning |
|
219 is embodied in the theorem @{thm[source]someI2_ex}: |
|
220 @{thm[display,eta_contract=false]someI2_ex} |
|
221 When we apply this theorem as an introduction rule, @{text"?P x"} becomes |
|
222 @{prop"(s, x) : M & Q x"} and @{text"?Q x"} becomes @{prop"(s,x) : M"} and we have to prove |
|
223 two subgoals: @{prop"EX a. (s, a) : M & Q a"}, which follows from the assumptions, and |
|
224 @{prop"(s, x) : M & Q x ==> (s,x) : M"}, which is trivial. Thus it is not surprising that |
|
225 @{text fast} can prove the base case quickly: |
|
226 *}; |
|
227 |
|
228 apply(fast intro: someI2_ex); |
|
229 |
|
230 txt{*\noindent |
|
231 What is worth noting here is that we have used \methdx{fast} rather than |
|
232 @{text blast}. The reason is that @{text blast} would fail because it cannot |
|
233 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current |
|
234 subgoal is non-trivial because of the nested schematic variables. For |
|
235 efficiency reasons @{text blast} does not even attempt such unifications. |
|
236 Although @{text fast} can in principle cope with complicated unification |
|
237 problems, in practice the number of unifiers arising is often prohibitive and |
|
238 the offending rule may need to be applied explicitly rather than |
|
239 automatically. This is what happens in the step case. |
|
240 |
|
241 The induction step is similar, but more involved, because now we face nested |
|
242 occurrences of @{text SOME}. As a result, @{text fast} is no longer able to |
|
243 solve the subgoal and we apply @{thm[source]someI2_ex} by hand. We merely |
|
244 show the proof commands but do not describe the details: |
|
245 *}; |
|
246 |
|
247 apply(simp); |
|
248 apply(rule someI2_ex); |
|
249 apply(blast); |
|
250 apply(rule someI2_ex); |
|
251 apply(blast); |
|
252 apply(blast); |
|
253 done; |
|
254 |
|
255 text{* |
|
256 Function @{const path} has fulfilled its purpose now and can be forgotten. |
|
257 It was merely defined to provide the witness in the proof of the |
|
258 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know |
|
259 that we could have given the witness without having to define a new function: |
|
260 the term |
|
261 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"} |
|
262 is extensionally equal to @{term"path s Q"}, |
|
263 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}. |
|
264 *}; |
|
265 (*<*) |
|
266 lemma |
|
267 "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow> |
|
268 \<exists> p\<in>Paths s. \<forall> i. Q(p i)"; |
|
269 apply(subgoal_tac |
|
270 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))"); |
|
271 apply(simp add: Paths_def); |
|
272 apply(blast); |
|
273 apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI); |
|
274 apply(simp); |
|
275 apply(intro strip); |
|
276 apply(induct_tac i); |
|
277 apply(simp); |
|
278 apply(fast intro: someI2_ex); |
|
279 apply(simp); |
|
280 apply(rule someI2_ex); |
|
281 apply(blast); |
|
282 apply(rule someI2_ex); |
|
283 apply(blast); |
|
284 by(blast); |
|
285 (*>*) |
|
286 |
|
287 text{* |
|
288 At last we can prove the opposite direction of @{thm[source]AF_lemma1}: |
|
289 *}; |
|
290 |
|
291 theorem AF_lemma2: "{s. \<forall>p \<in> Paths s. \<exists>i. p i \<in> A} \<subseteq> lfp(af A)"; |
|
292 |
|
293 txt{*\noindent |
|
294 The proof is again pointwise and then by contraposition: |
|
295 *}; |
|
296 |
|
297 apply(rule subsetI); |
|
298 apply(erule contrapos_pp); |
|
299 apply simp; |
|
300 |
|
301 txt{* |
|
302 @{subgoals[display,indent=0,goals_limit=1]} |
|
303 Applying the @{thm[source]infinity_lemma} as a destruction rule leaves two subgoals, the second |
|
304 premise of @{thm[source]infinity_lemma} and the original subgoal: |
|
305 *}; |
|
306 |
|
307 apply(drule infinity_lemma); |
|
308 |
|
309 txt{* |
|
310 @{subgoals[display,indent=0,margin=65]} |
|
311 Both are solved automatically: |
|
312 *}; |
|
313 |
|
314 apply(auto dest: not_in_lfp_afD); |
|
315 done; |
|
316 |
|
317 text{* |
|
318 If you find these proofs too complicated, we recommend that you read |
|
319 \S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to |
|
320 simpler arguments. |
|
321 |
|
322 The main theorem is proved as for PDL, except that we also derive the |
|
323 necessary equality @{text"lfp(af A) = ..."} by combining |
|
324 @{thm[source]AF_lemma1} and @{thm[source]AF_lemma2} on the spot: |
|
325 *} |
|
326 |
|
327 theorem "mc f = {s. s \<Turnstile> f}"; |
|
328 apply(induct_tac f); |
|
329 apply(auto simp add: EF_lemma equalityI[OF AF_lemma1 AF_lemma2]); |
|
330 done |
|
331 |
|
332 text{* |
|
333 |
|
334 The language defined above is not quite CTL\@. The latter also includes an |
|
335 until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path |
|
336 where @{term f} is true \emph{U}ntil @{term g} becomes true''. We need |
|
337 an auxiliary function: |
|
338 *} |
|
339 |
|
340 primrec |
|
341 until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool" where |
|
342 "until A B s [] = (s \<in> B)" | |
|
343 "until A B s (t#p) = (s \<in> A \<and> (s,t) \<in> M \<and> until A B t p)" |
|
344 (*<*)definition |
|
345 eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where |
|
346 "eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*) |
|
347 |
|
348 text{*\noindent |
|
349 Expressing the semantics of @{term EU} is now straightforward: |
|
350 @{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"} |
|
351 Note that @{term EU} is not definable in terms of the other operators! |
|
352 |
|
353 Model checking @{term EU} is again a least fixed point construction: |
|
354 @{text[display]"mc(EU f g) = lfp(\<lambda>T. mc g \<union> mc f \<inter> (M\<inverse> `` T))"} |
|
355 |
|
356 \begin{exercise} |
|
357 Extend the datatype of formulae by the above until operator |
|
358 and prove the equivalence between semantics and model checking, i.e.\ that |
|
359 @{prop[display]"mc(EU f g) = {s. s \<Turnstile> EU f g}"} |
|
360 %For readability you may want to annotate {term EU} with its customary syntax |
|
361 %{text[display]"| EU formula formula E[_ U _]"} |
|
362 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}. |
|
363 \end{exercise} |
|
364 For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}. |
|
365 *} |
|
366 |
|
367 (*<*) |
|
368 definition eufix :: "state set \<Rightarrow> state set \<Rightarrow> state set \<Rightarrow> state set" where |
|
369 "eufix A B T \<equiv> B \<union> A \<inter> (M\<inverse> `` T)" |
|
370 |
|
371 lemma "lfp(eufix A B) \<subseteq> eusem A B" |
|
372 apply(rule lfp_lowerbound) |
|
373 apply(auto simp add: eusem_def eufix_def) |
|
374 apply(rule_tac x = "[]" in exI) |
|
375 apply simp |
|
376 apply(rule_tac x = "xa#xb" in exI) |
|
377 apply simp |
|
378 done |
|
379 |
|
380 lemma mono_eufix: "mono(eufix A B)"; |
|
381 apply(simp add: mono_def eufix_def); |
|
382 apply blast; |
|
383 done |
|
384 |
|
385 lemma "eusem A B \<subseteq> lfp(eufix A B)"; |
|
386 apply(clarsimp simp add: eusem_def); |
|
387 apply(erule rev_mp); |
|
388 apply(rule_tac x = x in spec); |
|
389 apply(induct_tac p); |
|
390 apply(subst lfp_unfold[OF mono_eufix]) |
|
391 apply(simp add: eufix_def); |
|
392 apply(clarsimp); |
|
393 apply(subst lfp_unfold[OF mono_eufix]) |
|
394 apply(simp add: eufix_def); |
|
395 apply blast; |
|
396 done |
|
397 |
|
398 (* |
|
399 definition eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where |
|
400 "eusem A B \<equiv> {s. \<exists>p\<in>Paths s. \<exists>j. p j \<in> B \<and> (\<forall>i < j. p i \<in> A)}" |
|
401 |
|
402 axioms |
|
403 M_total: "\<exists>t. (s,t) \<in> M" |
|
404 |
|
405 consts apath :: "state \<Rightarrow> (nat \<Rightarrow> state)" |
|
406 primrec |
|
407 "apath s 0 = s" |
|
408 "apath s (Suc i) = (SOME t. (apath s i,t) \<in> M)" |
|
409 |
|
410 lemma [iff]: "apath s \<in> Paths s"; |
|
411 apply(simp add: Paths_def); |
|
412 apply(blast intro: M_total[THEN someI_ex]) |
|
413 done |
|
414 |
|
415 definition pcons :: "state \<Rightarrow> (nat \<Rightarrow> state) \<Rightarrow> (nat \<Rightarrow> state)" where |
|
416 "pcons s p == \<lambda>i. case i of 0 \<Rightarrow> s | Suc j \<Rightarrow> p j" |
|
417 |
|
418 lemma pcons_PathI: "[| (s,t) : M; p \<in> Paths t |] ==> pcons s p \<in> Paths s"; |
|
419 by(simp add: Paths_def pcons_def split: nat.split); |
|
420 |
|
421 lemma "lfp(eufix A B) \<subseteq> eusem A B" |
|
422 apply(rule lfp_lowerbound) |
|
423 apply(clarsimp simp add: eusem_def eufix_def); |
|
424 apply(erule disjE); |
|
425 apply(rule_tac x = "apath x" in bexI); |
|
426 apply(rule_tac x = 0 in exI); |
|
427 apply simp; |
|
428 apply simp; |
|
429 apply(clarify); |
|
430 apply(rule_tac x = "pcons xb p" in bexI); |
|
431 apply(rule_tac x = "j+1" in exI); |
|
432 apply (simp add: pcons_def split: nat.split); |
|
433 apply (simp add: pcons_PathI) |
|
434 done |
|
435 *) |
|
436 (*>*) |
|
437 |
|
438 text{* Let us close this section with a few words about the executability of |
|
439 our model checkers. It is clear that if all sets are finite, they can be |
|
440 represented as lists and the usual set operations are easily |
|
441 implemented. Only @{const lfp} requires a little thought. Fortunately, theory |
|
442 @{text While_Combinator} in the Library~\cite{HOL-Library} provides a |
|
443 theorem stating that in the case of finite sets and a monotone |
|
444 function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by |
|
445 iterated application of @{term F} to~@{term"{}"} until a fixed point is |
|
446 reached. It is actually possible to generate executable functional programs |
|
447 from HOL definitions, but that is beyond the scope of the tutorial.% |
|
448 \index{CTL|)} *} |
|
449 (*<*)end(*>*) |
|