×

Index appearance record for transforming Rabin automata into parity automata. (English) Zbl 1452.68108

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 I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 443-460 (2017).
Summary: Transforming deterministic \(\omega \)-automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.
For the entire collection see [Zbl 1360.68015].

MSC:

68Q45 Formal languages and automata

Software:

PGSolver; Rabinizer; SPOT
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log. 5(1), 1-25 (2004) · Zbl 1366.03181 · doi:10.1145/963927.963928
[2] 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
[3] Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411-420 (1999)
[4] Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, É., Xu, L.: Spot 2.0 — a framework for LTL and \(\omega \)-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122-129. Springer, Heidelberg (2016). doi:10.1007/978-3-319-46520-3_8 · doi:10.1007/978-3-319-46520-3_8
[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, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_13 · Zbl 1368.68233 · doi:10.1007/978-3-319-08867-9_13
[6] Finkbeiner, B., Ehlers, R., Kupriyanov, A: Automata, games, and verification (2011). https://www.react.uni-saarland.de/teaching/automata-games-verification-11/downloads/ps9.pdf. Accessed 30 Aug 2016
[7] Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182-196. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_15 · Zbl 1258.68077 · doi:10.1007/978-3-642-04761-9_15
[8] Gurevich, T., Harrington, L.: Trees, automata, and games. In: STOC, pp. 60-65 (1982)
[9] Klein, J., Baier, C.: Experiments with deterministic \(\omega \)-automata for formulas of linear temporal logic. Theoret. Comput. Sci. 363(2), 182-195 (2006) · Zbl 1153.03016 · doi:10.1016/j.tcs.2006.07.022
[10] 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
[11] 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, Heidelberg (2014). doi:10.1007/978-3-319-11936-6_17 · Zbl 1448.68268 · doi:10.1007/978-3-319-11936-6_17
[12] Křetínský, J., Meggendorfer, T., Waldmann, C., Weininger, M.: Index appearance record for transforming Rabin automata into parity automata. Technical report abs/1701.05738, arXiv.org (2017)
[13] Orna Kupferman and Moshe Y. Vardi. Safraless decision procedures. In FOCS, pp. 531-542, (2005)
[14] Löding, C.: Optimal bounds for transformations of \(\omega \)-automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 97-109. Springer, Heidelberg (1999). doi:10.1007/3-540-46691-6_8 · Zbl 0961.68074 · doi:10.1007/3-540-46691-6_8
[15] Löding, C.: Methods for the transformation of automata: complexity and connection to second order logic. Master’s thesis, Institute of Computer Science and Applied Mathematics, Christian-Albrechts-University of Kiel, Germany (1999)
[16] Meyer, P.J., Luttenberger, M.: Solving mean-payoff games on the GPU. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 262-267. Springer, Heidelberg (2016). doi:10.1007/978-3-319-46520-3_17 · doi:10.1007/978-3-319-46520-3_17
[17] Piterman, N.: From nondeterministic Buchi and Streett automata to deterministic parity automata. In: LICS, pp. 255-264 (2006) · Zbl 1125.68067
[18] Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46-57 (1977)
[19] 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
[20] Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179-190 (1989) · Zbl 0686.68015
[21] Redziejowski, R.R.: An improved construction of deterministic omega-automaton using derivatives. Fundam. Inform. 119(3-4), 393-406 (2012) · Zbl 1279.68173
[22] Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319-327 (1988)
[23] Safra, S.: Exponential determinization for omega-automata with strong-fairness acceptance condition (extended abstract). In: STOC, pp. 275-282 (1992)
[24] Schwoon, S.: Determinization and complementation of Streett automata. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata Logics, and Infinite Games. LNCS, vol. 2500, pp. 79-91. Springer, Heidelberg (2002). doi:10.1007/3-540-36387-4_5 · Zbl 1021.68047 · doi:10.1007/3-540-36387-4_5
[25] Schewe, S.: Tighter bounds for the determinisation of Büchi automata. In: Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 167-181. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00596-1_13 · Zbl 1234.68239 · doi:10.1007/978-3-642-00596-1_13
[26] Tsai, M. · doi:10.1007/978-3-642-39799-8_62
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.