@techreport(Andersen97anintroduction,
 author       = {Henrik Reif Andersen},
 year         = {1997},
 title        = {An introduction to binary decision diagrams},
 type         = {Technical Report},
 institution  = {Course Notes on the WWW},
)
@book(ag11,
 author       = {Krzysztof R. Apt and Erich Gr\"{a}del},
 year         = {2011},
 title        = {Lectures in game theory for computer scientists},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511973468},
)
@article(BloemJPPS-jcss12,
 author       = {Roderick Bloem and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Yaniv Sa'ar},
 year         = {2012},
 title        = {Synthesis of Reactive(1) designs},
 journal      = {Journal of Computer and System Sciences},
 volume       = {78},
 number       = {3},
 pages        = {911 -- 938},
 doi          = {10.1016/j.jcss.2011.08.007},
 url          = {http://www.sciencedirect.com/science/article/pii/S0022000011000869},
 note         = {In Commemoration of Amir Pnueli},
)
@inproceedings(bprs14,
 author       = {Romain Brenguier and Guillermo A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Ocan Sankur},
 year         = {2014},
 title        = {{A}bs{S}ynthe: abstract synthesis from succinct safety specifications},
 booktitle    = {Proceedings 3rd Workshop on Synthesis, {SYNT} 2014, Vienna, Austria, July 23-24, 2014.},
 pages        = {100--116},
 doi          = {10.4204/EPTCS.157.11},
)
@article(bryant86,
 author       = {Randal E. Bryant},
 year         = {1986},
 title        = {Graph-based algorithms for boolean function manipulation},
 journal      = {Computers, IEEE Transactions on},
 volume       = {100},
 number       = {8},
 pages        = {677--691},
 doi          = {10.1109/TC.1986.1676819},
)
@article(burch1991symbolic,
 author       = {Jerry Burch and Edmund M Clarke and David Long},
 year         = {1991},
 title        = {Symbolic model checking with partitioned transition relations},
 journal      = {Computer Science Department},
 pages        = {435},
)
@book(cgp01,
 author       = {Edmund M. Clarke and Orna Grumberg and Doron Peled},
 year         = {2001},
 title        = {Model checking},
 publisher    = {{MIT} Press},
 doi          = {10.1016/B978-044450813-3/50026-6},
)
@inproceedings(ej91,
 author       = {E. Allen Emerson and Charanjit S. Jutla},
 year         = {1991},
 title        = {Tree automata, mu-calculus and determinacy},
 booktitle    = {FOCS},
 organization = {IEEE},
 pages        = {368--377},
 doi          = {10.1109/SFCS.1991.185392},
)
@inproceedings(FiliotJR10,
 author       = {Emmanuel Filiot and Naiyong Jin and Jean{-}Fran{\c{c}}ois Raskin},
 year         = {2010},
 title        = {Compositional Algorithms for {LTL} Synthesis},
 booktitle    = {Automated Technology for Verification and Analysis - 8th International Symposium, {ATVA} 2010, Singapore, September 21-24, 2010. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {6252},
 publisher    = {Springer},
 pages        = {112--127},
 doi          = {10.1007/978-3-642-15643-4\textunderscore10},
)
@article(FiliotJR11,
 author       = {Emmanuel Filiot and Naiyong Jin and Jean{-}Fran{\c{c}}ois Raskin},
 year         = {2011},
 title        = {Antichains and compositional algorithms for {LTL} synthesis},
 journal      = {Formal Methods in System Design},
 volume       = {39},
 number       = {3},
 pages        = {261--296},
 doi          = {10.1007/s10703-011-0115-3},
)
@misc(ltl2aig,
 author       = {Guillermo A. P\'erez},
 title        = {{LTL2AIG}},
 note         = {\url{https://github.com/gaperez64/acacia_ltl2aig}},
)
@inproceedings(shs-vb94,
 author       = {Thomas R. Shiple and Ramin Hojati and Sangiovanni-Vincentelli, Alberto L. and Robert K. Brayton},
 year         = {1994},
 title        = {Heuristic minimization of BDDs using don't cares},
 booktitle    = {Proceedings of the 31st annual Design Automation Conference},
 organization = {ACM},
 pages        = {225--231},
 doi          = {10.1145/196244.196360},
)
@incollection(somenzi99,
 author       = {Fabio Somenzi},
 year         = {1999},
 title        = {Binary Decision Diagrams},
 booktitle    = {Calculational system design},
 volume       = {173},
 publisher    = {IOS Press},
 pages        = {303},
)
@article(tarski55,
 author       = {Alfred Tarski},
 year         = {1955},
 title        = {A lattice-theoretical fixpoint theorem and its applications},
 journal      = {Pacific journal of Mathematics},
 volume       = {5},
 number       = {2},
 pages        = {285--309},
 doi          = {10.2140/pjm.1955.5.285},
)
@inproceedings(tslbs-v90,
 author       = {H.J. Touti and H. Savoj and B. Lin and R.K. Brayton and Sangiovanni-Vincentelli, A.},
 year         = {1990},
 title        = {Implicit enumeration of finite state machines using bdd's},
 booktitle    = {IEEE Int. Conference on CAD},
 doi          = {10.1109/ICCAD.1990.129860},
)
@inproceedings(wang2003compositional,
 author       = {Chao Wang and Gary D Hachtel and Fabio Somenzi},
 year         = {2003},
 title        = {The compositional far side of image computation},
 booktitle    = {Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design},
 organization = {IEEE Computer Society},
 pages        = {334},
 doi          = {10.1109/ICCAD.2003.159708},
)