Author name cluster

Tim A. C. Willemse

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

GandALF Workshop 2018 Workshop Paper

A Comparison of BDD-Based Parity Game Solvers

Lisette Sanchez
Wieger Wesselink
Tim A. C. Willemse

Parity games are two player games with omega-winning conditions, played on finite graphs. Such games play an important role in verification, satisfiability and synthesis. It is therefore important to identify algorithms that can efficiently deal with large games that arise from such applications. In this paper, we describe our experiments with BDD-based implementations of four parity game solving algorithms, viz. Zielonka's recursive algorithm, the more recent Priority Promotion algorithm, the Fixpoint-Iteration algorithm and the automata based APT algorithm. We compare their performance on several types of random games and on a number of cases taken from the Keiren benchmark set.

PDF Details DOI

CSL Conference 2015 Conference Paper

Evidence for Fixpoint Logic

Sjoerd Cranen
Bas Luttik
Tim A. C. Willemse

For many modal logics, dedicated model checkers offer diagnostics (e. g. , counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking.

Details

GandALF Workshop 2015 Workshop Paper

Improvement in Small Progress Measures

Maciej Gazda
Tim A. C. Willemse

Small Progress Measures is one of the classical parity game solving algorithms. For games with n vertices, m edges and d different priorities, the original algorithm computes the winning regions and a winning strategy for one of the players in O(dm. (n/floor(d/2))^floor(d/2)) time. Computing a winning strategy for the other player requires a re-run of the algorithm on that player's winning region, thus increasing the runtime complexity to O(dm. (n/ceil(d/2))^ceil(d/2)) for computing the winning regions and winning strategies for both players. We modify the algorithm so that it derives the winning strategy for both players in one pass. This reduces the upper bound on strategy derivation for SPM to O(dm. (n/floor(d/2))^floor(d/2)). At the basis of our modification is a novel operational interpretation of the least progress measure that we provide.

PDF Details DOI

GandALF Workshop 2013 Workshop Paper

Zielonka's Recursive Algorithm: dull, weak and solitaire games and tighter bounds

Maciej Gazda
Tim A. C. Willemse

Dull, weak and nested solitaire games are important classes of parity games, capturing, among others, alternation-free mu-calculus and ECTL* model checking problems. These classes can be solved in polynomial time using dedicated algorithms. We investigate the complexity of Zielonka's Recursive algorithm for solving these special games, showing that the algorithm runs in O(d (n + m)) on weak games, and, somewhat surprisingly, that it requires exponential time to solve dull games and (nested) solitaire games. For the latter classes, we provide a family of games G, allowing us to establish a lower bound of 2^(n/3). We show that an optimisation of Zielonka's algorithm permits solving games from all three classes in polynomial time. Moreover, we show that there is a family of (non-special) games M that permits us to establish a lower bound of 2^(n/3), improving on the previous lower bound for the algorithm.

PDF Details DOI