Bibliography
============

.. role:: raw-html(raw)
   :format: html

:raw-html:`<a href="#bk08" id="bk08">[BK08]</a>`
    \C. Baier and J.-P. Katoen. *Principles of Model Checking*. MIT Press, 2008. 

:raw-html:`<a href="#kpp2005" id="kpp2005">[KPP2005]</a>`
    \Y. Kesten, N. Piterman, and A. Pnueli (2005). `Bridging the gap between fair simulation and trace inclusion <https://doi.org/10.1016/j.ic.2005.01.006>`_. *Information and Computation*, Volume 200, Issue 1, pages 35--61 

:raw-html:`<a href="#pps2006" id="pps2006">[PPS2006]</a>`
    \N. Piterman, A. Pnueli, and Y. Sa'ar (2006). `Synthesis of reactive(1) designs <https://doi.org/10.1007/11609773_24>`_. *Proc. of International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)*, pages 364--380 

:raw-html:`<a href="#bjpps12" id="bjpps12">[BJPPS12]</a>`
    \R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa'ar (2012). `Synthesis of Reactive(1) designs <http://dx.doi.org/10.1016/j.jcss.2011.08.007>`_. *Journal of Computer and System Sciences*, 78:911--938 

:raw-html:`<a href="#e10" id="e10">[E10]</a>`
    \R. Ehlers (2010). `Generalised Rabin(1) synthesis <http://arxiv.org/abs/1003.1684>`_, *CoRR*, abs/1003.1684 

:raw-html:`<a href="#fdlom16" id="fdlom16">[FDLOM16]</a>`
    \I. Filippidis, S. Dathathri, S.C. Livingston, N. Ozay, and R.M. Murray (2016). `Control design for hybrid systems with TuLiP: The temporal logic planning toolbox <https://doi.org/10.1109/CCA.2016.7587949>`_. In *Proc. of IEEE Multi-Conference on Systems and Control (MSC)*. 

:raw-html:`<a href="#ls11" id="ls11">[LS11]</a>`
    \E.A. Lee and S.A. Seshia. *Introduction to Embedded Systems - A Cyber-Physical Systems Approach*. `LeeSeshia.org <http://LeeSeshia.org>`_, 2011. 

:raw-html:`<a href="#m55" id="m55">[M55]</a>`
    \G.H. Mealy. `A Method for Synthesizing Sequential Circuits <http://dx.doi.org/10.1002/j.1538-7305.1955.tb03788.x>`_. *Bell System Technical Journal (BSTJ)*, Vol.34, No.5, pp. 1045 -- 1079, September, 1955. 

:raw-html:`<a href="#m56" id="m56">[M56]</a>`
    \E.F. Moore. `Gedanken-experiments on Sequential Machines <https://web.archive.org/web/20120216141113/http://people.mokk.bme.hu/~kornai/termeszetes/moore_1956.pdf>`_. *Annals of Mathematical Studies*, `No. 34 (Automata Studies) <http://dl.acm.org/citation.cfm?id=1096884>`_, pp 129 – 153, Princeton University Press, Princeton, N. J., 1956, ISBN: 0691079161. 

:raw-html:`<a href="#notm12" id="notm12">[NOTM12]</a>`
    \P. Nilsson, N. Ozay, U. Topcu, R.M. Murray (2012). `Temporal logic control of switched affine systems with an application in fuel balancing <http://dx.doi.org/10.1109/ACC.2012.6315141>`_. In *Proc. of 2012 American Control Conference (ACC)*. 

:raw-html:`<a href="#s12" id="s12">[S12]</a>`
    \N. Spooner (2012). `Evaluation and Benchmarking for Robot Motion Planning Problems Using TuLiP <http://resolver.caltech.edu/CaltechCDSTR:2012.007>`_. Caltech SURF Final Report. 

:raw-html:`<a href="#w10" id="w10">[W10]</a>`
    \T. Wongpiromsarn (2010). `Formal Methods for Design and Verification of Embedded Control Systems: Application to an Autonomous Vehicle <http://resolver.caltech.edu/CaltechTHESIS:05272010-153304667>`_. PhD thesis. California Institute of Technology. 

:raw-html:`<a href="#wtm12" id="wtm12">[WTM12]</a>`
    \T. Wongpiromsarn, U. Topcu, and R. Murray (2012). `Receding horizon temporal logic planning <http://dx.doi.org/10.1109/TAC.2012.2195811>`_. *IEEE Transactions on Automatic Control*, 57(11):2817--2830. 

:raw-html:`<a href="#wtoxm11" id="wtoxm11">[WTOXM11]</a>`
    \T. Wongpiromsarn, U. Topcu, N. Ozay, H. Xu, and R. Murray (2011). `TuLiP: a software toolbox for receding horizon temporal logic planning <http://dx.doi.org/10.1145/1967701.1967747>`_. In *Proc. of Hybrid Systems: Computation and Control (HSCC)*.