Reasoning about online algorithms with weighted automata

ABSTRACT

We describe an automata-theoretic approach for the competitive analysis of online algorithms. Our approach is based on weighted automata, which assign to each input word a cost in R^≥0. By relating the "unbounded look ahead" of optimal offline algorithms with nondeterminism, and relating the "no look ahead" of online algorithms with determinism, we are able to solve problems about the competitive ratio of online algorithms, and the memory they require, by reducing them to questions about determinization and approximated determinization of weighted automata.

REFERENCES

• 1: Alfred V. Aho , Peter J. Denning , Jeffrey D. Ullman, Principles of Optimal Page Replacement, Journal of the ACM (JACM), v.18 n.1, p.80-93, Jan. 1971 [doi>10.1145/321623.321632]
• 2: T. Ball, B. Cook, V. Levin, and S. K. Rajamani. Slam and static driver verifier: Technology transfer of formal methods inside microsoft. In Integrated Formal Methods, pages 1--20, 2004.
• 3: S. Ben-David, A. Borodin, R. M. Karp, G. Tardos, and A. Wigderson. On the power of randomization in online algorithms. algorithmica, 11(2):2--14, 1994.
• 4: Allan Borodin , Ran El-Yaniv, Online computation and competitive analysis, Cambridge University Press, New York, NY, 1998
• 5: A. Borodin , N. Linial , M. Saks, An optimal online algorithm for metrical task systems, Proceedings of the nineteenth annual ACM symposium on Theory of computing, p.373-382, January 1987, New York, New York, United States [doi>10.1145/28395.28435]
• 6: Wolfgang W. Bein , Lawrence L. Larmore, Trackless online algorithms for the server problem, Information Processing Letters, v.74 n.1-2, p.73-79, April 2000 [doi>10.1016/S0020-0190(00)00034-X]
• 7: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 8: A. Chakrabarti, K. Chatterjee, T. A. Henzinger, O. Kupferman, and R. Majumdar. Verifying quantitative properties using bound functions. In Proc. 13th CHARME, LNCS 3725, pages 50--64. Springer, 2005.
• 9: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 10: M. Chrobak and L. L. Larmore. The server problem and on-line games. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 7:11--64, 1991.
• 11: M. Chrobak and L. L. Larmore. Private communication. 2008.
• 12: Jacob Elgaard , Nils Klarlund , Anders Møller, MONA 1.x: New Techniques for WS1S and WS2S, Proceedings of the 10th International Conference on Computer Aided Verification, p.516-520, June 28-July 02, 1998
• 13: E. Allen Emerson , Vineet Kahlon, Reducing Model Checking of the Many to the Few, Proceedings of the 17th International Conference on Automated Deduction, p.236-254, June 17-20, 2000
• 14: T. A. Henzinger and N. Piterman. Solving games without determinization. In Proc. 15th CSL, LNCS 4207, pages 394--410. Springer, 2006.
• 15: Gerard Holzmann, Spin model checker, the: primer and reference manual, Addison-Wesley Professional, 2003
• 16: B. Jobstmann, S. Galler, M. Weiglhofer, and R. Bloem. Anzu: A tool for property synthesis. In Proc 19th CAV, LNCS 4590, pages 258--262, 2007.
• 17: H. W. Kuhn. Solvability and consistency for linear equations and inequalities. The American Mathematical Monthly, 63(4):217--232, 1956.
• 18: Werner Kuich , Arto Salomaa, Semirings, automata, languages, Springer-Verlag, London, 1985
• 19: Mark S. Manasse , Lyle A. McGeoch , Daniel D. Sleator, Competitive algorithms for server problems, Journal of Algorithms, v.11 n.2, p.208-230, Jun. 1990 [doi>10.1016/0196-6774(90)90003-W]
• 20: Mehryar Mohri, Finite-state transducers in language and speech processing, Computational Linguistics, v.23 n.2, p.269-311, June 1997
• 21: Daniel D. Sleator , Robert E. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM, v.28 n.2, p.202-208, Feb. 1985 [doi>10.1145/2786.2793]
• 22: Moshe Y. Vardi , Pierre Wolper, Reasoning about infinite computations, Information and Computation, v.115 n.1, p.1-37, Nov. 15, 1994 [doi>10.1006/inco.1994.1092]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Online computation

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)