@MISC{MODELC_3.MIZ,
  AUTHOR = {Ishida, Kazuhisa and Shidama, Yasunari},
  TITLE = {Model Checking, Part {III}},
  SECTION1 = {Definition of basic operations to
    build an automaton for LTL, and properties},
  SECTION2 = {Negation inner most LTL},
  SECTION3 = {Definition of Buchi automaton, and
    verification of the main theorem},
  DAY = {19},
  MONTH = {August},
  YEAR = {2008},
  ADDRESS1 = {Shinshu University, Nagano, Japan},
  ADDRESS2 = {Shinshu University, Nagano, Japan},
  SUMMARY = {This text includes verification of the basic
  algorithm in Simple On-the-fly Automatic Verification of
  Linear Temporal Logic(LTL).
  LTL formula can be transformed to Buchi automaton,
  and this transforming algorithm is mainly used at
  Simple On-the-fly Automatic Verification.
  In this article, we verified this transforming algorithm itself.
  At first we prepared some definitions and operations
  for transforming.
  And then, we defined the Buchi automaton and verified transforming
  algorithm.}}

@BOOK{CLARKE:1,
  AUTHOR={Edmund M. Clarke, Orna Grumberg and Doron Peled},
  TITLE={Model Checking},
  PUBLISHER={The MIT Press},
  YEAR={1999}}

@INPROCEEDINGS{GERTH:1,
 AUTHOR={R.Gerth, D.Peled, M.Y. Vardi, and P.Wolper},
 TITLE={Simple On-the-fly Automatic Verification of Linear Temporal Logic},
 BOOKTITLE={Protocol Specification Testing and Verification},
 YEAR=1995,
 PUBLISHER={North Holland}}
