@book(AhoHU74,
 author       = {Alfred~V. Aho and John~E. Hopcroft and Jeffrey~D. Ullman},
 year         = {1974},
 title        = {The Design and Analysis of Computer Algorithms},
 publisher    = {Addison-Wesley},
)
@inproceedings(ArmoniEFKV05,
 author       = {Roy Armoni and Sergey Egorov and Ranan Fraer and Dmitry Korchemny and Moshe~Y. Vardi},
 year         = {2005},
 title        = {{Efficient {LTL} compilation for SAT-based model checking}},
 booktitle    = {{ICCAD} 2005},
 pages        = {877--884},
 doi          = {10.1109/ICCAD.2005.1560185},
)
@article(BacchusK98,
 author       = {Fahiem Bacchus and Froduald Kabanza},
 year         = {1998},
 title        = {Planning for Temporally Extended Goals},
 journal      = {Ann. Math. Artif. Intell.},
 volume       = {22},
 number       = {1-2},
 pages        = {5--27},
 doi          = {10.1023/A:1018985923441},
)
@article(BacchusK00,
 author       = {Fahiem Bacchus and Froduald Kabanza},
 year         = {2000},
 title        = {Using temporal logics to express search control knowledge for planning},
 journal      = {Artif. Intell.},
 volume       = {116},
 number       = {1-2},
 pages        = {123--191},
 doi          = {10.1016/S0004-3702(99)00071-5},
)
@inproceedings(BLTV,
 author       = {Suguman Bansal and Yong Li and Lucas~M. Tabajara and Moshe~Y. Vardi},
 year         = {2020},
 title        = {{Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications}},
 booktitle    = {{AAAI}},
 pages        = {9766--9774},
 doi          = {10.1609/aaai.v34i06.6528},
)
@inproceedings(BertoglioLZ19,
 author       = {Nicola Bertoglio and Gianfranco Lamperti and Marina Zanella},
 year         = {2019},
 title        = {Temporal Diagnosis of Discrete-Event Systems with Dual Knowledge Compilation},
 editor       = {Andreas Holzinger and Peter Kieseberg and A~Min Tjoa and Edgar~R. Weippl},
 booktitle    = {{Machine Learning and Knowledge Extraction}},
 series       = {Lecture Notes in Computer Science},
 volume       = {11713},
 publisher    = {Springer},
 pages        = {333--352},
 doi          = {10.1007/978-3-030-29726-8\_21},
)
@inproceedings(BienvenuFM06,
 author       = {Meghyn Bienvenu and Christian Fritz and Sheila~A. McIlraith},
 title        = {Planning with Qualitative Temporal Preferences},
 editor       = {Patrick Doherty and John Mylopoulos and Christopher~A. Welty},
 booktitle    = {{KR}},
)
@inproceedings(Bloem15,
 author       = {Roderick Bloem},
 year         = {2015},
 title        = {{Reactive Synthesis}},
 booktitle    = {{FMCAD}},
 publisher    = {{IEEE}},
 pages        = {3},
 doi          = {10.1109/FMCAD.2015.7542241},
)
@article(BloemGJPPW07,
 author       = {Roderick Bloem and Stefan~J. Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer},
 year         = {2007},
 title        = {{Specify, Compile, Run: Hardware from {PSL}}},
 journal      = {Electron. Notes Theor. Comput. Sci.},
 volume       = {190},
 number       = {4},
 pages        = {3--16},
 doi          = {10.1016/j.entcs.2007.09.004},
)
@inproceedings(BrafmanG19,
 author       = {Ronen~I. Brafman and {De Giacomo}, Giuseppe},
 year         = {2019},
 title        = {Planning for {LTL}$_f$ /{LDL}$_f$ Goals in Non-Markovian Fully Observable Nondeterministic Domains},
 editor       = {Sarit Kraus},
 booktitle    = {{IJCAI}},
 pages        = {1602--1608},
 doi          = {10.24963/ijcai.2019/222},
)
@inproceedings(BrafmanGP18,
 author       = {Ronen~I. Brafman and {De Giacomo}, Giuseppe and Fabio Patrizi},
 year         = {2018},
 title        = {{LTL}$_f$/{LDL}$_f$ Non-Markovian Rewards},
 editor       = {Sheila~A. McIlraith and Kilian~Q. Weinberger},
 booktitle    = {{AAAI}},
 pages        = {1771--1778},
)
@article(Bryant92,
 author       = {Randal~E. Bryant},
 year         = {1992},
 title        = {{Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams}},
 journal      = {{ACM} Comput. Surv.},
 volume       = {24},
 number       = {3},
 pages        = {293--318},
 doi          = {10.1145/136035.136043},
)
@inproceedings(Brzozowski62,
 author       = {Janusz~A. Brzozowski},
 year         = {1962},
 title        = {{Canonical Regular Expressions and Minimal State Graphs for Definite Events}},
)
@article(CadoliD97,
 author       = {Marco Cadoli and Francesco~M. Donini},
 year         = {1997},
 title        = {A Survey on Knowledge Compilation},
 journal      = {{AI} Commun.},
 volume       = {10},
 number       = {3-4},
 pages        = {137--150},
)
@inproceedings(CalvaneseGV02,
 author       = {Diego Calvanese and {De Giacomo}, Giuseppe and Moshe~Y. Vardi},
 title        = {Reasoning about Actions and Planning in {LTL} Action Theories},
 editor       = {Dieter Fensel and Fausto Giunchiglia and Deborah~L. McGuinness and Mary{-}Anne Williams},
 booktitle    = {{KR}},
)
@inproceedings(CamachoBMM18,
 author       = {Alberto Camacho and Jorge~A. Baier and Christian~J. Muise and Sheila~A. McIlraith},
 year         = {2018},
 title        = {{Finite {LTL} Synthesis as Planning}},
 booktitle    = {{ICAPS}},
 pages        = {29--38},
)
@inproceedings(CamachoIKVM19,
 author       = {Alberto Camacho and Rodrigo~Toro Icarte and Toryn~Q. Klassen and Richard~Anthony Valenzano and Sheila~A. McIlraith},
 year         = {2019},
 title        = {{LTL} and Beyond: Formal Languages for Reward Function Specification in Reinforcement Learning},
 editor       = {Sarit Kraus},
 booktitle    = {{IJCAI}},
 pages        = {6065--6073},
 doi          = {10.24963/ijcai.2019/840},
)
@inproceedings(CTMBM17,
 author       = {Alberto Camacho and Eleni Triantafillou and Christian Muise and Jorge~A. Baier and Sheila McIlraith},
 year         = {2017},
 title        = {{Non-Deterministic Planning with Temporally Extended Goals: {LTL} over Finite and Infinite Traces}},
 booktitle    = {AAAI},
 pages        = {3716--3724},
)
@article(CKS81,
 author       = {A.K. Chandra and D.C. Kozen and L.J. Stockmeyer},
 year         = {1981},
 title        = {Alternation},
 journal      = {J. ACM},
 volume       = {28},
 number       = {1},
 pages        = {114--133},
 doi          = {10.1145/322234.322243},
)
@article(CiccioMMM17,
 author       = {Claudio~Di Ciccio and Fabrizio~Maria Maggi and Marco Montali and Jan Mendling},
 year         = {2017},
 title        = {Resolving inconsistencies and redundancies in declarative process models},
 journal      = {Inf. Syst.},
 volume       = {64},
 pages        = {425--446},
 doi          = {10.1016/j.is.2016.09.005},
)
@article(ConsoleTD02,
 author       = {Luca Console and Paolo Terenziani and Daniele~Theseider Dupr{\'{e}}},
 year         = {2002},
 title        = {Local Reasoning and Knowledge Compilation for Efficient Temporal Abduction},
 journal      = {{IEEE} Trans. Knowl. Data Eng.},
 volume       = {14},
 number       = {6},
 pages        = {1230--1248},
 doi          = {10.1109/TKDE.2002.1047764},
)
@article(DarwicheM02,
 author       = {Adnan Darwiche and Pierre Marquis},
 year         = {2002},
 title        = {A Knowledge Compilation Map},
 journal      = {J. Artif. Intell. Res.},
 volume       = {17},
 pages        = {229--264},
 doi          = {10.1613/jair.989},
)
@inproceedings(DaxEK07,
 author       = {Christian Dax and Jochen Eisinger and Felix Klaedtke},
 year         = {2007},
 title        = {{Mechanizing the Powerset Construction for Restricted Classes of \emph{omega} -Automata}},
 editor       = {Kedar~S. Namjoshi and Tomohiro Yoneda and Teruo Higashino and Yoshio Okamura},
 booktitle    = {{ATVA}},
 pages        = {223--236},
 doi          = {10.1007/978-3-540-75596-8\_17},
)
@inproceedings(GiacomoSFR20,
 author       = {{De Giacomo}, Giuseppe and {Di Stasio}, Antonio and Francesco Fuggitti and Sasha Rubin},
 year         = {2020},
 title        = {Pure-Past Linear Temporal and Dynamic Logic on Finite Traces},
 editor       = {Christian Bessiere},
 booktitle    = {{IJCAI}},
 pages        = {4959--4965},
 doi          = {10.24963/ijcai.2020/690},
)
@inproceedings(GiacomoIFP19,
 author       = {{De Giacomo}, Giuseppe and Luca Iocchi and Marco Favorito and Fabio Patrizi},
 year         = {2019},
 title        = {Foundations for Restraining Bolts: Reinforcement Learning with {LTL}$_f$/{LDL}$_f$ Restraining Specifications},
 booktitle    = {{ICAPS}},
 pages        = {128--136},
)
@inproceedings(DegRu18,
 author       = {{De Giacomo}, Giuseppe and Sasha Rubin},
 year         = {2018},
 title        = {{Automata-Theoretic Foundations of FOND Planning for {LTL}$_f$/{LDL}$_f$ Goals}},
 booktitle    = {{IJCAI}},
 pages        = {4729--4735},
 doi          = {10.24963/ijcai.2018/657},
)
@inproceedings(DegVa13,
 author       = {{De Giacomo}, Giuseppe and Moshe~Y. Vardi},
 year         = {2013},
 title        = {{Linear Temporal Logic and Linear Dynamic Logic on Finite Traces}},
 booktitle    = {{IJCAI}},
 pages        = {854--860},
 doi          = {10.5555/2540128.2540252},
)
@inproceedings(DegVa15,
 author       = {{De Giacomo}, Giuseppe and Moshe~Y. Vardi},
 year         = {2015},
 title        = {{Synthesis for {LTL} and {LDL} on Finite Traces}},
 booktitle    = {{IJCAI}},
 pages        = {1558--1564},
 doi          = {10.5555/2832415.2832466},
)
@inproceedings(spot,
 author       = {Duret-Lutz, Alexandre and Alexandre Lewkowicz and Amaury Fauchille and Thibaud Michaud and Etienne Renault and Laurent Xu},
 year         = {2016},
 title        = {{Spot 2.0 --- A Framework for {LTL} and $\omega$-automata Manipulation}},
 booktitle    = {ATVA},
 pages        = {122--129},
 doi          = {10.1007/978-3-319-46520-3\_8},
)
@inproceedings(DuttaVT13,
 author       = {Sonali Dutta and Moshe~Y. Vardi and Deian Tabakov},
 year         = {2013},
 title        = {{{CHIMP:} {A} Tool for Assertion-Based Dynamic Verification of SystemC Models}},
 booktitle    = {{DIFTS@FMCAD}},
)
@book(FHMV1995,
 author       = {Ronald Fagin and Joseph~Y. Halpern and Yoram Moses and Moshe~Y. Vardi},
 year         = {1995},
 title        = {Reasoning About Knowledge},
 publisher    = {{MIT} Press},
 doi          = {10.7551/mitpress/5803.001.0001},
)
@incollection(FisherW05,
 author       = {Michael Fisher and Michael~J. Wooldridge},
 year         = {2005},
 title        = {Temporal Reasoning in Agent-Based Systems},
 editor       = {Michael Fisher and Dov~M. Gabbay and Llu{\'{\i}}s Vila},
 booktitle    = {Handbook of Temporal Reasoning in Artificial Intelligence},
 series       = {Foundations of Artificial Intelligence},
 volume       = {1},
 publisher    = {Elsevier},
 pages        = {469--495},
 doi          = {10.1016/S1574-6526(05)80017-3},
)
@inproceedings(FogartyKVW13,
 author       = {Seth Fogarty and Orna Kupferman and Moshe~Y. Vardi and Thomas Wilke},
 year         = {2013},
 title        = {{Profile Trees for B{\"{u}}chi Word Automata, with Application to Determinization}},
 booktitle    = {{GandALF}},
 pages        = {107--121},
 doi          = {10.4204/EPTCS.119.11},
)
@inproceedings(DrLu.cav16,
 author       = {Dror Fried and Lucas~M. Tabajara and Moshe~Y. Vardi},
 year         = {2016},
 title        = {{BDD-Based Boolean Functional Synthesis}},
 booktitle    = {{CAV}},
 pages        = {402--421},
 doi          = {10.1007/978-3-319-41540-6\_22},
)
@inproceedings(GiacomoMGMM14,
 author       = {Giuseppe~De Giacomo and Riccardo~De Masellis and Marco Grasso and Fabrizio~Maria Maggi and Marco Montali},
 year         = {2014},
 title        = {Monitoring Business Metaconstraints Based on {LTL} and {LDL} for Finite Traces},
 editor       = {Shazia~Wasim Sadiq and Pnina Soffer and Hagen V{\"{o}}lzer},
 booktitle    = {{BPM}},
 series       = {Lecture Notes in Computer Science},
 volume       = {8659},
 pages        = {1--17},
 doi          = {10.1007/978-3-319-10172-9\_1},
)
@inproceedings(GiacomoV99,
 author       = {Giuseppe~De Giacomo and Moshe~Y. Vardi},
 year         = {1999},
 title        = {Automata-Theoretic Approach to Planning for Temporally Extended Goals},
 editor       = {Susanne Biundo and Maria Fox},
 booktitle    = {{ECP}},
 series       = {Lecture Notes in Computer Science},
 volume       = {1809},
 publisher    = {Springer},
 pages        = {226--238},
 doi          = {10.1007/10720246\_18},
)
@inproceedings(HeWKV19,
 author       = {Keliang He and Andrew~M. Wells and Lydia~E. Kavraki and Moshe~Y. Vardi},
 year         = {2019},
 title        = {{Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks}},
 booktitle    = {{ICRA}},
 pages        = {8993--8999},
 doi          = {10.1109/ICRA.2019.8794170},
)
@inproceedings(Mona,
 author       = {Jesper~G. Henriksen and Jakob~L. Jensen and J{\o}rgensen, Michael~E. and Nils Klarlund and Robert Paige and Theis Rauhe and Anders Sandholm},
 year         = {1995},
 title        = {{Mona: Monadic Second-order Logic in Practice}},
 booktitle    = {TACAS},
 pages        = {89--110},
 doi          = {10.1007/3-540-60630-0\_5},
)
@techreport(Hopcroft71,
 author       = {John~E. Hopcroft},
 year         = {1971},
 title        = {{An n Log n Algorithm for Minimizing States in a Finite Automaton}},
 type         = {Technical Report},
 address      = {Stanford, CA, USA},
)
@inproceedings(Kupferman12,
 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},
)
@inproceedings(KupfermanV98,
 author       = {Orna Kupferman and Moshe~Y. Vardi},
 year         = {1998},
 title        = {{Freedom, Weakness, and Determinism: From Linear-Time to Branching-Time}},
 booktitle    = {{LICS}},
 pages        = {81--92},
 doi          = {10.1109/LICS.1998.705645},
)
@article(KupfermanVa01,
 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},
)
@inproceedings(KupfermanV05,
 author       = {Orna Kupferman and Moshe~Y. Vardi},
 year         = {2005},
 title        = {{Safraless Decision Procedures}},
 booktitle    = {{FOCS}},
 pages        = {531--542},
 doi          = {10.1109/SFCS.2005.66},
)
@inproceedings(LichtensteinPZ85,
 author       = {Orna Lichtenstein and Amir Pnueli and Lenore~D. Zuck},
 year         = {1985},
 title        = {{The Glory of the Past}},
 booktitle    = {Logics of Programs},
 pages        = {196--218},
 doi          = {10.1007/3-540-15648-8\_16},
)
@inproceedings(MorgensternS08,
 author       = {Andreas Morgenstern and Klaus Schneider},
 year         = {2008},
 title        = {{From {LTL} to Symbolically Represented Deterministic Automata}},
 editor       = {Francesco Logozzo and Doron~A. Peled and Lenore~D. Zuck},
 booktitle    = {{VMCAI}},
 pages        = {279--293},
 doi          = {10.1007/978-3-540-78163-9\_24},
)
@inproceedings(PesicSA07,
 author       = {Maja Pesic and Helen Schonenberg and Wil M.~P. van~der Aalst},
 year         = {2007},
 title        = {{DECLARE:} Full Support for Loosely-Structured Processes},
 booktitle    = {{(EDOC}},
 pages        = {287--300},
 doi          = {10.1109/EDOC.2007.14},
)
@inproceedings(Pin87,
 author       = {Jean{-}Eric Pin},
 year         = {1987},
 title        = {{On the Language Accepted by Finite Reversible Automata}},
 editor       = {Thomas Ottmann},
 booktitle    = {{ICALP}},
 pages        = {237--249},
 doi          = {10.1007/3-540-18088-5\_19},
)
@inproceedings(Pnu77,
 author       = {Amir Pnueli},
 year         = {1977},
 title        = {{The temporal logic of programs}},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@inproceedings(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(RS59,
 author       = {M.O. Rabin and D.~Scott},
 year         = {1959},
 title        = {Finite automata and their decision problems},
 journal      = {IBM Journal of Research and Development},
 volume       = {3},
 pages        = {115--125},
 doi          = {10.1147/rd.32.0114},
)
@article(cudd,
 author       = {Fabio Somenzi},
 year         = {2016},
 title        = {{CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder}},
)
@inproceedings(TabajaraV19,
 author       = {Lucas~Martinelli Tabajara and Moshe~Y. Vardi},
 year         = {2019},
 title        = {{Partitioning Techniques in LTL$_f$ Synthesis}},
 booktitle    = {{IJCAI}},
 pages        = {5599--5606},
 doi          = {10.24963/ijcai.2019/777},
)
@article(TabakovRV12,
 author       = {Deian Tabakov and Kristin~Y. Rozier and Moshe~Y. Vardi},
 year         = {2012},
 title        = {{Optimized temporal monitors for {SystemC}}},
 journal      = {Formal Methods in System Design},
 volume       = {41},
 number       = {3},
 pages        = {236--268},
 doi          = {10.1007/s10703-011-0139-8},
)
@inproceedings(TabakovV05,
 author       = {Deian Tabakov and Moshe~Y. Vardi},
 year         = {2005},
 title        = {{Experimental Evaluation of Classical Automata Constructions}},
 booktitle    = {{LPAR}},
 pages        = {396--411},
 doi          = {10.1007/11591191\_28},
)
@inproceedings(AndrewGandalf,
 author       = {Andrew~M. Wells and Morteza Lahijanian and Lydia~E. Kavraki and Moshe~Y. Vardi},
 year         = {2020},
 title        = {LTL$_f$ Synthesis on Probabilistic Systems},
 editor       = {Jean{-}Fran{\c{c}}ois Raskin and Davide Bresolin},
 booktitle    = {{GandALF}},
 series       = {{EPTCS}},
 volume       = {326},
 pages        = {166--181},
 doi          = {10.4204/EPTCS.326.11},
)
@article(abs-2101-11981,
 author       = {Yaqi Xie and Fan Zhou and Harold Soh},
 year         = {2021},
 title        = {Embedding Symbolic Temporal Knowledge into Deep Sequential Models},
 journal      = {CoRR},
 volume       = {abs/2101.11981},
)
@inproceedings(ZhuGPV20,
 author       = {Shufang Zhu and Giuseppe~De Giacomo and Geguang Pu and Moshe~Y. Vardi},
 year         = {2020},
 title        = {{LTL}$_f$ Synthesis with Fairness and Stability Assumptions},
 booktitle    = {{AAAI}},
 pages        = {3088--3095},
 doi          = {10.1609/aaai.v34i03.5704},
)
@inproceedings(ZhuPV19,
 author       = {Shufang Zhu and Geguang Pu and Moshe~Y. Vardi},
 year         = {2019},
 title        = {{First-Order vs. Second-Order Encodings for LTL$_f$-to-Automata Translation}},
 booktitle    = {{TAMC}},
 pages        = {684--705},
 doi          = {10.1007/978-3-030-14812-6\_43},
)
@inproceedings(ZhuTLPV17,
 author       = {Shufang Zhu and Lucas~M. Tabajara and Jianwen Li and Geguang Pu and Moshe~Y. Vardi},
 year         = {2017},
 title        = {{A Symbolic Approach to Safety LTL Synthesis}},
 booktitle    = {HVC},
 pages        = {147--162},
 doi          = {10.1007/978-3-319-70389-3\_10},
)
@inproceedings(ZTLPV17,
 author       = {Shufang Zhu and Lucas~M. Tabajara and Jianwen Li and Geguang Pu and Moshe~Y. Vardi},
 year         = {2017},
 title        = {{Symbolic {LTL$_f$} Synthesis}},
 booktitle    = {{IJCAI}},
 pages        = {1362--1369},
 doi          = {10.24963/ijcai.2017/189},
)