@Book{		  abrial.96.b,
  author	= {Jean-Raymond Abrial},
  title		= {The {B} Book},
  publisher	= {Cambridge University Press},
  year		= {1996},
  month		= oct
}

@Book{		  aho.74,
  author	= {Alfred V. Aho and John E. Hopcroft and Jeffrey D. Ullman},
  title		= {The Design and Analysis of Computer Algorithms},
  publisher	= {Addison-Wesley},
  year		= {1974},
  series	= {Addison-Wesley Series in Computer Science and Information
		  Processing}
}

@InProceedings{	  ajami.98.tacas,
  author	= "K. Ajami and S. Haddad and J-M. Ili{\'e}",
  title		= "Exploiting Symmetry in Linear Time Temporal Logic Model
		  Checking: One Step Beyond",
  booktitle	= "First International Conference on Tools and Algorithms for
		  the Construction and Analysis of Systems (TACAS'98)",
  volume	= "1384",
  pages		= "52--67",
  year		= "1998",
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Article{	  alpern.85.ipl,
  author	= {Bowen Alpern and Fred B. Schneider},
  title		= {Defining liveness},
  journal	= {Information Processing Letters},
  year		= {1985},
  volume	= {21},
  number	= {4},
  pages		= {181--185}
}

@Article{	  alpern.87.dc,
  author	= {Bowen Alpern and Fred B. Schneider},
  title		= {Recognizing Safety and Liveness},
  journal	= {Distributed Computing},
  year		= {1987},
  volume	= {2},
  number	= {3},
  pages		= {117--126}
}

@Misc{		  andersen.97.bdd,
  author	= {Henrik Reif Andersen},
  title		= {An Introduction to Binary Decision Diagrams},
  howpublished	= {Lecture notes},
  month		= oct,
  year		= {1997},
  url		= {http://www.itu.dk/people/hra/bdd97-abstract.html}
}

@InProceedings{	  armoni.02.tacas,
  author	= {Roy Armoni and Limor Fix and Alon Flaisher and Rob Gerth
		  and Boris Ginsburg and Tomer Kanza and Avner Landver and
		  Sela Mador-Haim and Eli Singerman and Andreas Tiemeyer and
		  Moshe Y. Vardi and Yael Zbar},
  title		= {The ForSpec Temporal Logic: A New Temporal
		  Property-Specification Language},
  booktitle	= {Proceedings of Tools and Algorithms for Construction and
		  Analysis of Systems (TACAS'02)},
  pages		= {296--211},
  year		= {2002},
  volume	= {2280},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag},
  editor	= {J.-P. Katoen and P. Stevens}
}

@Book{		  arnold.94.fts,
  author	= {Andr{\'e} Arnold},
  title		= {Finite transition systems. Semantics of communicating
		  systems},
  publisher	= {Prentice-Hall},
  year		= {1994}
}

@InProceedings{	  baarir.04.wodes,
  author	= {Soheib Baarir and Serge Haddad and Jean-Michel Ili{\'e}},
  title		= {Exploiting Partial Symmetries in Well-formed nets for the
		  Reachability and the linear Time Model Checking Problems},
  booktitle	= {Proceedings of the 7th Workshop on Discrete Event Systems
		  (WODES'04)},
  pages		= {223--228},
  year		= {2004},
  month		= sep,
  address	= {Reims, France}
}

@TechReport{	  baarir.06.tr03,
  author	= {Souheib Baarir and Alexandre Duret-Lutz},
  title		= {Emptiness Check of Powerset {B\"u}chi Automata},
  institution	= {Universit{\'e} Pierre et Marie Curie, LIP6-CNRS},
  year		= {2006},
  type		= {Technical report},
  number	= {2006/003},
  address	= {Paris, France},
  month		= oct,
  pdf		= {adl/baarir.06.tr03.pdf}
}

@InProceedings{	  baarir.07.acsd,
  author	= {Souheib Baarir and Alexandre Duret-Lutz},
  title		= {Emptiness Check of Powerset {B\"u}chi Automata},
  booktitle	= {Proceedings of the 7th International Conference on
		  Application of Concurrency to System Design (ACSD'07)},
  year		= {2007},
  month		= jul,
  note		= {To appear}
}

@InProceedings{	  baarir.07.msr,
  author	= {Souheib Baarir and Alexandre Duret-Lutz},
  title		= {Test de vacuité pour automates de {B\"u}chi ensemblistes
		  avec tests d'inclusion},
  booktitle	= {Actes du 6e Colloque Francophone sur la Modélisation des
		  Systèmes Réactifs (MSR'07)},
  year		= {2007},
  month		= oct,
  note		= {{\`A} para{\^i}tre}
}

@PhDThesis{	  baarir.07.phd,
  author	= {Souheib Baarir},
  title		= {Exploitation des sym{\'e}tries partielles pour la
		  v{\'e}rification et l'{\'e}valuation de performances des
		  syst{\'e}mes finis},
  school	= {Universit{\'e} Pierre et Marie Curie (Paris 6)},
  year		= {2007},
  address	= {France},
  month		= may
}

@InProceedings{	  bardin.03.cav,
  author	= {Sebastien Bardin and Alain Finkel and J{\'e}r{\^o}me
		  Leroux and Laure Petrucci},
  title		= {{FAST}: {F}ast {A}cceleration of {S}ymbolic {T}ransition
		  systems},
  booktitle	= {Proceedings of the 15th International Conference on
		  Computer Aided Verification (CAV'03)},
  year		= {2003},
  volume	= {2725},
  series	= {Lecture Notes in Computer Science},
  month		= jul
}

@PhDThesis{	  barnat.05.phd,
  author	= {Ji{\v{r}{\'i}} Barnat},
  title		= {Distributed Memory LTL Model Checking},
  school	= {Faculty of Informatics, Masaryk University Brno},
  year		= {2005}
}

@InProceedings{	  barringer.89.avmfss,
  author	= {Howard Barringer and Michael D. Fisher and Graham D.
		  Gough},
  title		= {Fair {SMG} and Linear Time Model Checking},
  booktitle	= {Proceedings of the International Workshop on Automatic
		  Verification Methods for Finite State Systems},
  volume	= {407},
  series	= {Lecture Notes in Computer Science},
  pages		= {133--150},
  year		= {1989},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  behm.99.fm,
  author	= {Patrick Behm and Paul Benoit and Alain Faivre and
		  Jean-Marc Meynadier},
  title		= {M{\'e}t{\'e}or: A Successful Application of {B} in a Large
		  Project},
  editor	= {Jeannette M. Wing and Jim Woodcock and Jim Davies},
  booktitle	= {Proceedings of the World Congress on Formal Methods in the
		  Development of Computing Systems (FM'99)},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {1708},
  year		= {1999},
  address	= {Toulouse, France},
  month		= sep,
  isbn		= {3-540-66587-0},
  pages		= {369--387}
}

@InProceedings{	  benari.81.popl,
  author	= {Mordechai Ben-Ari and Zohar Manna and Amir Pnueli},
  title		= {The Temporal Logic of Branching Time},
  booktitle	= {Proceedings of the 8th ACM Symposium on Principles of
		  Programming Languages (POPL'81)},
  pages		= {164--176},
  year		= {1981},
  publisher	= {ACM}
}

@Book{		  beth.57.crise,
  author	= {Evert Willem Beth},
  title		= {La crise de la raison et la logique},
  publisher	= {Gauthier-Villars},
  year		= {1957}
}

@Book{		  beth.59.fom,
  author	= {Evert Willem Beth},
  title		= {The Foundations of Mathematics},
  publisher	= {North Holland},
  year		= {1959},
  note		= {Second edition revised in 1965.}
}

@InProceedings{	  bhat.95.lics,
  author	= {Girish Bhat and Rance Cleaveland and Orna Grumberg},
  title		= {Efficient On-the-Fly Model Checking for {CTL*}},
  booktitle	= {Proceedings of the Tenth Annual {IEEE} Symposium on Logic
		  in Computer Science (LICS'95)},
  pages		= {388--197},
  month		= jun,
  year		= {1995}
}

@InProceedings{	  bloem.00.fmcad,
  author	= {Roderick Bloem and Harold N. Gabow and Fabio Somenzi},
  title		= {An Algorithm for Strongly Connected Component Analysis in
		  $n \log n$ Symbolic Steps},
  booktitle	= {Formal Methods in Computer Aided Design (FMCAD'00)},
  pages		= {37--54},
  year		= {2000},
  editor	= {M. D. Aagaard, J. W. O'Leary},
  number	= {2517},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@PhDThesis{	  bloem.01.phd,
  author	= {Roderick Bloem},
  title		= {Search Techniques and Automata for Symbolic Model
		  Checking},
  school	= {University of Colorado},
  year		= {2001}
}

@InProceedings{	  bloem.99.cav,
  author	= {Roderick Bloem and Kavita Ravi and Fabio Somenzi},
  title		= {Efficient Decision Procedures for Model Checking of Linear
		  Time Logic Properties},
  booktitle	= {Proceedings of the Eleventh Conference on Computer Aided
		  Verification (CAV'99)},
  pages		= {222--235},
  year		= {1999},
  volume	= {1633},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Article{	  bouajjani.92.scp,
  author	= {Ahmed Bouajjani and Jean-Claude Fernandez and Nicolas
		  Halbwachs and Pascal Raymond and Christophe Ratel},
  title		= {Minimal State Graph Generation},
  journal	= {Science of Computer Programming},
  year		= {1992},
  volume	= {18},
  pages		= {247--269}
}

@InProceedings{	  bouquet.99.jnpc,
  author	= {Fabrice Bouquet and Laurent Henocque and Philippe
		  J{\'e}gou},
  title		= {{\'E}num{\'e}ration et repr{\'e}sentation d'impliquants
		  premiers},
  booktitle	= {Actes des cinqui{\`e}mes Journ{\'e}es Nationales sur la
		  r{\'e}solution pratique de Probl{\`e}mes NP-Complets
		  (JNPC'99)},
  pages		= {179--188},
  year		= {1999},
  address	= {Lyon, France},
  month		= jun
}

@TechReport{	  brand.00.aterm,
  author	= {Mark G. J. van den Brand and Hayco A. de Jong and Paul
		  Klint and Pieter A Olivier},
  title		= {Efficient annotated terms},
  institution	= {Centrum voor Wiskunde en Informatica},
  year		= {2002},
  number	= {SEN-E0003},
  month		= feb
}

@Article{	  brand.83.acm,
  author	= {Daniel Brand and Pitro Zafiropulo},
  title		= {On Communicating Finite-State Machines},
  journal	= {Journal of the ACM},
  volume	= {30},
  number	= {2},
  year		= {1983},
  pages		= {323--342},
  publisher	= {ACM Press},
  address	= {New York, NY, USA}
}

@InProceedings{	  bruns.00.concur,
  author	= {Glenn Bruns and Patrice Godefroid},
  title		= {Generalized Model Checking: Reasoning about Partial State
		  Space},
  booktitle	= {Proceedings of the 11th International Conference on
		  Concurrency Theory (Concur'00)},
  pages		= {168--182},
  year		= {2000},
  editor	= {C. Palamidessi},
  volume	= {1877},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Article{	  bryant.86.tc,
  author	= {Randal E. Bryant},
  title		= {Graph-Based Algorithms for Boolean Function Manipulation},
  journal	= {IEEE Transactions on Computers},
  year		= {1986},
  volume	= {35},
  number	= {8},
  pages		= {677--691},
  month		= aug
}

@Article{	  bryant.92.cs,
  author	= {Randal E. Bryant},
  title		= {Symbolic Boolean Manipulation with Ordered Binary-Decision
		  Diagrams},
  journal	= {ACM Computing Surveys},
  year		= {1992},
  volume	= {24},
  number	= {3},
  pages		= {293--318},
  month		= sep
}

@Article{	  brzozowski.80.tcs,
  author	= {Janusz. A. Brzozowski and Ernest. L. Leiss},
  title		= {Finite automata, and Sequential networks},
  journal	= {Theoretical Computer Science},
  year		= {1980},
  number	= {10},
  pages		= {19--35}
}

@InProceedings{	  buchi.60.clmps,
  author	= {J. Richard {B\"u}chi},
  title		= {On a decision method in restricted second order
		  arithmetic},
  booktitle	= {Proceedings of the International Congress on Logic,
		  Methodology, and Philosophy of Science, Berkley, 1960},
  pages		= {1--11},
  year		= {1962},
  publisher	= {Standford University Press},
  note		= {Republished in \cite{lane.90}}
}

@InProceedings{	  burch.91.slcd,
  author	= {Jerry R. Burch and Edmund M. Clarke and Kenneth L.
		  McMillan and David L. Dill and L.J. Hwang},
  title		= {Symbolic Model Checking: $10^{20}$ States and Beyond},
  booktitle	= {Proceedings of the Fifth Annual {IEEE} Symposium on Logic
		  in Computer Science},
  pages		= {1--33},
  year		= {1990},
  address	= {Washington, D.C.},
  publisher	= {IEEE Computer Society Press}
}

@InProceedings{	  capra.00.mtcs,
  author	= {Lorenzo Capra and Clauda Dutheillet and Giovanni
		  Franceschinis and Jean-Michel Ili{\'e}},
  title		= {Exploiting Partial Symmetries for Markov Chain
		  Aggregation},
  booktitle	= {First International Workshop on Models for Time-Critical
		  Systems (MTCS'2000)},
  editor	= {Flavio Corradini and Paola Inverardi},
  year		= {2000},
  volume	= {39},
  number	= {3},
  series	= {Electronic Notes in Theoretical Computer Science},
  month		= dec,
  publisher	= {Elsevier Science Publishers}
}

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

@InProceedings{	  chiola.90.atpn,
  author	= {Giovanni Chiola and Claude Dutheillet and Giuliana
		  Franceschinis and Serge Haddad},
  title		= {On well-formed coloured nets and their symbolic
		  reachability graph},
  booktitle	= {Procedings of the 11th International Conference on
		  Application and Theory of Petri Nets. Paris, France, June
		  1990. Reprinted in High-Level Petri Nets. Theory and
		  Application.},
  year		= {1991},
  editor	= {K. Jensen and G. Rozenberg},
  publisher	= {Springer-Verlag}
}

@Article{	  chiola.93.toc,
  author	= {Giovanni Chiola and Claude Dutheillet and Giuliana
		  Franceschinis and Serge Haddad},
  title		= {Stochastic well-formed coloured nets for symmetric
		  modelling applications},
  journal	= {IEEE Transactions on Computers},
  year		= {1993},
  volume	= {42},
  number	= {11},
  pages		= {1343--1360},
  month		= nov
}

@Article{	  chiola.95.pe,
  author	= {Giovanni Chiola and Giuliana Franceschinis and Rossano
		  Gaeta and Marina Ribaudo},
  title		= {{G}reat{SPN} 1.7: {GR}aphical {E}ditor and {A}nalyzer for
		  {T}imed and {S}tochastic {P}etri {N}ets},
  journal	= {Performance Evaluation},
  year		= {1995},
  volume	= {24},
  number	= {1--2},
  pages		= {47--68}
}

@Article{	  chiola.97.tcs,
  author	= {Giovanni Chiola and Claude Dutheillet and Giuliana
		  Franceschinis and Serge Haddad},
  title		= {A Symbolic Reachability Graph for Coloured {P}etri Nets},
  journal	= {Theoretical Computer Science},
  year		= {1997},
  volume	= {176},
  number	= {1--2},
  pages		= {39--65},
  month		= apr
}

@InProceedings{	  ciardo.00.icatpn,
  author	= {Gianfranco Ciardo and Gerarld L{\"u}ttgen and Radu
		  Siminiceanu},
  title		= {Efficient Symbolic State-Space Construction for
		  Asynchronous Systems},
  booktitle	= {Proceedings of the 21st International Conference on
		  Application and Theory of Petri Nets (ICATPN'00)},
  pages		= {103--122},
  year		= {2000},
  editor	= {Mogens Nielsen and Dan Simpson},
  volume	= {1825},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  cimatti.02.cav,
  author	= {Alessandro Cimatti and Edmund Clarke and Enrico
		  Giunchuglia and Fausto Giunchiglia and Marco Pistore and
		  Macro Roveri and Roberto Sebastiani and Armando Tacchella},
  title		= {NuSMV 2: An OpenSource Tool for Symbolic Model Checking},
  booktitle	= {Proceedings of the 14th International Conference on
		  Computer Aided Verification (CAV'02)},
  pages		= {359--364},
  year		= {2002},
  editor	= {E. Brinksma and K. Guldstrand Larsen},
  volume	= {2404},
  series	= {Lecture Notes in Computer Science},
  address	= {Copenhagen, Denmark},
  month		= jul,
  publisher	= {Springer-Verlag}
}

@Book{		  clarke.00.mc,
  author	= {Edmund M. Clarke and Orna Grumberg and Doron A. Peled},
  title		= {Model Checking},
  publisher	= {The MIT Press},
  year		= {2000}
}

@InCollection{	  clarke.01.har,
  author	= {Edmund M. Clarke and Bernd-Holger Schlingloff},
  editor	= {Alan Robinson and Andrei Voronkov},
  title		= {Model Checking},
  booktitle	= {Handbook of Automated Reasoning},
  chapter	= {4},
  publisher	= {Elsevier Science Publishers},
  year		= {2001},
  pages		= {1367--1522}
}

@InProceedings{	  clarke.02.lics,
  author	= {Edmund M. Clarke and Somesh Jha and Yuan Lu and Helmut
		  Veith},
  title		= {Proceedings of the 17th IEEE Symposium on Logic in
		  Computer Science (LICS'02)},
  booktitle	= {LICS},
  year		= {2002},
  pages		= {19--29},
  publisher	= {IEEE Computer Society},
  address	= {Copenhagen, Denmark},
  month		= jul
}

@InProceedings{	  clarke.83.popl,
  author	= {Edmund M. Clarke and E. Allen Emerson and A. Prasad
		  Sistla},
  title		= {Automatic verification of finite state concurrent system
		  using temporal logic specifications: a practical approach},
  booktitle	= {Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on
		  Principles of programming languages (POPL'83)},
  pages		= {117--126},
  year		= {1983},
  publisher	= {ACM Press}
}

@TechReport{	  clarke.94.tr204,
  author	= {Edmund M. Clarke and Orna Grumberg and Kenneth L. McMillan
		  and Xudong Zhao},
  title		= {Efficient Generation of Counterexamples and Witness in
		  Symbolic Model Checking},
  institution	= {Carnegie Mellon University, School of Compute Science},
  year		= {1994},
  type		= {Technical report},
  number	= {CMU-CS-94-204},
  address	= {Pittsburg},
  month		= oct,
  note		= {Later republished as \cite{clarke.95.dac}}
}

@InProceedings{	  clarke.95.dac,
  author	= {Edmund M. Clarke and Orna Grumberg and Kenneth L. McMillan
		  and Xudong Zhao},
  title		= {Efficient Generation of Counterexamples and Witness in
		  Symbolic Model Checking},
  booktitle	= {Proceedings of the 32nd ACM/IEEE Design Automation
		  Conference (DAC'95)},
  year		= {1995},
  pages		= {427-432},
  address	= {San Francisco, California, USA},
  month		= jun,
  publisher	= {ACM Press}
}

@Article{	  clarke.96.acm,
  author	= {Edmund M. Clarke and Jeannette M. Wing},
  title		= {Formal Methods: State of the Art and Future},
  journal	= {ACM Computing Surveys},
  volume	= {28},
  number	= {4},
  pages		= {626--643},
  year		= {1996}
}

@InProceedings{	  clarke.98.cav,
  author	= {Edmund M. Clarke and E. Allen Emerson and Somesh Jha and
		  A. Prasad Sistla},
  title		= {Efficient Decision Procedures for Model Checking of Linear
		  Time Logic Properties},
  booktitle	= {Proceedings of the Tenth Conference on Computer Aided
		  Verification (CAV'98)},
  pages		= {147--158},
  year		= {1998},
  volume	= {1427},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  clarke.98.tableaux,
  author	= {Edmund M. Clarke},
  title		= {Model Checking: Historical Perspective and Example },
  booktitle	= {Proceedings of Analytic Tableaux and Related Methods
		  (TABLEAUX'98)},
  pages		= {18--24},
  year		= {1998},
  volume	= {1397},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Article{	  coudert.94.tllm,
  author	= {Olivier Coudert},
  title		= {Two-level logic minimization: an overview},
  journal	= {Integration, the VLSI journal},
  year		= {1994},
  volume	= {17},
  number	= {2},
  pages		= {97--140},
  month		= oct
}

@InProceedings{	  courcoubetis.90.cav,
  author	= {Costas Courcoubetis and Moshe Y. Vardi and Pierre Wolper
		  and Mihalis Yannakakis},
  title		= {Memory-Efficient Algorithm for the Verification of
		  Temporal Properties},
  booktitle	= {Proceedings of the 2nd international workshop on Computer
		  Aided Verification (CAV'90)},
  pages		= {233--242},
  year		= {1991},
  editor	= {Edmund M. Clarke and Robert P. Kurshan},
  volume	= {531},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Article{	  courcoubetis.92.fmsd,
  author	= {Costas Courcoubetis and Moshe Y. Vardi and Pierre Wolper
		  and Mihalis Yannakakis},
  title		= {Memory-Efficient Algorithm for the Verification of
		  Temporal Properties},
  journal	= {Formal Methods in System Design},
  pages		= {275--288},
  year		= {1992},
  volume	= {1}
}

@InProceedings{	  couvreur.00.icatpn,
  author	= {Jean-Michel Couvreur and S{\'e}bastien Grivet and Denis
		  Poitrenaud},
  title		= {Designing a {LTL} Model-Checker Based on Unfolding
		  Graphs},
  booktitle	= {Proceedings of the 21th International Conference on
		  Applications and Theory of Petri Nets (ICATPN'00)},
  year		= {2000},
  series	= {Lecture Notes in Computer Science},
  volume	= {2075},
  address	= {Aarhus, Denmark},
  month		= jun,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  couvreur.00.lacim,
  author	= {Jean-Michel Couvreur},
  title		= {Un point de vue symbolique sur la logique temporelle
		  lin{\'e}aire},
  booktitle	= {Actes du Colloque LaCIM 2000},
  month		= aug,
  year		= {2000},
  pages		= {131--140},
  volume	= {27},
  series	= {Publications du LaCIM},
  address	= {Montr{\'e}al},
  publisher	= {Universit{\'e} du Qu{\'e}bec {\`a} Montr{\'e}al},
  editor	= {Pierre Leroux}
}

@InProceedings{	  couvreur.02.ictpn,
  author	= {Jean-Michel Couvreur and Emmanuelle Encrenaz and Emmanuel
		  Paviot-Adet and Denis Poitrenaud and Pierre-Andr{\'e}
		  Wacrenier},
  title		= {{D}ata {D}ecision {D}iagrams for {P}etri Net Analysis},
  booktitle	= {Proceedings of the 23rd International Conference on
		  Applications and Theory of Petri Nets (ICATPN'02)},
  pages		= {101-120},
  year		= {2002},
  editor	= {J. Esparza and C. Lakos},
  volume	= {2360},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Misc{		  couvreur.04.hdr,
  author	= {Jean-Michel Couvreur},
  title		= {Contribution {\`a} l'algorithmique de la v{\'e}rification},
  year		= {2004},
  howpublished	= {Habilitation {\`a} diriger des recherches, ENS Cachan}
}

@InProceedings{	  couvreur.05.spin,
  author	= {Jean-Michel Couvreur and Alexandre Duret-Lutz and Denis
		  Poitrenaud},
  title		= {On-the-Fly Emptiness Checks for Generalized {B\"u}chi
		  Automata},
  booktitle	= {Proceedings of the 12th International SPIN Workshop on
		  Model Checking of Software},
  pages		= {143--158},
  year		= {2005},
  editor	= {Patrice Godefroid},
  volume	= {3639},
  series	= {Lecture Notes in Computer Science},
  month		= aug,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  couvreur.99.fm,
  author	= {Jean-Michel Couvreur},
  title		= {On-the-fly Verification of Linear Temporal Logic},
  pages		= {253--271},
  editor	= {Jeannette M. Wing and Jim Woodcock and Jim Davies},
  booktitle	= {Proceedings of the World Congress on Formal Methods in the
		  Development of Computing Systems (FM'99)},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {1708},
  year		= {1999},
  address	= {Toulouse, France},
  month		= sep,
  isbn		= {3-540-66587-0}
}

@InProceedings{	  daniele.99.cav,
  author	= {Marco Daniele and Fausto Giunchiglia and Moshe Y. Vardi},
  title		= {Improved Automata Generation for {L}inear {T}emporal
		  {L}ogic},
  booktitle	= {Proceedings of the 11th International Conference on
		  Computer Aided Verification (CAV'99)},
  pages		= {249--260},
  year		= {1999},
  editor	= {N. Halbwachs and D. Peled},
  volume	= {1633},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@TechReport{	  daniele.99.tr,
  author	= {Marco Daniele and Fausto Giunchiglia and Moshe Y. Vardi},
  title		= {Improved Automata Generation for {L}inear {T}emporal
		  {L}ogic},
  institution	= {ITC-IRSC},
  year		= {1999},
  note		= {Later republished as \cite{daniele.99.cav}}
}

@Book{		  diaz.01.ic2,
  author	= {Michel Diaz},
  title		= {R{\'e}seaux de {P}etri, Mod{\`e}les fondamentaux},
  publisher	= {Hermes Science},
  year		= {2001},
  series	= {Trait{\'e} IC2, s{\'e}rie Informatique et syst{\`e}mes
		  d'information},
  month		= jun
}

@Misc{		  dijkstra.73.ewd376,
  author	= {Edsger Wybe Dijkstra},
  title		= {{EWD} 376: {F}inding the maximum strong components in a
		  directed graph.},
  howpublished	= {\url{http://www.cs.utexas.edu/users/EWD/ewd03xx/EWD376.PDF}}
		  ,
  month		= may,
  year		= {1973}
}

@InCollection{	  dijkstra.76.dop,
  author	= {Edsger Wybe Dijkstra},
  booktitle	= {A Discipline of Programming},
  title		= {{F}inding the maximal strong components in a directed
		  graph},
  chapter	= {25},
  publisher	= {Prentice-Hall},
  year		= {1976},
  pages		= {192--200}
}

@MastersThesis{	  duret.03.msc,
  author	= {Alexandre Duret-Lutz and Rachid Rebiha},
  title		= {SPOT\,: une biblioth{\`e}que de v{\'e}rification de
		  propri{\'e}t{\'e}s de logique temporelle {\`a} temps
		  lin{\'e}aire},
  school	= {DEA Syst{\`e}mes Informatiques R{\'e}partis,
		  Universit{\'e} de Paris 6},
  month		= sep,
  year		= {2003}
}

@InProceedings{	  duret.04.mascots,
  author	= {Alexandre Duret-Lutz and Denis Poitrenaud},
  title		= {SPOT: an Extensible Model Checking Library using
		  Transition-based Generalized {B\"u}chi Automata},
  booktitle	= {Proceedings of the 12th IEEE/ACM International Symposium
		  on Modeling, Analysis, and Simulation of Computer and
		  Telecommunication Systems (MASCOTS'04)},
  year		= {2004},
  address	= {Volendam, The Netherlands},
  month		= oct,
  publisher	= {IEEE Computer Society Press},
  pages		= {76--83}
}

@InProceedings{	  dwyer.98.fmsp,
  author	= {Matthew B. Dwyer and George S. Avrunin and James C.
		  Corbett},
  title		= {Property Specification Patterns for Finite-state
		  Verification},
  booktitle	= {Proceedings of the 2nd Workshop on Formal Methods in
		  Software Practice (FMSP'98)},
  publisher	= {ACM Press},
  address	= {New York},
  editor	= {Mark Ardis},
  month		= mar,
  year		= {1998},
  pages		= {7--15}
}

@InProceedings{	  edvardsson.99.ccsse,
  author	= {Jon Edvardsson},
  title		= {A Survey on Automatic Test Data Generation},
  booktitle	= {Proceedings of the Second Conference on Computer Science
		  and Engineering (CCSSE'99)},
  year		= {1999}
}

@InProceedings{	  eker.03.spin,
  author	= {Steven Eker and Jos{\'e} Meseguer and Ambarish
		  Sridharanarayanan},
  title		= {The {M}aude {LTL} Model Checker and Its Implementation},
  booktitle	= {Proceedings of the 10th International SPIN Workshop on
		  Model Checking Software (SPIN'03)},
  pages		= {230-2-34},
  optyear	= {2003},
  volume	= {2648},
  series	= {Lecture Notes in Computer Science},
  address	= {Portland, Oregon, USA},
  month		= may,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  emerson.84.stoc,
  author	= {E. Allen Emerson and A. Prasad Sistla},
  title		= {Deciding Branching Time Logic},
  booktitle	= {Proceedings of the 16th annual ACM symposium on Theory of
		  computing (STOC'84)},
  year		= {1984},
  isbn		= {0-89791-133-4},
  pages		= {14--24},
  publisher	= {ACM Press}
}

@InCollection{	  emerson.90.cwrb,
  author	= {E. Allen Emerson},
  title		= {The Role of {B\"u}chi's Automata in Computing Science},
  publisher	= {Springer-Verlag},
  year		= {1990},
  crossref	= {lane.90}
}

@InProceedings{	  emerson.96.banff,
  author	= {E. Allen Emerson},
  title		= {Automated Temporal Reasoning about Reactive Systems},
  booktitle	= {Proceedings of the 8th Banff Higher Order Workshop},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {1043},
  year		= {1996},
  pages		= {41--101},
  isbn		= {3-540-60915-6},
  address	= {Banff, Alberta, Canada}
}

@InCollection{	  emerson.97.dcfm,
  author	= {E. Allen Emerson},
  title		= {Model Checking and the Mu-calculus},
  booktitle	= {Descriptive Complexity and Finit Models},
  publisher	= {American Mathematical Society},
  year		= {1997},
  editor	= {N. Immerman and P. G. Kolaitis},
  volume	= {31},
  series	= {DIMACS: Series in Discrete Mathematics and Theoretical
		  Computer Science}
}

@Article{	  esparaza.02.fm,
  author	= {Javier Esparza and Stefan R{\"o}mer and Walter Vogler},
  title		= {An Improvement of McMillan's Unfolding Algorithm},
  journal	= {Formal Methods in System Design},
  volume	= {20},
  number	= {3},
  year		= {2002},
  pages		= {285--310},
  publisher	= {Kluwer Academic Publishers},
  address	= {Hingham, MA, USA}
}

@InProceedings{	  esparza.01.movep,
  author	= {Javier Esparza},
  title		= {Verification of Systems with an Infinite State Space},
  booktitle	= {Proceedings of the 4th Summer School on Modeling and
		  Verification of Parallel Processes (MOVEP'00)},
  pages		= {183--186},
  year		= {2001},
  editor	= {F. Cassez and C. Jard and B. Rozoy and M. Dermot},
  volume	= {2067},
  series	= {Lecture Notes in Computer Science},
  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}
}

@InProceedings{	  etessami.01.alp,
  author	= {Kousha Etessami and Thomas Wilke and Rebecca A. Schuller},
  title		= {Fair Simulation Relations, Parity Games, and State Space
		  Reduction for {B\"u}chi Automata},
  booktitle	= {Proceedings of the 28th international colloquium on
		  Automata, Languages and Programming},
  pages		= {694--707},
  year		= {2001},
  editor	= {Fernando Orejas and Paul G. Spirakis and Jan van Leeuwen},
  volume	= {2076},
  series	= {Lecture Notes in Computer Science},
  address	= {Crete, Greece},
  month		= jul,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  etessami.99.cav,
  author	= {Kousha Etessami},
  title		= {Stutter-Invariant Languages, {$\omega$}-Automata, and
		  Temporal Logic},
  booktitle	= {Proceedings of the 11th International Conference on
		  Computer Aided Verification (CAV'99)},
  pages		= {236--248},
  year		= {1999},
  editor	= {N. Halbwachs and D. Peled},
  volume	= {1633},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Article{	  even.81.acm,
  author	= {Shimon Even and Yossi Shiloach},
  title		= {An On-Line Edge-Deletion Problem},
  journal	= {Journal of the Association for Computing Machinery},
  volume	= {28},
  number	= {1},
  year		= {1981},
  pages		= {1-4}
}

@InProceedings{	  finkbeiner.01.tcs,
  author	= {Bernd Finkbeiner and Henry B. Sipma},
  title		= {Checking Finite Traces using Alternating Automata},
  booktitle	= {Proceedings of the First International Workshop on Runtime
		  Verification},
  volume	= {55},
  number	= {2},
  series	= {Electronic Notes in Theoretical Computer Science},
  publisher	= {Elsevier},
  year		= {2001}
}

@TechReport{	  finkel.02.tr14,
  author	= {Alain Finkel and J{\'e}r{\^o}me Leroux},
  title		= {How to Compose Presburger-Accelerations: Applications to
		  Broadcast Protocols},
  institution	= {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS
		  Cachan},
  year		= {2002},
  month		= sep
}

@Article{	  fisher.92.fac,
  author	= {Michael Fisher},
  title		= {A Model Checker for Linear Time Temporal Logic},
  journal	= {Formal Aspects of Computing},
  volume	= {4},
  number	= {3},
  pages		= {299--319},
  year		= {1992}
}

@Book{		  fitting.96,
  author	= {Melving Fitting},
  title		= {First-Order Logic and Automated Theorem Proving},
  publisher	= {Springer},
  year		= {1996},
  edition	= {2nd}
}

@Book{		  francez.89.fairness,
  author	= {Nissim Francez},
  title		= {Fairness},
  publisher	= {Springer-Verlag},
  year		= {1986}
}

@InProceedings{	  friedgut.04.atva,
  author	= {Ehud Friedgut and Orna Kupferman and Moshe Y. Vardi},
  title		= {{B\"u}chi Complementation Made Tighter},
  booktitle	= {Proceedings of the 2nd International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'04)},
  series	= {Lecture Notes in Computer Science},
  volume	= {3299},
  pages		= {64--78},
  publisher	= {Springer-Verlag},
  year		= 2004
}

@InProceedings{	  fritz.02.tcs,
  author	= {Carsten Fritz and Thomas Wilke},
  title		= {State Space Reductions for Alternating {B}{\"u}chi
		  Automata: Quotienting by Simulation Equivalences},
  booktitle	= {Proceedings of the 22nd Conference on Foundations of
		  Software Technology and Theoretical Computer Science
		  (FSTTCS'2002)},
  editor	= {Manindra Agrawal and Anil Seth},
  year		= 2002,
  series	= {Lecture Notes in Computer Science},
  volume	= 2556,
  pages		= {157--168},
  address	= {Kanpur, India}
}

@InProceedings{	  fritz.03.ciaa,
  author	= {Carsten Fritz},
  title		= {Constructing {B\"u}chi Automata from Linear Temporal Logic
		  Using Simulation Relations for Alternating {B\"u}chi
		  Automata},
  booktitle	= {Proceedings of the 8th International Conference on
		  Implementation and Application of Automata (CIAA'03)},
  pages		= {35--48},
  year		= {2003},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {2759},
  isbn		= {3-540-40561-5},
  editor	= {Oscar H. Ibarra and Zhe Dang},
  address	= {Santa Barbara, California},
  month		= jul
}

@InProceedings{	  fritz.05.lpar,
  author	= {Carsten Fritz},
  title		= {Concepts of Automata Construction from {LTL}},
  booktitle	= {Proceedings of the 12th Internation Conference on Logic
		  for Programming, Artifical Intelligence, and Reasoning
		  (LPAR'05)},
  pages		= {728--742},
  address	= {Montego Bay, Jamaica},
  year		= {2005},
  editor	= {G. Sutcliffe and A. Voronkov},
  volume	= {3835},
  series	= {Lecture Notes in Artificial Intelligence},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  gastin.01.cav,
  author	= {Paul Gastin and Denis Oddoux},
  title		= {Fast {LTL} to {B\"u}chi Automata Translation},
  booktitle	= {Proceedings of the 13th International Conference on
		  Computer Aided Verification (CAV'01)},
  pages		= {53--65},
  year		= {2001},
  editor	= {G. Berry and H. Comon and A. Finkel},
  volume	= {2102},
  series	= {Lecture Notes in Computer Science},
  address	= {Paris, France},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  gastin.04.spin,
  author	= {Paul Gastin and Pierre Moro and Marc Zeitoun},
  title		= {Minimization of counterexamples in {SPIN}},
  booktitle	= {Proceedings of the 11th International SPIN Workshop on
		  Model Checking of Software (SPIN'04)},
  year		= {2004},
  month		= apr,
  pages		= {92--108},
  editor	= {S. Graf and L. Mounier},
  volume	= {2989},
  series	= {Lecture Notes in Computer Science}
}

@InProceedings{	  geldenhuys.04.tacas,
  author	= {Jaco Geldenhuys and Antti Valmari},
  title		= {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification
		  More Efficient},
  booktitle	= {Proceedings of the 10th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'04)},
  editor	= {Kurt Jensen and Andreas Podelski},
  pages		= {205--219},
  year		= {2004},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {2988},
  isbn		= {3-540-21299-X}
}

@Article{	  geldenhuys.05.tcs,
  author	= {Jaco Geldenhuys and Antti Valmari},
  title		= {More Efficient On-the-fly {LTL} Verification with
		  {T}arjan's Algorithm},
  journal	= {Theoretical Computer Science},
  pages		= {60--82},
  year		= {2005},
  month		= nov,
  volume	= {345},
  number	= {1},
  note		= {Conference paper selected for journal publication}
}

@InProceedings{	  gerth.95.pstv,
  author	= {Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre
		  Wolper},
  title		= {Simple On-the-fly Automatic Verification of Linear
		  Temporal Logic},
  booktitle	= {Proceedings of the 15th Workshop on Protocol Specification
		  Testing and Verification (PSTV'95)},
  publisher	= {Chapman \& Hall},
  address	= {Warsaw, Poland},
  pages		= {3--18},
  year		= {1996},
  url		= {http://citeseer.nj.nec.com/gerth95simple.html}
}

@TechReport{	  giannakopoulou.01.tr,
  author	= {Dimitra Giannakopoulou and Flavio Lerda},
  title		= {Efficient translation of {LTL} formul{\ae} into {B\"u}chi
		  automata},
  institution	= {Research Institute for Advanced Computer Science},
  year		= {2001},
  number	= {01.29},
  month		= jun,
  note		= {Later republished as \cite{giannakopoulou.02.forte}}
}

@InProceedings{	  giannakopoulou.02.forte,
  author	= {Dimitra Giannakopoulou and Flavio Lerda},
  title		= {From States to Transitions: Improving Translation of {LTL}
		  Formul{\ae} to {B\"u}chi Automata},
  booktitle	= {Proceedings of the 22nd IFIP WG 6.1 International
		  Conference on Formal Techniques for Networked and
		  Distributed Systems (FORTE'02)},
  pages		= {308--326},
  year		= {2002},
  editor	= {D.A. Peled and M.Y. Vardi},
  volume	= {2529},
  series	= {Lecture Notes in Computer Science},
  address	= {Houston, Texas},
  month		= nov,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  godefroid.93.pstv,
  author	= {Patrice Godefroid and Gerard J. Holzmann},
  title		= {On the verification of temporal properties},
  booktitle	= {Proceedings of the 13th IFIP TC6/WG6.1 International
		  Symposium on Protocol Specification, Testing, and
		  Verification (PSTV'93)},
  month		= may,
  editor	= {Andr{\'e} A. S. Danthine and Guy Leduc and Pierre Wolper},
  address	= {Liege, Belgium},
  pages		= {109--124},
  publisher	= {North-Holland},
  year		= {1993},
  series	= {IFIP Transactions},
  volume	= {C-16},
  isbn		= {0-444-81648-8}
}

@Article{	  godefroid.95.fms,
  author	= {Patrice Godefroid and Gerard Holzmann and Didier
		  Pirottin},
  title		= {State-Space Caching Revisited},
  journal	= {Formal Methods in System Design},
  year		= {1995},
  volume	= {7},
  number	= {3},
  pages		= {227--241},
  month		= nov,
  publisher	= {Kluwer Academic Publishers}
}

@Book{		  godefroid.96.phdlncs,
  author	= {Patrice Godefroid},
  editor	= {J. van Leeuwen and J. Hartmanis and G. Goos},
  title		= {Partial-Order Methods for the Verification of Concurrent
		  Systems: An Approach to the State-Explosion Problem},
  year		= {1996},
  isbn		= {3540607617},
  volume	= {1032},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Book{		  grdel.02,
  author	= {Erich Gr{\"a}del and Wolfgang Thomas and Thomas Wilke},
  title		= {Automata, logic, and infinite games},
  publisher	= {Springer-Verlag},
  year		= {2002},
  volume	= {2500},
  series	= {Lecture Notes in Computer Science}
}

@InProceedings{	  gurumurthy.03.charme,
  author	= {Sankar Gurumurthy and Orna Kupferman and Fabio Somenzi and
		  Moshe Y. Vardi},
  title		= {On Complementing Nondeterminisitic {B\"u}chi Automata},
  booktitle	= {Proceedings of the 12th Advanced Research Working
		  Conference on Correct Hardware Design and Verification
		  Methods (CHARME'03)},
  pages		= {96--110},
  year		= {2003},
  volume	= {2860},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  haddad.00.forte,
  author	= {Serge Haddad and Jean-Michel Ili{\'e} and Khalil Ajami},
  title		= {A Model Checking Method for Partially Symmetric Systems},
  booktitle	= {Proceedings of the International Conference on Formal
		  Description techniques: theory, application and tools
		  (FORTE-PSTV'00)},
  year		= {2000},
  month		= oct
}

@InCollection{	  haddad.01.mf4,
  author	= {Serge Haddad},
  title		= {D{\'e}cidabili{\'e} et complexit{\'e} de probl{\`e}mes de
		  r{\'e}seaux de {P}etri},
  booktitle	= {R{\'e}seaux de {P}etri, Mod{\`e}les fondamentaux},
  publisher	= {Hermes Science},
  year		= {2001},
  editor	= {Michel Diaz},
  series	= {Trait{\'e} IC2, s{\'e}rie Informatique et syst{\`e}mes
		  d'information},
  chapter	= {4},
  month		= jun
}

@InProceedings{	  haddad.02.smc,
  author	= {Serge Haddad and Jean-Michel Ili{\'e} and Kais Klai},
  title		= {An Incremental Verification Technique using Decomposition
		  of {P}etri Nets},
  booktitle	= {Proceedings of the IEEE International Conference on
		  Systems, Man and Cybernetics},
  year		= {2002},
  month		= oct
}

@InBook{	  haddad.03.diaz,
  author	= {Serge Haddad and Jean-Michel Ili{\'e}},
  title		= {Sym{\'e}tries et logique temporelle},
  booktitle	= {V{\'e}rification et mise en {\oe}uvre des r{\'e}seaux de
		  Petri},
  year		= {2003},
  chapter	= {4},
  month		= feb,
  publisher	= {Hermes Science},
  editor	= {Michel Diaz},
  series	= {Trait{\'e} IC2, s{\'e}rie Informatique et syst{\`e}mes
		  d'information}
}

@InCollection{	  haddad.03.vps,
  author	= {Serge Haddad and Fran{\c{c}}ois Vernadat},
  title		= {V{\'e}rification de propri{\'e}t{\'e}s sp{\'e}cifiques},
  booktitle	= {V{\'e}rification et mise en \oe{}uvre des r{\'e}seaux de
		  {P}etri},
  publisher	= {Hermes Science},
  year		= {2003},
  editor	= {Michel Diaz},
  series	= {Trait{\'e} IC2, s{\'e}rie Informatique et syst{\`e}mes
		  d'information},
  chapter	= {1},
  month		= jan
}

@InProceedings{	  haddad.04.atva,
  author	= {Serge Haddad and Jean-Michel Ili{\'e} and Kais Klai},
  title		= {Design and Evaluation of a Symbolic and Abstraction-based
		  Model Checker},
  booktitle	= {Proceedings of the 2nd International Symposium on
		  Automated Technology for Verification and Analysis
		  (ATVA'04)},
  pages		= {198--210},
  editor	= {F. Wang},
  volume	= {3299},
  series	= {Lecture Notes in Computer Science},
  address	= {National Taiwan University, Taiwan},
  month		= oct,
  year		= {2004},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  haddad.95.icatpn,
  author	= {Serge Haddad and Jean-Michel Ili{\'e} and Mohamed Taghelit
		  and Belhassen Zouari.},
  title		= {Symbolic marking graph and partial symmetries},
  booktitle	= {Proceedings of the 16th International Conference on
		  Application and Theory of Petri Nets (ICATPN'95)},
  pages		= {238--257},
  year		= {1995},
  address	= {Torino, Italy}
}

@InProceedings{	  halpern.91.kr,
  author	= {Joseph Y. Halpern, Moshe Y. Vardi},
  title		= {Model Checking vs. Theorem Proving: A Manifesto},
  booktitle	= {Proceedings of the 2nd International Conference on
		  Principles of Knowledge Representation and Reasoning
		  (KR'91)},
  pages		= {325--334},
  year		= {1991},
  address	= {Cambridge, MA, USA},
  month		= apr,
  publisher	= {Morgan Kaufmann Publishers}
}

@InProceedings{	  hammer.05.tacas,
  author	= {Moritz Hammer and Alexander Knapp and Stephan Merz},
  title		= {Truly On-The-Fly {LTL} Model Checking},
  booktitle	= {Proceedings of the 11th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'05)},
  year		= {2005},
  editor	= {Nicolas Halbwachs and Lenore Zuck},
  series	= {Lecture Notes in Computer Science},
  address	= {Edinburgh, Scotland, UK},
  month		= apr,
  publisher	= {Springer-Verlag},
  volume	= {3440}
}

@InProceedings{	  hansen.02.fmics,
  author	= {Henri Hansen and Wojciech Penczek and Antti Valmari},
  title		= {Stuttering-Insensitive Automata for On-the-fly Detection
		  of Livelock Properties},
  booktitle	= {Proceedings of the 7th International ERCIM Workshop in
		  Formal Methods for Industrial Critical Systems (FMICS'02)},
  series	= {Electronic Notes in Theoretical Computer Science},
  volume	= {66(2)},
  publisher	= {Elsevier},
  editor	= {Rance Cleaveland and Hubert Garavel},
  year		= {2002},
  month		= jul,
  address	= {M{\'a}laga, Spain}
}

@PhDThesis{	  heljanko.02.phd,
  author	= {Keijo Heljanko},
  title		= {Combining Symbolic and Partial Order Methods for Model
		  Checking 1-Safe {P}etri Nets},
  school	= {Helsinki University of Technology},
  year		= {2002},
  month		= mar
}

@InProceedings{	  holzmann.00.nato,
  author	= {Gerard J. Holzmann},
  title		= {Software Model Checking },
  pages		= {309--355},
  year		= {2000},
  series	= {NATO Summer School},
  address	= {Marktoberdorf, Germany},
  month		= aug,
  publisher	= {IOS Press Computer and System Sciences}
}

@Book{		  holzmann.03.spinbook,
  author	= {Gerard J. Holzmann},
  title		= {The Spin Model Checker: Primer and Reference Manual},
  publisher	= {Addison-Wesley},
  isbn		= {0-321-22862-6},
  year		= {2003}
}

@InProceedings{	  holzmann.07.topmodels,
  author	= {Gerard J. Holzmann and Dragan Bo{\v{s}na\v{c}ki} },
  title		= {Multi-Core Model Checking with {\sc Spin}},
  booktitle	= {1st Workshop on Tools, Operating Systems and Programming
		  Models for Developing Reliable Systems (TOPMoDelS'07)}
}

@Article{	  holzmann.88.spe,
  author	= {Gerard J. Holzmann},
  title		= {An Improved Protocol Reachability Analysis Technique},
  journal	= {Software Practice and Experience},
  volume	= {18},
  number	= {2},
  year		= {1988},
  pages		= {137-161}
}

@InProceedings{	  holzmann.94.forte,
  author	= {Gerard J. Holzmann and Doron Peled},
  title		= {An Improvement in Formal Verification},
  booktitle	= {Proceeding of the 7th IFIP WG 6.1 International Conference
		  on Formal Description Techniques (FORTE'94)},
  address	= {Berne, Switzerland},
  pages		= {109--124},
  year		= {1994},
  series	= {IFIP Conference Proceedings},
  volume	= {6},
  publisher	= {Chapman {\&} Hall},
  isbn		= {0-412-64450-9}
}

@InProceedings{	  holzmann.96.spin,
  author	= {Gerard J. Holzmann and Doron A. Peled and Mihalis
		  Yannakakis},
  title		= {On Nested Depth First Search},
  booktitle	= {Proceedings of the 2nd Spin Workshop},
  year		= {1996},
  publisher	= {American Mathematical Society},
  editor	= {Jean-Charles Gr{\'e}goire and Gerard J. Holzmann and Doron
		  A. Peled},
  volume	= {32},
  series	= {DIMACS: Series in Discrete Mathematics and Theoretical
		  Computer Science},
  month		= may
}

@Article{	  holzmann.97.tse,
  author	= {Gerard J. Holzmann},
  title		= {The Model Checker {Spin}},
  journal	= {IEEE Transactions on software Engineering},
  year		= {1997},
  volume	= {23},
  number	= {5},
  pages		= {279--295},
  month		= may
}

@Article{	  holzmann.98.fmsd,
  author	= {Gerard J. Holzmann},
  title		= {An analysis of bitstate hashing},
  journal	= {Formal Methods in Systems Design},
  year		= {1998},
  month		= nov
}

@InProceedings{	  hugues.04.fmics,
  author	= {J{\'e}r{\^o}me Hugues and Yann Thierry-Mieg and Fabrice
		  Kordon and Laurent Pautet and Soheib Barrir and Thomas
		  Vergnaud},
  title		= {On the Formal Verification of Middleware Behavioral
		  Properties},
  booktitle	= {Proceedings of the 9th International Workshop on Formal
		  Methods for Industrial Critical Systems (FMICS'04)},
  pages		= {139--157},
  year		= {2004},
  series	= {Electronic Notes in Theoretical Computer Science},
  publisher	= {Elsevier Science Publishers},
  volume	= {133},
  month		= sep
}

@InProceedings{	  jard.89.cav,
  author	= {Claud Jard and Thierry J{\'e}ron},
  title		= {On-line model-checking for finite linear temporal logic
		  specifications},
  booktitle	= {Proceedings of the International Workshop on Automatic
		  Verification Methods for Finite State Systems},
  address	= {Grenoble, France},
  volume	= {407},
  pages		= {275--285},
  series	= {LNCS},
  publisher	= {Springer-Verlag},
  month		= jun,
  year		= {1989}
}

@InProceedings{	  jin.02.tacas,
  author	= {HoonSang Jin and Kavita Ravi and Fabio Somenzi},
  title		= {Fate and Free Will in Error Traces},
  booktitle	= {Proceedings of the International Conference on Tools and
		  Algorithms forConstruction and Analysis of Systems
		  (TACAS'02)},
  pages		= {445--459},
  year		= {2002},
  editor	= {J.-P. Katoen and P. Stevens},
  volume	= {2280},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@PhDThesis{	  junttila.03.phd,
  author	= {Tommi Junttila},
  title		= {On the Symmetry Reduction Method for Petri Nets and
		  Similar Formalisms},
  school	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  year		= {2003},
  address	= {Espoo, Finland}
}

@InProceedings{	  jurdzinski.00.stacs,
  author	= {Marcin Jurdzi{\'n}ski},
  title		= {Small Progress Measures for Solving Parity Games},
  year		= {2000},
  pages		= {290--301},
  month		= feb,
  booktitle	= {Proceedings of the 17th Symposium on Theoretical Aspects
		  of Computer Science (STACS 2000)},
  volume	= {1770},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Article{	  kesten.01.jcss,
  author	= {Yonit Kesten and Amir Pnueli and Moshe Y. Vardi},
  title		= {Verification by Augmented Abstraction: The
		  Automata-Theoretic View},
  journal	= {Journal of Computer and System Sciences},
  volume	= {62},
  number	= {4},
  pages		= {668-690},
  year		= {2001}
}

@Article{	  kesten.05.tcs,
  author	= {Ynoit Kesten and Amir Pnueli},
  title		= {A Compositional Approach to \textsc{ctl}$^*$ Verification},
  journal	= {Theoretical Computer Science},
  year		= {2005},
  volume	= {331},
  number	= {2--3},
  pages		= {397--428},
  month		= feb
}

@InProceedings{	  kesten.93.cav,
  author	= {Yonit Kesten and Zohar Manna and Hugh McGuire and Amir
		  Pnueli},
  title		= {A Decision Algorithm for Full Propositional Temporal
		  Logic},
  booktitle	= {Proceedings of the 5th Conference on Computer Aided
		  Verification (CAV'93)},
  pages		= {97--109},
  year		= {1993},
  editor	= {C. Courcoubetis},
  volume	= {697},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  kesten.98.icalp,
  author	= {Yonit Kesten and Amir Pnueli and Li-on Raviv},
  title		= {Algorithmic Verification of Linear Temporal Logic
		  Specifications},
  booktitle	= {Proceedins of the 5th International Colloquium on
		  Automata, Languages, and Programming (ICALP'98)},
  pages		= {1--16},
  year		= {1998},
  editor	= {K.G. Larsen and S. Skyum and G. Winskel},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {1443}
}

@PhDThesis{	  klai.03.phd,
  author	= {Kais Klai},
  title		= {R{\'e}seaux de {Petri}: v{\'e}rification symbolique et
		  modulaire},
  school	= {Universit{\'e} Paris 6},
  year		= {2003},
  address	= {France}
}

@InProceedings{	  klarlund.91.focs,
  author	= {Nils Klarlund},
  title		= {Progress Measures for Complementation of $\omega$-Automata
		  with Applications to Temporal Logic},
  booktitle	= {Proceedings of the 32nd annual symposium on Foundations of
		  computer science (FOCS'91)},
  pages		= {358--367},
  year		= {1991},
  address	= {San Juan, Puerto Rico},
  publisher	= {IEEE Computer Society Press}
}

@Book{		  kleene.67.ml,
  author	= {Stephen C. Kleene},
  title		= {Mathematical Logic},
  publisher	= {Wiley},
  year		= {1967},
  address	= {New York}
}

@InProceedings{	  kupferman.86.istc,
  author	= {Orna Kupferman and Moshe Y. Vardi},
  title		= {Weak alternating automata are not that weak},
  booktitle	= {Proceedings of the 5st Israeli Symposium on Theory of
		  Computing and Systems (ISTC'97)},
  pages		= {147--158},
  year		= {1997},
  publisher	= {IEEE Computer Society Press}
}

@InProceedings{	  kupferman.98.astc,
  author	= {Orna Kupferman and Moshe Y. Vardi},
  title		= {Weak alternating automata and tree automata emptiness},
  booktitle	= {Proceedings 30th ACM Symposium on Theory of Computing},
  pages		= {224--233},
  year		= {1998},
  publisher	= {ACM}
}

@InProceedings{	  kupferman.99.cav,
  author	= {Orna Kupferman and Moshe Y. Vardi},
  title		= {Model Checking of Safety Properties},
  booktitle	= {Proceedinfs of the 11th International Conference on
		  Computer Aided Verification (CAV'99)},
  pages		= {172--183},
  year		= {1999},
  editor	= {N. Halbwachs and D. Peled},
  volume	= {1633},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Book{		  lane.90,
  editor	= {Sounders Mac Lane and Dirk Siefkes},
  title		= {The Collected Works of {J.} {R}ichard {B\"u}chi},
  publisher	= {Springer-Verlag},
  year		= {1990}
}

@InProceedings{	  laroussinie.02.lics,
  author	= {Fran{\c{c}}ois Laroussinie and Nicolas Markey and Philippe
		  Schnoebelen},
  title		= {Temporal Logic with Forgettable Past},
  booktitle	= {Proceedings of the 17th IEEE Sumposium on Logic in
		  Computer Science (LICS'02)},
  year		= {2002},
  address	= {Copenhagen, Denmark},
  month		= jul,
  publisher	= {IEEE Computer Society Press}
}

@Article{	  laroussinie.95.tcs,
  author	= {Fran{\c{c}}ois Laroussinie and Philippe Schnoebelen},
  title		= {A Hierarchy of Temporal Logics with Past},
  journal	= {Theoretical Computer Science},
  year		= {1995},
  volume	= {297},
  number	= {1--3},
  pages		= {297--315}
}

@Article{	  latvala.00.fi,
  author	= {Timo Latvala and Keijo Heljanko},
  title		= {Coping With Strong Fairness},
  journal	= {Fundamenta Informaticae},
  year		= {2000},
  volume	= {43},
  number	= {1--4},
  pages		= {1--19},
  publisher	= {IOS Press}
}

@TechReport{	  latvala.01.a67,
  author	= {Timo Latvala},
  title		= {Model Checking Linear Temporal Logic Properties of {P}etri
		  Nets with Fairness Constraints},
  institution	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  month		= {January},
  number	= {A67},
  pages		= {44},
  address	= {Espoo, Finland},
  type		= {Research Report},
  year		= {2001}
}

@InProceedings{	  latvala.01.icatpn,
  author	= {Timo Latvala},
  title		= {Model Checking {LTL} Properties of High-Level {P}etri Nets
		  with Fairness Constraints},
  booktitle	= {Proceedings of the 22nd International Conference on
		  Application and Theory of Petri Nets (ICATPN'01)},
  pages		= {242--262},
  year		= {2001},
  volume	= {2075},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@TechReport{	  latvala.02.a76,
  author	= {Timo Latvala},
  title		= {On Model Checking Safety Properties},
  institution	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  year		= {2002},
  type		= {Technical Report},
  number	= {A76},
  address	= {Espoo, Finland},
  note		= {Reprint of Licentiate's thesis}
}

@InProceedings{	  latvala.03.spin,
  author	= {Timo Latvala},
  title		= {Efficient Model Checking of Safety Properties},
  booktitle	= {Proceedings of the 10th International SPIN Workshop on
		  Model Checking of Software},
  pages		= {74--88},
  year		= {2003},
  editor	= {T. Ball and S. K. Rajamani},
  volume	= {2648},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@PhDThesis{	  leroux.03.phd,
  author	= {J{\'e}r{\^o}me Leroux},
  title		= {Algorithmique de la v{\'e}rification des syst{\`e}mes
		  {\`a} compteurs. Approximation et acc{\'e}l{\'e}ration.
		  Impl{\'e}mentation de l'outil {\sc Fast}},
  school	= {{\'E}cole Normale Sup{\'e}rieure de Cachan},
  year		= {2003},
  month		= dec
}

@InProceedings{	  li.06.imsccs,
  author	= {Yige Li and Kanglin Xie and Tao Hao},
  title		= {Combining {Couvreur}'s Algorithm with Bitstate-hashing for
		  Emptiness Check},
  booktitle	= {Proceedings of the First International Multi-Symposium on
		  Computer and Computational Sciences (IMSCCS'06)},
  year		= {2006},
  pages		= {283-286},
  volume	= {2}
}

@InProceedings{	  lichtenstein.85.popl,
  author	= {Orna Lichtenstein and Amir Pnueli},
  title		= {Checking That Finite State Concurrent Programs Satisfy
		  Their Linear Specification},
  booktitle	= {Proceedings of the 12th ACM Symposium on Principles of
		  Programming Languages (POPL'85)},
  pages		= {97--107},
  year		= {1985},
  publisher	= {ACM}
}

@Misc{		  lind.02.buddy,
  author	= {J{\o}rn Lind-Nielsen},
  title		= {{BuDDy}: {B}inary {D}ecision {D}iagram package},
  howpublished	= {Release 2.2},
  month		= nov,
  year		= {2002},
  url		= {http://www.itu.dk/research/buddy/}
}

@InProceedings{	  maidl.00.focs,
  author	= {Monika Maidl},
  title		= {The Common Fragment of {CTL} and {LTL}},
  booktitle	= {Proceedings of the 31st Annula Symposium on Foundations of
		  Computer Science (FOCS'00)},
  pages		= {643--652},
  publisher	= {IEEE Computer Society},
  month		= nov,
  year		= {2000}
}

@InProceedings{	  maler.06.formats,
  author	= {Oded Maler and Dejan Nickovic and Amir Pnueli},
  title		= {From MITL to Timed Automata},
  booktitle	= {Proceedings of the 4th International Conference on Formal
		  Modelling and Analysis of Timed Systems (FORMATS'06)},
  pages		= {274--289},
  year		= {2006},
  volume	= {4202},
  series	= {Lecture Notes in Computer Science},
  month		= sep,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  manna.00.icalp,
  author	= {Zohar Manna and Henry B. Sipma},
  title		= {Alternating the temporal picture for safety},
  pages		= {429--450},
  editor	= {U. Montanari and J. D. Rolim and E. Welzl},
  booktitle	= {Proceedins of the 27th International Colloquium on
		  Automata, Languages, and Programming (ICALP'00)},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {1000},
  year		= {1995},
  address	= {Toulouse, France},
  month		= jul
}

@Book{		  manna.95.tvrs,
  author	= {Zohar Manna and Amir Pnueli},
  title		= {Temporal Verification of Reactive Systems -- Safety},
  publisher	= {Springer-Verlag},
  year		= {1995}
}

@InProceedings{	  markey.02.express,
  author	= {Nicolas Markey},
  title		= {Past is for Free: on the Complexity of Verifying Linear
		  Temporal Properties with Past},
  booktitle	= {Proceedings of the 9th International Workshop on
		  Expressiveness in Concurrency (EXPRESS'02)},
  year		= {2002},
  editor	= {Uwe Nestmann and Prakash Panangaden},
  volume	= {68.2},
  series	= {Electronic Notes in Theoretical of Computer Science},
  publisher	= {Elsevier Science Publishers}
}

@InProceedings{	  merz.01.mvpp,
  author	= {Stephan Merz},
  title		= {Model Checking: A Tutorial Overview},
  booktitle	= {Proceedings of the 4th Summer School on Modeling and
		  Verification of Parallel Processes (MOVEP'00)},
  pages		= {3--38},
  year		= {2001},
  editor	= {F. Cassez and C. Jard and B. Rozoy and M. Dermot},
  volume	= {2067},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@TechReport{	  merz.03.tr,
  author	= {Stephan Merz and Ali Sezgin},
  title		= {Emptiness of Linear Weak Alternating Automata},
  institution	= {LORIA},
  year		= {2003},
  month		= dec
}

@InProceedings{	  michel.84.stacs,
  author	= {Max Michel},
  title		= {Alg{\`e}bre de machines et logique temporelle},
  booktitle	= {Proceedings of the Symposium on Theoretical Aspects of
		  Computer Science (STACS'84)},
  pages		= {287--298},
  year		= {1984},
  editor	= {Max Fontet and Kurt Mehlhorn},
  volume	= {166},
  series	= {Lecture Notes in Computer Science},
  address	= {Paris},
  month		= apr
}

@InProceedings{	  minato.92.sasimi,
  author	= {{Shin-ichi} {Minato}},
  title		= {Fast Generation of Irredundant Sum-of-Products Forms from
		  Binary Decision Diagrams},
  booktitle	= {Proceedings of the third Synthesis and Simulation and
		  Meeting International Interchange workshop (SASIMI'92)},
  pages		= {64--73},
  year		= {1992},
  address	= {Kobe, Japan},
  month		= {April}
}

@Article{	  miyano.84.tcs,
  author	= {Satoru Miyano and Takeshi Hayashi},
  title		= {Alternating Finite Automata on $\omega$-words},
  journal	= {Theoretical Computer Science},
  year		= {1984},
  volume	= {32},
  pages		= {321--330}
}

@InProceedings{	  muller.84.lncs,
  author	= {David E. Muller and Paul E. Shupp},
  title		= {Alternating automata on infinite objects : Determinacy and
		  rabin's theorem},
  booktitle	= {Proceedings of the {\'E}cole de Printemps d'Informatique
		  Theorique on Automata on Infinite Words},
  volume	= {192},
  pages		= {100--107},
  year		= {1984},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer},
  editor	= {Maurice Nivat and Dominique Perrin}
}

@InProceedings{	  muller.86.lncs,
  author	= {David E. Muller and Ahmed Saoudi and Paul E. Shupp},
  title		= {Alternating automata, the weak monadic theory of the tree
		  and its complexiy},
  booktitle	= {Proceedings 13th of the International Colloquium on
		  Automata, Languages and Programming (ICALP'86)},
  pages		= {233--244},
  volume	= {226},
  year		= {1986},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer},
  editor	= {Laurent Kott}
}

@InProceedings{	  muller.87.tcs,
  author	= {David E. Muller and Paul. E. Shupp},
  title		= {Alternating automata on infinite trees},
  booktitle	= {Theoretical Computer Science},
  pages		= {10:267--276},
  year		= {1987}
}

@Article{	  nalumasu.02.fm,
  author	= {Ratan Nalumasu and Ganesh Gopalakrishnan},
  title		= {An Efficient Partial Order Reduction Algorithm with an
		  Alternative Proviso Implementation},
  journal	= {Formal Methods in System Design},
  year		= {2002},
  volume	= {20},
  number	= {1},
  pages		= {231-247},
  month		= jan
}

@TechReport{	  nalumasu.98.tr,
  author	= {Ratan Nalumasu and Ganesh Gopalakrishnan},
  title		= {Partial Order Reduction Without the Proviso},
  institution	= {University of Utah, Department of Computer Science},
  year		= {1998},
  type		= {Technical Report},
  number	= {UUCS-98-017}
}

@PhDThesis{	  oddoux.03.phd,
  author	= {Denis Oddoux},
  title		= {Utilisation des automates alternants pour un
		  model-checking efficace des logiques temporelles
		  lin{\'e}aires},
  school	= {Universit{\'e}e Paris 7},
  year		= {2003},
  address	= {Paris, France},
  month		= dec
}

@Article{	  pastor.01.tc,
  author	= {Enric Pastor and Jordi Cortadella and Oriol Roig},
  title		= {Symbolic Analysis of Bounded {P}etri Nets},
  journal	= {IEEE Transactions on Computers},
  year		= {2001},
  volume	= {50},
  number	= {5},
  pages		= {432--448},
  month		= may
}

@InProceedings{	  pastor.98.date,
  author	= {Enric Pastor and Jordi Cortadella},
  title		= {Efficient Encoding Schemes for Symbolic Analysis of
		  {P}etri Nets},
  booktitle	= {Proceedings of the Conference on Design, Automation and
		  Test in Europe},
  pages		= {790--795},
  year		= {1998},
  address	= {Paris},
  month		= mar,
  url		= {http://www.lsi.upc.es/~jordic/publications/conferences.html}
		  
}

@InProceedings{	  peled.94.cav,
  author	= {Doron Peled},
  title		= {Combining Partial Order Reductions with On-the-fly
		  Model-Checking},
  booktitle	= {Proceedings of the 6th International Conference on
		  Computer Aided Verification (CAV'94)},
  year		= {1994},
  pages		= {377--390},
  publisher	= {Springer-Verlag},
  volume	= {818},
  series	= {Lecture Notes in Computer Science}
}

@InProceedings{	  peled.95.pstv,
  author	= {Doron Peled and Wojciech Penczek},
  title		= {Using asynchronous {B\"u}chi automata for efficient
		  automatic verification of concurrent systems},
  booktitle	= {Proceedings of the 15th Workshop on Protocol Specification
		  Testing and Verification (PSTV'95)},
  publisher	= {Chapman \& Hall},
  address	= {Warsaw, Poland},
  pages		= {315--330},
  year		= {1996}
}

@InProceedings{	  pnueli.87.tls,
  author	= {Zohar Manna and Amir Pnueli},
  title		= {Specification and verification of concurrent programs by
		  $\forall$-automata},
  booktitle	= {Temporal Logic in Specification},
  pages		= {124--164},
  year		= {1987},
  editor	= {B.Banieqbal, H.Barringer and A.Pnueli},
  number	= {398},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  rauchhenzinger.96.swat,
  author	= {Monika {Rauch Henzinger} and Jan Arne Telle},
  title		= {Faster Algorithms for the Nonemptiness of Streett Automata
		  and for Communication Protocol Pruning.},
  booktitle	= {Proceedings of the 5th Scandinavian Workshop on Algorithm
		  Theory (SWAT'96)},
  year		= {1996},
  pages		= {16--27},
  series	= {Lecture Notes in Computer Science},
  volume	= {1097},
  publisher	= {Springer-Verlag},
  address	= {Reykjav{\'\i}k, Iceland},
  month		= jul
}

@InProceedings{	  ravi.00.fmcad,
  author	= {Kavita Ravi and Roderick Bloem and Fabio Somenzi},
  title		= {A Comparative Study of Symbolic Algorithms for the
		  Computation of Fair Cycles},
  booktitle	= {Proceedings of the 4th International Conference on Formal
		  Methods in Computer Aided Design (FMCAD'00)},
  pages		= {143--160},
  year		= {2000},
  editor	= {M. D. Aagaard, J. W. O'Leary},
  volume	= {2517},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@Misc{		  ronkko.99.lbt,
  author	= {Mauno R{\"o}nkk{\"o}},
  title		= {{LBT}: {LTL} to {B\"u}chi conversion },
  howpublished	= {{\small\url{http://www.tcs.hut.fi/Software/maria/tools/lbt/}}}
		  ,
  year		= {1999},
  note		= {Implements \cite{gerth.95.pstv}.}
}

@PhDThesis{	  safra.89.phd,
  author	= {Shmuel Safra},
  title		= {Complexity of Automata on Infinite Objects},
  school	= {The Weizmann Institute of Science},
  year		= {1989},
  address	= {Rehovot, Israel},
  month		= mar
}

@InProceedings{	  safra.92.stc,
  author	= {Shmuel Safra},
  title		= {Exponential Determinization for $\omega$-Automata with
		  Strong-Fairness Acceptance Condition},
  booktitle	= {Proceedings of the 24th ACM Symposium on Theory of
		  Computing},
  year		= {1992},
  month		= may,
  publisher	= {ACM}
}

@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{	  schneider.97.chdl,
  author	= {Klaus Schneider},
  title		= {{CTL} and Equivalent Sublanguages of {CTL*}},
  booktitle	= {Proceedings of International Conference on Computer
		  Hardware Description Languages and their Applications
		  (CHDL'97)},
  publisher	= "Chapman and Hall",
  address	= {Toledo, Spain},
  editor	= "{C. Delgado Kloos}",
  pages		= {40--59},
  year		= {1997}
}

@InProceedings{	  schroeter.03.atpn,
  author	= {Claus Schr{\"o}ter and Stefan Schwoon and Javier Esparza},
  booktitle	= {Proceedings of the 24th International Conference on
		  Applications and Theory of Petri Nets (ATPN'03)},
  editor	= {Wil van der Aalst and Eike Best},
  month		= jun,
  pages		= {463--472},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  title		= {{The Model-Checking Kit}},
  volume	= {2679},
  year		= {2003}
}

@InProceedings{	  schwendimann.98.tableaux,
  author	= {Stefan Schwendimann},
  title		= {A New One-Pass Tableau Calculus for {PLTL}},
  booktitle	= {Automated Reasoning with Analytic Tableaux and Related
		  Methods, proceedings of TABLEAUX'98},
  pages		= {277--291},
  year		= {1998},
  editor	= {H. de Swart},
  volume	= {1397},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@TechReport{	  schwoon.04.tr,
  author	= {Stefan Schwoon and Javier Esparza},
  title		= {A note on on-the-fly verification algorithms.},
  institution	= {Universit{\"a}t Stuttgart, Fakult{\"a}t Informatik,
		  Elektrotechnik und Informationstechnik},
  year		= {2004},
  month		= nov
}

@InProceedings{	  schwoon.05.tacas,
  author	= {Stefan Schwoon and Javier Esparza},
  title		= {A note on on-the-fly verification algorithms.},
  booktitle	= {Proceedings of the 11th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'05)},
  year		= {2005},
  series	= {Lecture Notes in Computer Science},
  editor	= {Nicolas Halbwachs and Lenore Zuck},
  address	= {Edinburgh, Scotland},
  publisher	= {Springer-Verlag},
  month		= apr,
  volume	= {3440}
}

@InProceedings{	  sebastiani.03.charme,
  author	= {Roberto Sebastiani and Stefano Tonetta},
  title		= {"More Deterministic" vs. "Smaller" {B\"u}chi Automata for
		  Efficient {LTL} Model Checking},
  booktitle	= {Proceedings of the 12th Advanced Research Working
		  Conference on Correct Hardware Design and Verification
		  Methods (CHARME'03)},
  pages		= {126--140},
  year		= {2003},
  editor	= {G. Goos and J. Hartmanis and J. van Leeuwen},
  volume	= {2860},
  address	= {L'Aquila, Italy},
  series	= {Lecture Notes in Computer Science},
  month		= oct,
  publisher	= {Springer-Verlag}
}

@TechReport{	  sebastiani.03.tr,
  author	= {Roberto Sebastiani and Stefano Tonetta},
  title		= {"More Deterministic" vs. "Smaller" {B\"u}chi Automata for
		  Efficient LTL Model Checking},
  institution	= {University of Trento},
  year		= {2003},
  number	= {\#DIT-03-041},
  month		= jul,
  note		= {Extended version of \cite{sebastiani.03.charme}}
}

@InProceedings{	  sebastiani.05.cav,
  author	= {Roberto Sebastiani and Stefano Tonetta and Moshe Y.
		  Vardi},
  title		= {Symbolic Systems, Explicit Properties: on Hybrid Approches
		  for LTL Symbolic Model Checking},
  booktitle	= {Proceedings of 17th International Conference on Computer
		  Aided Verification (CAV'05)},
  pages		= {350--363},
  year		= {2005},
  editor	= {Kousha Etessami and Sriram K. Rajamani},
  volume	= {3576},
  series	= {Lecture Notes in Computer Science},
  address	= {Edinburgh, Scotland, UK},
  month		= jul,
  publisher	= {Springer-Verlag}
}

@Book{		  smullyan.68.fol,
  author	= {Raymon M. Smullyan},
  title		= {First-Order Logic},
  publisher	= {Springer-Verlag},
  year		= {1968}
}

@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{	  stern.95.charme,
  author	= {Ulrich Stern and David L. Dill},
  title		= {Improved Probabilistic Verification by Hash Compaction},
  booktitle	= "Proceedings of the Advanced Research Working Conference on
		  Correct Hardware Design and Verification Methods
		  (CHARME'95)",
  volume	= {987},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag},
  editor	= {P.E. Camurati and H. Eveking},
  pages		= {206--224},
  year		= {1995}
}

@InProceedings{	  tabakov.07.lata,
  author	= {Deian Tabakov and Mushe Y. Vardi},
  title		= {Model Checking Büchi Specifications},
  booktitle	= {Proceedings of the 1st International Conference on
		  Language and Automata Theory and Applications (LATA'07)},
  year		= {2007},
  series	= {Lecture Notes in Computer Science},
  month		= apr,
  publisher	= {Springer-Verlag},
  note		= {To appear.}
}

@InProceedings{	  tarjan.71.ssat,
  author	= {Robert Tarjan},
  title		= {Depth-First Search and Linear Graph Algorithms},
  booktitle	= {Conference records of the 12th Annual IEEE Symposium on
		  Switching and Automata Theory},
  pages		= {114--121},
  year		= {1971},
  month		= {October},
  publisher	= {IEEE},
  note		= {Later republished as \cite{tarjan.72.siam}}
}

@Article{	  tarjan.72.siam,
  author	= {Robert Tarjan},
  title		= {Depth-First Search and Linear Graph Algorithms},
  journal	= {SIAM Journal on Computing},
  year		= {1972},
  volume	= {1},
  number	= {2},
  pages		= {146--160}
}

@TechReport{	  tauriainen.00.a66,
  author	= {Heikki Tauriainen},
  title		= {Automated Testing of {B\"u}chi Automata Translators for
		  {L}inear {T}emporal {L}ogic},
  address	= {Espoo, Finland},
  institution	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  number	= {A66},
  year		= {2000},
  url		= {http://citeseer.nj.nec.com/tauriainen00automated.html},
  type		= {Research Report},
  note		= {Reprint of Master's thesis}
}

@InProceedings{	  tauriainen.00.spin,
  author	= {Heikki Tauriainen and Keijo Heljanko},
  title		= {Testing {SPIN}'s {LTL} formula conversion into {B\"u}chi
		  automata with randomly generated input},
  booktitle	= {Proceedings of the 7th International SPIN Workshop on
		  Model Checking of Software (SPIN'2000)},
  pages		= {54--72},
  year		= {2000},
  editor	= {K. Havelund and J. Penix and W. Visser},
  volume	= {1885},
  series	= {Lecture Notes in Computer Science},
  address	= {Stanford University, California, USA},
  month		= aug,
  publisher	= {Springer-Verlag}
}

@Article{	  tauriainen.02.sttt,
  author	= {Heikki Tauriainen and Keijo Heljanko},
  title		= {Testing {LTL} formula translation into {B\"u}chi automata},
  journal	= {International Journal on Software Tools for Technology
		  Transfer},
  year		= {2002},
  volume	= {4},
  number	= {1},
  pages		= {57--70},
  publisher	= {Springer-Verlag}
}

@TechReport{	  tauriainen.03.a79,
  address	= {Espoo, Finland},
  author	= {Heikki Tauriainen},
  institution	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  month		= jul,
  number	= {A79},
  pages		= {16},
  title		= {Nested Emptiness Search for Generalized {B\"u}chi
		  Automata},
  type		= {Research Report},
  year		= {2003}
}

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

@InProceedings{	  tauriainen.04.acsd,
  author	= {Heikki Tauriainen},
  title		= {Nested Emptiness Search for Generalized {B\"u}chi
		  Automata},
  booktitle	= {Proceedings of the 4th International Conference on
		  Application of Concurrency to System Design (ACSD'04)},
  pages		= {165--174},
  publisher	= {IEEE Computer Society},
  month		= jun,
  adress	= {Hamilton, Canada},
  year		= {2004}
}

@TechReport{	  tauriainen.05.a96,
  author	= {Heikki Tauriainen},
  title		= {A note on the worst-case memory requirements of
		  generalized nested depth-first search},
  institution	= {Helsinki University of Technology, Laboratory for
		  Theoretical Computer Science},
  address	= {Espoo, Finland},
  month		= sep,
  number	= {A96},
  type		= {Research Report},
  year		= {2005}
}

@PhDThesis{	  tauriainen.06.phd,
  author	= {Heikki Tauriainen},
  title		= {Automata and Linear Temporal Logic: Translation with
		  Transition-based Acceptance},
  school	= {Helsinki University of Technology},
  year		= {2006},
  address	= {Espoo, Finland},
  month		= sep
}

@InProceedings{	  tauriainen.99,
  author	= {Heikki Tauriainen},
  title		= {A randomized testbench for algorithms translating linear
		  temporal logic formul{\ae} into {B\"u}chi automata.},
  booktitle	= {Proceedings of the Concurrency, Specification and
		  Programming 1999 Workshop (CS{\&}P'99)},
  pages		= {251--262},
  year		= {1999},
  editor	= {H-D. Burkhard and L. Czaja and H-S. Nguyen and P. Starke},
  address	= {Warsaw, Poland},
  month		= sep
}

@InProceedings{	  thierry-mieg.03.forte,
  author	= {Yann Thierry-Mieg and Jean-Michel Ili{\'e} and Denis
		  Poitrenaud},
  title		= {A Symbolic Symbolic State Space Representation},
  booktitle	= {Proceedings of the 24nd IFIP WG 6.1 International
		  Conference on Formal Techniques for Networked and
		  Distributed Systems (FORTE'04)},
  year		= {2004},
  address	= {Madrid, Spain},
  month		= sep
}

@InProceedings{	  thierry-mieg.03.icatpn,
  author	= {Yann Thierry-Mieg and Claude Dutheillet and Isabelle
		  Mounier},
  title		= {Automatic Symmetry Detection in Well-Formed Nets},
  booktitle	= {Proceedings of the 24th International Conference on
		  Application and Theory of Petri Nets (ICATPN'03)},
  address	= {Eindhoven, The Netherlands},
  editor	= {Wil van der Aalst and Eike Best},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag},
  volume	= {2679},
  month		= jun,
  year		= {2003},
  pages		= {82--101}
}

@Article{	  thierry-mieg.04.gl,
  author	= {Yann Thierry-Mieg and Soheib Baarir and Alexandre
		  Duret-Lutz and Fabrice Kordon},
  title		= {Nouvelles techniques de model-checking pour la
		  v{\'e}rification de syst{\`e}mes complexes},
  journal	= {G{\'e}nie Logiciel},
  year		= {2004},
  number	= {69},
  pages		= {17--23},
  month		= jun
}

@PhDThesis{	  thierry-mieg.04.phd,
  author	= {Yann Thierry-Mieg},
  title		= {Technique pour le Model-Checking de sp{\'e}cifications de
		  Haut Niveau},
  school	= {Universit{\'e} de Paris 6, LIP6},
  year		= {2004},
  address	= {Paris, France},
  month		= dec,
  note		= {In English}
}

@InProceedings{	  thirioux.02.fmics,
  author	= {Xavier Thirioux},
  title		= {Simple and Efficient Translation from {LTL} Formulas to
		  {B\"u}chi Automata},
  booktitle	= {Proceedings of the 7th International ERCIM Workshop in
		  Formal Methods for Industrial Critical Systems (FMICS'02)},
  series	= {Electronic Notes in Theoretical Computer Science},
  volume	= {66(2)},
  publisher	= {Elsevier},
  editor	= {Rance Cleaveland and Hubert Garavel},
  year		= {2002},
  month		= jul,
  address	= {M{\'a}laga, Spain}
}

@TechReport{	  thomas.96.tr,
  author	= {Wolfgang Thomas},
  title		= {Languages, Automata, and Logic},
  institution	= {Institut f{\"u}r Informatik und Praktische Mathematik,
		  Christian-Albrechts-Universit{\"a}t zu Kiel, Germany},
  year		= {1996},
  number	= {9607},
  month		= may
}

@InCollection{	  thomas.99.jewels,
  author	= {Wolfgang Thomas},
  title		= {Complementation of {B\"uchi} Automata Revisited},
  editor	= {J. Karhumäki and H.A. Maurer and G. Paun and G.
		  Rozenberg},
  booktitle	= {Jewels are Forever, Contributions on Theoretical Computer
		  Science in Honor of Arto Salomaa},
  publisher	= {Springer-Verlag},
  year		= {1999},
  pages		= {109--120}
}

@PhDThesis{	  tretmans.92.phd,
  author	= {Jan Tretmans},
  title		= {A Formal Approach to Conformance Testing},
  school	= {University of Twente},
  year		= {1992},
  address	= {Enschede, The Netherlands}
}

@InProceedings{	  tretmans.99.concur,
  author	= {Jan Tretmans},
  title		= {Testing Concurrent Systems: A Formal Approach},
  booktitle	= {Proceedings of the 10th International Conference on
		  Concurrency Theory (CONCUR'99)},
  year		= {1999},
  pages		= {46--65},
  series	= {Lecture Notes in Computer Science},
  volume	= {1664},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  valmari.91.icatpn,
  author	= {Antti Valmari},
  title		= {Stubborn sets for reduced state space generation},
  booktitle	= {Proceedings of the 10th International Conference on
		  Applications and Theory of Petri Nets (ICATPN'91)},
  year		= {1991},
  pages		= {491--515},
  publisher	= {Springer-Verlag},
  volume	= {618},
  series	= {Lecture Notes in Computer Science},
  address	= {London, UK}
}

@InProceedings{	  valmari.93.cav,
  author	= {Antti Valmari},
  title		= {On-the-Fly Verification with Stubborn Sets},
  booktitle	= {Proceedings of the 5th International Conference on
		  Computer Aided Verification (CAV '93)},
  year		= {1993},
  pages		= {397--408},
  publisher	= {Springer-Verlag},
  address	= {London, UK}
}

@InCollection{	  valmari.98.lpn,
  author	= {Antti Valmari},
  title		= {The State Explosion Problem},
  booktitle	= {Lectures on {P}etri Nets 1: Basic Models},
  pages		= {429--528},
  publisher	= {Springer-Verlag},
  year		= {1998},
  editor	= {W. Reisig and G. Rozenberg},
  volume	= {1491},
  series	= {Lecture Notes in Computer Science}
}

@InProceedings{	  vardi.01.tacas,
  author	= {Moshe Y. Vardi},
  title		= {Branching vs. Linear Time: Final Showdown},
  booktitle	= {Proceedings of the 7th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'01)},
  pages		= {1--22},
  year		= {2001},
  editor	= {T. Margaria and W. Yi},
  volume	= {2031},
  series	= {Lecture Notes in Computer Science},
  address	= {Genova, Italy},
  month		= apr,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  vardi.05.alc,
  author	= {Moshe Y. Vardi},
  title		= {Büchi Complementation: A Forty-Year Saga},
  year		= 2005,
  booktitle	= {5th symposium on Atomic Level Characterizations (ALC'05)},
  note		= {Invited extended abstract}
}

@InProceedings{	  vardi.07.stacs,
  author	= {Moshe Y. Vardi},
  title		= {The {B\"u}chi Complementation Saga},
  booktitle	= {Proceedings of the 17th Symposium on Theoretical Aspects
		  of Computer Science (STACS'07)},
  year		= {2007},
  address	= {Aachen, Germany},
  month		= feb,
  note		= {Invited paper.}
}

@InProceedings{	  vardi.07.vmcai,
  author	= {Moshe Y. Vardi},
  title		= {Automata-theoretic model checking revisited},
  booktitle	= {Proceedings of the 8th International Conference on
		  Verification, Model Checking and Abstract Interpretation
		  (VMCAI'07) },
  year		= {2007},
  volume	= {4349},
  series	= {Lecture Notes in Computer Science},
  address	= {Nice, France},
  month		= jan,
  publisher	= {Springer-Verlag},
  note		= {Invited paper.}
}

@InProceedings{	  vardi.86.lics,
  author	= {Moshe Y. Vardi},
  title		= {An Automata-Theoretic Approach to Automatic Program
		  Verification},
  booktitle	= {Proceedings of the 1st IEEE Symposium on Logic in Computer
		  Science (LICS'86)},
  pages		= {332--344},
  year		= {1986},
  publisher	= {IEEE Computer Society Press}
}

@Article{	  vardi.94.ic,
  author	= {Moshe Y. Vardi and Pierre Wolper},
  title		= {Reasoning about Infinite Computations},
  journal	= {Information and Computation},
  pages		= {1--37},
  volume	= {115},
  number	= {1},
  year		= {1994},
  month		= nov
}

@InProceedings{	  vardi.95.cst,
  author	= {Moshe Y. Vardi},
  title		= {Alternating Automata and Program Verification},
  pages		= {471--485},
  editor	= {J. van Leeuwen},
  booktitle	= {Computer Science Today, Recent Trends and Developments},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {1000},
  year		= {1995}
}

@InProceedings{	  vardi.96.banff,
  author	= {Moshe Y. Vardi},
  title		= {An Automata-Theoretic Approach to Linear Temporal Logic},
  pages		= {238--266},
  editor	= {Faron Moller and Graham M. Birtwistle},
  booktitle	= {Proceedings of the 8th Banff Higher Order Workshop
		  (Banff'94)},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {1043},
  year		= {1996},
  isbn		= {3-540-60915-6},
  address	= {Banff, Alberta, Canada}
}

@InProceedings{	  varpaaniemi.97.cav,
  author	= {Kimmo Varpaaniemi and Keijo Heljanko and Johan Lilius},
  title		= {{PROD} 3.2: An Advanced Tool for Efficient Reachability
		  Analysis},
  booktitle	= {Proceedings of the 9th International Conference on
		  Computer Aided Verification (CAV'97)},
  pages		= {472-475},
  year		= {1997},
  volume	= {1254},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  varpaaniemi.98.icatpn,
  author	= {Kimmo Varpaaniemi},
  title		= {On Stubborn Sets in the Verification of Linear Time
		  Temporal Properties},
  booktitle	= {Proceedings of the 19th International Conference on
		  Application and Theory of Petri Nets (ICATPN'98)},
  pages		= {124--143},
  year		= {1998},
  editor	= {J. Desel and M. Silva},
  volume	= {1420},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@PhDThesis{	  varpaaniemi.98.phd,
  author	= {Kimmo Varpaaniemi},
  title		= {On The Stubborn Set Method in Reduced State Space
		  Generation},
  school	= {Helsinki University of Technology},
  year		= {1998},
  month		= may
}

@InProceedings{	  vernadat.96.icatpn,
  author	= {Francois Vernadat and Pierre Azema and Francois Michel},
  title		= {Covering Step Graph},
  booktitle	= {Proceedings of the 17th International Conference on
		  Application and Theory of Petri Nets (ICATPN'96)},
  pages		= {516--535},
  year		= {1996},
  volume	= {1091},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@PhDThesis{	  visser.98.phd,
  author	= {Willem C. Visser},
  title		= {Efficient {CTL*} Model Checking Using Games and Automata},
  school	= {University of Manchester},
  year		= {1998},
  month		= jun
}

@InProceedings{	  vries.98.spin,
  author	= {Ren{\'e} G. de Vries and Jan Tretmans},
  title		= {On-the-Fly Conformance Testing using {Spin}},
  booktitle	= {Fourth Workshop on Automata Theoretic Verification with
		  the {Spin} Model Checker (SPIN'98)},
  year		= {1998},
  month		= nov,
  pages		= {115--128},
  series	= {ENST 98 S 002},
  publisher	= {Ecole Nationale Sup{\'e}rieure des
		  T{\'e}l{\'e}communications},
  address	= {Paris, France}
}

@InProceedings{	  wang.01.concur,
  author	= {Chao Wang and Roderick Bloem and Gary D. Hachtel and
		  Kavita Ravi and Fabio Somenzi},
  title		= {Divide and Compose: {SCC} Refinement for Language
		  Emptiness},
  booktitle	= {Proceedings of the 12th International Conference on
		  Concurrency Theory (Concur'01)},
  pages		= {456--471},
  year		= {2001},
  editor	= {K. G. Larsen and M. Nielsen},
  volume	= {2154},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}

@InProceedings{	  wolfgang.02.dlt,
  author	= {Wolfgang Thomas},
  title		= {A Short Introduction to Infinite Automata},
  booktitle	= {Proceedings of the 5th International Conference on
		  Developments in Language Theory (DLT'01)},
  publisher	= {Springer-Verlag},
  series	= {Lecture Notes in Computer Science},
  volume	= {2295},
  year		= {2002},
  isbn		= {3-540-43453-4},
  pages		= {130--144},
  editor	= {Werner Kuich and Grzegorz Rozenberg and Arto Salomaa}
}

@InProceedings{	  wolper.00.fmpa,
  author	= {Pierre Wolper},
  title		= {Constructing Automata from Temporal Logic Formulas: A
		  Tutorial},
  booktitle	= {Proceedings of the FMPA 2000 summer school},
  pages		= {261--277},
  year		= {2000},
  editor	= {E. Brinksma and H. Hermanns and J.-P. Katoen},
  volume	= {2090},
  series	= {Lecture Notes in Computer Science},
  address	= {Nijmegen, the Netherlands},
  month		= jul,
  publisher	= {Springer-Verlag}
}

@InProceedings{	  wolper.83.focs,
  author	= {Pierre Wolper and Moshe Y. Vardi and Aravinda Prasad
		  Sistla},
  title		= {Reasoning about Infinite Computation Paths},
  booktitle	= {Proceedings of the 24th IEEE Symposium on Foundations of
		  Computer Science (FOCS'83)},
  pages		= {185--194},
  year		= {1983},
  publisher	= {IEEE Computer Society Press},
  note		= {Later extended and published as \cite{vardi.94.ic}.}
}

@Article{	  wolper.83.ic,
  author	= {Pierre Wolper},
  title		= {Temporal Logic Can Be More Expressive},
  journal	= {Information and Control},
  volume	= 56,
  number	= {1--2},
  pages		= {72--99},
  year		= 1983
}

@Article{	  wolper.85.la,
  author	= {Pierre Wolper},
  title		= {The Tableau Method for Temporal Logic: An Overview},
  journal	= {Logique et Analyse},
  number	= {110--111},
  pages		= {119--136},
  year		= {1985}
}

@InProceedings{	  wolper.93.cav,
  author	= {Pierre Wolper and Denis Leroy},
  title		= {Reliable Hashing without Collision Detection},
  booktitle	= {Proceedings of the 5th Conference on Computer Aided
		  Verification (CAV'93)},
  pages		= {59--70},
  year		= {1993},
  editor	= {C. Courcoubetis},
  volume	= {697},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer-Verlag}
}