10123
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{CTL}%
|
10133
|
4 |
%
|
10971
|
5 |
\isamarkupsubsection{Computation Tree Logic --- CTL%
|
10395
|
6 |
}
|
10149
|
7 |
%
|
|
8 |
\begin{isamarkuptext}%
|
10217
|
9 |
\label{sec:CTL}
|
10867
|
10 |
The semantics of PDL only needs reflexive transitive closure.
|
|
11 |
Let us be adventurous and introduce a more expressive temporal operator.
|
|
12 |
We extend the datatype
|
10149
|
13 |
\isa{formula} by a new constructor%
|
|
14 |
\end{isamarkuptext}%
|
|
15 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
|
|
16 |
\begin{isamarkuptext}%
|
|
17 |
\noindent
|
10983
|
18 |
which stands for ``\emph{A}lways in the \emph{F}uture'':
|
|
19 |
on all infinite paths, at some point the formula holds.
|
|
20 |
Formalizing the notion of an infinite path is easy
|
10159
|
21 |
in HOL: it is simply a function from \isa{nat} to \isa{state}.%
|
10149
|
22 |
\end{isamarkuptext}%
|
10123
|
23 |
\isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
|
10187
|
24 |
\ \ \ \ \ \ \ \ \ {\isachardoublequote}Paths\ s\ {\isasymequiv}\ {\isacharbraceleft}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharparenright}{\isacharbraceright}{\isachardoublequote}%
|
10149
|
25 |
\begin{isamarkuptext}%
|
|
26 |
\noindent
|
10159
|
27 |
This definition allows a very succinct statement of the semantics of \isa{AF}:
|
10867
|
28 |
\footnote{Do not be misled: neither datatypes nor recursive functions can be
|
10149
|
29 |
extended by new constructors or equations. This is just a trick of the
|
|
30 |
presentation. In reality one has to define a new datatype and a new function.}%
|
|
31 |
\end{isamarkuptext}%
|
|
32 |
{\isachardoublequote}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequote}%
|
|
33 |
\begin{isamarkuptext}%
|
|
34 |
\noindent
|
|
35 |
Model checking \isa{AF} involves a function which
|
10159
|
36 |
is just complicated enough to warrant a separate definition:%
|
10149
|
37 |
\end{isamarkuptext}%
|
10123
|
38 |
\isacommand{constdefs}\ af\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequote}\isanewline
|
10149
|
39 |
\ \ \ \ \ \ \ \ \ {\isachardoublequote}af\ A\ T\ {\isasymequiv}\ A\ {\isasymunion}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\ t\ {\isasymin}\ T{\isacharbraceright}{\isachardoublequote}%
|
|
40 |
\begin{isamarkuptext}%
|
|
41 |
\noindent
|
10867
|
42 |
Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that includes
|
10159
|
43 |
\isa{mc\ f} and all states all of whose direct successors are in \isa{T}:%
|
|
44 |
\end{isamarkuptext}%
|
|
45 |
{\isachardoublequote}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
|
|
46 |
\begin{isamarkuptext}%
|
|
47 |
\noindent
|
|
48 |
Because \isa{af} is monotone in its second argument (and also its first, but
|
10983
|
49 |
that is irrelevant), \isa{af\ A} has a least fixed point:%
|
10149
|
50 |
\end{isamarkuptext}%
|
10123
|
51 |
\isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
|
10149
|
52 |
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
|
10159
|
53 |
\isacommand{apply}\ blast\isanewline
|
|
54 |
\isacommand{done}%
|
10149
|
55 |
\begin{isamarkuptext}%
|
10867
|
56 |
All we need to prove now is \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ AF\ f{\isacharbraceright}}, which states
|
|
57 |
that \isa{mc} and \isa{{\isasymTurnstile}} agree for \isa{AF}\@.
|
|
58 |
This time we prove the two inclusions separately, starting
|
10159
|
59 |
with the easy one:%
|
|
60 |
\end{isamarkuptext}%
|
10187
|
61 |
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{1}}{\isacharcolon}\isanewline
|
10159
|
62 |
\ \ {\isachardoublequote}lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymsubseteq}\ {\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}{\isachardoublequote}%
|
|
63 |
\begin{isamarkuptxt}%
|
10149
|
64 |
\noindent
|
10225
|
65 |
In contrast to the analogous property for \isa{EF}, and just
|
10242
|
66 |
for a change, we do not use fixed point induction but a weaker theorem,
|
10995
|
67 |
also known in the literature (after David Park) as \emph{Park-induction}:
|
|
68 |
\begin{center}
|
|
69 |
\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound})
|
|
70 |
\end{center}
|
10225
|
71 |
The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise,
|
10281
|
72 |
a decision that clarification takes for us:%
|
10159
|
73 |
\end{isamarkuptxt}%
|
10225
|
74 |
\isacommand{apply}{\isacharparenleft}rule\ lfp{\isacharunderscore}lowerbound{\isacharparenright}\isanewline
|
10159
|
75 |
\isacommand{apply}{\isacharparenleft}clarsimp\ simp\ add{\isacharcolon}\ af{\isacharunderscore}def\ Paths{\isacharunderscore}def{\isacharparenright}%
|
|
76 |
\begin{isamarkuptxt}%
|
10363
|
77 |
\begin{isabelle}%
|
10696
|
78 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}p\ {\isadigit{0}}\ {\isasymin}\ A\ {\isasymor}\isanewline
|
10950
|
79 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}p\ {\isadigit{0}}{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymlongrightarrow}\isanewline
|
|
80 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ }{\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
|
|
81 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}{\isasymforall}t{\isachardot}\ {\isacharparenleft}{\isasymforall}p{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
|
|
82 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isasymrbrakk}\isanewline
|
|
83 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
|
10159
|
84 |
\end{isabelle}
|
10187
|
85 |
Now we eliminate the disjunction. The case \isa{p\ {\isadigit{0}}\ {\isasymin}\ A} is trivial:%
|
10159
|
86 |
\end{isamarkuptxt}%
|
10123
|
87 |
\isacommand{apply}{\isacharparenleft}erule\ disjE{\isacharparenright}\isanewline
|
10159
|
88 |
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}%
|
|
89 |
\begin{isamarkuptxt}%
|
|
90 |
\noindent
|
10187
|
91 |
In the other case we set \isa{t} to \isa{p\ {\isadigit{1}}} and simplify matters:%
|
10159
|
92 |
\end{isamarkuptxt}%
|
10187
|
93 |
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}p\ {\isadigit{1}}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
|
10159
|
94 |
\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
|
|
95 |
\begin{isamarkuptxt}%
|
10363
|
96 |
\begin{isabelle}%
|
10696
|
97 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ {\isasymlbrakk}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}\ p\ {\isacharparenleft}Suc\ i{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M{\isacharsemicolon}\isanewline
|
10950
|
98 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ }{\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
|
|
99 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ \ \ \ {\isasymforall}pa{\isachardot}\ }{\isacharparenleft}{\isasymexists}i{\isachardot}\ pa\ i\ {\isasymin}\ A{\isacharparenright}{\isasymrbrakk}\isanewline
|
|
100 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}p{\isachardot}\ }{\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymin}\ A%
|
10159
|
101 |
\end{isabelle}
|
10187
|
102 |
It merely remains to set \isa{pa} to \isa{{\isasymlambda}i{\isachardot}\ p\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}}, i.e.\ \isa{p} without its
|
10159
|
103 |
first element. The rest is practically automatic:%
|
|
104 |
\end{isamarkuptxt}%
|
10187
|
105 |
\isacommand{apply}{\isacharparenleft}erule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}{\isasymlambda}i{\isachardot}\ p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isakeyword{in}\ allE{\isacharparenright}\isanewline
|
10159
|
106 |
\isacommand{apply}\ simp\isanewline
|
|
107 |
\isacommand{apply}\ blast\isanewline
|
|
108 |
\isacommand{done}%
|
10123
|
109 |
\begin{isamarkuptext}%
|
10867
|
110 |
The opposite inclusion is proved by contradiction: if some state
|
10159
|
111 |
\isa{s} is not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then we can construct an
|
10123
|
112 |
infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
|
|
113 |
that by unfolding \isa{lfp} we find that if \isa{s} is not in
|
|
114 |
\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
|
10983
|
115 |
direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite
|
10123
|
116 |
\isa{A}-avoiding path. Let us formalize this sketch.
|
|
117 |
|
10867
|
118 |
The one-step argument in the sketch above
|
|
119 |
is proved by a variant of contraposition:%
|
10123
|
120 |
\end{isamarkuptext}%
|
|
121 |
\isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
|
10983
|
122 |
\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
|
10237
|
123 |
\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline
|
11231
|
124 |
\isacommand{apply}{\isacharparenleft}subst\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharparenright}\isanewline
|
10159
|
125 |
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
|
|
126 |
\isacommand{done}%
|
10123
|
127 |
\begin{isamarkuptext}%
|
|
128 |
\noindent
|
10867
|
129 |
We assume the negation of the conclusion and prove \isa{s\ {\isasymin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}}.
|
10237
|
130 |
Unfolding \isa{lfp} once and
|
10123
|
131 |
simplifying with the definition of \isa{af} finishes the proof.
|
|
132 |
|
|
133 |
Now we iterate this process. The following construction of the desired
|
10895
|
134 |
path is parameterized by a predicate \isa{Q} that should hold along the path:%
|
10123
|
135 |
\end{isamarkuptext}%
|
|
136 |
\isacommand{consts}\ path\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}state\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}{\isachardoublequote}\isanewline
|
|
137 |
\isacommand{primrec}\isanewline
|
10895
|
138 |
{\isachardoublequote}path\ s\ Q\ {\isadigit{0}}\ {\isacharequal}\ s{\isachardoublequote}\isanewline
|
|
139 |
{\isachardoublequote}path\ s\ Q\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ n{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isachardoublequote}%
|
10123
|
140 |
\begin{isamarkuptext}%
|
|
141 |
\noindent
|
10187
|
142 |
Element \isa{n\ {\isacharplus}\ {\isadigit{1}}} on this path is some arbitrary successor
|
10895
|
143 |
\isa{t} of element \isa{n} such that \isa{Q\ t} holds. Remember that \isa{SOME\ t{\isachardot}\ R\ t}
|
10654
|
144 |
is some arbitrary but fixed \isa{t} such that \isa{R\ t} holds (see \S\ref{sec:SOME}). Of
|
10867
|
145 |
course, such a \isa{t} need not exist, but that is of no
|
|
146 |
concern to us since we will only use \isa{path} when a
|
10123
|
147 |
suitable \isa{t} does exist.
|
|
148 |
|
10895
|
149 |
Let us show that if each state \isa{s} that satisfies \isa{Q}
|
|
150 |
has a successor that again satisfies \isa{Q}, then there exists an infinite \isa{Q}-path:%
|
10123
|
151 |
\end{isamarkuptext}%
|
10159
|
152 |
\isacommand{lemma}\ infinity{\isacharunderscore}lemma{\isacharcolon}\isanewline
|
10895
|
153 |
\ \ {\isachardoublequote}{\isasymlbrakk}\ Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\isanewline
|
|
154 |
\ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
|
10123
|
155 |
\begin{isamarkuptxt}%
|
|
156 |
\noindent
|
10983
|
157 |
First we rephrase the conclusion slightly because we need to prove simultaneously
|
|
158 |
both the path property and the fact that \isa{Q} holds:%
|
10123
|
159 |
\end{isamarkuptxt}%
|
10895
|
160 |
\isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
|
10159
|
161 |
\begin{isamarkuptxt}%
|
|
162 |
\noindent
|
|
163 |
From this proposition the original goal follows easily:%
|
|
164 |
\end{isamarkuptxt}%
|
|
165 |
\ \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}Paths{\isacharunderscore}def{\isacharcomma}\ blast{\isacharparenright}%
|
|
166 |
\begin{isamarkuptxt}%
|
|
167 |
\noindent
|
10895
|
168 |
The new subgoal is proved by providing the witness \isa{path\ s\ Q} for \isa{p}:%
|
10159
|
169 |
\end{isamarkuptxt}%
|
10895
|
170 |
\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequote}path\ s\ Q{\isachardoublequote}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
|
10159
|
171 |
\isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
|
|
172 |
\begin{isamarkuptxt}%
|
|
173 |
\noindent
|
10983
|
174 |
After simplification and clarification, the subgoal has the following form
|
10363
|
175 |
\begin{isabelle}%
|
10895
|
176 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
|
10950
|
177 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
|
|
178 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymLongrightarrow}\ }Q\ {\isacharparenleft}path\ s\ Q\ i{\isacharparenright}%
|
10159
|
179 |
\end{isabelle}
|
|
180 |
and invites a proof by induction on \isa{i}:%
|
|
181 |
\end{isamarkuptxt}%
|
|
182 |
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ i{\isacharparenright}\isanewline
|
|
183 |
\ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
|
10123
|
184 |
\begin{isamarkuptxt}%
|
|
185 |
\noindent
|
10983
|
186 |
After simplification, the base case boils down to
|
10363
|
187 |
\begin{isabelle}%
|
10895
|
188 |
\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
|
10950
|
189 |
\isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M%
|
10159
|
190 |
\end{isabelle}
|
|
191 |
The conclusion looks exceedingly trivial: after all, \isa{t} is chosen such that \isa{{\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M}
|
|
192 |
holds. However, we first have to show that such a \isa{t} actually exists! This reasoning
|
10187
|
193 |
is embodied in the theorem \isa{someI{\isadigit{2}}{\isacharunderscore}ex}:
|
10159
|
194 |
\begin{isabelle}%
|
10696
|
195 |
\ \ \ \ \ {\isasymlbrakk}{\isasymexists}a{\isachardot}\ {\isacharquery}P\ a{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q\ {\isacharparenleft}SOME\ x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}%
|
10159
|
196 |
\end{isabelle}
|
|
197 |
When we apply this theorem as an introduction rule, \isa{{\isacharquery}P\ x} becomes
|
10895
|
198 |
\isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ x} and \isa{{\isacharquery}Q\ x} becomes \isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M} and we have to prove
|
|
199 |
two subgoals: \isa{{\isasymexists}a{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ a{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ a}, which follows from the assumptions, and
|
|
200 |
\isa{{\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ x\ {\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ M}, which is trivial. Thus it is not surprising that
|
10159
|
201 |
\isa{fast} can prove the base case quickly:%
|
10123
|
202 |
\end{isamarkuptxt}%
|
10187
|
203 |
\ \isacommand{apply}{\isacharparenleft}fast\ intro{\isacharcolon}someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}%
|
10159
|
204 |
\begin{isamarkuptxt}%
|
|
205 |
\noindent
|
10212
|
206 |
What is worth noting here is that we have used \isa{fast} rather than
|
|
207 |
\isa{blast}. The reason is that \isa{blast} would fail because it cannot
|
|
208 |
cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
|
11149
|
209 |
subgoal is non-trivial because of the nested schematic variables. For
|
10212
|
210 |
efficiency reasons \isa{blast} does not even attempt such unifications.
|
|
211 |
Although \isa{fast} can in principle cope with complicated unification
|
|
212 |
problems, in practice the number of unifiers arising is often prohibitive and
|
|
213 |
the offending rule may need to be applied explicitly rather than
|
|
214 |
automatically. This is what happens in the step case.
|
10159
|
215 |
|
10212
|
216 |
The induction step is similar, but more involved, because now we face nested
|
|
217 |
occurrences of \isa{SOME}. As a result, \isa{fast} is no longer able to
|
|
218 |
solve the subgoal and we apply \isa{someI{\isadigit{2}}{\isacharunderscore}ex} by hand. We merely
|
|
219 |
show the proof commands but do not describe the details:%
|
10159
|
220 |
\end{isamarkuptxt}%
|
10123
|
221 |
\isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline
|
10187
|
222 |
\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
|
10123
|
223 |
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
|
10187
|
224 |
\isacommand{apply}{\isacharparenleft}rule\ someI{\isadigit{2}}{\isacharunderscore}ex{\isacharparenright}\isanewline
|
10123
|
225 |
\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
|
10159
|
226 |
\isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
|
|
227 |
\isacommand{done}%
|
|
228 |
\begin{isamarkuptext}%
|
10867
|
229 |
Function \isa{path} has fulfilled its purpose now and can be forgotten.
|
|
230 |
It was merely defined to provide the witness in the proof of the
|
10171
|
231 |
\isa{infinity{\isacharunderscore}lemma}. Aficionados of minimal proofs might like to know
|
10159
|
232 |
that we could have given the witness without having to define a new function:
|
|
233 |
the term
|
|
234 |
\begin{isabelle}%
|
10895
|
235 |
\ \ \ \ \ nat{\isacharunderscore}rec\ s\ {\isacharparenleft}{\isasymlambda}n\ t{\isachardot}\ SOME\ u{\isachardot}\ {\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ u{\isacharparenright}%
|
10159
|
236 |
\end{isabelle}
|
10895
|
237 |
is extensionally equal to \isa{path\ s\ Q},
|
10867
|
238 |
where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.%
|
10159
|
239 |
\end{isamarkuptext}%
|
|
240 |
%
|
|
241 |
\begin{isamarkuptext}%
|
10187
|
242 |
At last we can prove the opposite direction of \isa{AF{\isacharunderscore}lemma{\isadigit{1}}}:%
|
10159
|
243 |
\end{isamarkuptext}%
|
10866
|
244 |
\isacommand{theorem}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharcolon}\ {\isachardoublequote}{\isacharbraceleft}s{\isachardot}\ {\isasymforall}\ p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}\ i{\isachardot}\ p\ i\ {\isasymin}\ A{\isacharbraceright}\ {\isasymsubseteq}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}%
|
10159
|
245 |
\begin{isamarkuptxt}%
|
|
246 |
\noindent
|
10237
|
247 |
The proof is again pointwise and then by contraposition:%
|
10159
|
248 |
\end{isamarkuptxt}%
|
10123
|
249 |
\isacommand{apply}{\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline
|
10237
|
250 |
\isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}pp{\isacharparenright}\isanewline
|
10159
|
251 |
\isacommand{apply}\ simp%
|
|
252 |
\begin{isamarkuptxt}%
|
10363
|
253 |
\begin{isabelle}%
|
|
254 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A%
|
10159
|
255 |
\end{isabelle}
|
|
256 |
Applying the \isa{infinity{\isacharunderscore}lemma} as a destruction rule leaves two subgoals, the second
|
|
257 |
premise of \isa{infinity{\isacharunderscore}lemma} and the original subgoal:%
|
|
258 |
\end{isamarkuptxt}%
|
|
259 |
\isacommand{apply}{\isacharparenleft}drule\ infinity{\isacharunderscore}lemma{\isacharparenright}%
|
|
260 |
\begin{isamarkuptxt}%
|
10363
|
261 |
\begin{isabelle}%
|
|
262 |
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\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
|
|
263 |
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ lfp\ {\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
|
10950
|
264 |
\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ }{\isasymexists}p{\isasymin}Paths\ x{\isachardot}\ {\isasymforall}i{\isachardot}\ p\ i\ {\isasymnotin}\ A%
|
10159
|
265 |
\end{isabelle}
|
|
266 |
Both are solved automatically:%
|
|
267 |
\end{isamarkuptxt}%
|
|
268 |
\ \isacommand{apply}{\isacharparenleft}auto\ dest{\isacharcolon}not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharparenright}\isanewline
|
|
269 |
\isacommand{done}%
|
|
270 |
\begin{isamarkuptext}%
|
10867
|
271 |
If you find these proofs too complicated, we recommend that you read
|
|
272 |
\S\ref{sec:CTL-revisited}, where we show how inductive definitions lead to
|
10217
|
273 |
simpler arguments.
|
|
274 |
|
|
275 |
The main theorem is proved as for PDL, except that we also derive the
|
|
276 |
necessary equality \isa{lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isacharequal}\ {\isachardot}{\isachardot}{\isachardot}} by combining
|
|
277 |
\isa{AF{\isacharunderscore}lemma{\isadigit{1}}} and \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} on the spot:%
|
10159
|
278 |
\end{isamarkuptext}%
|
10123
|
279 |
\isacommand{theorem}\ {\isachardoublequote}mc\ f\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ f{\isacharbraceright}{\isachardoublequote}\isanewline
|
|
280 |
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ f{\isacharparenright}\isanewline
|
10187
|
281 |
\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline
|
10159
|
282 |
\isacommand{done}%
|
|
283 |
\begin{isamarkuptext}%
|
10867
|
284 |
The language defined above is not quite CTL\@. The latter also includes an
|
10983
|
285 |
until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path
|
|
286 |
where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. With the help
|
10281
|
287 |
of an auxiliary function%
|
|
288 |
\end{isamarkuptext}%
|
|
289 |
\isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
|
|
290 |
\isacommand{primrec}\isanewline
|
|
291 |
{\isachardoublequote}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequote}\isanewline
|
|
292 |
{\isachardoublequote}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequote}%
|
|
293 |
\begin{isamarkuptext}%
|
|
294 |
\noindent
|
|
295 |
the semantics of \isa{EU} is straightforward:
|
10171
|
296 |
\begin{isabelle}%
|
10983
|
297 |
\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}%
|
10171
|
298 |
\end{isabelle}
|
10281
|
299 |
Note that \isa{EU} is not definable in terms of the other operators!
|
|
300 |
|
|
301 |
Model checking \isa{EU} is again a least fixed point construction:
|
10171
|
302 |
\begin{isabelle}%
|
10839
|
303 |
\ \ \ \ \ mc{\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ lfp{\isacharparenleft}{\isasymlambda}T{\isachardot}\ mc\ g\ {\isasymunion}\ mc\ f\ {\isasyminter}\ {\isacharparenleft}M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T{\isacharparenright}{\isacharparenright}%
|
10171
|
304 |
\end{isabelle}
|
10281
|
305 |
|
|
306 |
\begin{exercise}
|
|
307 |
Extend the datatype of formulae by the above until operator
|
|
308 |
and prove the equivalence between semantics and model checking, i.e.\ that
|
10186
|
309 |
\begin{isabelle}%
|
|
310 |
\ \ \ \ \ mc\ {\isacharparenleft}EU\ f\ g{\isacharparenright}\ {\isacharequal}\ {\isacharbraceleft}s{\isachardot}\ s\ {\isasymTurnstile}\ EU\ f\ g{\isacharbraceright}%
|
|
311 |
\end{isabelle}
|
|
312 |
%For readability you may want to annotate {term EU} with its customary syntax
|
|
313 |
%{text[display]"| EU formula formula E[_ U _]"}
|
|
314 |
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
|
|
315 |
\end{exercise}
|
10867
|
316 |
For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.%
|
10281
|
317 |
\end{isamarkuptext}%
|
|
318 |
%
|
|
319 |
\begin{isamarkuptext}%
|
10186
|
320 |
Let us close this section with a few words about the executability of our model checkers.
|
10159
|
321 |
It is clear that if all sets are finite, they can be represented as lists and the usual
|
|
322 |
set operations are easily implemented. Only \isa{lfp} requires a little thought.
|
10878
|
323 |
Fortunately, the HOL Library%
|
10983
|
324 |
\footnote{See theory \isa{While_Combinator}.}
|
10878
|
325 |
provides a theorem stating that
|
|
326 |
in the case of finite sets and a monotone function~\isa{F},
|
10983
|
327 |
the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
|
10242
|
328 |
a fixed point is reached. It is actually possible to generate executable functional programs
|
10159
|
329 |
from HOL definitions, but that is beyond the scope of the tutorial.%
|
|
330 |
\end{isamarkuptext}%
|
10123
|
331 |
\end{isabellebody}%
|
|
332 |
%%% Local Variables:
|
|
333 |
%%% mode: latex
|
|
334 |
%%% TeX-master: "root"
|
|
335 |
%%% End:
|