Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2009: Automated Technology for Verification and Analysis pp 228–243Cite as

On Minimal Odd Rankings for Büchi Complementation

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 5799))

Abstract

We study minimal odd rankings (as defined by Kupferman and Vardi[KV01]) for run-DAGs of words in the complement of a nondeterministic Büchi automaton. We present an optimized version of the ranking based complementation construction of Friedgut, Kupferman and Vardi[FKV06] and Schewe’s[Sch09] variant of it, such that every accepting run of the complement automaton assigns a minimal odd ranking to the corresponding run-DAG. This allows us to determine minimally inessential ranks and redundant slices in ranking-based complementation constructions. We exploit this to reduce the size of the complement Büchi automaton by eliminating all redundant slices. We demonstrate the practical importance of this result through a set of experiments using the NuSMV model checker.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. 1960 Int. Congr. for Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford Univ. Press, Stanford (1962)

    Google Scholar 

  2. Doyen, L., Raskin, J.-F.: Antichains for the automata based approach to model checking. Logical Methods in Computer Science 5, 1–20 (2009)

    Article  MathSciNet  Google Scholar 

  3. Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. Int. J. Found. Comput. Sci. 17(4), 851–868 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  4. Fogarty, S., Vardi., M.Y.: Büchi complementation and size-change termination. In: Proc. TACAS, pp. 16–30 (2009)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. Karmarkar, H., Chakraborty, S.: On minimal odd rankings for Büchi complementation (May 2009), http://www.cfdvs.iitb.ac.in/reports/index.php

  7. Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: Proc. 32nd IEEE FOCS, San Juan, pp. 358–367 (1991)

    Google Scholar 

  8. Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic 2(3), 408–429 (2001)

    Article  MathSciNet  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Löding, C.: Optimal bounds for transformations of ω-automata. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988)

    Google Scholar 

  12. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic Parity automata. Logical Methods in Computer Science 3(3:5), 1–217 (2007)

    MathSciNet  Google Scholar 

  13. Safra, S.: On the complexity of ω-automata. In: Proc. 29th IEEE FOCS, pp. 319–327 (1988)

    Google Scholar 

  14. Schewe, S.: Büchi complementation made tight. In: Proc. STACS, pp. 661–672 (2009)

    Google Scholar 

  15. Prasad Sistla, A., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  16. Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Chan, W.-C., Luo, C.-J.: Goal extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 346–350. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Vardi, M.Y.: The Büchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12–22. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Yan, Q.: Lower bounds for complementation of omega-automata via the full automata technique. Logical Methods in Computer Science 4(1), 1–20 (2008)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology Bombay,  

    Hrishikesh Karmarkar & Supratik Chakraborty

Authors
  1. Hrishikesh Karmarkar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Supratik Chakraborty
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute of Software Technology (UNI-IIST), United Nations University, Macao, China

    Zhiming Liu

  2. Department of Computer Science, Aalborg University, 9220, Aalborg, Denmark

    Anders P. Ravn

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Karmarkar, H., Chakraborty, S. (2009). On Minimal Odd Rankings for Büchi Complementation. In: Liu, Z., Ravn, A.P. (eds) Automated Technology for Verification and Analysis. ATVA 2009. Lecture Notes in Computer Science, vol 5799. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04761-9_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04761-9_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04760-2

  • Online ISBN: 978-3-642-04761-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation