*** empty log message ***
authornipkow
Wed Oct 11 13:39:52 2000 +0200 (2000-10-11)
changeset 101924c2584e23ade
parent 10191 e77662e9cabd
child 10193 1d6ae1ef8e64
*** empty log message ***
doc-src/TutorialI/CTL/Base.thy
doc-src/TutorialI/CTL/CTL.thy
doc-src/TutorialI/CTL/document/Base.tex
doc-src/TutorialI/CTL/document/CTL.tex
     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.