Formal Analysis of Online Algorithms

In [AKL10], we showed how viewing online algorithms as reactive systems enables the application of ideas from formal verification to the competitive analysis of online algorithms. Our approach is based on weighted automata, which assign to each input word a cost in IR≥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 were able to solve problems about the competitive ratio of online algorithms and the memory they require. In this paper we improve the application in three important and technically challenging aspects. First, we allow the competitive analysis to take into account assumptions about the environment. Second, we allow the online algorithm to have a bounded lookahead. Third, we describe a symbolic version of the model-checking algorithm and demonstrate its applicability. The first two contributions broaden the scope of our approach to settings in ...

• Type: Journal
• Year: 2011
• Where: ATVA
• Authors: Benjamin Aminof, Orna Kupferman, Robby Lampert
• Keywords: ATVA 2011, Hardware, Input Word, Symbolic Version, Weighted Automata