I am happy to announce that the following paper has been accepted at the International SPIN Symposium on Model Checking of Software, to be held on July 21–23 in San Jose, California. Is There a Best Büchi Automaton for Explicit Model Checking? František Blahoudek¹ Alexandre Duret-Lutz² Mojmír Křetínský¹ Jan Strejček¹ ¹Masaryk University, Brno, Czech Republic ²LRDE, EPITA, Le Kremlin-Bicêtre, France https://www.lrde.epita.fr/wiki/Publications/blahoudek.14.spin Abstract: LTL to Büchi automata (BA) translators are traditionally optimized to produce automata with a small number of states or a small number of non-deterministic states. In this paper, we search for properties of Büchi automata that really influence the performance of explicit model checkers. We do that by manual analysis of several automata and by experiments with common LTL-to-BA translators and realistic verification tasks. As a result of these experiences, we gain a better insight into the characteristics of automata that work well with Spin. -- Alexandre Duret-Lutz