David Avis and myself have just finished a paper on Cunningham’s Rule for solving linear programs, featuring an exponential lower bound. Have a look at the preprint here and let us know what you think.

# Category Archives: Publications

# New paper on the guarded transformation

Florian Bruse, Martin Lange and myself have just finished writing a paper on the guarded transformation for the modal mu calculus. See a preprint here.

# New paper on ramsey-based decision methods

Felix Klaedtke, Martin Lange and myself have just finished writing a paper on universality and subsumption checking for visibly pushdown automata using ramsey-based methods. See a preprint here.

You can also check out a prototype implementation here.

# New lower bound on Cunningham’s rule

We have been able to obtain yet another subexponential lower bound for a history-based pivoting rule for solving linear programs and games.

Also known as the Round-Rubin rule, Cunningham’s least recently considered pivoting method fixes an initial ordering on all variables first, and then selects the improving variables in a round-robin fashion.

See a pre-print here. Also, check out an animation to see how the algorithm operates on the construction.

Feel free to comment.

# New paper on branching-time logics

Markus Latte, Martin Lange and myself have just finished writing a paper on satisfiability games for branching-time logics, focussing on CTL, CTL+ and CTL*. See a preprint here.

It features optimal decision procedures based on infinite-duration games for deciding satisfiability for these logics.

# New lower bound on Fearnley’s non-oblivious policy iteration method

[latexpage]

I’ve managed to complete a new lower bound construction for Fearnley’s non-oblivious policy iteration method. See Fearnley’s paper here. See my preprint here.

The basic idea of Fearnley’s rule is to remember such intermediate cycle structures (it is a bit more general than that, but you get the idea) as I’ve used in my previous constructions whenever they occur. Then, whenever it is profitable, they are reapplied again. As it turns out, the binary counting behaviour of the original constructions breaks down, resulting in a quadratic number (educated guess, might be a little higher) of iterations.

My new subexponential lower bound for Fearnley’s rule works by introducing an exponential number of different intermediate cycles (rather than just a polynomial number). The idea is to have $2^n$ different cycle configurations for the first bit, $2^{n-1}$ configurations for the second bit and so on, where there is only one applicable configuration per global binary counter state. More precisely, the applicable cycle configuration of bit $i$ depends on the bit settings of all higher bits $i<j\leq n$. Hence, no matter which cycles are learned by the rule, they will never be applicable again, and therefore learning is of no use here.

To give you a rough idea of how this looks like, I’ve made some animations where you can see what the algorithm is actually doing on the game:

- Original Game with Switch All Rule (exponential number of iterations)
- Original Game with Non-Oblivious Rule (polynomial number of iterations)
- Enhanced Game with Switch All (exponential number of iterations)
- Enhanced Game with Non-Oblivious Rule (exponential number of iterations)

Let me know what you think.