@inproceedings(DBLP:conf/cav/AbdullaCCHHMV10,
 author       = {Parosh Aziz Abdulla and Yu{-}Fang Chen and Lorenzo Clemente and Hol{\'{\i}}k, Luk{\'{a}}s and Chih{-}Duo Hong and Richard Mayr and Tom{\'{a}}s Vojnar},
 year         = {2010},
 title        = {Simulation Subsumption in {Ramsey}-Based {B\"uchi} Automata Universality and Inclusion Testing},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {6174},
 publisher    = {Springer},
 pages        = {132--147},
 doi          = {10.1007/978-3-642-14295-6\_14},
)
@inproceedings(DBLP:conf/concur/AbdullaCCHHMV11,
 author       = {Parosh Aziz Abdulla and Yu{-}Fang Chen and Lorenzo Clemente and Hol{\'{\i}}k, Luk{\'{a}}s and Chih{-}Duo Hong and Richard Mayr and Tom{\'{a}}s Vojnar},
 year         = {2011},
 title        = {Advanced {Ramsey}-Based {B\"uchi} Automata Inclusion Testing},
 booktitle    = {CONCUR},
 series       = {LNCS},
 volume       = {6901},
 publisher    = {Springer},
 pages        = {187--202},
 doi          = {10.1007/978-3-642-23217-6\_13},
)
@book(baier2008principles,
 author       = {Christel Baier and Joost-Pieter Katoen},
 year         = {2008},
 title        = {Principles of model checking},
 publisher    = {MIT press},
)
@inproceedings(baier2016markov,
 author       = {Christel Baier and Stefan Kiefer and Joachim Klein and Sascha Kl{\"u}ppelholz and David M{\"u}ller and James Worrell},
 year         = {2016},
 title        = {Markov chains and unambiguous {B{\"u}chi} automata},
 booktitle    = {CAV},
 organization = {Springer},
 pages        = {23--42},
 doi          = {10.1007/978-3-319-41528-4\_2},
)
@inproceedings(Blahoudek16,
 author       = {Franti\v{s}ek Blahoudek and Matthias Heizmann and Sven Schewe and Strej\v{c}ek, Jan and Ming-Hsien Tsai},
 year         = {2016},
 title        = {Complementing Semi-deterministic {B\"{u}chi} Automata},
 booktitle    = {TACAS},
 series       = {LNCS},
 volume       = {9636},
 pages        = {770--787},
 doi          = {10.1007/978-3-662-49674-9\_49},
)
@inproceedings(bousquet2010equivalence,
 author       = {Nicolas Bousquet and Christof L{\"o}ding},
 year         = {2010},
 title        = {Equivalence and inclusion problem for strongly unambiguous {B{\"u}chi} automata},
 booktitle    = {LATA},
 organization = {Springer},
 pages        = {118--129},
 doi          = {10.1007/978-3-642-13089-2\_10},
)
@incollection(buchi90decision,
 author       = {J Richard B{\"u}chi},
 year         = {1990},
 title        = {On a decision method in restricted second order arithmetic},
 booktitle    = {The Collected Works of J. Richard B{\"u}chi},
 publisher    = {Springer},
 pages        = {425--435},
 doi          = {10.1007/978-1-4613-8928-6_23},
)
@inproceedings(BustanRV04,
 author       = {D. Bustan and S. Rubin and M.Y. Vardi},
 year         = {2004},
 title        = {Verifying omega-Regular Properties of {Markov Chains}},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {3114},
 publisher    = {Springer},
 pages        = {189--201},
 doi          = {10.1007/978-3-540-27813-9\_15},
)
@article(carton2003unambiguous,
 author       = {Olivier Carton and Max Michel},
 year         = {2003},
 title        = {Unambiguous {B{\"u}chi} automata},
 journal      = {Theoretical Computer Science},
 volume       = {297},
 number       = {1-3},
 pages        = {37--81},
 doi          = {10.1016/S0304-3975(02)00618-7},
)
@inproceedings(DBLP:conf/pldi/ChenHLLTTZ18,
 author       = {Yu{-}Fang Chen and Matthias Heizmann and Ondrej Leng{\'{a}}l and Yong Li and Ming{-}Hsien Tsai and Andrea Turrini and Lijun Zhang},
 year         = {2018},
 title        = {Advanced automata-based algorithms for program termination checking},
 booktitle    = {PLDI},
 pages        = {135--150},
 doi          = {10.1145/3192366.3192405},
)
@article(DBLP:journals/lmcs/ClementeM19,
 author       = {Lorenzo Clemente and Richard Mayr},
 year         = {2019},
 title        = {Efficient reduction of nondeterministic automata with application to language inclusion testing},
 journal      = {Logical Methods in Computer Science},
 volume       = {15},
 number       = {1},
 doi          = {10.23638/LMCS-15(1:12)2019},
)
@article(CourcoubetisY95,
 author       = {C. Courcoubetis and M. Yannakakis},
 year         = {1995},
 title        = {The Complexity of Probabilistic Verification},
 journal      = {J. {ACM}},
 volume       = {42},
 number       = {4},
 pages        = {857--907},
 doi          = {10.1145/210332.210339},
)
@article(DBLP:journals/corr/abs-0902-3958,
 author       = {Laurent Doyen and Jean{-}Fran{\c{c}}ois 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},
)
@article(DBLP:journals/corr/abs-1110-6183,
 author       = {Seth Fogarty and Moshe 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(DBLP:conf/cav/HeizmannHP14,
 author       = {Matthias Heizmann and Jochen Hoenicke and Andreas Podelski},
 year         = {2014},
 title        = {Termination Analysis by Learning Terminating Programs},
 booktitle    = {CAV},
 pages        = {797--813},
 doi          = {10.1007/978-3-319-08867-9\_53},
)
@inproceedings(kahler2008complementation,
 author       = {Detlef K{\"a}hler and Thomas Wilke},
 year         = {2008},
 title        = {Complementation, disambiguation, and determinization of {B{\"u}chi} automata unified},
 booktitle    = {ICALP},
 organization = {Springer},
 pages        = {724--735},
 doi          = {10.1007/978-3-540-70575-8\_59},
)
@inproceedings(DBLP:conf/cav/KupfermanV96a,
 author       = {Orna Kupferman and Moshe Y. Vardi},
 year         = {1996},
 title        = {Verification of Fair Transisiton Systems},
 editor       = {Rajeev Alur and Thomas A. Henzinger},
 booktitle    = {CAV},
 series       = {LNCS},
 volume       = {1102},
 publisher    = {Springer},
 pages        = {372--382},
 doi          = {10.1007/3-540-61474-5\_84},
)
@article(kupferman2001weak,
 author       = {Orna Kupferman and Moshe Y Vardi},
 year         = {2001},
 title        = {Weak alternating automata are not that weak},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {2},
 number       = {3},
 pages        = {408--429},
 doi          = {10.1145/377978.377993},
)
@article(DBLP:journals/jcss/Kurshan87,
 author       = {Robert P. Kurshan},
 year         = {1987},
 title        = {Complementing Deterministic B{\"{u}}chi Automata in Polynomial Time},
 journal      = {J. Comput. Syst. Sci.},
 volume       = {35},
 number       = {1},
 pages        = {59--71},
 doi          = {10.1016/0022-0000(87)90036-5},
)
@inproceedings(DBLP:conf/setta/LiLTHZ16,
 author       = {Yong Li and Wanwei Liu and Andrea Turrini and Ernst Moritz Hahn and Lijun Zhang},
 year         = {2016},
 title        = {An Efficient Synthesis Algorithm for Parametric {Markov Chains} Against Linear Time Properties},
 booktitle    = {{SETTA}},
 pages        = {280--296},
 doi          = {10.1007/978-3-319-47677-3\_18},
)
@inproceedings(LodingP18,
 author       = {Christof L{\"{o}}ding and Anton Pirogov},
 year         = {2018},
 title        = {On Finitely Ambiguous {B{\"{u}}chi} Automata},
 booktitle    = {DLT},
 pages        = {503--515},
 doi          = {10.1007/978-3-319-98654-8\_41},
)
@article(miyano1984alternating,
 author       = {Satoru Miyano and Takeshi Hayashi},
 year         = {1984},
 title        = {Alternating finite automata on $\omega$-words},
 journal      = {Theoretical Computer Science},
 volume       = {32},
 number       = {3},
 pages        = {321--330},
 doi          = {10.1016/0304-3975(84)90049-5},
)
@inproceedings(rabinovich18,
 author       = {Alexander Rabinovich},
 year         = {2018},
 title        = {Complementation of Finitely Ambiguous {B{\"u}chi} Automata},
 booktitle    = {DLT},
 organization = {Springer},
 pages        = {541--552},
 doi          = {10.1007/978-3-319-98654-8\_44},
)
@inproceedings(safra1988complexity,
 author       = {Shmuel Safra},
 year         = {1988},
 title        = {On the complexity of $\omega$-automata},
 booktitle    = {FOCS},
 organization = {IEEE},
 pages        = {319--327},
 doi          = {10.1109/SFCS.1988.21948},
)
@inproceedings(Schewe09,
 author       = {S. Schewe},
 year         = {2009},
 title        = {B{\"{u}}chi Complementation Made Tight},
 booktitle    = {STACS},
 series       = {LIPIcs},
 volume       = {3},
 publisher    = {Schloss Dagstuhl, Germany},
 pages        = {661--672},
 doi          = {10.4230/LIPIcs.STACS.2009.1854},
)
@article(sistla1987complementation,
 author       = {A Prasad Sistla and Moshe Y Vardi and Pierre Wolper},
 year         = {1987},
 title        = {The complementation problem for {B{\"u}chi} automata with applications to temporal logic},
 journal      = {Theoretical Computer Science},
 volume       = {49},
 number       = {2-3},
 pages        = {217--237},
 doi          = {10.1016/0304-3975(87)90008-9},
)
@article(TsaiFVT14,
 author       = {M.{-}H. Tsai and S. Fogarty and M.Y. Vardi and Y.{-}K. Tsay},
 year         = {2014},
 title        = {State of {B{\"{u}}chi} Complementation},
 journal      = {Logical Methods in Computer Science},
 volume       = {10},
 number       = {4},
 doi          = {10.2168/LMCS-10(4:13)2014},
)
@inproceedings(DBLP:conf/birthday/VardiW08,
 author       = {Moshe Y. Vardi and Thomas Wilke},
 year         = {2008},
 title        = {Automata: from logics to algorithms},
 booktitle    = {Logic and Automata: History and Perspectives},
 pages        = {629--736},
)
@inproceedings(DBLP:conf/lics/VardiW86,
 author       = {Moshe Y. Vardi and Pierre Wolper},
 year         = {1986},
 title        = {An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)},
 booktitle    = {LICS},
 publisher    = {{IEEE}},
 pages        = {332--344},
)
@article(Yan/08/lowerComplexity,
 author       = {Qiqi Yan},
 year         = {2008},
 title        = {Lower Bounds for Complementation of $\omega$-Automata Via the Full Automata Technique},
 journal      = {Logical Methods in Computer Science},
 volume       = {4},
 number       = {1:5},
 doi          = {10.2168/LMCS-4(1:5)2008},
)