author nipkow Wed, 11 Oct 2000 13:39:52 +0200 changeset 10192 4c2584e23ade parent 10191 e77662e9cabd child 10193 1d6ae1ef8e64
*** empty log message ***
 doc-src/TutorialI/CTL/Base.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/CTL/CTL.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/CTL/document/Base.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/CTL/document/CTL.tex file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/CTL/Base.thy	Wed Oct 11 13:33:38 2000 +0200
+++ b/doc-src/TutorialI/CTL/Base.thy	Wed Oct 11 13:39:52 2000 +0200
@@ -5,7 +5,7 @@
text{*
Model checking is a very popular technique for the verification of finite
state systems (implementations) w.r.t.\ temporal logic formulae
-(specifications) \cite{Clarke,Huth-Ryan-book}. Its foundations are completely set theoretic
+(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
and this section shall explore them a little in HOL. This is done in two steps: first
we consider a simple modal logic called propositional dynamic
logic (PDL) which we then extend to the temporal logic CTL used in many real
--- a/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 11 13:33:38 2000 +0200
+++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Oct 11 13:39:52 2000 +0200
@@ -386,7 +386,7 @@
%{text[display]"| EU formula formula    E[_ U _]"}
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
\end{exercise}
-For more CTL exercises see, for example \cite{Huth-Ryan-book,Clarke-as-well?}.
+For more CTL exercises see, for example \cite{Huth-Ryan-book}.
\bigskip

Let us close this section with a few words about the executability of our model checkers.
--- a/doc-src/TutorialI/CTL/document/Base.tex	Wed Oct 11 13:33:38 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Wed Oct 11 13:39:52 2000 +0200
@@ -7,7 +7,7 @@
\begin{isamarkuptext}%
Model checking is a very popular technique for the verification of finite
state systems (implementations) w.r.t.\ temporal logic formulae
-(specifications) \cite{Clarke,Huth-Ryan-book}. Its foundations are completely set theoretic
+(specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic
and this section shall explore them a little in HOL. This is done in two steps: first
we consider a simple modal logic called propositional dynamic
logic (PDL) which we then extend to the temporal logic CTL used in many real
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Wed Oct 11 13:33:38 2000 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Oct 11 13:39:52 2000 +0200
@@ -291,7 +291,7 @@
%{text[display]"| EU formula formula    E[_ U _]"}
%which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}.
\end{exercise}
-For more CTL exercises see, for example \cite{Huth-Ryan-book,Clarke-as-well?}.
+For more CTL exercises see, for example \cite{Huth-Ryan-book}.
\bigskip

Let us close this section with a few words about the executability of our model checkers.