Abstract
The translation of LTL formulas to nondeterministic automata involves an exponential blow-up, and so does the translation of nondeterministic automata to deterministic ones. This yields a \(2^{2^{O(n)}}\) upper bound for the translation of LTL to deterministic automata. A lower bound for the translation was studied in [KV05a], which describes a \(2^{2^{\Omega(\sqrt{n})}}\) lower bound, leaving the problem of the exact blow-up open. In this paper we solve this problem and tighten the lower bound to \(2^{2^{\Omega(n)}}\).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Boker, U., Kupferman, O.: Co-ing Büchi made tight and helpful. In: Proc. 24th IEEE Symp. on Logic in Computer Science, pp. 245–254 (2009)
Boker, U., Kupferman, O., Rosenberg, A.: Alternation Removal in Büchi Automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 76–87. Springer, Heidelberg (2010)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science. 1960, pp. 1–12. Stanford University Press, Standford (1962)
Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the Association for Computing Machinery 28(1), 114–133 (1981)
Dam, M.: CTL ⋆ and ECTL ⋆ as fragments of the modal μ-calculus. Theoretical Computer Science 126, 77–96 (1994)
Etessami, K., Holzmann, G.J.: Optimizing büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)
Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: Proc. 16th ACM Symp. on Theory of Computing, pp. 14–24 (1984)
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)
Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3–18. Chapman and Hall, Boca Raton (1995)
Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic ω-automata vis-a-vis deterministic Büchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994)
Kupferman, O.: Avoiding determinization. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 243–254 (2006)
Kupferman, O., Vardi, M.Y.: From linear time to branching time. ACM Transactions on Computational Logic 6(2), 273–294 (2005)
Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, pp. 531–540 (2005)
Landweber, L.H.: Decision problems for ω–automata. Mathematical Systems Theory 3, 376–384 (1969)
Miyano, S., Hayashi, T.: Alternating nite automata on!-words. Theoretical Computer Science 32, 321–330 (1984)
Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 255–264. IEEE Press, Los Alamitos (2006)
Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 179–190 (1989)
Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Transaction of the AMS 141, 1–35 (1969)
Safra, S.: On the complexity of ω-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 319–327 (1988)
Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Rosenberg, A. (2011). The Blow-Up in Translating LTL to Deterministic Automata. In: van der Meyden, R., Smaus, JG. (eds) Model Checking and Artificial Intelligence. MoChArt 2010. Lecture Notes in Computer Science(), vol 6572. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20674-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-20674-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20673-3
Online ISBN: 978-3-642-20674-0
eBook Packages: Computer ScienceComputer Science (R0)