@InProceedings{	  beer.01.cav,
  author	= {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana
		  Fisman and Anna Gringauze and Yoav Rodeh},
  title		= {The Temporal Logic Sugar},
  booktitle	= {Proceedings of the 13th international conferance on
		  Computer Aided Verification (CAV'01)},
  series	= {Lecture Notes in Computer Science},
  editor	= {Berry, Gérard and Comon, Hubert and Finkel, Alain},
  publisher	= {Springer},
  isbn		= {978-3-540-42345-4},
  pages		= {363--367},
  volume	= {2102},
  year		= {2001},
  month		= jul
}

@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{	  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}
}

@Article{	  cimatti.08.tcad,
  author	= {Alessandro Cimatti and Marco Roveri and Stefano Tonetta},
  journal	= {IEEE Transactions on Computer Aided Design of Integrated
		  Circuits and Systems},
  number	= 10,
  pages		= {1737--1750},
  title		= {Symbolic Compilation of PSL},
  volume	= 27,
  year		= 2008,
  date		= {2009-03-20},
  note		= {\url{https://es.fbk.eu/people/tonetta/tests/tcad07/}}
}

@Book{		  eisner.06.psl,
  author	= {Cindy Eisner and Dana Fisman},
  title		= {A Practical Introduction to {PSL}},
  publisher	= {Springer},
  year		= {2006},
  series	= {Series on Integrated Circuits and Systems}
}

@InCollection{	  eisner.08.hvc,
  author	= {Cindy Eisner and Dana Fisman},
  title		= {Structural Contradictions},
  booktitle	= {Proceedings of the 4th International Haifa Verification
		  Conference (HVC'2008)},
  series	= {Lecture Notes in Computer Science},
  editor	= {Hana Chockler and Alan Hu},
  publisher	= {Springer},
  isbn		= {978-3-642-01701-8},
  pages		= {164--178},
  volume	= {5394},
  year		= {2009},
  month		= oct
}

@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}
}

@Book{		  psl.04.lrm,
  title		= {Property Specification Language Reference Manual v1.1},
  publisher	= {Accellera},
  year		= {2004},
  month		= jun,
  note		= {\url{http://www.eda.org/vfv/}}
}

@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}
}

@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}
}

@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}
}