@misc(Filippidis15github-openpromela,
 title        = {open-\textsc{Promela} compiler (\textsc{Python} package)},
 url          = {https://github.com/johnyf/openpromela},
)
@misc(Filippidis15github-promela,
 title        = {\textsc{Promela} parser (\textsc{Python} package)},
 url          = {https://github.com/johnyf/promela},
)
@misc(slugsfork,
 title        = {\textsc{Slugs} instrumentation at tag \texttt{synt\_2015}},
 url          = {https://github.com/johnyf/slugs},
)
@misc(Filippidis15github-dd,
 title        = {\texttt{dd}: Decision diagrams (\textsc{Python} package)},
 url          = {https://github.com/johnyf/dd},
)
@misc(Filippidis15github-omega,
 title        = {\texttt{omega}: Symbolic and enumerated data structures and algorithms for manipulating $\omega$-regular sets (\textsc{Python} package)},
 url          = {https://github.com/johnyf/omega},
)
@conference(Abadi94podc,
 author       = {Mart\'{\i}n Abadi and Leslie Lamport},
 year         = {1994},
 title        = {Open systems in {TLA}},
 booktitle    = {PODC},
 pages        = {81--90},
 doi          = {10.1145/197917.197960},
)
@conference(Alur2013fmcad,
 author       = {Rajeev Alur and Rastislav Bodik and Garvit Juniwal and Milo MK Martin and Mukund Raghothaman and Sanjit A Seshia and Rishabh Singh and Solar-Lezama, Armando and Emina Torlak and Abhishek Udupa},
 year         = {2013},
 title        = {Syntax-guided synthesis},
 booktitle    = {FMCAD},
 pages        = {1--17},
 doi          = {10.1109/FMCAD.2013.6679385},
)
@article(Alur04tocl,
 author       = {Rajeev Alur and La Torre, Salvatore},
 year         = {2004},
 title        = {Deterministic generators and games for {LTL} fragments},
 journal      = {ACM Trans. Comput. Logic},
 volume       = {5},
 number       = {1},
 pages        = {1--25},
 doi          = {10.1145/963927.963928},
)
@manual(ARM99rev2,
 organization = {{ARM Ltd.}},
 year         = {1999},
 title        = {{AMBA\textsuperscript{\texttrademark} Specification}},
 edition      = {{Rev 2.0}},
 url          = {http://www-micro.deis.unibo.it/~magagni/amba99.pdf},
)
@book(Baier08,
 author       = {Christel Baier and Joost-Pieter Katoen},
 year         = {2008},
 title        = {Principles of model checking},
 publisher    = {The MIT Press},
)
@conference(Baldamus01spin,
 author       = {Michael Baldamus and Schr\"{o}der-Babo, Jochen},
 year         = {2001},
 title        = {{P2B}: A translation utility for linking \textsc{Promela} and symbolic model checking},
 booktitle    = {SPIN},
 pages        = {183--191},
 doi          = {10.1007/3-540-45139-0\_11},
)
@conference(Barnat13cav,
 author       = {Ji{\v r}{\'\i} Barnat and Lubo{\v s} Brim and Vojt{\v e}ch Havel and Havl{\'\i}{\v c}ek, Jan and Jan Kriho and Len{\v c}o, Milan and Ro{\v c}kai, Petr and {\v S}till, Vladim{\'\i}r and Ji{\v r}{\'\i} Weiser},
 year         = {2013},
 title        = {\textsc{DiVinE} 3.0 -- An explicit-state model checker for multithreaded {C \& C++} programs},
 booktitle    = {CAV},
 volume       = {8044},
 pages        = {863--868},
 doi          = {10.1007/978-3-642-39799-8\_60},
)
@article(Beaudenon10sttt,
 author       = {Vincent Beaudenon and Emmanuelle Encrenaz and Sami Taktak},
 year         = {2010},
 title        = {Data decision diagrams for promela systems analysis},
 journal      = {STTT},
 volume       = {12},
 number       = {5},
 pages        = {337--352},
 doi          = {10.1007/s10009-010-0135-0},
)
@misc(ply34doc,
 author       = {David M. Beazley},
 title        = {PLY (Python Lex-Yacc) v3.4},
 url          = {http://www.dabeaz.com/ply/ply.html},
)
@conference(Beyene2014popl,
 author       = {Tewodros Beyene and Swarat Chaudhuri and Corneliu Popeea and Andrey Rybalchenko},
 year         = {2014},
 title        = {A constraint-based approach to solving games on infinite graphs},
 booktitle    = {POPL},
 pages        = {221--233},
 doi          = {10.1145/2535838.2535860},
)
@conference(Bloem10cav,
 author       = {Roderick Bloem and Alessandro Cimatti and Karin Greimel and Georg Hofferek and Robert K{\"o}nighofer and Marco Roveri and Viktor Schuppan and Richard Seeber},
 year         = {2010},
 title        = {\textsc{Ratsy}--{A} new requirements analysis tool with synthesis},
 booktitle    = {CAV},
 pages        = {425--429},
 doi          = {10.1007/978-3-642-14295-6\_37},
)
@conference(Bloem07date,
 author       = {Roderick Bloem and Stefan Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer},
 year         = {2007},
 title        = {Interactive presentation: {Automatic} hardware synthesis from specifications: {A} case study},
 booktitle    = {Design, Automation and Test in Europe (DATE)},
 pages        = {1188--1193},
 url          = {http://dl.acm.org/citation.cfm?id=1266366.1266622},
)
@article(Bloem07cocv,
 author       = {Roderick Bloem and Stefan Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer},
 year         = {2007},
 title        = {Specify, compile, run: {Hardware} from \textsc{PSL}},
 journal      = {ENTCS},
 volume       = {190},
 number       = {4},
 pages        = {3--16},
 doi          = {10.1016/j.entcs.2007.09.004},
)
@conference(Bloem14amba,
 author       = {Roderick Bloem and Swen Jacobs and Ayrat Khalimov},
 year         = {2014},
 title        = {Parameterized synthesis case study: {AMBA AHB}},
 editor       = {Krishnendu Chatterjee and R\"{u}diger Ehlers and Susmit Jha},
 booktitle    = {SYNT},
 series       = {EPTCS},
 volume       = {157},
 pages        = {68--83},
 doi          = {10.4204/EPTCS.157.9},
 url          = {http://arxiv.org/abs/1407.6580v1},
)
@article(Bloem12jcss,
 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 (JCSS)},
 volume       = {78},
 number       = {3},
 pages        = {911--938},
 doi          = {10.1016/j.jcss.2011.08.007},
)
@conference(Bohy12cav,
 author       = {Aaron Bohy and V{\'e}ronique Bruy{\`e}re and Emmanuel Filiot and Naiyong Jin and Jean-Fran{\c{c}}ois Raskin},
 year         = {2012},
 title        = {\textsc{Acacia+}, a tool for {LTL} synthesis},
 booktitle    = {CAV},
 pages        = {652--657},
 doi          = {10.1007/978-3-642-31424-7\_45},
)
@article(Broy86tcs,
 author       = {Manfred Broy},
 year         = {1986},
 title        = {A theory for nondeterminism, parallelism, communication, and concurrency},
 journal      = {TCS},
 volume       = {45},
 number       = {0},
 pages        = {1--61},
 doi          = {10.1016/0304-3975(86)90040-X},
)
@article(Bryant86tc,
 author       = {Randal E. Bryant},
 year         = {1986},
 title        = {Graph-based algorithms for {Boolean} function manipulation},
 journal      = {IEEE Trans. Comput.},
 volume       = {35},
 number       = {8},
 pages        = {677--691},
 doi          = {10.1109/TC.1986.1676819},
)
@techreport(Cavada10nusmv,
 author       = {Roberto Cavada and Alessandro Cimatti and Charles Arthur Jochim and Gavin Keighren and Emanuele Olivetti and Marco Pistore and Marco Roveri and Andrei Tchaltsev},
 year         = {2010},
 title        = {\textsc{NuSMV} 2.5 {User Manual}},
 type         = {Technical Report},
 institution  = {Fondazione Bruno Kessler},
 address      = {18 Via Sommarive, 38055 Povo (Trento), Italy},
)
@article(Chandra81jacm,
 author       = {Ashok K. Chandra and Dexter C. Kozen and Larry J. Stockmeyer},
 year         = {1981},
 title        = {Alternation},
 journal      = {JACM},
 volume       = {28},
 number       = {1},
 pages        = {114--133},
 doi          = {10.1145/322234.322243},
)
@conference(Ciesinski08spin,
 author       = {Frank Ciesinski and Christel Baier and Gr{\"o}{\ss}er, Marcus and David Parker},
 year         = {2008},
 title        = {Generating compact {MTBDD}-representations from {Probmela} specifications},
 booktitle    = {SPIN},
 pages        = {60--76},
 doi          = {10.1007/978-3-540-85114-1\_7},
)
@article(Dijkstra75cacm,
 author       = {Edsger W. Dijkstra},
 year         = {1975},
 title        = {Guarded commands, nondeterminacy and formal derivation of programs},
 journal      = {CACM},
 volume       = {18},
 number       = {8},
 pages        = {453--457},
 doi          = {10.1145/360933.360975},
)
@conference(Dwyer99icse,
 author       = {M.B. Dwyer and G.S. Avrunin and J.C. Corbett},
 year         = {1999},
 title        = {Patterns in property specifications for finite-state verification},
 booktitle    = {ICSE},
 pages        = {411--420},
 doi          = {10.1145/302405.302672},
)
@article(Ehlers2011wigp,
 author       = {R{\"u}diger Ehlers},
 year         = {2011},
 title        = {Experimental aspects of synthesis},
 journal      = {EPTCS},
 volume       = {50},
 doi          = {10.4204/EPTCS.50},
)
@conference(Ehlers11nfm,
 author       = {R{\"u}diger Ehlers},
 year         = {2011},
 title        = {{Generalized Rabin(1)} synthesis with applications to robust system synthesis},
 booktitle    = {NFM},
 pages        = {101--115},
 doi          = {10.1007/978-3-642-20398-5\_9},
)
@conference(Ehlers11tacas,
 author       = {R\"{u}diger Ehlers},
 year         = {2011},
 title        = {Unbeast: Symbolic bounded synthesis},
 booktitle    = {TACAS},
 pages        = {272--275},
 doi          = {10.1007/978-3-642-19835-9\_25},
)
@article(Ehlers14synt,
 author       = {R{\"u}diger Ehlers and Vasumathi Raman},
 year         = {2014},
 title        = {Low-effort specification debugging and analysis},
 journal      = {EPTCS},
 volume       = {157},
 pages        = {117--133},
 doi          = {10.4204/EPTCS.157.12},
)
@misc(Filippidis13list,
 author       = {Ioannis Filippidis and contributors},
 year         = {2013},
 title        = {List of verification and synthesis tools},
 url          = {https://github.com/johnyf/tool_lists/blob/master/verification_synthesis.md},
)
@techreport(Filippidis15cds4-amba,
 author       = {Ioannis Filippidis and Richard M. Murray},
 year         = {2015},
 title        = {Revisiting the {AMBA AHB} bus case study},
 type         = {Technical Report},
 number       = {CaltechCDSTR:2015.004},
 institution  = {California Institute of Technology},
 address      = {Pasadena, CA},
 url          = {http://resolver.caltech.edu/CaltechCDSTR:2015.004},
)
@techreport(Filippidis15cds3-synt,
 author       = {Ioannis Filippidis and Richard M. Murray and Gerard J. Holzmann},
 year         = {2015},
 title        = {Synthesis from multi-paradigm specifications},
 type         = {Technical Report},
 number       = {CaltechCDSTR:2015.003},
 institution  = {California Institute of Technology},
 address      = {Pasadena, CA},
 url          = {http://resolver.caltech.edu/CaltechCDSTR:2015.003},
)
@article(Finkbeiner13sttt,
 author       = {Bernd Finkbeiner and Sven Schewe},
 year         = {2013},
 title        = {Bounded synthesis},
 journal      = {International Journal on Software Tools for Technology Transfer (STTT)},
 volume       = {15},
 number       = {5-6},
 pages        = {519--539},
 doi          = {10.1007/s10009-012-0228-z},
)
@article(Floyd67jacm,
 author       = {Robert W. Floyd},
 year         = {1967},
 title        = {Nondeterministic algorithms},
 journal      = {JACM},
 volume       = {14},
 number       = {4},
 pages        = {636--644},
 doi          = {10.1145/321420.321422},
)
@conference(FreemanBenson90ecoop,
 author       = {Freeman-Benson, Bjorn N.},
 year         = {1990},
 title        = {\textsc{Kaleidoscope}: {Mixing} objects, constraints, and imperative programming},
 booktitle    = {OOPSLA/ECOOP},
 pages        = {77--88},
 doi          = {10.1145/97946.97957},
)
@conference(FreemanBenson92ecoop,
 author       = {Freeman-Benson, Bj{\o}rn N. and Alan Borning},
 year         = {1992},
 title        = {Integrating constraints with an object-oriented language},
 booktitle    = {ECOOP},
 pages        = {268--286},
 doi          = {10.1007/BFb0053042},
)
@conference(FreemanBenson92iccl,
 author       = {Freeman-Benson, B.N. and A Borning},
 year         = {1992},
 title        = {The design and implementation of \textsc{Kaleidoscope}'90-{A} constraint imperative programming language},
 booktitle    = {ICCL},
 pages        = {174--180},
 doi          = {10.1109/ICCL.1992.185480},
)
@book(Gamatie09,
 author       = {Abdoulaye Gamati{\'e}},
 year         = {2010},
 title        = {Designing embedded systems with the Signal programming language: synchronous, reactive specification},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4419-0941-1},
)
@techreport(Gennari07cmu,
 author       = {Jeff Gennari and Shaun Hedrick and Fred Long and Justin Pincar and Robert Seacord},
 year         = {2007},
 title        = {Ranged integers for the {C} programming language},
 type         = {Technical Note},
 number       = {CMU/SEI-2007-TN-027},
 institution  = {Software Engineering Institute, Carnegie Mellon University},
 url          = {http://resources.sei.cmu.edu/library/asset-view.cfm?AssetID=8265},
)
@article(Godhal13sttt,
 author       = {Yashdeep Godhal and Krishnendu Chatterjee and Thomas A Henzinger},
 year         = {2013},
 title        = {Synthesis of {AMBA AHB} from formal specification: a case study},
 journal      = {International Journal on Software Tools for Technology Transfer (STTT)},
 volume       = {15},
 number       = {5-6},
 pages        = {585--601},
 doi          = {10.1007/s10009-011-0207-9},
)
@book(Halbwachs92,
 author       = {Nicolas Halbwachs},
 year         = {1993},
 title        = {Synchronous programming of reactive systems},
 series       = {Engineering and Computer Science},
 volume       = {215},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4757-2231-4},
 url          = {http://www-verimag.imag.fr/~halbwach/newbook.pdf},
)
@book(Hoare85csp,
 author       = {Charles Antony Richard Hoare},
 year         = {1985, 2004},
 title        = {Communicating sequential processes},
 volume       = {178},
 publisher    = {Prentice-Hall},
 url          = {http://www.usingcsp.com/cspbook.pdf},
)
@misc(spinroot,
 author       = {Gerard J. Holzmann},
 title        = {\textsc{Promela} Language Reference (\url{http://spinroot.com/spin/Man/promela.html})},
 url          = {http://spinroot.com/spin/Man/promela.html},
)
@book(Holzmann03,
 author       = {Gerard J. Holzmann},
 year         = {2003},
 title        = {The {SPIN} model checker: {Primer} and reference manual},
 publisher    = {Addison-Wesley},
)
@conference(Yong12spin,
 author       = {Yong Jiang and Zongyan Qiu},
 year         = {2012},
 title        = {{S2N}: model transformation from \textsc{Spin} to \textsc{NuSMV}},
 booktitle    = {SPIN},
 pages        = {255--260},
 doi          = {10.1007/978-3-642-31759-0\_20},
)
@conference(Jobstmann06fmcad,
 author       = {Barbara Jobstmann and Roderick Bloem},
 year         = {2006},
 title        = {Optimizations for {LTL} synthesis},
 booktitle    = {FMCAD},
 pages        = {117--124},
 doi          = {10.1109/FMCAD.2006.22},
)
@conference(Jobstmann07cav,
 author       = {Barbara Jobstmann and Stefan Galler and Martin Weiglhofer and Roderick Bloem},
 year         = {2007},
 title        = {\textsc{Anzu}: A tool for property synthesis},
 booktitle    = {CAV},
 pages        = {258--262},
 doi          = {10.1007/978-3-540-73368-3\_29},
)
@conference(Jobstmann05cav,
 author       = {Barbara Jobstmann and Andreas Griesmayer and Roderick Bloem},
 year         = {2005},
 title        = {Program repair as a game},
 booktitle    = {CAV},
 pages        = {226--238},
 doi          = {10.1007/11513988\_23},
)
@conference(Jourdan94iccl,
 author       = {Muriel Jourdan and Fabienne Lagnier and R Maraninchi and Pascal Raymond},
 year         = {1994},
 title        = {A multiparadigm language for reactive systems},
 booktitle    = {ICCL},
 pages        = {211--218},
 doi          = {10.1109/ICCL.1994.288379},
)
@article(Keller76cacm,
 author       = {Robert M. Keller},
 year         = {1976},
 title        = {Formal verification of parallel programs},
 journal      = {CACM},
 volume       = {19},
 number       = {7},
 pages        = {371--384},
 doi          = {10.1145/360248.360251},
)
@conference(Kesten1998icalp,
 author       = {Yonit Kesten and Amir Pnueli and Li-on Raviv},
 year         = {1998},
 title        = {Algorithmic verification of linear temporal logic specifications},
 booktitle    = {ICALP},
 volume       = {1443},
 pages        = {1--16},
 doi          = {10.1007/BFb0055036},
)
@conference(Klein12vmcai,
 author       = {Uri Klein and Nir Piterman and Amir Pnueli},
 year         = {2012},
 title        = {Effective synthesis of asynchronous systems from {GR(1)} specifications},
 booktitle    = {VMCAI},
 pages        = {283--298},
 doi          = {10.1007/978-3-642-27940-9\_19},
)
@article(Kloetzer08tac,
 author       = {M. Kloetzer and C. Belta},
 year         = {2008},
 title        = {A fully automated framework for control of linear systems from temporal logic specifications},
 journal      = {TAC},
 volume       = {53},
 number       = {1},
 pages        = {287--297},
 doi          = {10.1109/TAC.2007.914952},
)
@article(KressGazit09tro,
 author       = {Kress-Gazit, H. and G.E. Fainekos and G.J. Pappas},
 year         = {2009},
 title        = {Temporal-logic-based reactive mission and motion planning},
 journal      = {IEEE Transactions on Robotics (TRO)},
 volume       = {25},
 number       = {6},
 pages        = {1370--1381},
 doi          = {10.1109/TRO.2009.2030225},
)
@book(Kroening08,
 author       = {Daniel Kroening and Ofer Strichman},
 year         = {2008},
 title        = {Decision procedures: {An} algorithmic point of view},
 publisher    = {Springer},
)
@conference(Kupferman05focs,
 author       = {O. Kupferman and M.Y. Vardi},
 year         = {2005},
 title        = {Safraless decision procedures},
 booktitle    = {FOCS},
 pages        = {531--540},
 doi          = {10.1109/SFCS.2005.66},
)
@conference(Kupferman12sofsem,
 author       = {Orna Kupferman},
 year         = {2012},
 title        = {Recent challenges and ideas in temporal synthesis},
 booktitle    = {SOFSEM},
 pages        = {88--98},
 doi          = {10.1007/978-3-642-27660-6\_8},
)
@article(Lamport94tpls,
 author       = {Leslie Lamport},
 year         = {1994},
 title        = {The Temporal Logic of Actions},
 journal      = {ACM Trans. Program. Lang. Syst.},
 volume       = {16},
 number       = {3},
 pages        = {872--923},
 doi          = {10.1145/177492.177726},
)
@book(Lamport02,
 author       = {Leslie Lamport},
 year         = {2002},
 title        = {Specifying systems: The {TLA}+ language and tools or hardware and software engineers},
 publisher    = {Addison-Wesley},
 url          = {http://research.microsoft.com/en-us/um/people/lamport/tla/book.html},
)
@conference(Lamport85popl,
 author       = {Leslie Lamport and Fred B. Schneider},
 year         = {1985},
 title        = {Constraints: {A} uniform approach to aliasing and typing},
 booktitle    = {POPL},
 pages        = {205--216},
 doi          = {10.1145/318593.318640},
)
@conference(Leino10lpair,
 author       = {K Rustan M Leino},
 year         = {2010},
 title        = {{Dafny}: An automatic program verifier for functional correctness},
 booktitle    = {LPAR},
 volume       = {6355},
 pages        = {348--370},
 doi          = {10.1007/978-3-642-17511-4\_20},
)
@phdthesis(Lezama08phd,
 author       = {A Solar Lezama},
 year         = {2008},
 title        = {Program synthesis by sketching},
 school       = {Citeseer},
 url          = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.html},
)
@conference(Lichtenstein85clp,
 author       = {Orna Lichtenstein and Amir Pnueli and Lenore Zuck},
 year         = {1985},
 title        = {The glory of the past},
 booktitle    = {Logics of Programs},
 volume       = {193},
 pages        = {196--218},
 doi          = {10.1007/3-540-15648-8\_16},
)
@conference(Livingston12icra,
 author       = {Scott C. Livingston and Richard M. Murray and Joel W. Burdick},
 year         = {2012},
 title        = {Backtracking temporal logic synthesis for uncertain environments},
 booktitle    = {ICRA},
 pages        = {5163--5170},
 doi          = {10.1109/ICRA.2012.6225208},
)
@conference(Lopez94oopsla,
 author       = {Gus Lopez and Freeman-Benson, Bjorn and Alan Borning},
 year         = {1994},
 title        = {Implementing constraint imperative programming languages: {The} \textsc{Kaleidoscope}'93 virtual machine},
 booktitle    = {OOPSLA},
 pages        = {259--271},
 doi          = {10.1145/191080.191118},
)
@techreport(Manna90stanford-tr,
 author       = {Z Manna and Amir Pnueli},
 year         = {1990},
 title        = {Tools and rules for the practicing verifier},
 type         = {Technical Report},
 number       = {CS-TR-90-1321},
 institution  = {Stanford University},
 address      = {CA, USA},
 url          = {http://i.stanford.edu/pub/cstr/reports/cs/tr/90/1321/CS-TR-90-1321.pdf},
)
@incollection(Manna89lncs,
 author       = {Zohar Manna and Amir Pnueli},
 year         = {1989},
 title        = {The anchored version of the temporal framework},
 booktitle    = {Linear time, branching time and partial order in Logics and models for concurrency},
 series       = {LNCS},
 volume       = {354},
 publisher    = {Springer},
 pages        = {201--284},
 doi          = {10.1007/BFb0013024},
)
@conference(Manna90podc,
 author       = {Zohar Manna and Amir Pnueli},
 year         = {1990},
 title        = {A hierarchy of temporal properties},
 booktitle    = {PODC},
 pages        = {377--410},
 doi          = {10.1145/93385.93442},
)
@conference(Maoz11aosd,
 author       = {Shahar Maoz and Yaniv Sa'ar},
 year         = {2011},
 title        = {\textsc{AspectLTL}: {An} aspect language for {LTL} specifications},
 booktitle    = {Aspect-oriented Software Development (AOSD)},
 publisher    = {ACM},
 pages        = {19--30},
 doi          = {10.1145/1960275.1960280},
)
@incollection(McCarthy63,
 author       = {John McCarthy},
 year         = {1959},
 title        = {A basis for a mathematical theory of computation},
 editor       = {P. Braffort and D. Hirschberg},
 booktitle    = {{Computer Programming and Formal Systems}},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {26},
 publisher    = {North-Holland},
 pages        = {33--70},
 doi          = {10.1016/S0049-237X(09)70099-0},
)
@phdthesis(McMillan92phd,
 author       = {Kenneth Lauchlin McMillan},
 year         = {1992},
 title        = {Symbolic model checking: {An} approach to the state explosion problem},
 school       = {Carnegie Mellon University},
 address      = {Pittsburgh, PA, USA},
 doi          = {10.1007/978-1-4615-3190-6},
 url          = {http://www.kenmcmil.com/pubs/thesis.pdf},
 note         = {UMI Order No. GAX92-24209},
)
@article(Mealy55,
 author       = {George H Mealy},
 year         = {1955},
 title        = {A method for synthesizing sequential circuits},
 journal      = {Bell System Technical Journal},
 volume       = {34},
 number       = {5},
 pages        = {1045--1079},
 doi          = {10.1002/j.1538-7305.1955.tb03788.x},
)
@article(Moore56,
 author       = {Edward F Moore},
 year         = {1956},
 title        = {Gedanken-experiments on sequential machines},
 journal      = {Automata studies},
 volume       = {34},
 pages        = {129--153},
)
@phdthesis(Morgenstern10phd,
 author       = {A. Morgenstern},
 year         = {2010},
 title        = {Symbolic controller synthesis for {LTL} specifications},
 school       = {{Computer Science}},
 url          = {http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz:386-kluedo-25721},
)
@article(Morgenstern11wigp,
 author       = {A. {Morgenstern} and K. {Schneider}},
 year         = {2011},
 title        = {A {LTL} fragment for {GR(1)}-synthesis},
 journal      = {EPTCS},
 volume       = {50},
 pages        = {33--45},
 doi          = {10.4204/EPTCS.50.3},
)
@conference(Muller86alp,
 author       = {David E Muller and Ahmed Saoudi and Paul E Schupp},
 year         = {1986},
 title        = {Alternating automata, the weak monadic theory of the tree, and its complexity},
 booktitle    = {ICALP},
 pages        = {275--283},
 doi          = {10.1007/3-540-16761-7\_77},
)
@conference(Najm96spin,
 author       = {Elie Najm and Frank Olsen},
 year         = {1996},
 title        = {Protocol verification with {Reactive \textsc{Proela}/RSPIN}},
 booktitle    = {SPIN},
 pages        = {109--128},
 url          = {http://spinroot.com/spin/Workshops/ws96/Ol.pdf},
)
@conference(Najm96tacas,
 author       = {Elie Najm and Frank Olsen},
 year         = {1996},
 title        = {{Reactive EFSMs --- Reactive Promela/RSPIN}},
 booktitle    = {TACAS},
 pages        = {349--368},
 doi          = {10.1007/3-540-61042-1\_54},
)
@conference(Panda95iccad,
 author       = {Shipra Panda and Fabio Somenzi},
 year         = {1995},
 title        = {Who are the variables in your neighbourhood},
 booktitle    = {ICCAD},
 pages        = {74--77},
 doi          = {10.1109/ICCAD.1995.479994},
)
@conference(Piterman06,
 author       = {Nir Piterman and Amir Pnueli and Yaniv Sa'ar},
 year         = {2006},
 title        = {Synthesis of reactive(1) designs},
 booktitle    = {VMCAI},
 pages        = {364--380},
 doi          = {10.1007/11609773\_24},
)
@conference(Pnueli89popl,
 author       = {A. Pnueli and R. Rosner},
 year         = {1989},
 title        = {On the synthesis of a reactive module},
 booktitle    = {POPL},
 pages        = {179--190},
 doi          = {10.1145/75277.75293},
)
@conference(Pnueli77,
 author       = {Amir Pnueli},
 year         = {1977},
 title        = {The temporal logic of programs},
 booktitle    = {FOCS},
 pages        = {46 --57},
 doi          = {10.1109/SFCS.1977.32},
)
@conference(Pnueli09memocode,
 author       = {Amir Pnueli and Uri Klein},
 year         = {2009},
 title        = {Synthesis of programs from temporal property specifications},
 booktitle    = {MEMOCODE},
 pages        = {1--7},
 doi          = {10.1109/MEMCOD.2009.5185372},
)
@conference(Pnueli89icalp,
 author       = {Amir Pnueli and Roni Rosner},
 year         = {1989},
 title        = {On the synthesis of an asynchronous reactive module},
 booktitle    = {ICALP},
 pages        = {652--671},
 doi          = {10.1007/BFb0035790},
)
@conference(Pnueli10cav,
 author       = {Amir Pnueli and Yaniv Sa'ar and Lenore D Zuck},
 year         = {2010},
 title        = {\textsc{Jtlv}: {A} framework for developing verification algorithms},
 booktitle    = {CAV},
 pages        = {171--174},
 doi          = {10.1007/978-3-642-14295-6\_18},
)
@phdthesis(Rosner92,
 author       = {Roni Rosner},
 year         = {1992},
 title        = {Modular synthesis of reactive systems},
 school       = {Weizmann Institute of Science},
 address      = {Rehovot, Israel},
 url          = {http://www.researchgate.net/publication/238759536_Modular_synthesis_of_reactive_systems/file/50463527f8b648c3ba.pdf},
)
@conference(Rudell1993iccad,
 author       = {Richard Rudell},
 year         = {1993},
 title        = {Dynamic variable ordering for ordered binary decision diagrams},
 booktitle    = {ICCAD},
 pages        = {42--47},
 doi          = {10.1109/ICCAD.1993.580029},
)
@conference(Schlaipfer12,
 author       = {Matthias Schlaipfer and Georg Hofferek and Roderick Bloem},
 year         = {2012},
 title        = {Generalized reactivity(1) synthesis without a monolithic strategy},
 booktitle    = {HSVT},
 pages        = {20--34},
 doi          = {10.1007/978-3-642-34188-5\_6},
)
@book(Schneider04,
 author       = {Klaus Schneider},
 year         = {2004},
 title        = {Verification of reactive systems: formal methods and algorithms},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-10778-2},
)
@conference(Sohail08vmcai,
 author       = {Saqib Sohail and Fabio Somenzi and Kavita Ravi},
 year         = {2008},
 title        = {A hybrid algorithm for {LTL} games},
 booktitle    = {VMCAI},
 pages        = {309--323},
 doi          = {10.1007/978-3-540-78163-9\_26},
)
@article(Somenzi12cudd,
 author       = {Fabio Somenzi},
 year         = {2012},
 title        = {\textsc{Cudd}: {CU Decision Diagram} package - release 2.5.0},
 journal      = {University of Colorado at Boulder},
 url          = {http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html},
)
@article(Sondergaard1992cj,
 author       = {S{\o}ndergaard, Harald and Peter Sestoft},
 year         = {1992},
 title        = {Non-determinism in functional languages},
 journal      = {The Computer Journal},
 volume       = {35},
 number       = {5},
 pages        = {514--523},
 doi          = {10.1093/comjnl/35.5.514},
)
@article(Thomas08npgi,
 author       = {Wolfgang Thomas},
 year         = {2008},
 title        = {Solution of {Church's} Problem: {A} tutorial},
 journal      = {New Perspectives on Games and interaction},
 volume       = {5},
)
@book(vanRoy04,
 author       = {Van-Roy, Peter and Seif Haridi},
 year         = {2004},
 title        = {Concepts, techniques, and models of computer programming},
 publisher    = {MIT press},
)
@incollection(Vardi95cst,
 author       = {Moshe Y Vardi},
 year         = {1995},
 title        = {Alternating automata and program verification},
 booktitle    = {Computer Science Today},
 publisher    = {Springer},
 pages        = {471--485},
 doi          = {10.1007/BFb0015261},
)
@incollection(Vardi96lc,
 author       = {Moshe Y Vardi},
 year         = {1996},
 title        = {An automata-theoretic approach to linear temporal logic},
 booktitle    = {Logics for concurrency},
 series       = {LNCS},
 volume       = {1043},
 publisher    = {Springer},
 pages        = {238--266},
 doi          = {10.1007/3-540-60915-6\_6},
)
@article(Walukiewicz04lics,
 author       = {Igor Walukiewicz},
 year         = {2004},
 title        = {A Landscape with games in the background},
 journal      = {LICS},
 volume       = {0},
 pages        = {356--366},
 doi          = {10.1109/LICS.2004.1319630},
)
@article(Wongpiromsarn13us,
 author       = {Tichakorn Wongpiromsarn and Ufuk Topcu and Richard M Murray},
 year         = {2013},
 title        = {Synthesis of control protocols for autonomous systems},
 journal      = {Unmanned Systems},
 volume       = {1},
 number       = {01},
 pages        = {21--39},
 doi          = {10.1142/S2301385013500027},
)