references.bib

@article{C64,
author = {Alonzo Church},
doi = {10.2307/2270398},
journal = {Journal of Symbolic Logic},
number = {4},
pages = {210--210},
publisher = {Association for Symbolic Logic},
title = {Logic, Arithmetic, and Automata},
volume = {29},
year = {1964}
}

@incollection{B66,
title = {Symposium on Decision Problems: On a Decision Method in Restricted Second Order Arithmetic},
editor = {Ernest Nagel and Patrick Suppes and Alfred Tarski},
series = {Studies in Logic and the Foundations of Mathematics},
publisher = {Elsevier},
volume = {44},
pages = {1-11},
year = {1966},
booktitle = {Logic, Methodology and Philosophy of Science},
issn = {0049-237X},
doi = {https://doi.org/10.1016/S0049-237X(09)70564-6},
url = {https://www.sciencedirect.com/science/article/pii/S0049237X09705646},
author = {J. {Richard Büchi}}
}

@article{R68,
  title={Decidability of second-order theories and automata on infinite trees},
  author={Michael O. Rabin},
  journal={Bulletin of the American Mathematical Society},
  year={1968},
  volume={74},
  pages={1025-1029},
  url={https://api.semanticscholar.org/CorpusID:6015948}
}

@book{cf-automata,
author = {McNaughton, Robert and Papert, Seymour A.},
title = {Counter-Free Automata (M.I.T. Research Monograph No. 65)},
year = {1971},
isbn = {0262130769},
publisher = {The MIT Press}
}

@inproceedings{pnueli1990,
author = {Manna, Zohar and Pnueli, Amir},
title = {A Hierarchy of Temporal Properties (Invited Paper, 1989)},
year = {1990},
isbn = {089791404X},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/93385.93442},
doi = {10.1145/93385.93442},
booktitle = {Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing},
pages = {377–410},
numpages = {34},
location = {Quebec City, Quebec, Canada},
series = {PODC '90}
}

@inproceedings{VW86,
  author       = {Moshe Y. Vardi and
                  Pierre Wolper},
  title        = {An Automata-Theoretic Approach to Automatic Program Verification (Preliminary
                  Report)},
  booktitle    = {Proceedings of the Symposium on Logic in Computer Science {(LICS}
                  '86), Cambridge, Massachusetts, USA, June 16-18, 1986},
  pages        = {332--344},
  publisher    = {{IEEE} Computer Society},
  year         = {1986},
  timestamp    = {Thu, 22 Jan 2015 10:45:18 +0100},
  biburl       = {https://dblp.org/rec/conf/lics/VardiW86.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@Inbook{BL90,
author="Buchi, J. Richard and Landweber, Lawrence H.",
editor="Mac Lane, Saunders and Siefkes, Dirk",
title="Solving Sequential Conditions by Finite-State Strategies",
bookTitle="The Collected Works of J. Richard B{\"u}chi",
year="1990",
publisher="Springer New York",
address="New York, NY",
pages="525--541",
isbn="978-1-4613-8928-6",
doi="10.1007/978-1-4613-8928-6_29",
url="https://doi.org/10.1007/978-1-4613-8928-6_29"
}

@inproceedings{wolgang-1991,
author = {Thomas, Wolfgang},
title = {Automata on Infinite Objects},
year = {1991},
isbn = {0444880747},
publisher = {MIT Press},
address = {Cambridge, MA, USA},
booktitle = {Handbook of Theoretical Computer Science (Vol. B): Formal Models and Semantics},
pages = {133–191},
numpages = {59}
}

@inproceedings{W95,
  title={On the Synthesis of Strategies in Infinite Games},
  author={Wolfgang Thomas},
  booktitle={Symposium on Theoretical Aspects of Computer Science},
  year={1995},
  url={https://api.semanticscholar.org/CorpusID:11461317}
}


@article{KV99,
author = {Kupferman, Orna and Vardi, Moshe},
year = {1999},
month = {09},
pages = {},
title = {Model Checking of Safety Properties},
volume = {19},
isbn = {978-3-540-66202-0},
journal = {Formal Methods in System Design},
doi = {10.1023/A:1011254632723}
}

@inproceedings{gastin-oddoux-2001,
author="Gastin, Paul
and Oddoux, Denis",
editor="Berry, G{\'e}rard
and Comon, Hubert
and Finkel, Alain",
title="Fast LTL to B{\"u}chi Automata Translation",
booktitle="Computer Aided Verification",
year="2001",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="53--65",
isbn="978-3-540-44585-2"
}

@article{MLJ2004,
author = {Wulf, Martin and Doyen, Laurent and Raskin, Jean-Francois},
year = {2004},
month = {02},
pages = {296-310},
title = {Almost ASAP Semantics: from Timed Models to Timed Implementations},
volume = {17},
isbn = {978-3-540-21259-1},
journal = {Formal Aspects of Computing},
doi = {10.1007/978-3-540-24743-2_20}
}

@article{BB05,
author = {Boscain, Ugo and Piccoli, Benedetto},
year = {2005},
month = {01},
pages = {},
title = {An introduction to optimal control},
journal = {Contrôle Non Linéaire et Applications}
}

@book{intro-automata,
author = {Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.},
title = {Introduction to Automata Theory, Languages, and Computation (3rd Edition)},
year = {2006},
isbn = {0321455363},
publisher = {Addison-Wesley Longman Publishing Co., Inc.},
address = {USA}
}

@article{BLOEM20073,
title = {Specify, Compile, Run: Hardware from PSL},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {190},
number = {4},
pages = {3-16},
year = {2007},
note = {Proceedings of the Workshop on Compiler Optimization meets Compiler Verification (COCV 2007)},
issn = {1571-0661},
doi = {https://doi.org/10.1016/j.entcs.2007.09.004},
url = {https://www.sciencedirect.com/science/article/pii/S157106610700583X},
author = {Roderick Bloem and Stefan Galler and Barbara Jobstmann and Nir Piterman and Amir Pnueli and Martin Weiglhofer},
keywords = {temporal logic, synthesis, games, binary decision diagrams},
}

@InProceedings{W08,
author="Thomas, Wolfgang",
editor="Geffert, Viliam
and Karhum{\"a}ki, Juhani
and Bertoni, Alberto
and Preneel, Bart
and N{\'a}vrat, Pavol
and Bielikov{\'a}, M{\'a}ria",
title="Optimizing Winning Strategies in Regular Infinite Games ",
booktitle="SOFSEM 2008: Theory and Practice of Computer Science",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="118--123",
isbn="978-3-540-77566-9"
}


@article{CGMT13,
author = {Cimatti, Alessandro and Griggio, Alberto and Mover, Sergio and Tonetta, Stefano},
year = {2013},
month = {10},
pages = {165-168},
title = {Parameter synthesis with IC3},
journal = {2013 Formal Methods in Computer-Aided Design, FMCAD 2013},
doi = {10.1109/FMCAD.2013.6679406}
}

@InProceedings{CCD14,
author="Cavada, Roberto and Cimatti, Alessandro and Dorigatti, Michele and Griggio, Alberto and Mariotti, Alessandro and Micheli, Andrea and Mover, Sergio and Roveri, Marco and Tonetta, Stefano",
editor="Biere, Armin
and Bloem, Roderick",
title="The nuXmv Symbolic Model Checker",
booktitle="Computer Aided Verification",
year="2014",
publisher="Springer International Publishing",
address="Cham",
pages="334--342",
isbn="978-3-319-08867-9"
}

@misc{HWWZ14,
      title={Optimal Strategy Synthesis for Request-Response Games}, 
      author={Florian Horn and Wolfgang Thomas and Nico Wallmeier and Martin Zimmermann},
      year={2014},
      eprint={1406.4648},
      archivePrefix={arXiv},
      primaryClass={cs.FL}
}

@misc{jacobs2014extended,
    title={Extended AIGER Format for Synthesis}, 
    author={Swen Jacobs},
    year={2014},
    eprint={1405.5793},
    archivePrefix={arXiv},
    primaryClass={cs.OH},
    doi={10.48550/arXiv.1405.5793}
}

@article{jacobs2015,
  author       = {Swen Jacobs and
                  Roderick Bloem and
                  Romain Brenguier and
                  R{\"{u}}diger Ehlers and
                  Timotheus Hell and
                  Robert K{\"{o}}nighofer and
                  Guillermo A. P{\'{e}}rez and
                  Jean{-}Fran{\c{c}}ois Raskin and
                  Leonid Ryzhyk and
                  Ocan Sankur and
                  Martina Seidl and
                  Leander Tentrup and
                  Adam Walker},
  title        = {The First Reactive Synthesis Competition {(SYNTCOMP} 2014)},
  journal      = {CoRR},
  volume       = {abs/1506.08726},
  year         = {2015},
  url          = {http://arxiv.org/abs/1506.08726},
  eprinttype    = {arXiv},
  eprint       = {1506.08726},
  timestamp    = {Thu, 08 Apr 2021 08:40:39 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/JacobsBBEHKPRRS15.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{ELNR2015, 
    title={SAT-Based Strategy Extraction in Reachability Games}, 
    volume={29}, 
    url={https://ojs.aaai.org/index.php/AAAI/article/view/9752}, 
    DOI={10.1609/aaai.v29i1.9752}, 
    number={1}, 
    journal={Proceedings of the AAAI Conference on Artificial Intelligence}, 
    author={Een, Niklas and Legg, Alexander and Narodytska, Nina and Ryzhyk, Leonid}, 
    year={2015},
    month={Mar.}
}

@book{principles-cps,
author = {Alur, Rajeev},
title = {Principles of Cyber-Physical Systems},
year = {2015},
isbn = {0262029111},
publisher = {The MIT Press}
}

@misc{infinite-games,
    author = {Martin, Zimmermann and Felix, Klein and Alexander, Weinert},
    title = {Infinite Games},
    url = {https://www.react.uni-saarland.de/teaching/infinite-games-16/lecture-notes.pdf},
    year = {2016}
}

@article{CS19,
author = {Belta, Calin and Sadraddini, Sadra},
title = {Formal Methods for Control Synthesis: An Optimization Perspective},
journal = {Annual Review of Control, Robotics, and Autonomous Systems},
volume = {2},
number = {1},
pages = {115-140},
year = {2019},
doi = {10.1146/annurev-control-053018-023717},
URL = {https://doi.org/10.1146/annurev-control-053018-023717}
}

@article{geatti-2020-08,
author       = {Cimatti, Alessandro and Geatti, Luca and Gigante, Nicola and Montanari, Angelo and Tonetta, Stefano},
title        = {Reactive Synthesis from Extended Bounded Response {LTL} Specifications},
journal      = {CoRR},
volume       = {abs/2008.05335},
year         = {2020},
month        = {08},
url          = {https://arxiv.org/abs/2008.05335},
eprinttype   = {arXiv},
eprint       = {2008.05335},
timestamp    = {Sun, 16 Aug 2020 17:19:29 +0200},
biburl       = {https://dblp.org/rec/journals/corr/abs-2008-05335.bib},
bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{geatti-2021-09,
author = {Cimatti, Alessandro and Geatti, Luca and Gigante, Nicola and Montanari, Angelo and Tonetta, Stefano},
year = {2021},
month = {09},
pages = {152-165},
title = {Expressiveness of Extended Bounded Response LTL},
volume = {346},
journal = {Electronic Proceedings in Theoretical Computer Science},
doi = {10.4204/EPTCS.346.10}
}

@article{geatti-2021-11,
author = {Cimatti, Alessandro and Geatti, Luca and Gigante, Nicola and Montanari, Angelo and Tonetta, Stefano},
year = {2021},
month = {11},
pages = {1-49},
title = {Extended bounded response LTL: a new safety fragment for efficient reactive synthesis},
journal = {Formal Methods in System Design},
doi = {10.1007/s10703-021-00383-3}
}

@inproceedings{GAMS2020,
author = {De Giacomo, Giuseppe and Di Stasio, Antonio and Vardi, Moshe and Zhu, Shufang},
year = {2020},
month = {07},
pages = {},
title = {Two-Stage Technique for LTLf Synthesis Under LTL Assumptions},
booktitle={Proceedings of KR 2020},
doi = {10.24963/kr.2020/31}
}

@inproceedings{BGS2021,
author = {Aminof, Benjamin and De Giacomo, Giuseppe and Rubin, Sasha},
year = {2021},
month = {08},
pages = {1766-1772},
title = {Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up},
booktitle={Proceedings of IJCAI 2021},
doi = {10.24963/ijcai.2021/243}
}

@misc{dhiraj-2023,
author = {Ciesielski, Maciej and Jabir, Abusaleh and Pradhan, Dhiraj},
year = {2023},
month = {11},
pages = {},
title = {Canonical Graph-based Representations for Verification of Logic and Arithmetic Designs}
}