@inproceedings(AbdullaCCHHMV10,
 author       = "P. A. Abdulla and Y.-F. Chen and L. Clemente and L. Hol\'{\i }k and C.-D. Hong and R. Mayr and T. Vojnar",
 year         = "2010",
 title        = "Simulation Subsumption in Ramsey-Based {B}{\"u}chi Automata Universality and Inclusion Testing",
 booktitle    = "Proc.\ 22nd Int.\ Conf.\ on Computer-Aided Verification, {CAV'10}",
 series       = "LNCS",
 volume       = "6174",
 publisher    = "Springer",
 pages        = "132--147",
 doi          = "10.1007/978-3-642-14295-6\_14",
)
@inproceedings(AbdullaCCHHMV11,
 author       = "P. Aziz Abdulla and Y.-F. Chen and L. Clemente and L. Hol\'{\i }k and C.-D. Hong and R. Mayr and T. Vojnar",
 year         = "2011",
 title        = "Advanced Ramsey-Based {B}{\"u}chi Automata Inclusion Testing",
 booktitle    = "Proc.\ 22nd Int.\ Conf.\ on Concurrency Theory, {CONCUR'11}",
 series       = "LNCS",
 volume       = "6901",
 publisher    = "Springer",
 pages        = "187--202",
 doi          = "10.1007/978-3-642-23217-6\_13",
)
@inproceedings(Boas97theconvenience,
 author       = "Peter Van Emde Boas",
 year         = "1997",
 title        = "The Convenience of Tilings",
 booktitle    = "In Complexity, Logic, and Recursion Theory",
 publisher    = "Marcel Dekker Inc",
 pages        = "331--363",
 doi          = "10.1.1.38.763",
)
@inproceedings(buc62,
 author       = "J. R. B{\"u}chi",
 year         = "1962",
 title        = "On a Decision Method in Restricted Second Order Arithmetic",
 booktitle    = "Proc.\ Congress on Logic, Method, and Philosophy of Science",
 publisher    = "Stanford University Press",
 address      = "Stanford, CA, USA",
 pages        = "1--12",
 doi          = "10.1007/978-1-4613-8928-6\_23",
)
@article(Bustan:2003:SM:635499.635502,
 author       = "D. Bustan and O. Grumberg",
 year         = "2003",
 title        = "Simulation-based minimization",
 journal      = "ACM Trans. Comput. Logic",
 volume       = "4",
 number       = "2",
 pages        = "181--206",
 doi          = "10.1145/635499.635502",
)
@article(CeceF05,
 author       = "G. C{\'e}c{\'e} and A. Finkel",
 year         = "2005",
 title        = "Verification of programs with half-duplex communication",
 journal      = "Inf. Comput.",
 volume       = "202",
 number       = "2",
 pages        = "166--190",
 doi          = "10.1016/j.ic.2005.05.006",
)
@article(Chlebus86,
 author       = "B. S. Chlebus",
 year         = "1986",
 title        = "Domino-Tiling Games",
 journal      = "Journal of Computer and System Sciences",
 volume       = "32",
 pages        = "374--392",
 doi          = "10.1016/0022-0000(86)90036-X",
)
@phdthesis(phd-clemente,
 author       = "L. Clemente",
 year         = "2012",
 title        = "Generalized Simulation Relations with Applications in Automata Theory",
 school       = "University of Edinburgh",
)
@inproceedings(MayrC13,
 author       = "Lorenzo Clemente and Richard Mayr",
 year         = "2013",
 title        = "Advanced automata minimization",
 booktitle    = "Proc.\ 40th Symp.\ on Principles of Programming Languages, {POPL'13}",
 publisher    = "ACM",
 pages        = "63--74",
 doi          = "10.1145/2429069.2429079",
)
@inproceedings(dhl-fsttcs06,
 author       = "C. Dax and M. Hofmann and M. Lange",
 year         = "2006",
 title        = "A proof system for the linear time $\mu $-calculus",
 booktitle    = "Proc.\ 26th Conf.\ on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS'06}",
 series       = "LNCS",
 volume       = "4337",
 publisher    = "Springer",
 pages        = "274--285",
 doi          = "10.1007/11944836\_26",
)
@inproceedings(DillHW91,
 author       = "D. L. Dill and A. J. Hu and H. Wong-Toi",
 year         = "1991",
 title        = "Checking for Language Inclusion Using Simulation Preorders",
 booktitle    = "Proc.\ 3rd Int.\ Workshop on Computer-Aided Verification, {CAV'91}",
 series       = "LNCS",
 volume       = "575",
 publisher    = "Springer",
 pages        = "255--265",
 doi          = "10.1007/3-540-55179-4\_25",
)
@article(antichain-journal,
 author       = "L. Doyen and J.-F. Raskin",
 year         = "2009",
 title        = "Antichains for the Automata-Based Approach to Model-Checking",
 journal      = "Logical Methods in Computer Science",
 volume       = "5",
 number       = "1",
 doi          = "10.2168/LMCS-5(1:5)2009",
)
@inproceedings(EtessamiH00,
 author       = "K. Etessami and G. J. Holzmann",
 year         = "2000",
 title        = "Optimizing {B}{\"u}chi Automata",
 booktitle    = "Proc.\ 11th Int.\ Conf. on Concurrency Theory, {CONCUR'00}",
 series       = "LNCS",
 volume       = "1877",
 publisher    = "Springer",
 pages        = "153--167",
 doi          = "10.1007/3-540-44618-4\_13",
)
@inproceedings(EtessamiWS01,
 author       = "K. Etessami and T. Wilke and R. A. Schuller",
 year         = "2001",
 title        = "Fair Simulation Relations, Parity Games, and State Space Reduction for {B}{\"u}chi Automata",
 booktitle    = "Proc.\ 28th Int.\ Coll.\ on Algorithms, Languages and Programming, {ICALP'01}",
 series       = "LNCS",
 volume       = "2076",
 publisher    = "Springer",
 pages        = "694--707",
 doi          = "10.1137/S0097539703420675",
)
@inproceedings(pebble,
 author       = "Kousha Etessami",
 year         = "2002",
 title        = "A Hierarchy of Polynomial-Time Computable Simulations for Automata",
 editor       = "Luboš Brim and Mojmír Křetínský and Antonín Kučera and Petr Jančar",
 booktitle    = "CONCUR 2002 — Concurrency Theory",
 series       = "Lecture Notes in Computer Science",
 volume       = "2421",
 publisher    = "Springer Berlin Heidelberg",
 pages        = "131--144",
 doi          = "10.1007/3-540-45694-5\_10",
)
@inproceedings(conf/tacas/FogartyV10,
 author       = "S. Fogarty and M. Y. Vardi",
 year         = "2010",
 title        = "Efficient {B}{\"u}chi Universality Checking",
 booktitle    = "Proc.\ 16th Int.\ Conf.\ on Tools and Algorithms for the Construction and Analysis of Systems, {TACAS'10}",
 series       = "LNCS",
 volume       = "6015",
 publisher    = "Springer",
 pages        = "205--220",
 doi          = "10.1007/978-3-642-12002-2\_17",
)
@article(fogarty-vardi-2012,
 author       = "S. Fogarty and M. Y. Vardi",
 year         = "2012",
 title        = "{B}{\"u}chi Complementation and Size-Change Termination",
 journal      = "Logical Methods in Computer Science",
 volume       = "8",
 number       = "1",
 doi          = "10.2168/LMCS-8(1:13)2012",
)
@inproceedings(fairsimmini,
 author       = "S. Gurumurthy and R. Bloem and F. Somenzi",
 year         = "2002",
 title        = "Fair simulation minimization",
 booktitle    = "Proc.\ 14th Int.\ Conf.\ on Computer-Aided Verification, {CAV'02}",
 series       = "LNCS",
 volume       = "2404",
 publisher    = "Springer",
 pages        = "610--624",
 doi          = "10.1007/3-540-45657-0\_51",
)
@article(HenzingerKR02,
 author       = "T. A. Henzinger and O. Kupferman and S. K. Rajamani",
 year         = "2002",
 title        = "Fair Simulation",
 journal      = "Inf. Comput.",
 volume       = "173",
 number       = "1",
 pages        = "64--81",
 doi          = "10.1006/inco.2001.3085",
)
@article(DBLP:journals/corr/abs-1209-0800,
 author       = "M. Holtmann and L. Kaiser and W. Thomas",
 year         = "2012",
 title        = "Degrees of Lookahead in Regular Infinite Games",
 journal      = "Logical Methods in Computer Science",
 volume       = "8",
 number       = "3",
 doi          = "10.2168/LMCS-8(3:24)2012",
)
@book(spin-book,
 author       = "Gerard J. Holzmann",
 year         = "2004",
 title        = "The SPIN Model Checker - primer and reference manual",
 publisher    = "Addison-Wesley",
)
@inproceedings(HutagalungLL13,
 author       = "M. Hutagalung and M. Lange and {\'E}. Lozes",
 year         = "2013",
 title        = "Revealing vs. Concealing: More Simulation Games for {B}{\"u}chi Inclusion",
 booktitle    = "Proc.\ 7th Int.\ Conf.\ on Language and Automata Theory and Applications, {LATA'13}",
 series       = "LNCS",
 publisher    = "Springer",
 pages        = "347--358",
 doi          = "10.1007/978-3-642-37064-9\_31",
)
@article(KupfermanV01,
 author       = "O. Kupferman and M. Y. Vardi",
 year         = "2001",
 title        = "Weak Alternating Automata Are Not That Weak",
 journal      = "ACM Trans.\ on Comput.\ Logic",
 volume       = "2",
 number       = "3",
 pages        = "408--429",
 doi          = "10.1145/377978.377993",
)
@inproceedings(size-change-termination,
 author       = "C. S. Lee and N. D. Jones and A. M. Ben-Amram",
 year         = "2001",
 title        = "The size-change principle for program termination",
 booktitle    = "Proc.\ 28th Symp.\ on Principles of Programming Languages, {POPL'01}",
 publisher    = "ACM",
 pages        = "81--92",
 doi          = "10.1145/360204.360210",
)
@inproceedings(STOC73*1,
 author       = "A. R. Meyer and L. J. Stockmeyer",
 year         = "1973",
 title        = "Word problems requiring exponential time",
 booktitle    = "Proc.\ 5th Symp.\ on Theory of Computing, {STOC'73}",
 publisher    = "ACM",
 address      = "New York",
 pages        = "1--9",
 doi          = "10.1145/800125.804029",
)
@article(Ramsey:30,
 author       = "F. P. Ramsey",
 year         = "1930",
 title        = "On a problem in formal logic",
 journal      = "Proc.\ London Math.\ Soc.\ (3)",
 volume       = "30",
 pages        = "264--286",
 doi          = "10.1007/978-0-8176-4842-8\_1",
)
@inproceedings(FOCS88*319,
 author       = "S. Safra",
 year         = "1988",
 title        = "On the complexity of $\omega $-automata",
 booktitle    = "Proc.\ 29th Symp.\ on Foundations of Computer Science, {FOCS'88}",
 publisher    = "IEEE",
 pages        = "319--327",
 doi          = "10.1109/SFCS.1988.21948",
)
@article(Savitch70,
 author       = "W. J. Savitch",
 year         = "1970",
 title        = "Relationships between nondeterministic and deterministic tape complexities",
 journal      = "Journal of Computer and System Sciences",
 volume       = "4",
 pages        = "177--192",
 doi          = "10.1016/S0022-0000(70)80006-X",
)
@incollection(thomas-salomaa,
 author       = "W. Thomas",
 year         = "1999",
 title        = "Complementation of {B{\"u}}chi automata revisited",
 editor       = "J. Karhum{{\"a}}ki et al.",
 booktitle    = "Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa",
 publisher    = "Springer",
 pages        = "109--122",
 doi          = "10.1007/978-3-642-60207-8\_10",
)
@inbook(Vardi96,
 author       = "M. Y. Vardi",
 year         = "1996",
 title        = "An Automata-Theoretic Approach to Linear Temporal Logic",
 pages        = "238--266",
 series       = "LNCS",
 volume       = "1043",
 publisher    = "Springer",
 address      = "New York, NY, USA",
 doi          = "10.1007/3-540-60915-6\_6",
)