@article(AlTo04,
 author       = "R. Alur and S. {La Torre}",
 year         = "2004",
 title        = "Deterministic Generators and Games for {LTL} Fragments",
 journal      = "ACM Transactions on Computational Logic (TOCL)",
 volume       = "5",
 number       = "1",
 pages        = "1--15",
 doi          = "10.1145/963927.963928",
)
@inproceedings(BCGH10,
 author       = "R. Bloem and K. Chatterjee and K. Greimel and T.A. Henzinger and B. Jobstmann",
 year         = "2010",
 title        = "Robustness in the Presence of Liveness",
 editor       = "T. Touili and B. Cook and P. Jackson",
 booktitle    = "Computer Aided Verification (CAV)",
 series       = "LNCS",
 volume       = "6174",
 publisher    = "Springer",
 address      = "Edinburgh, UK",
 pages        = "410--424",
 doi          = "10.1007/978-3-642-14295-6\_36",
)
@inproceedings(BCGH10a,
 author       = "R. Bloem and A. Cimatti and K. Greimel and G. Hofferek and R. K\IeC {\"o}nighofer and M. Roveri and V. Schuppan and R. Seeber",
 year         = "2010",
 title        = "{RATSY} - A New Requirements Analysis Tool with Synthesis",
 editor       = "T. Touili and B. Cook and P. Jackson",
 booktitle    = "Computer Aided Verification (CAV)",
 series       = "LNCS",
 volume       = "6174",
 publisher    = "Springer",
 address      = "Edinburgh, UK",
 pages        = "425--429",
 doi          = "10.1007/978-3-642-14295-6",
)
@inproceedings(BGJP07,
 author       = "R. Bloem and S. Galler and B. Jobstmann and N. Piterman and A. Pnueli and M. Weiglhofer",
 year         = "2007",
 title        = "Automatic hardware synthesis from specifications: a case study",
 editor       = "R. Lauwereins and J. Madsen",
 booktitle    = "Design, Automation and Test in Europe (DATE)",
 publisher    = "IEEE Computer Society",
 address      = "Nice, France",
 pages        = "1188--1193",
)
@article(BGJP07a,
 author       = "R. Bloem and S. Galler and B. Jobstmann and N. Piterman and A. Pnueli and M. Weiglhofer",
 year         = "2007",
 title        = "Specify, Compile, Run: Hardware from {PSL}",
 journal      = "Electronic Notes in Theoretical Computer Science (ENTCS)",
 volume       = "190",
 pages        = "3--16",
 doi          = "10.1016/j.entcs.2007.09.004",
)
@inproceedings(BoKu09a,
 author       = "U. Boker and O. Kupferman",
 year         = "2009",
 title        = "Co-ing {B\IeC {\"u}chi} Made Tight and Useful",
 booktitle    = "Logic in Computer Science (LICS)",
 publisher    = "IEEE Computer Society",
 address      = "Los Angeles, California, USA",
 pages        = "245--254",
 doi          = "10.1109/LICS.2009.32",
)
@inproceedings(BCMD90,
 author       = "J.R. Burch and E.M. Clarke and K.L. McMillan and D.L. Dill and L.J. Hwang",
 year         = "1990",
 title        = "Symbolic Model Checking: $10^{20}$ States and Beyond",
 booktitle    = "Logic in Computer Science (LICS)",
 publisher    = "IEEE Computer Society",
 address      = "Washington, DC, USA",
 pages        = "1--33",
 doi          = "10.1109/LICS.1990.113767",
)
@inproceedings(ChMP92,
 author       = "E.Y. Chang and Z. Manna and A. Pnueli",
 year         = "1992",
 title        = "Characterization of Temporal Property Classes",
 editor       = "W. Kuich",
 booktitle    = "International Colloquium on Automata, Languages and Programming (ICALP)",
 series       = "LNCS",
 volume       = "623",
 publisher    = "Springer",
 address      = "Vienna, Austria",
 pages        = "474--486",
)
@incollection(Emer90,
 author       = "E.A. Emerson",
 year         = "1990",
 title        = "Temporal and Modal Logic",
 editor       = "J. {van Leeuwen}",
 booktitle    = "Handbook of Theoretical Computer Science",
 chapter      = "16",
 volume       = "B: Formal Models and Semantics",
 publisher    = "Elsevier",
 pages        = "995--1072",
)
@phdthesis(Frit05b,
 author       = "C. Fritz",
 year         = "2005",
 title        = "Simulation-Based Simplification of omega-Automata",
 school       = "Technischen Fakult\IeC {\"a}t der Christian-Albrechts-Universit\IeC {\"a}t zu Kiel, Germany",
)
@inproceedings(JGWB07,
 author       = "B. Jobstmann and S. Galler and M. Weiglhofer and R. Bloem",
 year         = "2007",
 title        = "{Anzu}: A Tool for Property Synthesis",
 editor       = "W. Damm and H. Hermanns",
 booktitle    = "Computer Aided Verification (CAV)",
 series       = "LNCS",
 volume       = "4590",
 publisher    = "Springer",
 address      = "Berlin, Germany",
 pages        = "258--262",
 doi          = "10.1007/978-3-540-73368-3\_29",
)
@inproceedings(KuVa98c,
 author       = "O. Kupferman and M.Y. Vardi",
 year         = "1998",
 title        = "Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time",
 booktitle    = "Logic in Computer Science (LICS)",
 publisher    = "IEEE Computer Society",
 address      = "Indianapolis, Indiana, USA",
 pages        = "81--92",
 doi          = "10.1109/LICS.1998.705645",
)
@inproceedings(KoHB09,
 author       = "R. K\IeC {\"o}nighofer and G. Hofferek and R. Bloem",
 year         = "2009",
 title        = "Debugging formal specifications using simple counterstrategies",
 booktitle    = "Formal Methods in Computer-Aided Design (FMCAD)",
 publisher    = "IEEE Computer Society",
 address      = "Austin, Texas, USA",
 pages        = "152--159",
 doi          = "10.1109/FMCAD.2009.5351127",
)
@inproceedings(Maid00,
 author       = "M. Maidl",
 year         = "2000",
 title        = "The Common Fragment of {CTL} and {LTL}",
 booktitle    = "Foundations of Computer Science (FOCS)",
 pages        = "643--652",
)
@inproceedings(MaPn87c,
 author       = "Z. Manna and A. Pnueli",
 year         = "1987",
 title        = "A Hierarchy of Temporal Properties",
 booktitle    = "Principles of Distributed Computing (PODC)",
 pages        = "205",
 doi          = "10.1145/41840.41857",
)
@inproceedings(MaPn90,
 author       = "Z. Manna and A. Pnueli",
 year         = "1990",
 title        = "A hierarchy of temporal properties",
 booktitle    = "Principles of Distributed Computing (PODC)",
 publisher    = "ACM",
 address      = "Quebec City, Quebec, Canada",
 pages        = "377--408",
)
@article(MaPn91,
 author       = "Z. Manna and A. Pnueli",
 year         = "1991",
 title        = "Completing the temporal picture",
 journal      = "Theoretical Computer Science (TCS)",
 volume       = "83",
 number       = "1",
 pages        = "97--130",
 doi          = "10.1016/0304-3975(91)90041-Y",
)
@article(MiHa84,
 author       = "S. Miyano and T. Hayashi",
 year         = "1984",
 title        = "Alternating automata on $\omega $-words",
 journal      = "Theoretical Computer Science (TCS)",
 volume       = "32",
 pages        = "321--330",
 doi          = "10.1016/0304-3975(84)90049-5",
)
@inproceedings(MoSL08,
 author       = "A. Morgenstern and K. Schneider and S. Lamberti",
 year         = "2008",
 title        = "Generating Deterministic $\omega $-Automata for most {LTL} Formulas by the Breakpoint Construction",
 editor       = "C. Scholl and S. Disch",
 booktitle    = "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)",
 publisher    = "Shaker",
 address      = "Freiburg, Germany",
 pages        = "119--128",
)
@inproceedings(PiPS06,
 author       = "N. Piterman and A. Pnueli and Y. {Sa\IeC {\textquoteright }ar}",
 year         = "2006",
 title        = "Synthesis of Reactive(1) Designs",
 editor       = "E.A. Emerson and K.S. Namjoshi",
 booktitle    = "Verification, Model Checking, and Abstract Interpretation (VMCAI)",
 series       = "LNCS",
 volume       = "3855",
 publisher    = "Springer",
 address      = "Charleston, South Carolina, USA",
 pages        = "364--380",
 doi          = "10.1007/11609773\_24",
)
@inproceedings(Pnue77a,
 author       = "A. Pnueli",
 year         = "1977",
 title        = "The Temporal Logic of Programs",
 booktitle    = "Foundations of Computer Science (FOCS)",
 publisher    = "IEEE Computer Society",
 address      = "Providence, Rhode Island, USA",
 pages        = "46--57",
 doi          = "10.1109/SFCS.1977.32",
)
@inproceedings(Schn01b,
 author       = "K. Schneider",
 year         = "2001",
 title        = "Improving Automata Generation for Linear Temporal Logic by Considering the Automata Hierarchy",
 editor       = "R. Nieuwenhuis and A. Voronkov",
 booktitle    = "Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)",
 series       = "LNAI",
 volume       = "2250",
 publisher    = "Springer",
 address      = "Havana, Cuba",
 pages        = "39--54",
 doi          = "10.1007/3-540-45653-8\_3",
)
@book(Schn03,
 author       = "K. Schneider",
 year         = "2003",
 title        = "Verification of Reactive Systems - Formal Methods and Algorithms",
 series       = "Texts in Theoretical Computer Science (EATCS Series)",
 publisher    = "Springer",
)
@techreport(Schn09,
 author       = "K. Schneider",
 year         = "2009",
 title        = "The Synchronous Programming Language {Quartz}",
 type         = "Internal Report",
 number       = "375",
 institution  = "Department of Computer Science, University of Kaiserslautern",
 address      = "Kaiserslautern, Germany",
)
@incollection(Thom90a,
 author       = "W. Thomas",
 year         = "1990",
 title        = "Automata on Infinite Objects",
 editor       = "J. {van Leeuwen}",
 booktitle    = "Handbook of Theoretical Computer Science",
 chapter      = "4",
 volume       = "B: Formal Models and Semantics",
 publisher    = "Elsevier",
 pages        = "133--191",
)
@article(Wagn79,
 author       = "K. Wagner",
 year         = "1979",
 title        = "On $\omega $-regular sets",
 journal      = "Information and Control",
 volume       = "43",
 number       = "2",
 pages        = "123--177",
)
@inproceedings(WaHT03,
 author       = "N. Wallmeier and P. H\IeC {\"u}tten and W. Thomas",
 year         = "2003",
 title        = "Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications",
 editor       = "O.H. Ibarra and Z. Dang",
 booktitle    = "Conference on Implementation and Application of Automata (CIAA)",
 series       = "LNCS",
 volume       = "2759",
 publisher    = "Springer",
 address      = "Santa Barbara, California, USA",
 pages        = "11--22",
 doi          = "10.1007/3-540-45089-0\_3",
)
@inproceedings(WoTM10,
 author       = "T. Wongpiromsarn and U. Topcu and R.M. Murray",
 year         = "2010",
 title        = "Receding horizon control for temporal logic specifications",
 editor       = "K.H. Johansson and W. Yi",
 booktitle    = "Hybrid Systems: Computation and Control (HSCC)",
 publisher    = "ACM",
 address      = "Stockholm, Sweden",
 pages        = "101--110",
 doi          = "10.1145/1755952.1755968",
)