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