1 (*<*)theory PDL = Base:(*>*)
3 subsection{*Propositional Dynamic Logic---PDL*}
6 The formulae of PDL are built up from atomic propositions via the customary
7 propositional connectives of negation and conjunction and the two temporal
8 connectives @{text AX} and @{text EF}. Since formulae are essentially
9 syntax trees, they are naturally modelled as a datatype:
12 datatype formula = Atom atom
19 This is almost the same as in the boolean expression case study in
22 The meaning of these formulae is given by saying which formula is true in
26 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80)
29 The syntax annotation allows us to write @{term"s \<Turnstile> f"} instead of
30 \hbox{@{text"valid s f"}}.
33 The definition of @{text"\<Turnstile>"} is by recursion over the syntax:
37 "s \<Turnstile> Atom a = (a \<in> L s)"
38 "s \<Turnstile> Neg f = (\<not>(s \<Turnstile> f))"
39 "s \<Turnstile> And f g = (s \<Turnstile> f \<and> s \<Turnstile> g)"
40 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)"
41 "s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)";
44 The first three equations should be self-explanatory. The temporal formula
45 @{term"AX f"} means that @{term f} is true in all next states whereas
46 @{term"EF f"} means that there exists some future state in which @{term f} is
47 true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive
48 closure. Because of reflexivity, the future includes the present.
50 Now we come to the model checker itself. It maps a formula into the set of
51 states where the formula is true and is defined by recursion over the syntax,
55 consts mc :: "formula \<Rightarrow> state set";
57 "mc(Atom a) = {s. a \<in> L s}"
59 "mc(And f g) = mc f \<inter> mc g"
60 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}"
61 "mc(EF f) = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))"
64 Only the equation for @{term EF} deserves some comments. Remember that the
65 postfix @{text"\<inverse>"} and the infix @{text"``"} are predefined and denote the
66 converse of a relation and the image of a set under a relation. Thus
67 @{term "M\<inverse> `` T"} is the set of all predecessors of @{term T} and the least
68 fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
69 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
70 find it hard to see that @{term"mc(EF f)"} contains exactly those states from
71 which there is a path to a state where @{term f} is true, do not worry---that
72 will be proved in a moment.
74 First we prove monotonicity of the function inside @{term lfp}
75 in order to make sure it really has a least fixed point.
78 lemma mono_ef: "mono(\<lambda>T. A \<union> (M\<inverse> `` T))"
84 Now we can relate model checking and semantics. For the @{text EF} case we need
89 "lfp(\<lambda>T. A \<union> (M\<inverse> `` T)) = {s. \<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<in> A}"
92 The equality is proved in the canonical fashion by proving that each set
93 includes the other; the inclusion is shown pointwise:
96 apply(rule equalityI);
98 apply(simp)(*<*)apply(rename_tac s)(*>*)
101 Simplification leaves us with the following first subgoal
102 @{subgoals[display,indent=0,goals_limit=1]}
103 which is proved by @{term lfp}-induction:
106 apply(erule lfp_induct)
109 (*pr(latex xsymbols symbols);*)
111 Having disposed of the monotonicity subgoal,
112 simplification leaves us with the following main goal
114 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ A\ {\isasymor}\isanewline
115 \ \ \ \ \ \ \ \ \ x\ {\isasymin}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}{\isacharbackquote}\ {\isacharparenleft}lfp\ {\isacharparenleft}\dots{\isacharparenright}\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A{\isacharbraceright}{\isacharparenright}\isanewline
116 \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}t{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\isactrlsup {\isacharasterisk}\ {\isasymand}\ t\ {\isasymin}\ A
118 which is proved by @{text blast} with the help of transitivity of @{text"\<^sup>*"}:
121 apply(blast intro: rtrancl_trans);
124 We now return to the second set inclusion subgoal, which is again proved
132 After simplification and clarification we are left with
133 @{subgoals[display,indent=0,goals_limit=1]}
134 This goal is proved by induction on @{term"(s,t)\<in>M\<^sup>*"}. But since the model
135 checker works backwards (from @{term t} to @{term s}), we cannot use the
136 induction theorem @{thm[source]rtrancl_induct} because it works in the
137 forward direction. Fortunately the converse induction theorem
138 @{thm[source]converse_rtrancl_induct} already exists:
139 @{thm[display,margin=60]converse_rtrancl_induct[no_vars]}
140 It says that if @{prop"(a,b):r\<^sup>*"} and we know @{prop"P b"} then we can infer
141 @{prop"P a"} provided each step backwards from a predecessor @{term z} of
142 @{term b} preserves @{term P}.
145 apply(erule converse_rtrancl_induct)
149 @{subgoals[display,indent=0,goals_limit=1]}
150 is solved by unrolling @{term lfp} once
153 apply(rule ssubst[OF lfp_unfold[OF mono_ef]])
156 @{subgoals[display,indent=0,goals_limit=1]}
157 and disposing of the resulting trivial subgoal automatically:
163 The proof of the induction step is identical to the one for the base case:
166 apply(rule ssubst[OF lfp_unfold[OF mono_ef]])
171 The main theorem is proved in the familiar manner: induction followed by
172 @{text auto} augmented with the lemma as a simplification rule.
175 theorem "mc f = {s. s \<Turnstile> f}";
177 apply(auto simp add:EF_lemma);
182 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
183 as that is the ASCII equivalent of @{text"\<exists>"}}
184 (``there exists a next state such that'') with the intended semantics
185 @{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
186 Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
188 Show that the semantics for @{term EF} satisfies the following recursion equation:
189 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"}
194 theorem main: "mc f = {s. s \<Turnstile> f}";
196 apply(auto simp add:EF_lemma);
199 lemma aux: "s \<Turnstile> f = (s : mc f)";
200 apply(simp add:main);
203 lemma "(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> Neg(AX(Neg(EF f))))";
204 apply(simp only:aux);
206 apply(rule ssubst[OF lfp_unfold[OF mono_ef]], fast);