Abstract
The complementation problem for nondeterministic word automata has numerous applications in formal verification. In particular, the language-containment problem, to which many verification problems is reduced, involves complementation. For automata on finite words, which correspond to safety properties, complementation involves determinization. The 2n blow-up that is caused by the subset construction is justified by a tight lower bound. For Büchi automata on infinite words, which are required for the modeling of liveness properties, optimal complementation constructions are quite complicated, as the subset construction is not sufficient. From a theoretical point of view, the problem is considered solved since 1988, when Safra came up with a determinization construction for Büchi automata, leading to a 2O(nlogn) complementation construction, and Michel came up with a matching lower bound. A careful analysis, however, of the exact blow-up in Safra’s and Michel’s bounds reveals an exponential gap in the constants hiding in the O() notations: while the upper bound on the number of states in Safra’s complementary automaton is n 2n, Michel’s lower bound involves only an n! blow up, which is roughly (n/e)n. The exponential gap exists also in more recent complementation constructions. In particular, the upper bound on the number of states in the complementation construction in [KV01], which avoids determinization, is (6n)n. This is in contrast with the case of automata on finite words, where the upper and lower bounds coincides. In this work we describe an improved complementation construction for nondeterministic Büchi automata and analyze its complexity. We show that the new construction results in an automaton with at most (1.06n)n states. While this leaves the problem about the exact blow up open, the gap is now exponentially smaller. From a practical point of view, our solution enjoys the simplicity of [KV01], and results in much smaller automata.
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
Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 211–296. Springer, Heidelberg (2002)
Birget, J.C.: Partial orders on words, minimal elements of regular languages, and state complexity. Theoretical Computer Science 119, 267–291 (1993)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci., pp. 1–12. Stanford University Press, Stanford (1960)
Daniele, N., Guinchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 610–623. Springer, Heidelberg (2002)
Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)
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)
Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. Information and Computation 173(1), 64–81 (2002)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering 23(5), 279–295 (1997), Special issue on Formal Methods in Software Practice
Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, San Juan, October 1991, pp. 358–367 (1991)
Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace containment. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 381–393. Springer, Heidelberg (2003)
Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. on Computational Logic (2), 408–429 (2001)
Michel, M.: Complementation is more difficult with automata on infinite words, CNET, Paris (1988)
Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theoretical Computer Science 54, 267–276 (1987)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)
Safra, S.: On the complexity of ω-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, White Plains, October 1988, 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)
Sakoda, W., Sipser, M.: Non-determinism and the size of two-way automata. In: Proc. 10th ACM Symp. on Theory of Computing, pp. 275–286 (1978)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)
Temme, N.M.: Asymptotic estimates of stirling numbers. Stud. Appl. Math. 89, 233–243 (1993)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1-2), 72–99 (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Friedgut, E., Kupferman, O., Vardi, M.Y. (2004). Büchi Complementation Made Tighter. In: Wang, F. (eds) Automated Technology for Verification and Analysis. ATVA 2004. Lecture Notes in Computer Science, vol 3299. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30476-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-30476-0_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23610-8
Online ISBN: 978-3-540-30476-0
eBook Packages: Springer Book Archive