Skip to main content
SpringerLink
Log in

Complexity of Model Checking by Iterative Improvement: The Pseudo-Boolean Framework

  • Conference paper
Perspectives of System Informatics (PSI 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2890))

Abstract

We present several new algorithms as well as new lower and upper bounds for optimizing functions underlying infinite games pertinent to computer-aided verification.

Supported by Swedish Research Council Grants “Infinite Games: Algorithms and Complexity” and “Interior-Point Methods for Infinite Games”.

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aarts, E., Lenstra, J.K. (eds.): Local Search in Combinatorial Optimization. John Wiley & Sons, Chichester (1997)

    MATH  Google Scholar 

  2. Björklund, H., Petersson, V., Vorobyov, S.: Experiments with iterative improvement algorithms on completely unimodal hypercubes. Technical Report 2001-017, Information Technology/Uppsala University (September 2001), http://www.it.uu.se/research/reports/

  3. Björklund, H., Sandberg, S.: Algorithms for combinatorial optimization and games adapted from linear programming. In: ten Cate, B. (ed.) Proceedings of the Eighth ESSLLI Student Session (2003) (to appear)

    Google Scholar 

  4. Björklund, H., Sandberg, S., Vorobyov, S.: An experimental study of algorithms for completely unimodal optimization. Technical Report 2002- 030, Department of Information Technology, Uppsala University (October 2002), http://www.it.uu.se/research/reports/

  5. Björklund, H., Sandberg, S., Vorobyov, S.: Optimization on completely unimodal hypercubes. Technical Report 018, Uppsala University / Information Technology (May 2002), http://www.it.uu.se/research/reports/

  6. Björklund, H., Sandberg, S., Vorobyov, S.: A discrete subexponential algorithm for parity games. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 663–674. Springer, Heidelberg (2003); Full preliminary version: TR-2002-026, Department of Information Technology, Uppsala University (September 2002)

    Chapter  Google Scholar 

  7. Björklund, H., Sandberg, S., Vorobyov, S.: On combinatorial structure and algorithms for parity games. Technical Report 2003-002, Department of Information Technology, Uppsala University (January 2003), http://www.it.uu.se/research/reports/

  8. Björklund, H., Sandberg, S., Vorobyov, S.: Randomized subexponential algorithms for parity games. Technical Report 2003-019, Department of Information Technology, Uppsala University (April 2003), http://www.it.uu.se/research/reports/

  9. Boros, E., Hammer, P.L.: Pseudo-boolean optimization. Technical Report RRR 48-2001, RUTCOR Rutger Center for Operations Research (2001)

    Google Scholar 

  10. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  11. Condon, A.: The complexity of stochastic games. Information and Computation 96, 203–224 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  12. Condon, A.: On algorithms for simple stochastic games. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 13, 51–71 (1993)

    MathSciNet  Google Scholar 

  13. Emerson, E.A.: Model checking and the Mu-calculus. In: Immerman, N., Kolaitis, P.G. (eds.) DIMACS. Series in Discrete Mathematics, vol. 31, pp. 185–214 (1997)

    Google Scholar 

  14. Emerson, E.A., Jutla, C.S.: Tree automata, μ-calculus and determinacy. In: Annual IEEE Symp. on Foundations of Computer Science, pp. 368–377 (1991)

    Google Scholar 

  15. Gärtner, B.: A subexponential algorithm for abstract optimization problems. SIAM Journal on Computing 24, 1018–1035 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  16. Gärtner, B.: Combinatorial linear programming: Geometry can help. In: Rolim, J.D.P., Serna, M., Luby, M. (eds.) RANDOM 1998. LNCS, vol. 1518, pp. 82–96. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  17. Gärtner, B.: The random-facet simplex algorithm on combinatorial cubes. Random Structures and Algorithms 20(3), 353–381 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  18. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata Logics and Infinite Games. A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  19. Hammer, P.L., Simeone, B., Liebling, T.M., De Werra, D.: From linear separability to unimodality: a hierarchy of pseudo-boolean functions. SIAM J. Disc. Math. 1(2), 174–184 (1988)

    Article  MATH  Google Scholar 

  20. Hansen, P., Jaumard, B., Mathon, V.: Constrained nonlinear 0-1 programming (state-of-the-art survey). ORSA Journal on Computing 5(2), 97–119 (1993)

    MATH  MathSciNet  Google Scholar 

  21. Hoffman, J., Karp, R.M.: On nonterminating stochastic games. Management Science 12(5), 359–370 (1966)

    Article  MathSciNet  Google Scholar 

  22. Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  23. Kalai, G.: A subexponential randomized simplex algorithm. In: 24th ACM STOC, pp. 475–482 (1992)

    Google Scholar 

  24. Ludwig, W.: A subexponential randomized algorithm for the simple stochastic game problem. Information and Computation 117, 151–155 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  25. Mansour, Y., Singh, S.: On the complexity of policy iteration. In: Uncertainty in Artificial Intelligence 1999 (1999)

    Google Scholar 

  26. Matoušek, J., Sharir, M., Welzl, M.: A subexponential bound for linear programming. In: 8th ACM Symp. on Computational Geometry, pp. 1–8 (1992)

    Google Scholar 

  27. Papadimitriou, C.: Algorithms, games, and the internet. In: ACM Annual Symposium on Theory of Computing, July 2001, pp. 749–753. ACM, New York (2001)

    Google Scholar 

  28. Petersson, V., Vorobyov, S.: A randomized subexponential algorithm for parity games. Nordic Journal of Computing 8, 324–345 (2001)

    MATH  MathSciNet  Google Scholar 

  29. Sharir, M., Welzl, E.: A combinatorial bound for linear programming and related problems. In: Finkel, A., Jantzen, M. (eds.) STACS 1992. LNCS, vol. 577, pp. 569–579. Springer, Heidelberg (1992)

    Google Scholar 

  30. Tovey, C.A.: Local improvement on discrete structures. In: Aarts, E., Lenstra, J.K. (eds.) Local Search in Combinatorial Optimization, pp. 57–89. John Wiley & Sons, Chichester (1997)

    Google Scholar 

  31. Vöge, J., Jurdziński, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  32. Wiedemann, D.: Unimodal set-functions. Congressus Numerantium 50, 165–169 (1985)

    MathSciNet  Google Scholar 

  33. Williamson Hoke, K.: Completely unimodal numberings of a simple polytope. Discrete Applied Mathematics 20, 69–81 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  34. Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158, 343–359 (1996)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Information Technology Department, Uppsala University, Box 337, 751 05, Uppsala, Sweden

    Henrik Björklund, Sven Sandberg & Sergei Vorobyov

Authors
  1. Henrik Björklund
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sven Sandberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sergei Vorobyov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technische Universität München, Germany

    Manfred Broy

  2. A.P. Ershov Institute of Informatics Systems, Siberian Branch of Russian Academy of Sciences, 630090, Novosibirsk, Russia

    Alexandre V. Zamulin

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Björklund, H., Sandberg, S., Vorobyov, S. (2004). Complexity of Model Checking by Iterative Improvement: The Pseudo-Boolean Framework. In: Broy, M., Zamulin, A.V. (eds) Perspectives of System Informatics. PSI 2003. Lecture Notes in Computer Science, vol 2890. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39866-0_38

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-39866-0_38

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20813-6

  • Online ISBN: 978-3-540-39866-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation