@MISC{MODELC_2.MIZ,
  AUTHOR = {Ishida, Kazuhisa},
  TITLE = {Model Checking, Part II},
  DAY = {21},
  MONTH = {April},
  YEAR = {2008},
  ADDRESS1 = {Shinshu University, Nagano, Japan},
  SUMMARY = {This article provides the definition of
    linear temporal logic (LTL) and its properties
    relevant to model checking based on LTL (\cf. \cite{ModelChecking}).}}

@BOOK{ModelChecking,
AUTHOR={Clarke, Edmund M. and Grumberg, Orna and Pelad, Doron A.},
TITLE={Model Checking},
PUBLISHER={MIT Press},
YEAR={2000}}



