Optimal translation of LTL to limit deterministic automata. (English) Zbl 1452.68121
Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part II. Berlin: Springer. Lect. Notes Comput. Sci. 10206, 113-129 (2017).
Summary: A crucial step in model checking Markov Decision Processes (MDP) is to translate the LTL specification into automata. Efforts have been made in improving deterministic automata construction for LTL but such translations are double exponential in the worst case. For model checking MDPs though limit deterministic automata suffice. Recently it was shown how to translate the fragment \(\mathrm{LTL}\setminus GU\) to exponential sized limit deterministic automata which speeds up the model checking problem by an exponential factor for that fragment. In this paper we show how to construct limit deterministic automata for full LTL. This translation is not only efficient for \(\mathrm{LTL}\setminus GU\) but for a larger fragment \(\mathrm{LTL}_{\mathrm{D}}\) which is provably more expressive. We show experimental results demonstrating that our construction yields smaller automata when compared to state of the art techniques that translate LTL to deterministic and limit deterministic automata.
For the entire collection see [Zbl 1360.68016].
For the entire collection see [Zbl 1360.68016].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B44 | Temporal logic |
| 68Q45 | Formal languages and automata |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
References:
| [1] | Büchifier. http://kini2.web.engr.illinois.edu/buchifier/ |
| [2] | Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Logic 5(1), 1-25 (2004) · Zbl 1366.03181 · doi:10.1145/963927.963928 |
| [3] | Babiak, T., Blahoudek, F., Křetínský, M., Strejček, J.: Effective translation of LTL to deterministic Rabin automata: beyond the (F,G)-fragment. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 24-39. Springer, Heidelberg (2013). doi:10.1007/978-3-319-02444-8_4 · Zbl 1414.03003 · doi:10.1007/978-3-319-02444-8_4 |
| [4] | Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857-907 (1995) · Zbl 0885.68109 · doi:10.1145/210332.210339 |
| [5] | Esparza, J., Křetínský, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192-208. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_13 · Zbl 1368.68233 · doi:10.1007/978-3-319-08867-9_13 |
| [6] | Hahn, E.M., Li, G., Schewe, S., Turrini, A., Zhang, L.: Lazy probabilistic model checking without determinisation. In: CONCUR, pp. 354-367 (2015) · Zbl 1374.68290 |
| [7] | Henzinger, T.A., Piterman, N.: Solving games without determinization. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395-410. Springer, Heidelberg (2006). doi:10.1007/11874683_26 · Zbl 1225.68118 · doi:10.1007/11874683_26 |
| [8] | Kini, D., Viswanathan, M.: Limit deterministic and probabilistic automata for \(\text{ LTL }{\setminus }\text{ GU } \). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 628-642. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_57 · Zbl 1420.68132 · doi:10.1007/978-3-662-46681-0_57 |
| [9] | Kini, D., Viswanathan, M.: Optimal translation of LTL to limit deterministic automata. Technical report, University of Illinois at Urbana-Champaign (2017). http://hdl.handle.net/2142/95004 |
| [10] | Klein, J., Baier, C.: Experiments with deterministic \(\omega \)-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182-195 (2006) · Zbl 1153.03016 · doi:10.1016/j.tcs.2006.07.022 |
| [11] | Klein, J., Müller, D., Baier, C., Klüppelholz, S.: Are good-for-games automata good for probabilistic model checking? In: Dediu, A.-H., Martín-Vide, C., Sierra-Rodríguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 453-465. Springer, Cham (2014). doi:10.1007/978-3-319-04921-2_37 · Zbl 1408.68093 · doi:10.1007/978-3-319-04921-2_37 |
| [12] | Komárková, Z., Křetínský, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 235-241. Springer, Cham (2014). doi:10.1007/978-3-319-11936-6_17 · Zbl 1448.68268 · doi:10.1007/978-3-319-11936-6_17 |
| [13] | Křetínský, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7-22. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_7 · doi:10.1007/978-3-642-31424-7_7 |
| [14] | Křetínský, J., Garza, R.L.: Rabinizer 2: small deterministic automata for \(\text{ LTL }{\setminus }\text{ GU } \). In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 446-450. Springer, Heidelberg (2013). doi:10.1007/978-3-319-02444-8_32 · Zbl 1410.68231 · doi:10.1007/978-3-319-02444-8_32 |
| [15] | Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585-591. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_47 · doi:10.1007/978-3-642-22110-1_47 |
| [16] | Morgenstern, A., Schneider, K.: From LTL to symbolically represented deterministic automata. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 279-293. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78163-9_24 · Zbl 1138.68454 · doi:10.1007/978-3-540-78163-9_24 |
| [17] | Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: VMCAI, pp. 279-293 (2006) |
| [18] | Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364-380. Springer, Heidelberg (2005). doi:10.1007/11609773_24 · Zbl 1176.68126 · doi:10.1007/11609773_24 |
| [19] | Puterman, M.L.: Markov Decision Processes. Wiley, Hoboken (1994) · Zbl 0829.90134 · doi:10.1002/9780470316887 |
| [20] | Sickert, S., Esparza, J., Jaax, S., Křetínský, J.: Limit-deterministic Büchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 312-332. Springer, Cham (2016). doi:10.1007/978-3-319-41540-6_17 · Zbl 1411.68054 · doi:10.1007/978-3-319-41540-6_17 |
| [21] | Sickert, S., Křetínský, J.: MoChiBA: probabilistic LTL model checking using limit-deterministic Büchi automata. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 130-137. Springer, Cham (2016). doi:10.1007/978-3-319-46520-3_9 · doi:10.1007/978-3-319-46520-3_9 |
| [22] | Vardi, M., Wolper, P., Sistla, A.P.: Reasoning about infinite computation paths. In: FOCS (1983) |
| [23] | Vardi, M. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
