@InProceedings{	  somenzi.00.cav,
  author	= {Fabio Somenzi and Roderick Bloem},
  title		= {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
  booktitle	= {Proceedings of the 12th International Conference on
		  Computer Aided Verification (CAV'00)},
  pages		= {247--263},
  year		= {2000},
  volume	= {1855},
  series	= {Lecture Notes in Computer Science},
  address	= {Chicago, Illinois, USA},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  etessami.00.concur,
  author	= {Kousha Etessami and Gerard J. Holzmann},
  title		= {Optimizing {B\"u}chi Automata},
  booktitle	= {Proceedings of the 11th International Conference on
		  Concurrency Theory (Concur'00)},
  pages		= {153--167},
  year		= {2000},
  editor	= {C. Palamidessi},
  volume	= {1877},
  series	= {Lecture Notes in Computer Science},
  address	= {Pennsylvania, USA},
  publisher	= {Springer-Verlag},
  note          = {Beware of a typo in the version from the
                  proceedings: $f \U g$ is purely eventual if both
                  operands are purely eventual.  The revision of the
                  paper available at
                  \url{http://www.bell-labs.com/project/TMP/} is
                  fixed.  We fixed the bug in Spot in 2005, thanks to
                  LBTT.  See also \url{http://arxiv.org/abs/1011.4214v2}
                  for a discussion about this problem.}
}

@InProceedings{manna.87.podc,
 author = {Zohar Manna and Amir Pnueli},
 title = {A hierarchy of temporal properties},
 booktitle = {Proceedings of the sixth annual ACM Symposium on Principles of distributed computing (PODC'90)},
 year = {1990},
 location = {Quebec City, Canada},
 pages = {377--410},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@InProceedings{	  chang.92.icalp,
  author	= {Edward Y. Chang and Zohar Manna and Amir Pnueli},
  title		= {Characterization of Temporal Property Classes},
  booktitle	= {Proceedings of the 19th International Colloquium on
		  Automata, Languages and Programming (ICALP'92)},
  year		= {1992},
  pages		= {474--486},
  publisher	= {Springer-Verlag},
  address	= {London, UK}
}

@InProceedings{	  cerna.03.mfcs,
  author	= {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek},
  title		= {Relating Hierarchy of Temporal Properties to Model
		  Checking},
  booktitle	= {Proceedings of the 28th International Symposium on
		  Mathematical Foundations of Computer Science (MFCS'03)},
  pages		= {318--327},
  year		= {2003},
  editor	= {Branislav Rovan and Peter Vojt{\'a}{\v{a}}},
  volume	= {2747},
  series	= {Lecture Notes in Computer Science},
  address	= {Bratislava, Slovak Republic},
  month		= aug,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  schneider.01.lpar,
  author	= {Klaus Schneider},
  title		= {Improving Automata Generation for Linear Temporal Logic by
		  Considering the Automaton Hierarchy},
  booktitle	= {Proceedings of the 8th International Conference on Logic
		  for Programming, Artificial Intelligence and Reasoning},
  pages		= {39--54},
  year		= {2001},
  volume	= {2250},
  series	= {Lecture Notes in Artificial Intelligence},
  address	= {Havana, Cuba},
  publisher	= {Springer-Verlag}
}

@TechReport{	  tauriainen.03.a83,
  author	= {Heikki Tauriainen},
  title		= {On Translating Linear Temporal Logic into Alternating and
		  Nondeterministic Automata},
  institution	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  address	= {Espoo, Finland},
  month		= dec,
  number	= {A83},
  pages		= {132},
  type		= {Research Report},
  year		= {2003},
  note		= {Reprint of Licentiate's thesis}
}
