@inproceedings(Babiak2015HOA,
 author       = {Tom{\'a}{\v{s}} Babiak and Franti{\v{s}}ek Blahoudek and Duret-Lutz, Alexandre and Joachim Klein and K{\v{r}}et{\'i}nsk{\'y}, Jan and David M{\"u}ller and David Parker and Strej{\v{c}}ek, Jan},
 year         = {2015},
 title        = {The Hanoi Omega-Automata Format},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer Intl. Publishing},
 address      = {Cham},
 pages        = {479--486},
 doi          = {10.1007/978-3-319-21690-4\_31},
)
@incollection(babiak2013ltl3dra,
 author       = {Tom{\'a}{\v{s}} Babiak and Franti{\v{s}}ek Blahoudek and K{\v{r}}et{\'\i}nsk{\`y}, Mojm{\'\i}r and Strej{\v{c}}ek, Jan},
 year         = {2013},
 title        = {Effective translation of {LTL} to deterministic Rabin automata: Beyond the (F, G)-fragment},
 booktitle    = {Automated Technology for Verification and Analysis},
 publisher    = {Springer},
 pages        = {24--39},
 doi          = {10.1007/10722167\_21},
)
@inproceedings(bacchus1996rewarding,
 author       = {Fahiem Bacchus and Craig Boutilier and Adam Grove},
 year         = {1996},
 title        = {Rewarding Behaviors},
 booktitle    = {Proc. of the Thirteenth Natl. Conf. on Artificial Intelligence - Volume 2},
 series       = {AAAI’96},
 publisher    = {AAAI Press},
 pages        = {1160–1167},
)
@inproceedings(bacchus1997structured,
 author       = {Fahiem Bacchus and Craig Boutilier and Adam Grove},
 year         = {1997},
 title        = {Structured Solution Methods for Non-Markovian Decision Processes},
 booktitle    = {Proc. of the (AAAI-97) and (IAAI-97)},
 series       = {AAAI’97/IAAI’97},
 publisher    = {AAAI Press},
 pages        = {112–117},
)
@book(baier2008principles,
 author       = {Christel Baier and Joost-Pieter Katoen},
 year         = {2008},
 title        = {Principles of Model Checking},
 publisher    = {The MIT Press},
)
@inproceedings(brafman2018ltlf,
 author       = {Ronen I. Brafman and {De Giacomo}, Giuseppe and Fabio Patrizi},
 year         = {2018},
 title        = {LTLf/LDLf Non-Markovian Rewards},
 booktitle    = {Proc. of (AAAI-18), (IAAI-18), and (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018},
 publisher    = {{AAAI} Press},
 pages        = {1771--1778},
)
@inproceedings(camacho2017nonmarkovian,
 author       = {Alberto Camacho and Oscar Chen and Scott Sanner and Sheila A. McIlraith},
 year         = {2017},
 title        = {Non-Markovian Rewards Expressed in LTL: Guiding Search Via Reward Shaping},
 booktitle    = {SOCS},
)
@article(Courcoubetis1995complexity,
 author       = {Costas Courcoubetis and Mihalis Yannakakis},
 year         = {1995},
 title        = {The Complexity of Probabilistic Verification},
 journal      = {J. ACM},
 volume       = {42},
 number       = {4},
 pages        = {857--907},
 doi          = {10.1145/210332.210339},
)
@phdthesis(de1997formal,
 author       = {De Alfaro, Luca},
 year         = {1998},
 title        = {Formal Verification of Probabilistic Systems},
 address      = {Stanford, CA, USA},
)
@inproceedings(de2013linear,
 author       = {De Giacomo, Giuseppe and Moshe Y Vardi},
 year         = {2013},
 title        = {Linear Temporal Logic and Linear Dynamic Logic on Finite Traces.},
 booktitle    = {Intl. Joint Conf. on Artificial Intelligence (IJCAI)},
 volume       = {13},
 pages        = {854--860},
)
@inproceedings(de2015synthesis,
 author       = {De Giacomo, Giuseppe and Moshe Y Vardi},
 year         = {2015},
 title        = {Synthesis for {LTL} and {LDL} on Finite Traces},
 booktitle    = {Intl. Joint Conf. on Artificial Intelligence (IJCAI)},
 volume       = {15},
 pages        = {1558--1564},
)
@inproceedings(duret2016spot,
 author       = {Duret-Lutz, Alexandre and Alexandre Lewkowicz and Amaury Fauchille and Thibaud Michaud and {\'E}tienne Renault and Laurent Xu},
 year         = {2016},
 title        = {Spot 2.0 --- a framework for {LTL} and $\omega$-automata manipulation},
 booktitle    = {Automated Technology for Verification and Analysis (ATVA'16)},
 series       = {Lecture Notes in Computer Science},
 volume       = {9938},
 publisher    = {Springer},
 pages        = {122--129},
 doi          = {10.1007/3-540-60915-6\_6},
)
@article(He:RAL:2018,
 author       = {Keliang He and Morteza Lahijanian and Lydia E Kavraki and Moshe Y Vardi},
 year         = {2018},
 title        = {Automated Abstraction of Manipulation Domains for Cost-Based Reactive Synthesis},
 journal      = {IEEE Robotics and Automation Letters},
 volume       = {4},
 number       = {2},
 pages        = {285--292},
 doi          = {10.1109/LRA.2018.2889191},
)
@inproceedings(he2019efficient,
 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    = {2019 Intl. Conf. on Robotics and Automation (ICRA)},
 organization = {IEEE},
 pages        = {8993--8999},
 doi          = {10.1109/ICRA.2019.8794170},
)
@inproceedings(He:IROS:2017,
 author       = {Keling He and Morteza Lahijanian and Lydia E. Kavraki and Moshe Y. Vardi},
 year         = {2017},
 title        = {Reactive Synthesis for Finite Tasks Under Resource Constraints},
 booktitle    = {Int. Conf. on Intelligent Robots and Systems (IROS)},
 publisher    = {IEEE},
 address      = {Vancouver, BC, Canada},
 pages        = {5326--5332},
 doi          = {10.1109/IROS.2017.8206426},
)
@inproceedings(henriksen1995mona,
 author       = {Jesper G Henriksen and Jakob Jensen and J{\o}rgensen, Michael and Nils Klarlund and Robert Paige and Theis Rauhe and Anders Sandholm},
 year         = {1995},
 title        = {Mona: Monadic second-order logic in practice},
 booktitle    = {Intl. Workshop on Tools and Algorithms for the Construction and Analysis of Systems},
 organization = {Springer},
 pages        = {89--110},
 doi          = {10.1007/3-540-60630-0\_5},
)
@inproceedings(kretinsky2018rabinizer,
 author       = {K{\v{r}}et{\'i}nsk{\'y}, Jan and Tobias Meggendorfer and Salomon Sickert and Christopher Ziegler},
 year         = {2018},
 title        = {Rabinizer 4: From LTL to Your Favourite Deterministic Automaton},
 booktitle    = {Computer Aided Verification},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {567--577},
 doi          = {10.1007/978-3-319-46520-3\_9},
)
@inproceedings(kwiatowska2011prism,
 author       = {M. Kwiatkowska and G. Norman and D. Parker},
 year         = {2011},
 title        = {{PRISM} 4.0: Verification of Probabilistic Real-time Systems},
 booktitle    = {Proc. 23rd Intl. Conf. on Computer Aided Verification (CAV'11)},
 series       = {LNCS},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {585--591},
 doi          = {10.1007/3-540-45657-0\_17},
)
@inproceedings(Li:AAAI:2019,
 author       = {Jianwen Li and Kristin Y Rozier and Geguang Pu and Yueling Zhang and Moshe Y Vardi},
 year         = {2019},
 title        = {{SAT}-Based Explicit {LTLf} Satisfiability Checking},
 booktitle    = {Proc. of the AAAI Conf. on Artificial Intelligence},
 volume       = {33},
 pages        = {2946--2953},
 doi          = {10.1007/978-3-030-25543-5\_1},
)
@inproceedings(tabajara2019partitioning,
 author       = {Martinelli Tabajara, Lucas and Y. Vardi, Moshe},
 year         = {2019},
 title        = {Partitioning Techniques in LTLf Synthesis},
 booktitle    = {Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, {IJCAI-19}},
 publisher    = {International Joint Conferences on Artificial Intelligence Organization},
 pages        = {5599--5606},
 doi          = {10.24963/ijcai.2019/777},
)
@inproceedings(pnueli1977temporal,
 author       = {Amir Pnueli},
 year         = {1977},
 title        = {The temporal logic of programs},
 booktitle    = {Foundations of Computer Science, 1977., 18th Annual Symposium on},
 organization = {IEEE},
 pages        = {46--57},
)
@inproceedings(sickert2016mochiba,
 author       = {Salomon Sickert and Kret{\'{\i}}nsk{\'{y}}, Jan},
 year         = {2016},
 title        = {MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic B{\"{u}}chi Automata},
 booktitle    = {Automated Technology for Verification and Analysis (ATVA'16)},
 series       = {Lecture Notes in Computer Science},
 volume       = {9938},
 pages        = {130--137},
 doi          = {10.1007/978-3-319-45856-4},
)
@article(thiebaux2006decision,
 author       = {Sylvie Thi\'{e}baux and Charles Gretton and John Slaney and David Price and Froduald Kabanza},
 year         = {2006},
 title        = {Decision-Theoretic Planning with Non-Markovian Rewards},
 journal      = {J. Artif. Int. Res.},
 volume       = {25},
 number       = {1},
 pages        = {17–74},
 doi          = {10.1613/jair.1676},
)
@inproceedings(Var85b,
 author       = {Moshe Y. Vardi},
 year         = {1985},
 title        = {Automatic Verification of Probabilistic Concurrent Finite State Programs},
 booktitle    = {Proceedings of the 26th Annual Symposium on Foundations of Computer Science},
 series       = {SFCS '85},
 publisher    = {IEEE Computer Society},
 address      = {USA},
 pages        = {327–338},
 doi          = {10.1109/SFCS.1985.12},
)
@misc(wells2020github,
 author       = {Andrew M. Wells},
 title        = {LTLf for PRISM},
 url          = {https://github.com/andrewmw94/ltlf_prism},
)
@inproceedings(wells2019ltlf,
 author       = {Andrew M Wells and Morteza Lahijanian and Lydia E Kavraki and Moshe Y Vardi},
 title        = {{LTLf} Synthesis on Probabilistic Systems (Online version)},
 url          = {http://www.andrewmwells.com/ltlf-synthesis-on-probabilistic-systems/},
)
@inproceedings(zhu2017symbolic,
 author       = {Shufang Zhu and Lucas M Tabajara and Jianwen Li and Geguang Pu and Moshe Y Vardi},
 year         = {2017},
 title        = {Symbolic {LTLf} synthesis},
 booktitle    = {Proc. of the 26th Intl. Joint Conf. on Artificial Intelligence},
 organization = {AAAI Press},
 pages        = {1362--1369},
)