24 Search Results for "Parys, Paweł"

Document
APPROX
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2024.23
On Instance-Optimal Algorithms for a Generalization of Nuts and Bolts and Generalized Sorting

Authors: Mayank Goswami and Riko Jacob

Published in: LIPIcs, Volume 317, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024)

Abstract
We generalize the classical nuts and bolts problem to a setting where the input is a collection of n nuts and m bolts, and there is no promise of any matching pairs. It is not allowed to compare a nut directly with a nut or a bolt directly with a bolt, and the goal is to perform the fewest nut-bolt comparisons to discover the partial order between the nuts and bolts. We term this problem bipartite sorting. We show that instances of bipartite sorting of the same size exhibit a wide range of complexity, and propose to perform a fine-grained analysis for this problem. We rule out straightforward notions of instance-optimality as being too stringent, and adopt a neighborhood-based definition. Our definition may be of independent interest as a unifying lens for instance-optimal algorithms for other static problems existing in literature. This includes problems like sorting (Estivill-Castro and Woods, ACM Comput. Surv. 1992), convex hull (Afshani, Barbay and Chan, JACM 2017), adaptive joins (Demaine, López-Ortiz and Munro, SODA 2000), and the recent concept of universal optimality for graphs (Haeupler, Hladík, Rozhoň, Tarjan and Tětek, 2023). As our main result on bipartite sorting, we give a randomized algorithm that is within a factor of O(log³(n+m)) of being instance-optimal w.h.p., with respect to the neighborhood-based definition. As our second contribution, we generalize bipartite sorting to DAG sorting, when the underlying DAG is not necessarily bipartite. As an unexpected consequence of a simple algorithm for DAG sorting, we rule out a potential lower bound on the widely-studied problem of sorting with priced information, posed by (Charikar, Fagin, Guruswami, Kleinberg, Raghavan and Sahai, STOC 2000). In this problem, comparing keys i and j has a known cost c_{ij} ∈ ℝ^+ ∪ {∞}, and the goal is to sort the keys in an instance-optimal way, by keeping the total cost of an algorithm as close as possible to ∑_{i=1}^{n-1} c_{x(i)x(i+1)}. Here x(1) < ⋯ < x(n) is the sorted order. While several special cases of cost functions have received a lot of attention in the community, no progress on the general version with arbitrary costs has been reported so far. One reason for this lack of progress seems to be a widely-cited Ω(n) lower bound on the competitive ratio for finding the maximum. This Ω(n) lower bound by (Gupta and Kumar, FOCS 2000) uses costs in {0,1,n, ∞}, and although not extended to sorting, this barrier seems to have stalled any progress on the general cost case. We rule out such a potential lower bound by showing the existence of an algorithm with a Õ(n^{3/4}) competitive ratio for the {0,1,n,∞} cost version. This generalizes the setting of generalized sorting proposed by (Huang, Kannan and Khanna, FOCS 2011), where the costs are either 1 or infinity, and the cost of the cheapest proof is always n-1.
Cite as

Mayank Goswami and Riko Jacob. On Instance-Optimal Algorithms for a Generalization of Nuts and Bolts and Generalized Sorting. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 317, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{goswami_et_al:LIPIcs.APPROX/RANDOM.2024.23,
  author =	{Goswami, Mayank and Jacob, Riko},
  title =	{{On Instance-Optimal Algorithms for a Generalization of Nuts and Bolts and Generalized Sorting}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024)},
  pages =	{23:1--23:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-348-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{317},
  editor =	{Kumar, Amit and Ron-Zewi, Noga},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2024.23},
  URN =		{urn:nbn:de:0030-drops-210168},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2024.23},
  annote =	{Keywords: Sorting, Priced Information, Instance Optimality, Nuts and Bolts}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.18
Weighted Basic Parallel Processes and Combinatorial Enumeration

