summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 11 Oct 2000 13:39:52 +0200 | |

changeset 10192 | 4c2584e23ade |

parent 10191 | e77662e9cabd |

child 10193 | 1d6ae1ef8e64 |

*** empty log message ***

--- 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.