author | nipkow |

Wed Oct 11 13:39:52 2000 +0200 (2000-10-11) | |

changeset 10192 | 4c2584e23ade |

parent 10191 | e77662e9cabd |

child 10193 | 1d6ae1ef8e64 |

*** empty log message ***

1.1 --- a/doc-src/TutorialI/CTL/Base.thy Wed Oct 11 13:33:38 2000 +0200 1.2 +++ b/doc-src/TutorialI/CTL/Base.thy Wed Oct 11 13:39:52 2000 +0200 1.3 @@ -5,7 +5,7 @@ 1.4 text{* 1.5 Model checking is a very popular technique for the verification of finite 1.6 state systems (implementations) w.r.t.\ temporal logic formulae 1.7 -(specifications) \cite{Clarke,Huth-Ryan-book}. Its foundations are completely set theoretic 1.8 +(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic 1.9 and this section shall explore them a little in HOL. This is done in two steps: first 1.10 we consider a simple modal logic called propositional dynamic 1.11 logic (PDL) which we then extend to the temporal logic CTL used in many real

2.1 --- a/doc-src/TutorialI/CTL/CTL.thy Wed Oct 11 13:33:38 2000 +0200 2.2 +++ b/doc-src/TutorialI/CTL/CTL.thy Wed Oct 11 13:39:52 2000 +0200 2.3 @@ -386,7 +386,7 @@ 2.4 %{text[display]"| EU formula formula E[_ U _]"} 2.5 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}. 2.6 \end{exercise} 2.7 -For more CTL exercises see, for example \cite{Huth-Ryan-book,Clarke-as-well?}. 2.8 +For more CTL exercises see, for example \cite{Huth-Ryan-book}. 2.9 \bigskip 2.10 2.11 Let us close this section with a few words about the executability of our model checkers.

3.1 --- a/doc-src/TutorialI/CTL/document/Base.tex Wed Oct 11 13:33:38 2000 +0200 3.2 +++ b/doc-src/TutorialI/CTL/document/Base.tex Wed Oct 11 13:39:52 2000 +0200 3.3 @@ -7,7 +7,7 @@ 3.4 \begin{isamarkuptext}% 3.5 Model checking is a very popular technique for the verification of finite 3.6 state systems (implementations) w.r.t.\ temporal logic formulae 3.7 -(specifications) \cite{Clarke,Huth-Ryan-book}. Its foundations are completely set theoretic 3.8 +(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic 3.9 and this section shall explore them a little in HOL. This is done in two steps: first 3.10 we consider a simple modal logic called propositional dynamic 3.11 logic (PDL) which we then extend to the temporal logic CTL used in many real

4.1 --- a/doc-src/TutorialI/CTL/document/CTL.tex Wed Oct 11 13:33:38 2000 +0200 4.2 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Wed Oct 11 13:39:52 2000 +0200 4.3 @@ -291,7 +291,7 @@ 4.4 %{text[display]"| EU formula formula E[_ U _]"} 4.5 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}. 4.6 \end{exercise} 4.7 -For more CTL exercises see, for example \cite{Huth-Ryan-book,Clarke-as-well?}. 4.8 +For more CTL exercises see, for example \cite{Huth-Ryan-book}. 4.9 \bigskip 4.10 4.11 Let us close this section with a few words about the executability of our model checkers.