Authors: Lorenzo Clemente

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We study weighted basic parallel processes (WBPP), a nonlinear recursive generalisation of weighted finite automata inspired from process algebra and Petri net theory. Our main result is an algorithm of 2-EXPSPACE complexity for the WBPP equivalence problem. While (unweighted) BPP language equivalence is undecidable, we can use this algorithm to decide multiplicity equivalence of BPP and language equivalence of unambiguous BPP, with the same complexity. These are long-standing open problems for the related model of weighted context-free grammars. Our second contribution is a connection between WBPP, power series solutions of systems of polynomial differential equations, and combinatorial enumeration. To this end we consider constructible differentially finite power series (CDF), a class of multivariate differentially algebraic series introduced by Bergeron and Reutenauer in order to provide a combinatorial interpretation to differential equations. CDF series generalise rational, algebraic, and a large class of D-finite (holonomic) series, for which no complexity upper bound for equivalence was known. We show that CDF series correspond to commutative WBPP series. As a consequence of our result on WBPP and commutativity, we show that equivalence of CDF power series can be decided with 2-EXPTIME complexity. In order to showcase the CDF equivalence algorithm, we show that CDF power series naturally arise from combinatorial enumeration, namely as the exponential generating series of constructible species of structures. Examples of such species include sequences, binary trees, ordered trees, Cayley trees, set partitions, series-parallel graphs, and many others. As a consequence of this connection, we obtain an algorithm to decide multiplicity equivalence of constructible species, decidability of which was not known before. The complexity analysis is based on effective bounds from algebraic geometry, namely on the length of chains of polynomial ideals constructed by repeated application of finitely many, not necessarily commuting derivations of a multivariate polynomial ring. This is obtained by generalising a result of Novikov and Yakovenko in the case of a single derivation, which is noteworthy since generic bounds on ideal chains are non-primitive recursive in general. On the way, we develop the theory of WBPP series and CDF power series, exposing several of their appealing properties.
Cite as

