Abid, N., Dal-Zilio, S., Botlan, D.L.: A formal framework to specify and verify real-time properties on critical systems. Int. J. Crit. Comput.-Based Syst. 5(1/2), 4–30 (2014)
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993)
Barnat, J., et al.: DiVinE 3.0 – an explicit-state model checker for multithreaded C & C++ programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863–868. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_60
Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 164–177. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40708-6 13
Bersani, M.M., Rossi, M., San Pietro, P.: A tool for deciding the satisfiability of continuous-time metric temporal logic. Acta Inform. 53(2), 171–206 (2016)
Bloem, R., Cimatti, A., Pill, I., Roveri, M.: Symbolic implementation of alternating automata. Int. J. Found. Comput. Sci. 18(4), 727–743 (2007)
Bouyer, P., Colange, M., Markey, N.: Symbolic optimal reachability in weighted timed automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 513–530. Springer, Cham (2016). doi:10.1007/978-3-319-41528-4 28
Brihaye, T., Estiévenart, M., Geeraerts, G.: On MITL and alternating timed automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 47–61. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40229-6 4
Brihaye, T., Estiévenart, M., Geeraerts, G.: On MITL and alternating timed automata over infinite words. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 69–84. Springer, Cham (2014). doi:10.1007/978-3-319-10512-3 6
Bulychev, P.E., David, A., Larsen, K.G., Li, G.: Efficient controller synthesis for a fragment of MTL0,∞. Acta Inform. 51(3–4), 165–192 (2014)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0 29
Claessen, K., Een, N., Sterin, B.: A circuit approach to LTL model checking. In: FMCAD 2013. IEEE (2013)
De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)
Dokhanchi, A., Hoxha, B., Fainekos, G.: Formal requirement debugging for testing and verification of cyber-physical systems. Research report 1607.02549. arXiv (2016)
D’Souza, D., Matteplackel, R.: A clock-optimal hierarchical monitoring automaton construction for MITL. Research report 2013–1, IIS (2013). http://www.csa.iisc. ernet.in/TR/2013/1/lics2013-tr.pdf
Fu, J., Topcu, U.: Computational methods for stochastic control with metric interval temporal logic specifications. In: CDC 2015, pp. 7440–7447. IEEE (2015)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001). doi:10.1007/3-540-44585-4 6
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995. pp. 3–18. Chapman & Hall (1995)
Hammer, M., Knapp, A., Merz, S.: Truly on-the-fly LTL model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 191–205. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31980-1 13
Hirshfeld, Y., Rabinovich, A.M.: Logics for real time: decidability and complexity. Fundam. Informaticae 62(1), 1–28 (2004)
Hirshfeld, Y., Rabinovich, A.: An expressive temporal logic for real time. In: Královič, R., Urzyczyn, P. (eds.) MFCS 2006. LNCS, vol. 4162, pp. 492–504. Springer, Heidelberg (2006). doi:10.1007/11821069 43
Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692–707. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0 61
Karaman, S.: Optimal planning with temporal logic specifications. Master’s thesis, Massachussetts Institute of Technology (2009)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: ISTCS 1997, pp. 147–158. IEEE (1997)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transfer 1(1–2), 134–152 (1997)
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006). doi:10.1007/11867340 20
Muller, D.E., Saoudi, A., Schupp, P.E.: Alternating automata, the weak monadic theory of the tree, and its complexity. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 275–283. Springer, Heidelberg (1986). doi:10.1007/3-540-16761-7 77
Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. In: Logical Methods in Computer Science, vol. 3, no. 1 (2007)
Plaku, E., Karaman, S.: Motion planning with temporal-logic specifications: progress and challenges. AI Communications 29, 151–162 (2016)
Pnueli, A.: The temporal logic of programs. In: FOCS 1977. pp. 46–57. IEEE (1977)
Raskin, J.F., Schobbens, P.Y.: The logic of event clocks: decidability, complexity and expressiveness. J. Automata Lang. Comb. 4(3), 247–282 (1999)
Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417–431. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21437-0 31
Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231–237. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0 20
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996). doi:10.1007/3-540-60915-6 6
Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994). doi:10.1007/3-540-58468-4 191
de Wulf, M., Doyen, L., Maquet, N., Raskin, J.-F.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 63–77. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3 6
Zhou, Y., Maity, D., Baras, J.S.: Timed automata approach for motion planning using metric interval temporal logic. Research report 1603.08246. arXiv (2016)
