6 results
Karoliina Lehtinen ; Udi Boker.
The complexity of parity games is a long standing open problem that saw a major breakthrough in 2017 when two quasi-polynomial algorithms were published. This article presents a third, independent approach to solving parity games in quasi-polynomial time, based on the notion of register game, a […]
Published on May 19, 2020
Karoliina Lehtinen ; Martin Zimmermann.
We introduce good-for-games $\omega$-pushdown automata ($\omega$-GFG-PDA). These are automata whose nondeterminism can be resolved based on the input processed so far. Good-for-gameness enables automata to be composed with games, trees, and other automata, applications which otherwise require […]
Published on February 15, 2023
Karoliina Lehtinen ; Paweł Parys ; Sven Schewe ; Dominik Wojtczak.
Zielonka's classic recursive algorithm for solving parity games is perhaps the simplest among the many existing parity game algorithms. However, its complexity is exponential, while currently the state-of-the-art algorithms have quasipolynomial complexity. Here, we present a modification of […]
Published on January 12, 2022
Udi Boker ; Karoliina Lehtinen.
A nondeterministic automaton is history-deterministic if its nondeterminism can be resolved by only considering the prefix of the word read so far. Due to their good compositional properties, history-deterministic automata are useful in solving games and synthesis problems. Deciding whether a given […]
Published on November 3, 2023
Shibashis Guha ; Ismaël Jecker ; Karoliina Lehtinen ; Martin Zimmermann.
We study the expressiveness and succinctness of history-deterministic pushdown automata (HD-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. These are also known as […]
Published on January 11, 2024
Sougata Bose ; Thomas A. Henzinger ; Karoliina Lehtinen ; Sven Schewe ; Patrick Totzke.
We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits […]
Published on October 2, 2024