Abstract
The complementation of Büchi automata, required for checking automata universality, remains one of the outstanding automata-theoretic challenges in formal verification. Early constructions using a Ramsey-based argument have been supplanted by rank-based constructions with exponentially better bounds. The best rank-based algorithm for Büchi universality, by Doyen and Raskin, employs a subsumption technique to minimize the size of the working set. Separately, in the context of program termination, Lee et al. have specialized the Ramsey-based approach to size-change termination (SCT) problems. In this context, Ramsey-based algorithms have proven to be surprisingly competitive. The strongest tool, from Ben-Amram and Lee, also uses a subsumption technique, although only for the special case of SCT problems.
We extend the subsumption technique of Ben-Amram and Lee to the general case of Büchi universality problems, and experimentally demonstrate the necessity of subsumption for the scalability of the Ramsey-based approach. We then empirically compare the Ramsey-based tool to the rank-based tool of Doyen and Raskin over a terrain of random Büchi universality problems. We discover that the two algorithms exhibit distinct behavior over this problem terrain. As expected, on many of the most difficult areas the rank-based approach provides the superior tool. Surprisingly, there also exist several areas, including the area most difficult for rank-based tools, on which the Ramsey-based solver scales better than the rank-based solver. This result demonstrates the pitfalls of using worst-case complexity to evaluate algorithms. We suggest that a portfolio approach may be the best approach to checking the universality of Büchi automata.
Work supported in part by NSF grants CCF-0613889, ANI-0216467, OISE-0913807, and CCF-0728882, by BSF grant 9800096, and by gift from Intel. Proofs and additional figures available at http://www.cs.rice.edu/ vardi/papers/tacas10rj.pdf
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ben-Amram, A.M., Lee, C.S.: Program termination analysis in polynomial time. TOPLAS 29(1) (2007)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: ICLMPS (1962)
Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. In: JCSS (1974)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press/McGraw-Hill (1990)
Jones, N.D., Lee, C.S., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81–92 (2001)
Doyen, L., Raskin, J.-F.: Antichains for the automata-based approach to model-checking. LMCS 1(5), 1–20 (2009)
Devkar, A., Shoham, Y., Nudelman, E., Leyton-Brown, K., Hoos, H.: Understanding random SAT: Beyond the clauses-to-variables ratio. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258, pp. 438–452. Springer, Heidelberg (2004)
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus. In: LICS, pp. 267–278 (1986)
Fogarty, S., Vardi, M.Y.: Büchi complementation and size-change termination. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 16–30. Springer, Heidelberg (2009)
Andrew, G., McFadden, J., Leyton-Brown, K., Nudelman, E., Shoham, Y.: A portfolio approach to algorithm selection. In: IJCAI, pp. 1542–1543 (2003)
Kähler, D., Wilke, T.: Complementation, disambiguation, and determinization of Büchi automata unified. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part I. LNCS, vol. 5125, pp. 724–735. Springer, Heidelberg (2008)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(2), 408–429 (2001)
Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)
Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 149–167. Springer, Heidelberg (2007)
Safra, S.: On the complexity of ω-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 319–327 (1988)
Schewe, S.: Büchi complementation made tight. In: STACS, pp. 661–672 (2009)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 465–474. Springer, Heidelberg (1985)
Tabakov, D., Vardi, M.Y.: Model checking Büchi specifications. In: LATA (2007)
Vardi, M.Y.: Automata-theoretic model checking revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 137–150. Springer, Heidelberg (2007)
Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fogarty, S., Vardi, M.Y. (2010). Efficient Büchi Universality Checking. In: Esparza, J., Majumdar, R. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2010. Lecture Notes in Computer Science, vol 6015. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12002-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-12002-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12001-5
Online ISBN: 978-3-642-12002-2
eBook Packages: Computer ScienceComputer Science (R0)