19 citations · 44 across the 18 of their papers we have counts for
24 papers
Weak Bisimulation Finiteness of Pushdown Systems With Deterministic -Transitions Is 2-ExpTime-Complete
Stefan Göller, Paweł Parys
We consider the problem of deciding whether a given pushdown system all of whose -transitions are deterministic is weakly bisimulation finite, that is, whether it is w…
A finer reparameterisation theorem for MSO and FO queries on strings
Lê Thành Dũng Nguyên, Paweł Parys
We show a theorem on monadic second-order k-ary queries on finite words. It may be illustrated by the following example: if the number of results of a query on binary strings is O(…
Improved Complexity Analysis of Quasi-Polynomial Algorithms Solving Parity Games
Paweł Parys, Aleksander Wiącek
We improve the complexity of solving parity games (with priorities in vertices) for by a factor of : the best complexity known to date was $O(mdn^{1.45+\log_2…
Unboundedness for Recursion Schemes: A Simpler Type System
David Barozzini, Paweł Parys, Jan Wróblewski
Decidability of the problems of unboundedness and simultaneous unboundedness (aka. the diagonal problem) for higher-order recursion schemes was established by Clemente, Parys, Salv…
Higher-Order Model Checking Step by Step
Paweł Parys
We show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted b…
A Recursive Approach to Solving Parity Games in Quasipolynomial Time
Karoliina Lehtinen, Paweł Parys, Sven Schewe +1
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, whil…
Higher-Order Nonemptiness Step by Step
Paweł Parys
We show a new simple algorithm that checks whether a given higher-order grammar generates a nonempty language of trees. The algorithm amounts to a procedure that transforms a gramm…
On the Expressive Power of Higher-Order Pushdown Systems
Paweł Parys
We show that deterministic collapsible pushdown automata of second order can recognize a language that is not recognizable by any deterministic higher-order pushdown automaton (wit…
Bisimulation Finiteness of Pushdown Systems Is Elementary
Stefan Göller, Paweł Parys
We show that in case a pushdown system is bisimulation equivalent to a finite system, there is already a bisimulation equivalent finite system whose size is elementarily bounded in…
Compositionality of the MSO+U Logic
Paweł Parys
We prove that the MSO+U logic is compositional in the following sense: whether an MSO+U formula holds in a tree T depends only on MSO+U-definable properties of the root of T and of…
Cost Automata, Safe Schemes, and Downward Closures
David Barozzini, Lorenzo Clemente, Thomas Colcombet +1
In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to sho…
Parity Games: Another View on Lehtinen's Algorithm
Paweł Parys
Recently, five quasi-polynomial-time algorithms solving parity games were proposed. We elaborate on one of the algorithms, by Lehtinen (2018). Czerwiński et al. (2019) observe that…
Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time
Paweł Parys
Calude, Jain, Khoussainov, Li, and Stephan (2017) proposed a quasi-polynomial-time algorithm solving parity games. After this breakthrough result, a few other quasi-polynomial-time…
Intersection Types for Unboundedness Problems
Paweł Parys
Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter…
Recursion Schemes, the MSO Logic, and the U quantifier
Paweł Parys
We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known t…
Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games
Wojciech Czerwiński, Laure Daviaud, Nathanaël Fijalkow +3
Several distinct techniques have been proposed to design quasi-polynomial algorithms for solving parity games since the breakthrough result of Calude, Jain, Khoussainov, Li, and St…
Intersection Types and Counting
Paweł Parys
We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an in…
Intersection Types and Counting
Paweł Parys
We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an in…
The Diagonal Problem for Higher-Order Recursion Schemes is Decidable
Lorenzo Clemente, Paweł Parys, Sylvain Salvati +1
A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We…
Ordered Tree-Pushdown Systems
Lorenzo Clemente, Paweł Parys, Sylvain Salvati +1
We define a new class of pushdown systems where the pushdown is a tree instead of a word. We allow a limited form of lookahead on the pushdown conforming to a certain ordering rest…
The MSO+U theory of (N, <) is undecidable
Mikołaj Bojańczyk, Paweł Parys, Szymon Toruńczyk
We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets ho…
Higher-Order Pushdown Systems with Data
Paweł Parys
We propose a new extension of higher-order pushdown automata, which allows to use an infinite alphabet. The new automata recognize languages of data words (instead of normal words)…
Weak Alternating Timed Automata
Pawel Parys, Igor Walukiewicz
Alternating timed automata on infinite words are considered. The main result is a characterization of acceptance conditions for which the emptiness problem for these automata is de…
Strictness of the Collapsible Pushdown Hierarchy
Alexander Kartzow, Paweł Parys
We present a pumping lemma for each level of the collapsible pushdown graph hierarchy in analogy to the second author's pumping lemma for higher-order pushdown graphs (without coll…