20 Search Results for "Parys, Paweł"

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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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-dev.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}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.11
Models of Lambda-Calculus and the Weak MSO Logic

Authors: Pawel Parys and Szymon Torunczyk

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
We study the weak MSO logic in relationship to infinitary lambda-calculus. We show that for every formula phi of weak MSO there exists a finitary model of infinitary lambda-calculus recognizing the set of infinitary lambda-terms whose Böhm tree satisfies phi. The model is effective, in the sense that for every lambda-Y-term we can effectively compute its value in the model. In particular, given a finite lambda-Y-term, one can decide whether the resulting Böhm tree satisfies a given formula of weak MSO, which is a special case of the result of Ong, which concerns unrestricted MSO. The existence of effective models for weak MSO and MSO was proved earlier by Salvati and Walukiewicz but our proof uses a different method, as it does not involve automata, but works directly with logics.
Cite as

Pawel Parys and Szymon Torunczyk. Models of Lambda-Calculus and the Weak MSO Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 11:1-11:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{parys_et_al:LIPIcs.CSL.2016.11,
  author =	{Parys, Pawel and Torunczyk, Szymon},
  title =	{{Models of Lambda-Calculus and the Weak MSO Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{11:1--11:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.11},
  URN =		{urn:nbn:de:0030-drops-65511},
  doi =		{10.4230/LIPIcs.CSL.2016.11},
  annote =	{Keywords: typed lambda-calculus, models, weak MSO logic}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2016.20
Reasoning About Integrity Constraints for Tree-Structured Data

Authors: Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys

Published in: LIPIcs, Volume 48, 19th International Conference on Database Theory (ICDT 2016)

Abstract
We study a class of integrity constraints for tree-structured data modelled as data trees, whose nodes have a label from a finite alphabet and store a data value from an infinite data domain. The constraints require each tuple of nodes selected by a conjunctive query (using navigational axes and labels) to satisfy a positive combination of equalities and a positive combination of inequalities over the stored data values. Such constraints are instances of the general framework of XML-to-relational constraints proposed recently by Niewerth and Schwentick. They cover some common classes of constraints, including W3C XML Schema key and unique constraints, as well as domain restrictions and denial constraints, but cannot express inclusion constraints, such as reference keys. Our main result is that consistency of such integrity constraints with respect to a given schema (modelled as a tree automaton) is decidable. An easy extension gives decidability for the entailment problem. Equivalently, we show that validity and containment of unions of conjunctive queries using navigational axes, labels, data equalities and inequalities is decidable, as long as none of the conjunctive queries uses both equalities and inequalities; without this restriction, both problems are known to be undecidable. In the context of XML data exchange, our result can be used to establish decidability for a consistency problem for XML schema mappings. All the decision procedures are doubly exponential, with matching lower bounds. The complexity may be lowered to singly exponential, when conjunctive queries are replaced by tree patterns, and the number of data comparisons is bounded.
Cite as

Wojciech Czerwinski, Claire David, Filip Murlak, and Pawel Parys. Reasoning About Integrity Constraints for Tree-Structured Data. In 19th International Conference on Database Theory (ICDT 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 48, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICDT.2016.20,
  author =	{Czerwinski, Wojciech and David, Claire and Murlak, Filip and Parys, Pawel},
  title =	{{Reasoning About Integrity Constraints for Tree-Structured Data}},
  booktitle =	{19th International Conference on Database Theory (ICDT 2016)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-002-6},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{48},
  editor =	{Martens, Wim and Zeume, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2016.20},
  URN =		{urn:nbn:de:0030-drops-57897},
  doi =		{10.4230/LIPIcs.ICDT.2016.20},
  annote =	{Keywords: data trees, integrity constraints, unions of conjunctive queries, schema mappings, entailment, containment, consistency}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.19
On a Fragment of AMSO and Tiling Systems

Authors: Achim Blumensath, Thomas Colcombet, and Pawel Parys

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
We prove that satisfiability over infinite words is decidable for a fragment of asymptotic monadic second-order logic. In this fragment we only allow formulae of the form "exists t forall s exists r: phi(r,s,t)", where phi does not use quantifiers over number variables, and variables r and s can be only used simultaneously, in subformulae of the form s < f(x) <= r.
Cite as

Achim Blumensath, Thomas Colcombet, and Pawel Parys. On a Fragment of AMSO and Tiling Systems. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{blumensath_et_al:LIPIcs.STACS.2016.19,
  author =	{Blumensath, Achim and Colcombet, Thomas and Parys, Pawel},
  title =	{{On a Fragment of AMSO and Tiling Systems}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.19},
  URN =		{urn:nbn:de:0030-drops-57202},
  doi =		{10.4230/LIPIcs.STACS.2016.19},
  annote =	{Keywords: monadic second-order logic, boundedness, tiling problems}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.21
The MSO+U Theory of (N,<) Is Undecidable

Authors: Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
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 holds for sets of arbitrarily large size. We prove that the logic is undecidable on infinite words, i.e. the MSO+U theory of (N,<) is undecidable. This settles an open problem about the logic, and improves a previous undecidability result, which used infinite trees and additional axioms from set theory.
Cite as

Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U Theory of (N,<) Is Undecidable. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 21:1-21:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2016.21,
  author =	{Bojanczyk, Mikolaj and Parys, Pawel and Torunczyk, Szymon},
  title =	{{The MSO+U Theory of (N,\langle) Is Undecidable}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{21:1--21:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.21},
  URN =		{urn:nbn:de:0030-drops-57223},
  doi =		{10.4230/LIPIcs.STACS.2016.21},
  annote =	{Keywords: automata, logic, unbounding quantifier, bounds, undecidability}
}
  • Refine by Author
  • 12 Parys, Pawel
  • 8 Parys, Paweł
  • 2 Barozzini, David
  • 2 Bojanczyk, Mikolaj
  • 2 Clemente, Lorenzo
  • Show More...

  • Refine by Classification
  • 6 Theory of computation → Rewrite systems
  • 3 Theory of computation → Logic and verification
  • 2 Theory of computation → Algorithmic game theory
  • 2 Theory of computation → Verification by model checking
  • 1 Mathematics of computing → Lambda calculus

  • 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
  • 20 document

  • Refine by Publication Year
  • 4 2016
  • 3 2012
  • 3 2018
  • 3 2020
  • 2 2021
  • 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