34 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" | |
34 "s \<Turnstile> AX f = (\<forall>t. (s,t) \<in> M \<longrightarrow> t \<Turnstile> f)" | |
35 "s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)" |
35 "s \<Turnstile> EF f = (\<exists>t. (s,t) \<in> M\<^sup>* \<and> t \<Turnstile> f)" |
36 |
36 |
37 text\<open>\noindent |
37 text\<open>\noindent |
38 The first three equations should be self-explanatory. The temporal formula |
38 The first three equations should be self-explanatory. The temporal formula |
39 @{term"AX f"} means that @{term f} is true in \emph{A}ll ne\emph{X}t states whereas |
39 \<^term>\<open>AX f\<close> means that \<^term>\<open>f\<close> is true in \emph{A}ll ne\emph{X}t states whereas |
40 @{term"EF f"} means that there \emph{E}xists some \emph{F}uture state in which @{term f} is |
40 \<^term>\<open>EF f\<close> means that there \emph{E}xists some \emph{F}uture state in which \<^term>\<open>f\<close> is |
41 true. The future is expressed via \<open>\<^sup>*\<close>, the reflexive transitive |
41 true. The future is expressed via \<open>\<^sup>*\<close>, the reflexive transitive |
42 closure. Because of reflexivity, the future includes the present. |
42 closure. Because of reflexivity, the future includes the present. |
43 |
43 |
44 Now we come to the model checker itself. It maps a formula into the |
44 Now we come to the model checker itself. It maps a formula into the |
45 set of states where the formula is true. It too is defined by |
45 set of states where the formula is true. It too is defined by |
51 "mc(And f g) = mc f \<inter> mc g" | |
51 "mc(And f g) = mc f \<inter> mc g" | |
52 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" | |
52 "mc(AX f) = {s. \<forall>t. (s,t) \<in> M \<longrightarrow> t \<in> mc f}" | |
53 "mc(EF f) = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))" |
53 "mc(EF f) = lfp(\<lambda>T. mc f \<union> (M\<inverse> `` T))" |
54 |
54 |
55 text\<open>\noindent |
55 text\<open>\noindent |
56 Only the equation for @{term EF} deserves some comments. Remember that the |
56 Only the equation for \<^term>\<open>EF\<close> deserves some comments. Remember that the |
57 postfix \<open>\<inverse>\<close> and the infix \<open>``\<close> are predefined and denote the |
57 postfix \<open>\<inverse>\<close> and the infix \<open>``\<close> are predefined and denote the |
58 converse of a relation and the image of a set under a relation. Thus |
58 converse of a relation and the image of a set under a relation. Thus |
59 @{term "M\<inverse> `` T"} is the set of all predecessors of @{term T} and the least |
59 \<^term>\<open>M\<inverse> `` T\<close> is the set of all predecessors of \<^term>\<open>T\<close> and the least |
60 fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set |
60 fixed point (\<^term>\<open>lfp\<close>) of \<^term>\<open>\<lambda>T. mc f \<union> M\<inverse> `` T\<close> is the least set |
61 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you |
61 \<^term>\<open>T\<close> containing \<^term>\<open>mc f\<close> and all predecessors of \<^term>\<open>T\<close>. If you |
62 find it hard to see that @{term"mc(EF f)"} contains exactly those states from |
62 find it hard to see that \<^term>\<open>mc(EF f)\<close> contains exactly those states from |
63 which there is a path to a state where @{term f} is true, do not worry --- this |
63 which there is a path to a state where \<^term>\<open>f\<close> is true, do not worry --- this |
64 will be proved in a moment. |
64 will be proved in a moment. |
65 |
65 |
66 First we prove monotonicity of the function inside @{term lfp} |
66 First we prove monotonicity of the function inside \<^term>\<open>lfp\<close> |
67 in order to make sure it really has a least fixed point. |
67 in order to make sure it really has a least fixed point. |
68 \<close> |
68 \<close> |
69 |
69 |
70 lemma mono_ef: "mono(\<lambda>T. A \<union> (M\<inverse> `` T))" |
70 lemma mono_ef: "mono(\<lambda>T. A \<union> (M\<inverse> `` T))" |
71 apply(rule monoI) |
71 apply(rule monoI) |
90 apply(simp)(*<*)apply(rename_tac s)(*>*) |
90 apply(simp)(*<*)apply(rename_tac s)(*>*) |
91 |
91 |
92 txt\<open>\noindent |
92 txt\<open>\noindent |
93 Simplification leaves us with the following first subgoal |
93 Simplification leaves us with the following first subgoal |
94 @{subgoals[display,indent=0,goals_limit=1]} |
94 @{subgoals[display,indent=0,goals_limit=1]} |
95 which is proved by @{term lfp}-induction: |
95 which is proved by \<^term>\<open>lfp\<close>-induction: |
96 \<close> |
96 \<close> |
97 |
97 |
98 apply(erule lfp_induct_set) |
98 apply(erule lfp_induct_set) |
99 apply(rule mono_ef) |
99 apply(rule mono_ef) |
100 apply(simp) |
100 apply(simp) |
121 apply(simp, clarify) |
121 apply(simp, clarify) |
122 |
122 |
123 txt\<open>\noindent |
123 txt\<open>\noindent |
124 After simplification and clarification we are left with |
124 After simplification and clarification we are left with |
125 @{subgoals[display,indent=0,goals_limit=1]} |
125 @{subgoals[display,indent=0,goals_limit=1]} |
126 This goal is proved by induction on @{term"(s,t)\<in>M\<^sup>*"}. But since the model |
126 This goal is proved by induction on \<^term>\<open>(s,t)\<in>M\<^sup>*\<close>. But since the model |
127 checker works backwards (from @{term t} to @{term s}), we cannot use the |
127 checker works backwards (from \<^term>\<open>t\<close> to \<^term>\<open>s\<close>), we cannot use the |
128 induction theorem @{thm[source]rtrancl_induct}: it works in the |
128 induction theorem @{thm[source]rtrancl_induct}: it works in the |
129 forward direction. Fortunately the converse induction theorem |
129 forward direction. Fortunately the converse induction theorem |
130 @{thm[source]converse_rtrancl_induct} already exists: |
130 @{thm[source]converse_rtrancl_induct} already exists: |
131 @{thm[display,margin=60]converse_rtrancl_induct[no_vars]} |
131 @{thm[display,margin=60]converse_rtrancl_induct[no_vars]} |
132 It says that if @{prop"(a,b)\<in>r\<^sup>*"} and we know @{prop"P b"} then we can infer |
132 It says that if \<^prop>\<open>(a,b)\<in>r\<^sup>*\<close> and we know \<^prop>\<open>P b\<close> then we can infer |
133 @{prop"P a"} provided each step backwards from a predecessor @{term z} of |
133 \<^prop>\<open>P a\<close> provided each step backwards from a predecessor \<^term>\<open>z\<close> of |
134 @{term b} preserves @{term P}. |
134 \<^term>\<open>b\<close> preserves \<^term>\<open>P\<close>. |
135 \<close> |
135 \<close> |
136 |
136 |
137 apply(erule converse_rtrancl_induct) |
137 apply(erule converse_rtrancl_induct) |
138 |
138 |
139 txt\<open>\noindent |
139 txt\<open>\noindent |
140 The base case |
140 The base case |
141 @{subgoals[display,indent=0,goals_limit=1]} |
141 @{subgoals[display,indent=0,goals_limit=1]} |
142 is solved by unrolling @{term lfp} once |
142 is solved by unrolling \<^term>\<open>lfp\<close> once |
143 \<close> |
143 \<close> |
144 |
144 |
145 apply(subst lfp_unfold[OF mono_ef]) |
145 apply(subst lfp_unfold[OF mono_ef]) |
146 |
146 |
147 txt\<open> |
147 txt\<open> |
169 apply(auto simp add: EF_lemma) |
169 apply(auto simp add: EF_lemma) |
170 done |
170 done |
171 |
171 |
172 text\<open> |
172 text\<open> |
173 \begin{exercise} |
173 \begin{exercise} |
174 @{term AX} has a dual operator @{term EN} |
174 \<^term>\<open>AX\<close> has a dual operator \<^term>\<open>EN\<close> |
175 (``there exists a next state such that'')% |
175 (``there exists a next state such that'')% |
176 \footnote{We cannot use the customary \<open>EX\<close>: it is reserved |
176 \footnote{We cannot use the customary \<open>EX\<close>: it is reserved |
177 as the \textsc{ascii}-equivalent of \<open>\<exists>\<close>.} |
177 as the \textsc{ascii}-equivalent of \<open>\<exists>\<close>.} |
178 with the intended semantics |
178 with the intended semantics |
179 @{prop[display]"(s \<Turnstile> EN f) = (\<exists>t. (s,t) \<in> M \<and> t \<Turnstile> f)"} |
179 @{prop[display]"(s \<Turnstile> EN f) = (\<exists>t. (s,t) \<in> M \<and> t \<Turnstile> f)"} |
180 Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How? |
180 Fortunately, \<^term>\<open>EN f\<close> can already be expressed as a PDL formula. How? |
181 |
181 |
182 Show that the semantics for @{term EF} satisfies the following recursion equation: |
182 Show that the semantics for \<^term>\<open>EF\<close> satisfies the following recursion equation: |
183 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"} |
183 @{prop[display]"(s \<Turnstile> EF f) = (s \<Turnstile> f | s \<Turnstile> EN(EF f))"} |
184 \end{exercise} |
184 \end{exercise} |
185 \index{PDL|)} |
185 \index{PDL|)} |
186 \<close> |
186 \<close> |
187 (*<*) |
187 (*<*) |