equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{PDL}% |
3 \def\isabellecontext{PDL}% |
4 % |
4 % |
5 \isamarkupsubsection{Propositional Dynamic Logic---PDL% |
5 \isamarkupsubsection{Propositional Dynamic Logic --- PDL% |
6 } |
6 } |
7 % |
7 % |
8 \begin{isamarkuptext}% |
8 \begin{isamarkuptext}% |
9 \index{PDL|(} |
9 \index{PDL|(} |
10 The formulae of PDL are built up from atomic propositions via the customary |
10 The formulae of PDL are built up from atomic propositions via the customary |
66 converse of a relation and the image of a set under a relation. Thus |
66 converse of a relation and the image of a set under a relation. Thus |
67 \isa{M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the set of all predecessors of \isa{T} and the least |
67 \isa{M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the set of all predecessors of \isa{T} and the least |
68 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set |
68 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set |
69 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you |
69 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you |
70 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from |
70 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from |
71 which there is a path to a state where \isa{f} is true, do not worry---that |
71 which there is a path to a state where \isa{f} is true, do not worry --- that |
72 will be proved in a moment. |
72 will be proved in a moment. |
73 |
73 |
74 First we prove monotonicity of the function inside \isa{lfp} |
74 First we prove monotonicity of the function inside \isa{lfp} |
75 in order to make sure it really has a least fixed point.% |
75 in order to make sure it really has a least fixed point.% |
76 \end{isamarkuptext}% |
76 \end{isamarkuptext}% |