Is there a best büchi automaton for explicit model checking?

Frantisek Blahoudek, Alexandre Duret-Lutz, Mojmír Kretínský, Jan Strejcek. Is there a best büchi automaton for explicit model checking?. In Neha Rungta, Oksana Tkachuk, editors, 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014. pages 68-76, ACM, 2014. [doi]

@inproceedings{BlahoudekDKS14,
  title = {Is there a best büchi automaton for explicit model checking?},
  author = {Frantisek Blahoudek and Alexandre Duret-Lutz and Mojmír Kretínský and Jan Strejcek},
  year = {2014},
  doi = {10.1145/2632362.2632377},
  url = {http://doi.acm.org/10.1145/2632362.2632377},
  researchr = {https://researchr.org/publication/BlahoudekDKS14},
  cites = {0},
  citedby = {0},
  pages = {68-76},
  booktitle = {2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014},
  editor = {Neha Rungta and Oksana Tkachuk},
  publisher = {ACM},
  isbn = {978-1-4503-2452-6},
}