doc-src/TutorialI/CTL/Base.thy

 text{*
 Model checking is a very popular technique for the verification of finite
 state systems (implementations) w.r.t.\ temporal logic formulae
 (specifications) \cite{Clark}. Its foundations are completely set theoretic
 and this section shall develop them in HOL. This is done in two steps: first
-we consider a very simple ``temporal'' logic called propositional dynamic
+we consider a simple modal logic called propositional dynamic
 logic (PDL) which we then extend to the temporal logic CTL used in many real
 model checkers. In each case we give both a traditional semantics (@{text \<Turnstile>}) and a
 recursive function @{term mc} that maps a formula into the set of all states of
 the system where the formula is valid. If the system has a finite number of
 states, @{term mc} is directly executable, i.e.\ a model checker, albeit not a