@article(DBLP:journals/ipl/AlpernS85,
 author       = "Bowen Alpern and Fred B. Schneider",
 year         = "1985",
 title        = "Defining Liveness",
 journal      = "Inf. Process. Lett.",
 volume       = "21",
 number       = "4",
 pages        = "181--185",
 doi          = "10.1016/0020-0190(85)90056-0",
)
@article(DBLP:journals/fmsd/BeerBER01,
 author       = "Ilan Beer and Shoham Ben-David and Cindy Eisner and Yoav Rodeh",
 year         = "2001",
 title        = "Efficient Detection of Vacuity in Temporal Model Checking",
 journal      = "Formal Methods in System Design",
 volume       = "18",
 number       = "2",
 pages        = "141--163",
 doi          = "10.1023/A:1008779610539",
)
@inproceedings(DBLP:conf/lata/Ehlers10,
 author       = "R{\"u}diger Ehlers",
 year         = "2010",
 title        = "Short Witnesses and Accepting Lassos in $\omega $-Automata",
 editor       = "Adrian Horia Dediu and Henning Fernau and Carlos Mart\'{\i }n-Vide",
 booktitle    = "LATA",
 series       = "LNCS",
 volume       = "6031",
 publisher    = "Springer",
 pages        = "261--272",
 doi          = "10.1007/978-3-642-13089-2_22",
)
@inproceedings(DBLP:conf/lics/FinkbeinerS05,
 author       = "Bernd Finkbeiner and Sven Schewe",
 year         = "2005",
 title        = "Uniform Distributed Synthesis",
 booktitle    = "LICS",
 publisher    = "IEEE Computer Society",
 pages        = "321--330",
 doi          = "10.1109/LICS.2005.53",
)
@article(DBLP:journals/fmsd/FinkbeinerS04,
 author       = "Bernd Finkbeiner and Henny Sipma",
 year         = "2004",
 title        = "Checking Finite Traces Using Alternating Automata",
 journal      = "Formal Methods in System Design",
 volume       = "24",
 number       = "2",
 pages        = "101--127",
 doi          = "10.1023/B:FORM.0000017718.28096.48",
)
@inproceedings(DBLP:conf/icalp/GreimelBJV08,
 author       = "Karin Greimel and Roderick Bloem and Barbara Jobstmann and Moshe Y. Vardi",
 year         = "2008",
 title        = "Open Implication",
 editor       = "Luca Aceto and Ivan Damg{\r a}rd and Leslie Ann Goldberg and Magn{\'u}s M. Halld{\'o}rsson and Anna Ing{\'o}lfsd{\'o}ttir and Igor Walukiewicz",
 booktitle    = "ICALP (2)",
 series       = "LNCS",
 volume       = "5126",
 publisher    = "Springer",
 pages        = "361--372",
 doi          = "10.1007/978-3-540-70583-3_30",
)
@inproceedings(DBLP:conf/stacs/Jurdzinski00,
 author       = "Marcin Jurdzinski",
 year         = "2000",
 title        = "Small Progress Measures for Solving Parity Games",
 editor       = "Horst Reichel and Sophie Tison",
 booktitle    = "STACS",
 series       = "LNCS",
 volume       = "1770",
 publisher    = "Springer",
 pages        = "290--301",
)
@inproceedings(KV97c,
 author       = "O. Kupferman and M.Y. Vardi",
 year         = "1997",
 title        = "Synthesis with Incomplete Informatio",
 booktitle    = "2nd International Conference on Temporal Logic",
 address      = "Manchester",
 pages        = "91--106",
)
@article(DBLP:journals/fmsd/KupfermanV01,
 author       = "Orna Kupferman and Moshe Y. Vardi",
 year         = "2001",
 title        = "Model Checking of Safety Properties",
 journal      = "Formal Methods in System Design",
 volume       = "19",
 number       = "3",
 pages        = "291--314",
 doi          = "10.1023/A:1011254632723",
)
@article(Lamport/77/proving,
 author       = "Leslie Lamport",
 year         = "1977",
 title        = "Proving the Correctness of Multiprocess Programs",
 journal      = "IEEE Trans. Software Eng.",
 volume       = "3",
 number       = "2",
 pages        = "125--143",
 doi          = "10.1109/TSE.1977.229904",
)
@inproceedings(Manna+Pnueli/89/Completing,
 author       = "Zohar Manna and Amir Pnueli",
 year         = "1989",
 title        = "Completing the Temporal Picture",
 editor       = "G. Ausiello and M. {Dezani-Ciancaglini} and S. Ronchi Della Rocca",
 booktitle    = "ICALP",
 series       = "LNCS",
 volume       = "372",
 publisher    = "Springer",
 pages        = "534--558",
 note         = "Also in Theoretical Computer Science",
)
@inproceedings(DBLP:conf/lics/ManoliosT01,
 author       = "Panagiotis Manolios and Richard J. Trefler",
 year         = "2001",
 title        = "Safety and Liveness in Branching Time",
 booktitle    = "LICS",
 pages        = "366--374",
)
@inproceedings(DBLP:conf/podc/ManoliosT03,
 author       = "Panagiotis Manolios and Richard J. Trefler",
 year         = "2003",
 title        = "A lattice-theoretic characterization of safety and liveness",
 booktitle    = "PODC",
 pages        = "325--333",
 doi          = "10.1145/872035.872083",
)
@article(Muller+Schupp/87/Dual,
 author       = "David E. Muller and Paul E. Schupp",
 year         = "1987",
 title        = "Alternating automata on infinite trees",
 journal      = "Theor. Comput. Sci.",
 volume       = "54",
 number       = "2-3",
 pages        = "267--276",
 doi          = "10.1016/0304-3975(87)90133-2",
)
@article(Muller+Schupp/95/Alternating,
 author       = "David E. Muller and Paul E. Schupp",
 year         = "1995",
 title        = "Simulating alternating tree automata by nondeterministic automata: new results and new proofs of the theorems of {R}abin, {M}c{N}aughton and {S}afra",
 journal      = "Theor. Comput. Sci.",
 volume       = "141",
 number       = "1-2",
 pages        = "69--107",
 doi          = "10.1016/0304-3975(94)00214-4",
)
@book(Mueller2000,
 author       = "Silvia M. M{\"u}ller and Wolfgang J. Paul",
 year         = "2000",
 title        = "Computer Architecture: Complexity and Correctness",
 publisher    = "Springer",
)
@article(DBLP:journals/lmcs/Piterman07,
 author       = "Nir Piterman",
 year         = "2007",
 title        = "From Nondeterministic {B}{\"u}chi and {S}treett Automata to Deterministic Parity Automata",
 journal      = "Logical Methods in Computer Science",
 volume       = "3",
 number       = "3",
 doi          = "10.2168/LMCS-3(3:5)2007",
)
@inproceedings(DBLP:conf/focs/Pnueli77,
 author       = "Amir Pnueli",
 year         = "1977",
 title        = "The Temporal Logic of Programs",
 booktitle    = "FOCS",
 publisher    = "IEEE",
 pages        = "46--57",
)
@inproceedings(DBLP:conf/popl/PnueliR89,
 author       = "Amir Pnueli and Roni Rosner",
 year         = "1989",
 title        = "On the Synthesis of a Reactive Module",
 booktitle    = "POPL",
 pages        = "179--190",
 doi          = "10.1145/75277.75293",
)
@article(DBLP:journals/entcs/PnueliZZ06,
 author       = "Amir Pnueli and Aleksandr Zaks and Lenore D. Zuck",
 year         = "2006",
 title        = "Monitoring Interfaces for Faults",
 journal      = "Electr. Notes Theor. Comput. Sci.",
 volume       = "144",
 number       = "4",
 pages        = "73--89",
 doi          = "10.1016/j.entcs.2006.02.005",
)
@inproceedings(DBLP:conf/fmcad/SohailS09,
 author       = "Saqib Sohail and Fabio Somenzi",
 year         = "2009",
 title        = "Safety First: A Two-stage Algorithm for {LTL} Games",
 booktitle    = "FMCAD",
 publisher    = "IEEE",
 pages        = "77--84",
 doi          = "10.1109/FMCAD.2009.5351138",
)
@inproceedings(DBLP:conf/birthday/Thomas08,
 author       = "Wolfgang Thomas",
 year         = "2008",
 title        = "Church's Problem and a Tour through Automata Theory",
 editor       = "Arnon Avron and Nachum Dershowitz and Alexander Rabinovich",
 booktitle    = "Pillars of Computer Science",
 series       = "LNCS",
 volume       = "4800",
 publisher    = "Springer",
 pages        = "635--655",
 doi          = "10.1007/978-3-540-78127-1_35",
)
@inproceedings(Vardi1996,
 author       = "Moshe Y. Vardi",
 year         = "1996",
 title        = "An Automata-theoretic Approach to Linear Temporal Logic",
 booktitle    = "Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency: structure versus automata",
 publisher    = "Springer",
 pages        = "238--266",
)
@incollection(VardiWilke-2007,
 author       = "Moshe Y. Vardi and Thomas Wilke",
 year         = "2007",
 title        = "Automata: from logics to algorithms",
 editor       = "J\"org Flum and Erich Gr\"adel and Thomas Wilke",
 booktitle    = "Logic and Automata: History and Perspectives",
 series       = "Texts in Logic and Games",
 volume       = "2",
 publisher    = "Amsterdam University Press",
 address      = "Amsterdam",
 pages        = "629--736",
)
@article(Vardi94reasoningabout,
 author       = "Moshe Y. Vardi and Pierre Wolper",
 year         = "1994",
 title        = "Reasoning about Infinite Computations",
 journal      = "Information and Computation",
 volume       = "115",
 pages        = "1--37",
 doi          = "10.1006/inco.1994.1092",
)