Arrow Research search

Author name cluster

Oliver Friedmann

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers
2 author rows

Possible papers

4

Highlights Conference 2013 Conference Abstract

Polynomial guarded transformation for the modal mu-calculus is still open

  • Florian Bruse
  • Oliver Friedmann
  • Martin Lange

Guarded normal form requires occurrences of fixpoint variables in a μ-calculus formula to occur under the scope of a modal operator. The literature contains guarded transformations that effectively bring a μ-calculus formula into guarded normal form. We show that the known guarded transformations can cause an exponential blowup in formula size, contrary to existing claims of polynomial behaviour. We also show that any poly- nomial guarded transformation for μ-calculus formulas in the more relaxed vectorial form gives rise to a polynomial solution algorithm for parity games, the existence of which is an open problem.

SODA Conference 2011 Conference Paper

A subexponential lower bound for the Random Facet algorithm for Parity Games

  • Oliver Friedmann
  • Thomas Dueholm Hansen
  • Uri Zwick

Parity Games form an intriguing family of infinite duration games whose solution is equivalent to the solution of important problems in automatic verification and automata theory. They also form a very natural subclass of Deterministic Mean Payoff Games, which in turn is a very natural subclass of turn-based Stochastic Mean Payoff Games. It is a major open problem whether these game families can be solved in polynomial time. The currently theoretically fastest algorithms for the solution of all these games are adaptations of the randomized algorithms of Kalai and of Matousek, Sharir and Welzl for LP-type problems, an abstract generalization of linear programming. The expected running time of both algorithms is subexponential in the size of the game, i. e. ,, where n is the number of vertices in the game. We focus in this paper on the algorithm of Matousek, Sharir and Welzl and refer to it as the Random Facet algorithm. Matoušek constructed a family of abstract optimization problems such that the expected running time of the Random Facet algorithm, when run on a random instance from this family, is close to the subexponential upper bound given above. This shows that in the abstract setting, the upper bound on the complexity of the Random Facet algorithm is essentially tight. It is not known, however, whether the abstract optimization problems constructed by Matoušek correspond to games of any of the families mentioned above. There was some hope, therefore, that the Random Facet algorithm, when applied to, say, parity games, may run in polynomial time. We show, that this, unfortunately, is not the case by constructing explicit parity games on which the expected running time of the Random Facet algorithm is close to the subexponential upper bound. The games we use mimic the behavior of a randomized counter. They are also the first explicit LP-type problems on which the Random Facet algorithm is not polynomial.

STOC Conference 2011 Conference Paper

Subexponential lower bounds for randomized pivoting rules for the simplex algorithm

  • Oliver Friedmann
  • Thomas Dueholm Hansen
  • Uri Zwick

The simplex algorithm is among the most widely used algorithms for solving linear programs in practice. With essentially all deterministic pivoting rules it is known, however, to require an exponential number of steps to solve some linear programs. No non-polynomial lower bounds were known, prior to this work, for randomized pivoting rules. We provide the first subexponential (i.e., of the form 2 Ω(n α ) , for some α>0) lower bounds for the two most natural, and most studied, randomized pivoting rules suggested to date.

GandALF Workshop 2010 Workshop Paper

Local Strategy Improvement for Parity Game Solving

  • Oliver Friedmann
  • Martin Lange

The problem of solving a parity game is at the core of many problems in model checking, satisfiability checking and program synthesis. Some of the best algorithms for solving parity game are strategy improvement algorithms. These are global in nature since they require the entire parity game to be present at the beginning. This is a distinct disadvantage because in many applications one only needs to know which winning region a particular node belongs to, and a witnessing winning strategy may cover only a fractional part of the entire game graph. We present a local strategy improvement algorithm which explores the game graph on-the-fly whilst performing the improvement steps. We also compare it empirically with existing global strategy improvement algorithms and the currently only other local algorithm for solving parity games. It turns out that local strategy improvement can outperform these others by several orders of magnitude.

v2026.09.13