Advertisement

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

  • Henrik Björklund
  • Sven Sandberg
  • Sergei Vorobyov
Part of the Lecture Notes in Computer Science book series (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.

Keywords

Model Check Stochastic Game Unimodal Function Tree Automaton Iterative Improvement 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aarts, E., Lenstra, J.K. (eds.): Local Search in Combinatorial Optimization. John Wiley & Sons, Chichester (1997)zbMATHGoogle Scholar
  2. 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. 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. 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. 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. 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)CrossRefGoogle Scholar
  7. 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. 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. 9.
    Boros, E., Hammer, P.L.: Pseudo-boolean optimization. Technical Report RRR 48-2001, RUTCOR Rutger Center for Operations Research (2001)Google Scholar
  10. 10.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  11. 11.
    Condon, A.: The complexity of stochastic games. Information and Computation 96, 203–224 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Condon, A.: On algorithms for simple stochastic games. DIMACS Series in Discrete Mathematics and Theoretical Computer Science 13, 51–71 (1993)MathSciNetGoogle Scholar
  13. 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. 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. 15.
    Gärtner, B.: A subexponential algorithm for abstract optimization problems. SIAM Journal on Computing 24, 1018–1035 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 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)CrossRefGoogle Scholar
  17. 17.
    Gärtner, B.: The random-facet simplex algorithm on combinatorial cubes. Random Structures and Algorithms 20(3), 353–381 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 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)zbMATHGoogle Scholar
  19. 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)zbMATHCrossRefGoogle Scholar
  20. 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)zbMATHMathSciNetGoogle Scholar
  21. 21.
    Hoffman, J., Karp, R.M.: On nonterminating stochastic games. Management Science 12(5), 359–370 (1966)CrossRefMathSciNetGoogle Scholar
  22. 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)CrossRefGoogle Scholar
  23. 23.
    Kalai, G.: A subexponential randomized simplex algorithm. In: 24th ACM STOC, pp. 475–482 (1992)Google Scholar
  24. 24.
    Ludwig, W.: A subexponential randomized algorithm for the simple stochastic game problem. Information and Computation 117, 151–155 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Mansour, Y., Singh, S.: On the complexity of policy iteration. In: Uncertainty in Artificial Intelligence 1999 (1999)Google Scholar
  26. 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. 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. 28.
    Petersson, V., Vorobyov, S.: A randomized subexponential algorithm for parity games. Nordic Journal of Computing 8, 324–345 (2001)zbMATHMathSciNetGoogle Scholar
  29. 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. 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. 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)CrossRefGoogle Scholar
  32. 32.
    Wiedemann, D.: Unimodal set-functions. Congressus Numerantium 50, 165–169 (1985)MathSciNetGoogle Scholar
  33. 33.
    Williamson Hoke, K.: Completely unimodal numberings of a simple polytope. Discrete Applied Mathematics 20, 69–81 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  34. 34.
    Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158, 343–359 (1996)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Henrik Björklund
    • 1
  • Sven Sandberg
    • 1
  • Sergei Vorobyov
    • 1
  1. 1.Information Technology DepartmentUppsala UniversityUppsalaSweden

Personalised recommendations