Lorenzo Clemente. Weighted Basic Parallel Processes and Combinatorial Enumeration. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{clemente:LIPIcs.CONCUR.2024.18,
  author =	{Clemente, Lorenzo},
  title =	{{Weighted Basic Parallel Processes and Combinatorial Enumeration}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{18:1--18:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.18},
  URN =		{urn:nbn:de:0030-drops-207903},
  doi =		{10.4230/LIPIcs.CONCUR.2024.18},
  annote =	{Keywords: weighted automata, combinatorial enumeration, shuffle, algebraic differential equations, process algebra, basic parallel processes, species of structures}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.124
Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata

Authors: Rohan Acharya, Marcin Jurdziński, and Aditya Prakash

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Our main technical contribution is a polynomial-time determinisation procedure for history-deterministic Büchi automata, which settles an open question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead game, which is a variant of Bagnol and Kuperberg’s token game, in which Adam is given a fixed lookahead. We prove that the lookahead game is equivalent to the 1-token game. This allows us to show that the 1-token game characterises history-determinism for semantically-deterministic Büchi automata, which paves the way to our polynomial-time determinisation procedure.
Cite as

Rohan Acharya, Marcin Jurdziński, and Aditya Prakash. Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 124:1-124:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{acharya_et_al:LIPIcs.ICALP.2024.124,
  author =	{Acharya, Rohan and Jurdzi\'{n}ski, Marcin and Prakash, Aditya},
  title =	{{Lookahead Games and Efficient Determinisation of History-Deterministic B\"{u}chi Automata}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{124:1--124:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.124},
  URN =		{urn:nbn:de:0030-drops-202672},
  doi =		{10.4230/LIPIcs.ICALP.2024.124},
  annote =	{Keywords: History determinism, Good-for-games, Automata over infinite words, Games}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.131
The Structure of Trees in the Pushdown Hierarchy

Authors: Arnaud Carayol and Lucien Charamond

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
In this article, we investigate the structure of the trees in the pushdown hierarchy, a hierarchy of infinite graphs having a decidable MSO-theory. We show that a binary complete tree in the pushdown hierarchy must contain at least two different subtrees which are isomorphic. We extend this property to any tree with no leaves and with chains of unary vertices of bounded length. We provided two applications of this result. A first application in formal language theory, gives a simple argument to show that some languages are not deterministic higher-order indexed languages. A second application in number theory shows that the real numbers defined by deterministic higher-order pushdown automata are either rational or transcendental.
Cite as

Arnaud Carayol and Lucien Charamond. The Structure of Trees in the Pushdown Hierarchy. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 131:1-131:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{carayol_et_al:LIPIcs.ICALP.2024.131,
  author =	{Carayol, Arnaud and Charamond, Lucien},
  title =	{{The Structure of Trees in the Pushdown Hierarchy}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{131:1--131:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.131},
  URN =		{urn:nbn:de:0030-drops-202749},
  doi =		{10.4230/LIPIcs.ICALP.2024.131},
  annote =	{Keywords: Pushdown hierarchy, Monadic second-order logic, Automatic numbers}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.12
Extending the WMSO+U Logic with Quantification over Tuples

Authors: Anita Badyl and Paweł Parys

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We study a new extension of the weak MSO logic, talking about boundedness. Instead of a previously considered quantifier 𝖴, expressing the fact that there exist arbitrarily large finite sets satisfying a given property, we consider a generalized quantifier 𝖴, expressing the fact that there exist tuples of arbitrarily large finite sets satisfying a given property. First, we prove that the new logic WMSO+𝖴_{tup} is strictly more expressive than WMSO+𝖴. In particular, WMSO+𝖴_{tup} is able to express the so-called simultaneous unboundedness property, for which we prove that it is not expressible in WMSO+𝖴. Second, we prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+𝖴_{tup}.
Cite as

Anita Badyl and Paweł Parys. Extending the WMSO+U Logic with Quantification over Tuples. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{badyl_et_al:LIPIcs.CSL.2024.12,
  author =	{Badyl, Anita and Parys, Pawe{\l}},
  title =	{{Extending the WMSO+U Logic with Quantification over Tuples}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.12},
  URN =		{urn:nbn:de:0030-drops-196557},
  doi =		{10.4230/LIPIcs.CSL.2024.12},
  annote =	{Keywords: Boundedness, logic, decidability, expressivity, recursion schemes}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.112
Unboundedness for Recursion Schemes: A Simpler Type System

Authors: David Barozzini, Paweł Parys, and Jan Wróblewski

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
Decidability of the problems of unboundedness and simultaneous unboundedness (aka. the diagonal problem) for higher-order recursion schemes was established by Clemente, Parys, Salvati, and Walukiewicz (2016). Then a procedure of optimal complexity was presented by Parys (2017); this procedure used a complicated type system, involving multiple flags and markers. We present here a simpler and much more intuitive type system serving the same purpose. We prove that this type system allows to solve the unboundedness problem for a widely considered subclass of recursion schemes, called safe schemes. For unsafe recursion schemes we only have soundness of the type system: if one can establish a type derivation claiming that a recursion scheme is unbounded then it is indeed unbounded. Completeness of the type system for unsafe recursion schemes is left as an open question. Going further, we discuss an extension of the type system that allows to handle the simultaneous unboundedness problem. We also design and implement an algorithm that fully automatically checks unboundedness of a given recursion scheme, completing in a short time for a wide variety of inputs.
Cite as

David Barozzini, Paweł Parys, and Jan Wróblewski. Unboundedness for Recursion Schemes: A Simpler Type System. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 112:1-112:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{barozzini_et_al:LIPIcs.ICALP.2022.112,
  author =	{Barozzini, David and Parys, Pawe{\l} and Wr\'{o}blewski, Jan},
  title =	{{Unboundedness for Recursion Schemes: A Simpler Type System}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{112:1--112:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.112},
  URN =		{urn:nbn:de:0030-drops-164533},
  doi =		{10.4230/LIPIcs.ICALP.2022.112},
  annote =	{Keywords: Higher-order recursion schemes, boundedness, intersection types, safe schemes}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.140
Higher-Order Model Checking Step by Step

Authors: Paweł Parys

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
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 by a given alternating parity automaton. The algorithm amounts to a procedure that transforms a recursion scheme of order n to a recursion scheme of order n-1, preserving acceptance, and increasing the size only exponentially. After repeating the procedure n times, we obtain a recursion scheme of order 0, for which the problem boils down to solving a finite parity game. Since the size grows exponentially at each step, the overall complexity is n-EXPTIME, which is known to be optimal. More precisely, the transformation is linear in the size of the recursion scheme, assuming that the arity of employed nonterminals and the size of the automaton are bounded by a constant; this results in an FPT algorithm for the model-checking problem. Our transformation is a generalization of a previous transformation of the author (2020), working for reachability automata in place of parity automata. The step-by-step approach can be opposed to previous algorithms solving the considered problem "in one step", being compulsorily more complicated.
Cite as

Paweł Parys. Higher-Order Model Checking Step by Step. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 140:1-140:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.ICALP.2021.140,
  author =	{Parys, Pawe{\l}},
  title =	{{Higher-Order Model Checking Step by Step}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{140:1--140:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.140},
  URN =		{urn:nbn:de:0030-drops-142098},
  doi =		{10.4230/LIPIcs.ICALP.2021.140},
  annote =	{Keywords: Higher-order recursion schemes, Parity automata, Model-checking, Transformation, Order reduction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.9
A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation

Authors: André Arnold, Damian Niwiński, and Paweł Parys

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
We consider nested fixed-point expressions like μ z. ν y. μ x. f(x,y,z) evaluated over a finite lattice, and ask how many queries to a function f are needed to find the value. The previous upper bounds for a monotone function f of arity d over the lattice {0,1}ⁿ were of the order n^{𝒪(d)}, whereas a lower bound of Ω(n²/(lg n)) is known in case when at least one alternation between the least (μ) and the greatest (ν) fixed point occurs in the expression. Following a recent development for parity games, we show here that a quasi-polynomial number of queries is sufficient, namely n^{lg(d/lg n)+𝒪(1)}. The algorithm is an abstract version of several algorithms proposed recently by a number of authors, which involve (implicitly or explicitly) the structure of a universal tree. We then show a quasi-polynomial lower bound for the number of queries used by the algorithms in consideration.
Cite as

André Arnold, Damian Niwiński, and Paweł Parys. A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{arnold_et_al:LIPIcs.CSL.2021.9,
  author =	{Arnold, Andr\'{e} and Niwi\'{n}ski, Damian and Parys, Pawe{\l}},
  title =	{{A Quasi-Polynomial Black-Box Algorithm for Fixed Point Evaluation}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{9:1--9:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.9},
  URN =		{urn:nbn:de:0030-drops-134430},
  doi =		{10.4230/LIPIcs.CSL.2021.9},
  annote =	{Keywords: Mu-calculus, Parity games, Quasi-polynomial time, Black-box algorithm}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.53
Higher-Order Nonemptiness Step by Step

Authors: Paweł Parys

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
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 grammar of order n to a grammar of order n-1, preserving nonemptiness, and increasing the size only exponentially. After repeating the procedure n times, we obtain a grammar of order 0, whose nonemptiness can be easily checked. Since the size grows exponentially at each step, the overall complexity is n-EXPTIME, which is known to be optimal. More precisely, the transformation (and hence the whole algorithm) is linear in the size of the grammar, assuming that the arity of employed nonterminals is bounded by a constant. The same algorithm allows to check whether an infinite tree generated by a higher-order recursion scheme is accepted by an alternating safety (or reachability) automaton, because this question can be reduced to the nonemptiness problem by taking a product of the recursion scheme with the automaton. A proof of correctness of the algorithm is formalised in the proof assistant Coq. Our transformation is motivated by a similar transformation of Asada and Kobayashi (2020) changing a word grammar of order n to a tree grammar of order n-1. The step-by-step approach can be opposed to previous algorithms solving the nonemptiness problem "in one step", being compulsorily more complicated.
Cite as

Paweł Parys. Higher-Order Nonemptiness Step by Step. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 53:1-53:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.FSTTCS.2020.53,
  author =	{Parys, Pawe{\l}},
  title =	{{Higher-Order Nonemptiness Step by Step}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{53:1--53:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.53},
  URN =		{urn:nbn:de:0030-drops-132941},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.53},
  annote =	{Keywords: Higher-order grammars, Nonemptiness, Model-checking, Transformation, Order reduction}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.109
Cost Automata, Safe Schemes, and Downward Closures

Authors: David Barozzini, Lorenzo Clemente, Thomas Colcombet, and Paweł Parys

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
Higher-order recursion schemes are an expressive formalism used to define languages of possibly infinite ranked trees. They extend regular and context-free grammars, and are equivalent to simply typed λY-calculus and collapsible pushdown automata. In this work we prove, under a syntactical constraint called safety, decidability of the model-checking problem for recursion schemes against properties defined by alternating B-automata, an extension of alternating parity automata for infinite trees with a boundedness acceptance condition. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes.
Cite as

David Barozzini, Lorenzo Clemente, Thomas Colcombet, and Paweł Parys. Cost Automata, Safe Schemes, and Downward Closures. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 109:1-109:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{barozzini_et_al:LIPIcs.ICALP.2020.109,
  author =	{Barozzini, David and Clemente, Lorenzo and Colcombet, Thomas and Parys, Pawe{\l}},
  title =	{{Cost Automata, Safe Schemes, and Downward Closures}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{109:1--109:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.109},
  URN =		{urn:nbn:de:0030-drops-125169},
  doi =		{10.4230/LIPIcs.ICALP.2020.109},
  annote =	{Keywords: Cost logics, cost automata, downward closures, higher-order recursion schemes, safe recursion schemes}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.32
Parity Games: Another View on Lehtinen’s Algorithm

Authors: Paweł Parys

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
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 four of the algorithms can be expressed as constructions of separating automata (of quasi-polynomial size), that is, automata that accept all plays decisively won by one of the players, and rejecting all plays decisively won by the other player. The separating automata corresponding to three of the algorithms are deterministic, and it is clear that deterministic separating automata can be used to solve parity games. The separating automaton corresponding to the algorithm of Lehtinen is nondeterministic, though. While this particular automaton can be used to solve parity games, this is not true for every nondeterministic separating automaton. As a first (more conceptual) contribution, we specify when a nondeterministic separating automaton can be used to solve parity games. We also repeat the correctness proof of the Lehtinen’s algorithm, using separating automata. In this part, we prove that her construction actually leads to a faster algorithm than originally claimed in her paper: its complexity is n^{O(log n)} rather than n^{O(log d ⋅ log n)} (where n is the number of nodes, and d the number of priorities of a considered parity game), which is similar to complexities of the other quasi-polynomial-time algorithms.
Cite as

Paweł Parys. Parity Games: Another View on Lehtinen’s Algorithm. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.CSL.2020.32,
  author =	{Parys, Pawe{\l}},
  title =	{{Parity Games: Another View on Lehtinen’s Algorithm}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{32:1--32:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.32},
  URN =		{urn:nbn:de:0030-drops-116757},
  doi =		{10.4230/LIPIcs.CSL.2020.32},
  annote =	{Keywords: Parity games, quasi-polynomial time, separating automata, good-for-games automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.10
Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time

Authors: Paweł Parys

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
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 algorithms were introduced; none of them is easy to understand. Moreover, it turns out that in practice they operate very slowly. On the other side there is Zielonka’s recursive algorithm, which is very simple, exponential in the worst case, and the fastest in practice. We combine these two approaches: we propose a small modification of Zielonka’s algorithm, which ensures that the running time is at most quasi-polynomial. In effect, we obtain a simple algorithm that solves parity games in quasi-polynomial time. We also hope that our algorithm, after further optimizations, can lead to an algorithm that shares the good performance of Zielonka’s algorithm on typical inputs, while reducing the worst-case complexity on difficult inputs.
Cite as

Paweł Parys. Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 10:1-10:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.MFCS.2019.10,
  author =	{Parys, Pawe{\l}},
  title =	{{Parity Games: Zielonka’s Algorithm in Quasi-Polynomial Time}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{10:1--10:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.10},
  URN =		{urn:nbn:de:0030-drops-109543},
  doi =		{10.4230/LIPIcs.MFCS.2019.10},
  annote =	{Keywords: Parity games, Zielonka’s algorithm, quasi-polynomial time}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.27
Homogeneity Without Loss of Generality

Authors: Pawel Parys

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We consider higher-order recursion schemes as generators of infinite trees. A sort (simple type) is called homogeneous when all arguments of higher order are taken before any arguments of lower order. We prove that every scheme can be converted into an equivalent one (i.e, generating the same tree) that is homogeneous, that is, uses only homogeneous sorts. Then, we prove the same for safe schemes: every safe scheme can be converted into an equivalent safe homogeneous scheme. Furthermore, we compare two definition of safe schemes: the original definition of Damm, and the modern one. Finally, we prove a lemma which illustrates usefulness of the homogeneity assumption. The results are known, but we prove them in a novel way: by directly manipulating considered schemes.
Cite as

Pawel Parys. Homogeneity Without Loss of Generality. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.FSCD.2018.27,
  author =	{Parys, Pawel},
  title =	{{Homogeneity Without Loss of Generality}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{27:1--27:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.27},
  URN =		{urn:nbn:de:0030-drops-91972},
  doi =		{10.4230/LIPIcs.FSCD.2018.27},
  annote =	{Keywords: higher-order recursion schemes, lambda-calculus, homogeneous types, safe schemes}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.53
Recursion Schemes and the WMSO+U Logic

Authors: Pawel Parys

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
We study the weak MSO logic extended by the unbounding quantifier (WMSO+U), expressing the fact that there exist arbitrarily large finite sets satisfying a given property. We prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+U.
Cite as

Pawel Parys. Recursion Schemes and the WMSO+U Logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 53:1-53:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.STACS.2018.53,
  author =	{Parys, Pawel},
  title =	{{Recursion Schemes and the WMSO+U Logic}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{53:1--53:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.53},
  URN =		{urn:nbn:de:0030-drops-85122},
  doi =		{10.4230/LIPIcs.STACS.2018.53},
  annote =	{Keywords: higher-order recursion schemes, intersection types, WMSO+U logic, boundedness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.45
The Complexity of the Diagonal Problem for Recursion Schemes

Authors: Pawel Parys

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
We consider nondeterministic higher-order recursion schemes as recognizers of languages of finite words or finite trees. We establish the complexity of the diagonal problem for schemes: given a set of letters A and a scheme G, is it the case that for every number n the scheme accepts a word (a tree) in which every letter from A appears at least n times. We prove that this problem is (m-1)-EXPTIME-complete for word-recognizing schemes of order m, and m-EXPTIME-complete for tree-recognizing schemes of order m.
Cite as

Pawel Parys. The Complexity of the Diagonal Problem for Recursion Schemes. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 45:1-45:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{parys:LIPIcs.FSTTCS.2017.45,
  author =	{Parys, Pawel},
  title =	{{The Complexity of the Diagonal Problem for Recursion Schemes}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{45:1--45:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.45},
  URN =		{urn:nbn:de:0030-drops-83757},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.45},
  annote =	{Keywords: diagonal problem, higher-order recursion schemes, intersection types, downward closure}
}
  • Refine by Author
  • 12 Parys, Pawel
  • 8 Parys, Paweł
  • 3 Clemente, Lorenzo
  • 2 Barozzini, David
  • 2 Bojanczyk, Mikolaj
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Rewrite systems
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Verification by model checking
  • 2 Theory of computation → Algorithmic game theory
  • 2 Theory of computation → Automata over infinite objects
  • Show More...

  • Refine by Keyword
  • 4 higher-order recursion schemes
  • 3 Parity games
  • 3 boundedness
  • 3 intersection types
  • 2 Higher-order recursion schemes
  • Show More...

  • Refine by Type
  • 24 document

  • Refine by Publication Year
  • 5 2024
  • 4 2016
  • 3 2012
  • 3 2018
  • 3 2020
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact