Checking whether one formal language is included in another is important in many verification tasks. In this article, we provide solutions for checking the inclusion of languages given by visibly pushdown automata over both finite and infinite words. Visibly pushdown automata are a richer automaton model than the classical finite-state automata, which allows one, for example, to reason about the nesting of procedure calls in the executions of recursive imperative programs. The presented solutions do not rely on explicit automaton constructions for determinization and complementation. Instead, they are more direct and generalize the so-called Ramsey-based inclusion-checking algorithms, which apply to classical finite-state automata and proved to be effective there to visibly pushdown automata. We also experimentally evaluate these algorithms, demonstrating the virtues of avoiding explicit determinization and complementation constructions.

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.

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.

Abstract Discrete Interval Encoding Trees are data structures for the representation of fat, i.e. densely populated sets over a discrete linear order. In this paper, we introduce algorithms for set-theoretic operations like intersection, union, etc. on sets represented as balanced diets. We empirically analyse their performance and show that these algorithms can outperform previously known algorithms on sets, such as the ones implemented in OCaml's standard library.

This paper presents a new lower bound for the discrete strategy improvement algorithm for solving parity games due to Voege and Jurdzinski. First, we informally show which structures are difficult to solve for the algorithm. Second, we outline a family of games on which the algorithm requires exponentially many strategy iterations, answering in the negative the long-standing question whether this algorithm runs in polynomial time. Additionally we note that the same family of games can be used to prove a similar result w.r.t. the strategy improvement variant by Schewe as well as the strategy iteration for solving discounted payoff games due to Puri.