Abstract
In this work we study Good-For-Games (GFG) automata over \(\omega \)-words: non-deterministic automata where the non-determinism can be resolved by a strategy depending only on the prefix of the \(\omega \)-word read so far. These automata retain some advantages of determinism: they can be composed with games and trees in a sound way, and inclusion \(\mathrm {L} (\mathcal {A})\supseteq \mathrm {L} (\mathcal {B})\) can be reduced to a parity game over \(\mathcal {A} \times \mathcal {B} \) if \(\mathcal {A} \) is GFG. Therefore, they could be used to some advantage in verification, for instance as solutions to the synthesis problem.
The main results of this work answer the question whether parity GFG automata actually present an improvement in terms of state-complexity (the number of states) compared to the deterministic ones. We show that a frontier lies between the Büchi condition, where GFG automata can be determinised with only quadratic blow-up in state-complexity; and the co-Büchi condition, where GFG automata can be exponentially smaller than any deterministic automaton for the same language. We also study the complexity of deciding whether a given automaton is GFG.
Research funded by ANR/DGA project Cx (ref. ANR-13-ASTR-0006); and by fondation STAE project BRIefcaSE. The second author has been supported by Poland’s National Science Centre grant (decision DEC-2014-13/B/ST6/03595).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boker, U., Kuperberg, D., Kupferman, O., Skrzypczak, M.: Nondeterminism in the presence of a diverse or unknown future. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 89–100. Springer, Heidelberg (2013)
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society 138, 295–311 (1969)
Colcombet, T.: The theory of stabilisation monoids and regular cost functions. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol. 5556, pp. 139–150. Springer, Heidelberg (2009)
Colcombet, T.: Forms of determinism for automata (invited talk). In: STACS, pp. 1–23 (2012)
Henzinger, T.A., Piterman, N.: Solving games without determinization. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395–410. Springer, Heidelberg (2006)
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, Heidelberg (2014)
McNaughton, R.: Testing and generating infinite sequences by a finite automaton. Information and Control 9(5), 521–530 (1966)
Rabin, M.O.: Automata on Infinite Objects and Church’s Problem. American Mathematical Society, Boston (1972)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kuperberg, D., Skrzypczak, M. (2015). On Determinisation of Good-for-Games Automata. In: Halldórsson, M., Iwama, K., Kobayashi, N., Speckmann, B. (eds) Automata, Languages, and Programming. ICALP 2015. Lecture Notes in Computer Science(), vol 9135. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-47666-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-662-47666-6_24
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-47665-9
Online ISBN: 978-3-662-47666-6
eBook Packages: Computer ScienceComputer Science (R0)