Found 2 Possible Name Variants:

Document

Invited Talk

**Published in:** LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Sparsity theory, initiated by Ossona de Mendez and Nešetřil, identifies those classes of sparse graphs that are tractable in various ways - algorithmically, combinatorially, and logically - as exactly the nowhere dense classes. An ongoing effort aims at generalizing sparsity theory to classes of graphs that are not necessarily sparse. Twin-width theory, developed by Bonnet, Thomassé and co-authors, is a step in that direction. A theory unifying the two is anticipated. It is conjectured that the relevant notion characterising dense graph classes that are tractable, generalising nowhere denseness and bounded twin-width, is the notion of a monadically dependent class, introduced by Shelah in model theory. I will survey the recent, rapid progress in the understanding of those classes, and of the related monadically stable classes. This development combines tools from structural graph theory, logic (finite and infinite model theory), and algorithms (parameterised algorithms and range search queries).

Szymon Toruńczyk. Structurally Tractable Graph Classes (Invited Talk). In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{torunczyk:LIPIcs.STACS.2024.3, author = {Toru\'{n}czyk, Szymon}, title = {{Structurally Tractable Graph Classes}}, booktitle = {41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-311-9}, ISSN = {1868-8969}, year = {2024}, volume = {289}, editor = {Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.3}, URN = {urn:nbn:de:0030-drops-197134}, doi = {10.4230/LIPIcs.STACS.2024.3}, annote = {Keywords: Structural graph theory, Monadic dependence, monadic NIP, twin-width} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Monadically stable and monadically NIP classes of structures were initially studied in the context of model theory and defined in logical terms. They have recently attracted attention in the area of structural graph theory, as they generalize notions such as nowhere denseness, bounded cliquewidth, and bounded twinwidth.
Our main result is the - to the best of our knowledge first - purely combinatorial characterization of monadically stable classes of graphs, in terms of a property dubbed flip-flatness. A class C of graphs is flip-flat if for every fixed radius r, every sufficiently large set of vertices of a graph G ∈ C contains a large subset of vertices with mutual distance larger than r, where the distance is measured in some graph G' that can be obtained from G by performing a bounded number of flips that swap edges and non-edges within a subset of vertices. Flip-flatness generalizes the notion of uniform quasi-wideness, which characterizes nowhere dense classes and had a key impact on the combinatorial and algorithmic treatment of nowhere dense classes. To obtain this result, we develop tools that also apply to the more general monadically NIP classes, based on the notion of indiscernible sequences from model theory. We show that in monadically stable and monadically NIP classes indiscernible sequences impose a strong combinatorial structure on their definable neighborhoods. All our proofs are constructive and yield efficient algorithms.

Jan Dreier, Nikolas Mählmann, Sebastian Siebertz, and Szymon Toruńczyk. Indiscernibles and Flatness in Monadically Stable and Monadically NIP Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 125:1-125:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dreier_et_al:LIPIcs.ICALP.2023.125, author = {Dreier, Jan and M\"{a}hlmann, Nikolas and Siebertz, Sebastian and Toru\'{n}czyk, Szymon}, title = {{Indiscernibles and Flatness in Monadically Stable and Monadically NIP Classes}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {125:1--125:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.125}, URN = {urn:nbn:de:0030-drops-181779}, doi = {10.4230/LIPIcs.ICALP.2023.125}, annote = {Keywords: stability, NIP, combinatorial characterization, first-order model checking} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

A class of graphs C is monadically stable if for every unary expansion Ĉ of C, one cannot encode - using first-order transductions - arbitrarily long linear orders in graphs from C. It is known that nowhere dense graph classes are monadically stable; these include classes of bounded maximum degree and classes that exclude a fixed topological minor. On the other hand, monadic stability is a property expressed in purely model-theoretic terms that is also suited for capturing structure in dense graphs.
In this work we provide a characterization of monadic stability in terms of the Flipper game: a game on a graph played by Flipper, who in each round can complement the edge relation between any pair of vertex subsets, and Localizer, who in each round is forced to restrict the game to a ball of bounded radius. This is an analog of the Splitter game, which characterizes nowhere dense classes of graphs (Grohe, Kreutzer, and Siebertz, J. ACM '17).
We give two different proofs of our main result. The first proof is based on tools borrowed from model theory, and it exposes an additional property of monadically stable graph classes that is close in spirit to definability of types. Also, as a byproduct, we show that monadic stability for graph classes coincides with monadic stability of existential formulas with two free variables, and we provide another combinatorial characterization of monadic stability via forbidden patterns. The second proof relies on the recently introduced notion of flip-flatness (Dreier, Mählmann, Siebertz, and Toruńczyk, arXiv 2206.13765) and provides an efficient algorithm to compute Flipper’s moves in a winning strategy.

Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokołowski, and Szymon Toruńczyk. Flipper Games for Monadically Stable Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 128:1-128:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2023.128, author = {Gajarsk\'{y}, Jakub and M\"{a}hlmann, Nikolas and McCarty, Rose and Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Siebertz, Sebastian and Soko{\l}owski, Marek and Toru\'{n}czyk, Szymon}, title = {{Flipper Games for Monadically Stable Graph Classes}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {128:1--128:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.128}, URN = {urn:nbn:de:0030-drops-181804}, doi = {10.4230/LIPIcs.ICALP.2023.128}, annote = {Keywords: Stability theory, structural graph theory, games} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

We use model-theoretic tools originating from stability theory to derive a result we call the Finitary Substitute Lemma, which intuitively says the following. Suppose we work in a stable graph class 𝒞, and using a first-order formula φ with parameters we are able to define, in every graph G ∈ 𝒞, a relation R that satisfies some hereditary first-order assertion ψ. Then we are able to find a first-order formula φ' that has the same property, but additionally is finitary: there is finite bound k ∈ ℕ such that in every graph G ∈ 𝒞, different choices of parameters give only at most k different relations R that can be defined using φ'.
We use the Finitary Substitute Lemma to derive two corollaries about the existence of certain canonical decompositions in classes of well-structured graphs.
- We prove that in the Splitter game, which characterizes nowhere dense graph classes, and in the Flipper game, which characterizes monadically stable graph classes, there is a winning strategy for Splitter, respectively Flipper, that can be defined in first-order logic from the game history. Thus, the strategy is canonical.
- We show that for any fixed graph class 𝒞 of bounded shrubdepth, there is an 𝒪(n²)-time algorithm that given an n-vertex graph G ∈ 𝒞, computes in an isomorphism-invariant way a structure H of bounded treedepth in which G can be interpreted. A corollary of this result is an 𝒪(n²)-time isomorphism test and canonization algorithm for any fixed class of bounded shrubdepth.

Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 135:1-135:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ohlmann_et_al:LIPIcs.ICALP.2023.135, author = {Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Toru\'{n}czyk, Szymon}, title = {{Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {135:1--135:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.135}, URN = {urn:nbn:de:0030-drops-181874}, doi = {10.4230/LIPIcs.ICALP.2023.135}, annote = {Keywords: Model Theory, Stability Theory, Shrubdepth, Nowhere Dense, Monadically Stable} }

Document

Track A: Algorithms, Complexity and Games

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

We introduce a new data structure for answering connectivity queries in undirected graphs subject to batched vertex failures. Precisely, given any graph G and integer parameter k, we can in fixed-parameter time construct a data structure that can later be used to answer queries of the form: "are vertices s and t connected via a path that avoids vertices u₁,…, u_k?" in time 2^𝒪(k). In the terminology of the literature on data structures, this gives the first deterministic data structure for connectivity under vertex failures where for every fixed number of failures, all operations can be performed in constant time.
With the aim to understand the power and the limitations of our new techniques, we prove an algorithmic meta theorem for the recently introduced separator logic, which extends first-order logic with atoms for connectivity under vertex failures. We prove that the model-checking problem for separator logic is fixed-parameter tractable on every class of graphs that exclude a fixed topological minor. We also show a weak converse. This implies that from the point of view of parameterized complexity, under standard complexity theoretical assumptions, the frontier of tractability of separator logic is almost exactly delimited by classes excluding a fixed topological minor.
The backbone of our proof relies on a decomposition theorem of Cygan, Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh [SICOMP '19], which provides a tree decomposition of a given graph into bags that are unbreakable. Crucially, unbreakability allows to reduce separator logic to plain first-order logic within each bag individually. Guided by this observation, we design our model-checking algorithm using dynamic programming over the tree decomposition, where the transition at each bag amounts to running a suitable model-checking subprocedure for plain first-order logic. This approach is robust enough to provide also an extension to efficient enumeration of answers to a query expressed in separator logic.

Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny. Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 102:1-102:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{pilipczuk_et_al:LIPIcs.ICALP.2022.102, author = {Pilipczuk, Micha{\l} and Schirrmacher, Nicole and Siebertz, Sebastian and Toru\'{n}czyk, Szymon and Vigny, Alexandre}, title = {{Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {102:1--102:18}, 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.102}, URN = {urn:nbn:de:0030-drops-164432}, doi = {10.4230/LIPIcs.ICALP.2022.102}, annote = {Keywords: Combinatorics and graph theory, Computational applications of logic, Data structures, Fixed-parameter algorithms and complexity, Graph algorithms} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

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

We study problems connected to first-order logic in graphs of bounded twin-width. Inspired by the approach of Bonnet et al. [FOCS 2020], we introduce a robust methodology of local types and describe their behavior in contraction sequences - the decomposition notion underlying twin-width. We showcase the applicability of the methodology by proving the following two algorithmic results. In both statements, we fix a first-order formula φ(x_1,…,x_k) and a constant d, and we assume that on input we are given a graph G together with a contraction sequence of width at most d.
- One can in time 𝒪(n) construct a data structure that can answer the following queries in time 𝒪(log log n): given w_1,…,w_k, decide whether φ(w_1,…,w_k) holds in G.
- After 𝒪(n)-time preprocessing, one can enumerate all tuples w₁,…,w_k that satisfy φ(x_1,…,x_k) in G with 𝒪(1) delay. In the first case, the query time can be reduced to 𝒪(1/ε) at the expense of increasing the construction time to 𝒪(n^{1+ε}), for any fixed ε > 0. Finally, we also apply our tools to prove the following statement, which shows optimal bounds on the VC density of set systems that are first-order definable in graphs of bounded twin-width.
- Let G be a graph of twin-width d, A be a subset of vertices of G, and φ(x_1,…,x_k,y_1,…,y_l) be a first-order formula. Then the number of different subsets of A^k definable by φ using l-tuples of vertices from G as parameters, is bounded by O(|A|^l).

Jakub Gajarský, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Twin-Width and Types. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 123:1-123:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2022.123, author = {Gajarsk\'{y}, Jakub and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Toru\'{n}czyk, Szymon}, title = {{Twin-Width and Types}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {123:1--123:21}, 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.123}, URN = {urn:nbn:de:0030-drops-164640}, doi = {10.4230/LIPIcs.ICALP.2022.123}, annote = {Keywords: twin-width, FO logic, model checking, query answering, enumeration} }

Document

**Published in:** LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

We consider a generic algorithmic paradigm that we call progressive exploration, which can be used to develop simple and efficient parameterized graph algorithms. We identify two model-theoretic properties that lead to efficient progressive algorithms, namely variants of the Helly property and stability. We demonstrate our approach by giving linear-time fixed-parameter algorithms for the Distance-r Dominating Set problem (parameterized by the solution size) in a wide variety of restricted graph classes, such as powers of nowhere dense classes, map graphs, and (for r=1) biclique-free graphs. Similarly, for the Distance-r Independent Set problem the technique can be used to give a linear-time fixed-parameter algorithm on any nowhere dense class. Despite the simplicity of the method, in several cases our results extend known boundaries of tractability for the considered problems and improve the best known running times.

Grzegorz Fabiański, Michał Pilipczuk, Sebastian Siebertz, and Szymon Toruńczyk. Progressive Algorithms for Domination and Independence. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{fabianski_et_al:LIPIcs.STACS.2019.27, author = {Fabia\'{n}ski, Grzegorz and Pilipczuk, Micha{\l} and Siebertz, Sebastian and Toru\'{n}czyk, Szymon}, title = {{Progressive Algorithms for Domination and Independence}}, booktitle = {36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)}, pages = {27:1--27:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-100-9}, ISSN = {1868-8969}, year = {2019}, volume = {126}, editor = {Niedermeier, Rolf and Paul, Christophe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.27}, URN = {urn:nbn:de:0030-drops-102660}, doi = {10.4230/LIPIcs.STACS.2019.27}, annote = {Keywords: Dominating Set, Independent Set, nowhere denseness, stability, fixed-parameter tractability} }

Document

**Published in:** LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

The notion of bounded expansion captures uniform sparsity of graph classes and renders various algorithmic problems that are hard in general tractable. In particular, the model-checking problem for first-order logic is fixed-parameter tractable over such graph classes. With the aim of generalizing such results to dense graphs, we introduce classes of graphs with structurally bounded expansion, defined as first-order interpretations of classes of bounded expansion. As a first step towards their algorithmic treatment, we provide their characterization analogous to the characterization of classes of bounded expansion via low treedepth decompositions, replacing treedepth by its dense analogue called shrubdepth.

Jakub Gajarský, Stephan Kreutzer, Jaroslav Nesetril, Patrice Ossona de Mendez, Michal Pilipczuk, Sebastian Siebertz, and Szymon Torunczyk. First-Order Interpretations of Bounded Expansion Classes. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 126:1-126:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2018.126, author = {Gajarsk\'{y}, Jakub and Kreutzer, Stephan and Nesetril, Jaroslav and Ossona de Mendez, Patrice and Pilipczuk, Michal and Siebertz, Sebastian and Torunczyk, Szymon}, title = {{First-Order Interpretations of Bounded Expansion Classes}}, booktitle = {45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)}, pages = {126:1--126:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-076-7}, ISSN = {1868-8969}, year = {2018}, volume = {107}, editor = {Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.126}, URN = {urn:nbn:de:0030-drops-91300}, doi = {10.4230/LIPIcs.ICALP.2018.126}, annote = {Keywords: Logical interpretations/transductions, structurally sparse graphs, bounded expansion} }

Document

**Published in:** LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

We study the problem of finding the worst-case size of the result Q(D) of a fixed conjunctive query Q applied to a database D satisfying given functional dependencies. We provide a characterization of this bound in terms of entropy vectors, and in terms of finite groups. In particular, we show that an upper bound provided by [Gottlob, Lee, Valiant and Valiant, J.ACM, 2012] is tight, and that a correspondence of [Chan and Yeung, ACM TOIT, 2002] is preserved in the presence of functional dependencies. However, tightness of a weaker upper bound provided by Gottlob et al., which would have immediate applications to evaluation of join queries ([Khamis, Ngo, and Suciu, PODS, 2016]) remains open. Our result shows that the problem of computing the worst-case size bound, in the general case, is closely related to difficult problems from information theory.

Tomasz Gogacz and Szymon Torunczyk. Entropy Bounds for Conjunctive Queries with Functional Dependencies. In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gogacz_et_al:LIPIcs.ICDT.2017.15, author = {Gogacz, Tomasz and Torunczyk, Szymon}, title = {{Entropy Bounds for Conjunctive Queries with Functional Dependencies}}, booktitle = {20th International Conference on Database Theory (ICDT 2017)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-024-8}, ISSN = {1868-8969}, year = {2017}, volume = {68}, editor = {Benedikt, Michael and Orsi, Giorgio}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017.15}, URN = {urn:nbn:de:0030-drops-70479}, doi = {10.4230/LIPIcs.ICDT.2017.15}, annote = {Keywords: database theory, conjunctive queries, size bounds, entropy, finite groups, entropy cone} }

Document

**Published in:** LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

We investigate several variants of the homomorphism problem: given two relational structures, is there a homomorphism from one to the other? The input structures are possibly infinite, but definable by first-order interpretations in a fixed structure. Their signatures can be either finite or infinite but definable. The homomorphisms can be either arbitrary, or definable with parameters, or definable without parameters. For each of these variants, we determine its decidability status.

Bartek Klin, Slawomir Lasota, Joanna Ochremiak, and Szymon Torunczyk. Homomorphism Problems for First-Order Definable Structures. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.FSTTCS.2016.14, author = {Klin, Bartek and Lasota, Slawomir and Ochremiak, Joanna and Torunczyk, Szymon}, title = {{Homomorphism Problems for First-Order Definable Structures}}, booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)}, pages = {14:1--14:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-027-9}, ISSN = {1868-8969}, year = {2016}, volume = {65}, editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.14}, URN = {urn:nbn:de:0030-drops-68498}, doi = {10.4230/LIPIcs.FSTTCS.2016.14}, annote = {Keywords: Sets with atoms, first-order interpretations, homomorphism problem} }

Document

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

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.

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.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

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

Homogenization is a powerful way of taming a class of finite structures with several interesting applications in different areas, from Ramsey theory in combinatorics to constraint satisfaction problems (CSPs) in computer science, through (finite) model theory. A few sufficient conditions for a class of finite structures to allow homogenization are known, and here we provide a necessary condition. This lets us show that certain natural classes are not homogenizable: 1) the class of locally consistent systems of linear equations over the two-element field or any finite Abelian group, and 2) the class of finite structures that forbid homomorphisms from a specific MSO-definable class of structures of treewidth two. In combination with known results, the first example shows that, up to pp-interpretability, the CSPs that are solvable by local consistency methods are distinguished from the rest by the fact that their classes of locally consistent instances are homogenizable. The second example shows that, for MSO-definable classes of forbidden patterns, treewidth one versus two is the dividing line to homogenizability.

Albert Atserias and Szymon Torunczyk. Non-Homogenizable Classes of Finite Structures. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{atserias_et_al:LIPIcs.CSL.2016.16, author = {Atserias, Albert and Torunczyk, Szymon}, title = {{Non-Homogenizable Classes of Finite Structures}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {16:1--16:16}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.16}, URN = {urn:nbn:de:0030-drops-65563}, doi = {10.4230/LIPIcs.CSL.2016.16}, annote = {Keywords: Fra\"{i}ss\'{e} class, amalgmation class, reduct, Constraint Satisfaction Problem, bounded width} }

Document

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

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.

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.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} }

Document

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

Regular cost functions form a quantitative extension of regular languages that share the array of characterisations the latter possess. In this theory, functions are treated only up to preservation of boundedness on all subsets of the domain. In this work, we subject the well known distance automata (also called min-automata), and their dual max-automata to this framework, and obtain a number of effective characterisations in terms of logic, expressions and algebra.

Thomas Colcombet, Denis Kuperberg, Amaldev Manuel, and Szymon Torunczyk. Cost Functions Definable by Min/Max Automata. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2016.29, author = {Colcombet, Thomas and Kuperberg, Denis and Manuel, Amaldev and Torunczyk, Szymon}, title = {{Cost Functions Definable by Min/Max Automata}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {29:1--29:13}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.29}, URN = {urn:nbn:de:0030-drops-57305}, doi = {10.4230/LIPIcs.STACS.2016.29}, annote = {Keywords: distance automata, B-automata, regular cost functions, stabilisation monoids, decidability, min-automata, max-automata} }

Document

**Published in:** LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

We define an imperative programming language, which extends while programs with a type for storing atoms or hereditarily orbit-finite sets. To deal with an orbit-finite set, the language has a loop construction, which is executed in parallel for all elements of an orbit-finite set. We show examples of programs in this language, e.g. a program for minimising deterministic orbit-finite automata.

Mikolaj Bojanczyk and Szymon Torunczyk. Imperative Programming in Sets with Atoms. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 4-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2012.4, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Imperative Programming in Sets with Atoms}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)}, pages = {4--15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-47-7}, ISSN = {1868-8969}, year = {2012}, volume = {18}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.4}, URN = {urn:nbn:de:0030-drops-38437}, doi = {10.4230/LIPIcs.FSTTCS.2012.4}, annote = {Keywords: Nominal sets, sets with atoms, while programs} }

Document

**Published in:** LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

We prove that, over infinite trees, satisfiability is decidable for Weak Monadic Second-Order Logic extended by the unbounding quantifier U. We develop an automaton model, prove that it is effectively equivalent to the logic, and that the automaton model has decidable emptiness.

Mikolaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 648-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2012.648, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Weak MSO+U over infinite trees}}, booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)}, pages = {648--660}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-35-4}, ISSN = {1868-8969}, year = {2012}, volume = {14}, editor = {D\"{u}rr, Christoph and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.648}, URN = {urn:nbn:de:0030-drops-34279}, doi = {10.4230/LIPIcs.STACS.2012.648}, annote = {Keywords: Infinite trees, distance automata, MSO+U, profinite words} }

Document

**Published in:** LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

In this paper we work over linearly ordered data domains equipped with finitely many unary predicates and constants. We consider nondeterministic automata processing words and storing finitely many variables ranging over the domain. During a transition, these automata can compare the data values of the current configuration with those of the previous configuration using the linear order, the unary predicates and the constants.
We show that emptiness for such automata is decidable, both over finite and infinite words, under reasonable computability assumptions on the linear order.
Finally, we show how our automata model can be used for verifying properties of workflow specifications in the presence of an underlying database.

Luc Segoufin and Szymon Torunczyk. Automata based verification over linearly ordered data domains. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 81-92, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{segoufin_et_al:LIPIcs.STACS.2011.81, author = {Segoufin, Luc and Torunczyk, Szymon}, title = {{Automata based verification over linearly ordered data domains}}, booktitle = {28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)}, pages = {81--92}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-25-5}, ISSN = {1868-8969}, year = {2011}, volume = {9}, editor = {Schwentick, Thomas and D\"{u}rr, Christoph}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.81}, URN = {urn:nbn:de:0030-drops-30017}, doi = {10.4230/LIPIcs.STACS.2011.81}, annote = {Keywords: register automata, data values, linear order} }

Document

**Published in:** LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

We introduce a new class of automata on infinite words, called
min-automata. We prove that min-automata have the same expressive
power as weak monadic second-order logic (weak MSO) extended with a new
quantifier, the recurrence quantifier. These results are dual to a
framework presented in \cite{max-automata}, where max-automata were proved equivalent
to weak MSO extended with an unbounding
quantifier. We also present a general framework, which tries to
explain which types of automata on infinite words correspond to
extensions of weak MSO. As another example for the usefulness framework,
apart from min- and max-automata, we define an extension of weak MSO
with a quantifier that talks about ultimately periodic sets.

Mikolaj Bojanczyk and Szymon Torunczyk. Deterministic Automata and Extensions of Weak MSO. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 73-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2009.2308, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Deterministic Automata and Extensions of Weak MSO}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {73--84}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2308}, URN = {urn:nbn:de:0030-drops-23081}, doi = {10.4230/LIPIcs.FSTTCS.2009.2308}, annote = {Keywords: Deterministic automata, Weak MSO, min-automata, max-automata, BS-automata} }

Document

Invited Talk

**Published in:** LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Sparsity theory, initiated by Ossona de Mendez and Nešetřil, identifies those classes of sparse graphs that are tractable in various ways - algorithmically, combinatorially, and logically - as exactly the nowhere dense classes. An ongoing effort aims at generalizing sparsity theory to classes of graphs that are not necessarily sparse. Twin-width theory, developed by Bonnet, Thomassé and co-authors, is a step in that direction. A theory unifying the two is anticipated. It is conjectured that the relevant notion characterising dense graph classes that are tractable, generalising nowhere denseness and bounded twin-width, is the notion of a monadically dependent class, introduced by Shelah in model theory. I will survey the recent, rapid progress in the understanding of those classes, and of the related monadically stable classes. This development combines tools from structural graph theory, logic (finite and infinite model theory), and algorithms (parameterised algorithms and range search queries).

Szymon Toruńczyk. Structurally Tractable Graph Classes (Invited Talk). In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{torunczyk:LIPIcs.STACS.2024.3, author = {Toru\'{n}czyk, Szymon}, title = {{Structurally Tractable Graph Classes}}, booktitle = {41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)}, pages = {3:1--3:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-311-9}, ISSN = {1868-8969}, year = {2024}, volume = {289}, editor = {Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.3}, URN = {urn:nbn:de:0030-drops-197134}, doi = {10.4230/LIPIcs.STACS.2024.3}, annote = {Keywords: Structural graph theory, Monadic dependence, monadic NIP, twin-width} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Monadically stable and monadically NIP classes of structures were initially studied in the context of model theory and defined in logical terms. They have recently attracted attention in the area of structural graph theory, as they generalize notions such as nowhere denseness, bounded cliquewidth, and bounded twinwidth.
Our main result is the - to the best of our knowledge first - purely combinatorial characterization of monadically stable classes of graphs, in terms of a property dubbed flip-flatness. A class C of graphs is flip-flat if for every fixed radius r, every sufficiently large set of vertices of a graph G ∈ C contains a large subset of vertices with mutual distance larger than r, where the distance is measured in some graph G' that can be obtained from G by performing a bounded number of flips that swap edges and non-edges within a subset of vertices. Flip-flatness generalizes the notion of uniform quasi-wideness, which characterizes nowhere dense classes and had a key impact on the combinatorial and algorithmic treatment of nowhere dense classes. To obtain this result, we develop tools that also apply to the more general monadically NIP classes, based on the notion of indiscernible sequences from model theory. We show that in monadically stable and monadically NIP classes indiscernible sequences impose a strong combinatorial structure on their definable neighborhoods. All our proofs are constructive and yield efficient algorithms.

Jan Dreier, Nikolas Mählmann, Sebastian Siebertz, and Szymon Toruńczyk. Indiscernibles and Flatness in Monadically Stable and Monadically NIP Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 125:1-125:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dreier_et_al:LIPIcs.ICALP.2023.125, author = {Dreier, Jan and M\"{a}hlmann, Nikolas and Siebertz, Sebastian and Toru\'{n}czyk, Szymon}, title = {{Indiscernibles and Flatness in Monadically Stable and Monadically NIP Classes}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {125:1--125:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.125}, URN = {urn:nbn:de:0030-drops-181779}, doi = {10.4230/LIPIcs.ICALP.2023.125}, annote = {Keywords: stability, NIP, combinatorial characterization, first-order model checking} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

A class of graphs C is monadically stable if for every unary expansion Ĉ of C, one cannot encode - using first-order transductions - arbitrarily long linear orders in graphs from C. It is known that nowhere dense graph classes are monadically stable; these include classes of bounded maximum degree and classes that exclude a fixed topological minor. On the other hand, monadic stability is a property expressed in purely model-theoretic terms that is also suited for capturing structure in dense graphs.
In this work we provide a characterization of monadic stability in terms of the Flipper game: a game on a graph played by Flipper, who in each round can complement the edge relation between any pair of vertex subsets, and Localizer, who in each round is forced to restrict the game to a ball of bounded radius. This is an analog of the Splitter game, which characterizes nowhere dense classes of graphs (Grohe, Kreutzer, and Siebertz, J. ACM '17).
We give two different proofs of our main result. The first proof is based on tools borrowed from model theory, and it exposes an additional property of monadically stable graph classes that is close in spirit to definability of types. Also, as a byproduct, we show that monadic stability for graph classes coincides with monadic stability of existential formulas with two free variables, and we provide another combinatorial characterization of monadic stability via forbidden patterns. The second proof relies on the recently introduced notion of flip-flatness (Dreier, Mählmann, Siebertz, and Toruńczyk, arXiv 2206.13765) and provides an efficient algorithm to compute Flipper’s moves in a winning strategy.

Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokołowski, and Szymon Toruńczyk. Flipper Games for Monadically Stable Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 128:1-128:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2023.128, author = {Gajarsk\'{y}, Jakub and M\"{a}hlmann, Nikolas and McCarty, Rose and Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Siebertz, Sebastian and Soko{\l}owski, Marek and Toru\'{n}czyk, Szymon}, title = {{Flipper Games for Monadically Stable Graph Classes}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {128:1--128:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.128}, URN = {urn:nbn:de:0030-drops-181804}, doi = {10.4230/LIPIcs.ICALP.2023.128}, annote = {Keywords: Stability theory, structural graph theory, games} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

**Published in:** LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

We use model-theoretic tools originating from stability theory to derive a result we call the Finitary Substitute Lemma, which intuitively says the following. Suppose we work in a stable graph class 𝒞, and using a first-order formula φ with parameters we are able to define, in every graph G ∈ 𝒞, a relation R that satisfies some hereditary first-order assertion ψ. Then we are able to find a first-order formula φ' that has the same property, but additionally is finitary: there is finite bound k ∈ ℕ such that in every graph G ∈ 𝒞, different choices of parameters give only at most k different relations R that can be defined using φ'.
We use the Finitary Substitute Lemma to derive two corollaries about the existence of certain canonical decompositions in classes of well-structured graphs.
- We prove that in the Splitter game, which characterizes nowhere dense graph classes, and in the Flipper game, which characterizes monadically stable graph classes, there is a winning strategy for Splitter, respectively Flipper, that can be defined in first-order logic from the game history. Thus, the strategy is canonical.
- We show that for any fixed graph class 𝒞 of bounded shrubdepth, there is an 𝒪(n²)-time algorithm that given an n-vertex graph G ∈ 𝒞, computes in an isomorphism-invariant way a structure H of bounded treedepth in which G can be interpreted. A corollary of this result is an 𝒪(n²)-time isomorphism test and canonization algorithm for any fixed class of bounded shrubdepth.

Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 135:1-135:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ohlmann_et_al:LIPIcs.ICALP.2023.135, author = {Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Toru\'{n}czyk, Szymon}, title = {{Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes}}, booktitle = {50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)}, pages = {135:1--135:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-278-5}, ISSN = {1868-8969}, year = {2023}, volume = {261}, editor = {Etessami, Kousha and Feige, Uriel and Puppis, Gabriele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.135}, URN = {urn:nbn:de:0030-drops-181874}, doi = {10.4230/LIPIcs.ICALP.2023.135}, annote = {Keywords: Model Theory, Stability Theory, Shrubdepth, Nowhere Dense, Monadically Stable} }

Document

Track A: Algorithms, Complexity and Games

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

We introduce a new data structure for answering connectivity queries in undirected graphs subject to batched vertex failures. Precisely, given any graph G and integer parameter k, we can in fixed-parameter time construct a data structure that can later be used to answer queries of the form: "are vertices s and t connected via a path that avoids vertices u₁,…, u_k?" in time 2^𝒪(k). In the terminology of the literature on data structures, this gives the first deterministic data structure for connectivity under vertex failures where for every fixed number of failures, all operations can be performed in constant time.
With the aim to understand the power and the limitations of our new techniques, we prove an algorithmic meta theorem for the recently introduced separator logic, which extends first-order logic with atoms for connectivity under vertex failures. We prove that the model-checking problem for separator logic is fixed-parameter tractable on every class of graphs that exclude a fixed topological minor. We also show a weak converse. This implies that from the point of view of parameterized complexity, under standard complexity theoretical assumptions, the frontier of tractability of separator logic is almost exactly delimited by classes excluding a fixed topological minor.
The backbone of our proof relies on a decomposition theorem of Cygan, Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh [SICOMP '19], which provides a tree decomposition of a given graph into bags that are unbreakable. Crucially, unbreakability allows to reduce separator logic to plain first-order logic within each bag individually. Guided by this observation, we design our model-checking algorithm using dynamic programming over the tree decomposition, where the transition at each bag amounts to running a suitable model-checking subprocedure for plain first-order logic. This approach is robust enough to provide also an extension to efficient enumeration of answers to a query expressed in separator logic.

Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny. Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 102:1-102:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{pilipczuk_et_al:LIPIcs.ICALP.2022.102, author = {Pilipczuk, Micha{\l} and Schirrmacher, Nicole and Siebertz, Sebastian and Toru\'{n}czyk, Szymon and Vigny, Alexandre}, title = {{Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {102:1--102:18}, 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.102}, URN = {urn:nbn:de:0030-drops-164432}, doi = {10.4230/LIPIcs.ICALP.2022.102}, annote = {Keywords: Combinatorics and graph theory, Computational applications of logic, Data structures, Fixed-parameter algorithms and complexity, Graph algorithms} }

Document

Track B: Automata, Logic, Semantics, and Theory of Programming

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

We study problems connected to first-order logic in graphs of bounded twin-width. Inspired by the approach of Bonnet et al. [FOCS 2020], we introduce a robust methodology of local types and describe their behavior in contraction sequences - the decomposition notion underlying twin-width. We showcase the applicability of the methodology by proving the following two algorithmic results. In both statements, we fix a first-order formula φ(x_1,…,x_k) and a constant d, and we assume that on input we are given a graph G together with a contraction sequence of width at most d.
- One can in time 𝒪(n) construct a data structure that can answer the following queries in time 𝒪(log log n): given w_1,…,w_k, decide whether φ(w_1,…,w_k) holds in G.
- After 𝒪(n)-time preprocessing, one can enumerate all tuples w₁,…,w_k that satisfy φ(x_1,…,x_k) in G with 𝒪(1) delay. In the first case, the query time can be reduced to 𝒪(1/ε) at the expense of increasing the construction time to 𝒪(n^{1+ε}), for any fixed ε > 0. Finally, we also apply our tools to prove the following statement, which shows optimal bounds on the VC density of set systems that are first-order definable in graphs of bounded twin-width.
- Let G be a graph of twin-width d, A be a subset of vertices of G, and φ(x_1,…,x_k,y_1,…,y_l) be a first-order formula. Then the number of different subsets of A^k definable by φ using l-tuples of vertices from G as parameters, is bounded by O(|A|^l).

Jakub Gajarský, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Twin-Width and Types. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 123:1-123:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2022.123, author = {Gajarsk\'{y}, Jakub and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Toru\'{n}czyk, Szymon}, title = {{Twin-Width and Types}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {123:1--123:21}, 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.123}, URN = {urn:nbn:de:0030-drops-164640}, doi = {10.4230/LIPIcs.ICALP.2022.123}, annote = {Keywords: twin-width, FO logic, model checking, query answering, enumeration} }

Document

**Published in:** LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

We consider a generic algorithmic paradigm that we call progressive exploration, which can be used to develop simple and efficient parameterized graph algorithms. We identify two model-theoretic properties that lead to efficient progressive algorithms, namely variants of the Helly property and stability. We demonstrate our approach by giving linear-time fixed-parameter algorithms for the Distance-r Dominating Set problem (parameterized by the solution size) in a wide variety of restricted graph classes, such as powers of nowhere dense classes, map graphs, and (for r=1) biclique-free graphs. Similarly, for the Distance-r Independent Set problem the technique can be used to give a linear-time fixed-parameter algorithm on any nowhere dense class. Despite the simplicity of the method, in several cases our results extend known boundaries of tractability for the considered problems and improve the best known running times.

Grzegorz Fabiański, Michał Pilipczuk, Sebastian Siebertz, and Szymon Toruńczyk. Progressive Algorithms for Domination and Independence. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{fabianski_et_al:LIPIcs.STACS.2019.27, author = {Fabia\'{n}ski, Grzegorz and Pilipczuk, Micha{\l} and Siebertz, Sebastian and Toru\'{n}czyk, Szymon}, title = {{Progressive Algorithms for Domination and Independence}}, booktitle = {36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)}, pages = {27:1--27:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-100-9}, ISSN = {1868-8969}, year = {2019}, volume = {126}, editor = {Niedermeier, Rolf and Paul, Christophe}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.27}, URN = {urn:nbn:de:0030-drops-102660}, doi = {10.4230/LIPIcs.STACS.2019.27}, annote = {Keywords: Dominating Set, Independent Set, nowhere denseness, stability, fixed-parameter tractability} }

Document

**Published in:** LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

The notion of bounded expansion captures uniform sparsity of graph classes and renders various algorithmic problems that are hard in general tractable. In particular, the model-checking problem for first-order logic is fixed-parameter tractable over such graph classes. With the aim of generalizing such results to dense graphs, we introduce classes of graphs with structurally bounded expansion, defined as first-order interpretations of classes of bounded expansion. As a first step towards their algorithmic treatment, we provide their characterization analogous to the characterization of classes of bounded expansion via low treedepth decompositions, replacing treedepth by its dense analogue called shrubdepth.

Jakub Gajarský, Stephan Kreutzer, Jaroslav Nesetril, Patrice Ossona de Mendez, Michal Pilipczuk, Sebastian Siebertz, and Szymon Torunczyk. First-Order Interpretations of Bounded Expansion Classes. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 126:1-126:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2018.126, author = {Gajarsk\'{y}, Jakub and Kreutzer, Stephan and Nesetril, Jaroslav and Ossona de Mendez, Patrice and Pilipczuk, Michal and Siebertz, Sebastian and Torunczyk, Szymon}, title = {{First-Order Interpretations of Bounded Expansion Classes}}, booktitle = {45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)}, pages = {126:1--126:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-076-7}, ISSN = {1868-8969}, year = {2018}, volume = {107}, editor = {Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.126}, URN = {urn:nbn:de:0030-drops-91300}, doi = {10.4230/LIPIcs.ICALP.2018.126}, annote = {Keywords: Logical interpretations/transductions, structurally sparse graphs, bounded expansion} }

Document

**Published in:** LIPIcs, Volume 68, 20th International Conference on Database Theory (ICDT 2017)

We study the problem of finding the worst-case size of the result Q(D) of a fixed conjunctive query Q applied to a database D satisfying given functional dependencies. We provide a characterization of this bound in terms of entropy vectors, and in terms of finite groups. In particular, we show that an upper bound provided by [Gottlob, Lee, Valiant and Valiant, J.ACM, 2012] is tight, and that a correspondence of [Chan and Yeung, ACM TOIT, 2002] is preserved in the presence of functional dependencies. However, tightness of a weaker upper bound provided by Gottlob et al., which would have immediate applications to evaluation of join queries ([Khamis, Ngo, and Suciu, PODS, 2016]) remains open. Our result shows that the problem of computing the worst-case size bound, in the general case, is closely related to difficult problems from information theory.

Tomasz Gogacz and Szymon Torunczyk. Entropy Bounds for Conjunctive Queries with Functional Dependencies. In 20th International Conference on Database Theory (ICDT 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 68, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gogacz_et_al:LIPIcs.ICDT.2017.15, author = {Gogacz, Tomasz and Torunczyk, Szymon}, title = {{Entropy Bounds for Conjunctive Queries with Functional Dependencies}}, booktitle = {20th International Conference on Database Theory (ICDT 2017)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-024-8}, ISSN = {1868-8969}, year = {2017}, volume = {68}, editor = {Benedikt, Michael and Orsi, Giorgio}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2017.15}, URN = {urn:nbn:de:0030-drops-70479}, doi = {10.4230/LIPIcs.ICDT.2017.15}, annote = {Keywords: database theory, conjunctive queries, size bounds, entropy, finite groups, entropy cone} }

Document

**Published in:** LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

We investigate several variants of the homomorphism problem: given two relational structures, is there a homomorphism from one to the other? The input structures are possibly infinite, but definable by first-order interpretations in a fixed structure. Their signatures can be either finite or infinite but definable. The homomorphisms can be either arbitrary, or definable with parameters, or definable without parameters. For each of these variants, we determine its decidability status.

Bartek Klin, Slawomir Lasota, Joanna Ochremiak, and Szymon Torunczyk. Homomorphism Problems for First-Order Definable Structures. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.FSTTCS.2016.14, author = {Klin, Bartek and Lasota, Slawomir and Ochremiak, Joanna and Torunczyk, Szymon}, title = {{Homomorphism Problems for First-Order Definable Structures}}, booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)}, pages = {14:1--14:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-027-9}, ISSN = {1868-8969}, year = {2016}, volume = {65}, editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.14}, URN = {urn:nbn:de:0030-drops-68498}, doi = {10.4230/LIPIcs.FSTTCS.2016.14}, annote = {Keywords: Sets with atoms, first-order interpretations, homomorphism problem} }

Document

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

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.

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.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

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

Homogenization is a powerful way of taming a class of finite structures with several interesting applications in different areas, from Ramsey theory in combinatorics to constraint satisfaction problems (CSPs) in computer science, through (finite) model theory. A few sufficient conditions for a class of finite structures to allow homogenization are known, and here we provide a necessary condition. This lets us show that certain natural classes are not homogenizable: 1) the class of locally consistent systems of linear equations over the two-element field or any finite Abelian group, and 2) the class of finite structures that forbid homomorphisms from a specific MSO-definable class of structures of treewidth two. In combination with known results, the first example shows that, up to pp-interpretability, the CSPs that are solvable by local consistency methods are distinguished from the rest by the fact that their classes of locally consistent instances are homogenizable. The second example shows that, for MSO-definable classes of forbidden patterns, treewidth one versus two is the dividing line to homogenizability.

Albert Atserias and Szymon Torunczyk. Non-Homogenizable Classes of Finite Structures. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{atserias_et_al:LIPIcs.CSL.2016.16, author = {Atserias, Albert and Torunczyk, Szymon}, title = {{Non-Homogenizable Classes of Finite Structures}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {16:1--16:16}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.16}, URN = {urn:nbn:de:0030-drops-65563}, doi = {10.4230/LIPIcs.CSL.2016.16}, annote = {Keywords: Fra\"{i}ss\'{e} class, amalgmation class, reduct, Constraint Satisfaction Problem, bounded width} }

Document

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

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.

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.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} }

Document

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

Regular cost functions form a quantitative extension of regular languages that share the array of characterisations the latter possess. In this theory, functions are treated only up to preservation of boundedness on all subsets of the domain. In this work, we subject the well known distance automata (also called min-automata), and their dual max-automata to this framework, and obtain a number of effective characterisations in terms of logic, expressions and algebra.

Thomas Colcombet, Denis Kuperberg, Amaldev Manuel, and Szymon Torunczyk. Cost Functions Definable by Min/Max Automata. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.STACS.2016.29, author = {Colcombet, Thomas and Kuperberg, Denis and Manuel, Amaldev and Torunczyk, Szymon}, title = {{Cost Functions Definable by Min/Max Automata}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {29:1--29:13}, 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.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.29}, URN = {urn:nbn:de:0030-drops-57305}, doi = {10.4230/LIPIcs.STACS.2016.29}, annote = {Keywords: distance automata, B-automata, regular cost functions, stabilisation monoids, decidability, min-automata, max-automata} }

Document

**Published in:** LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

We define an imperative programming language, which extends while programs with a type for storing atoms or hereditarily orbit-finite sets. To deal with an orbit-finite set, the language has a loop construction, which is executed in parallel for all elements of an orbit-finite set. We show examples of programs in this language, e.g. a program for minimising deterministic orbit-finite automata.

Mikolaj Bojanczyk and Szymon Torunczyk. Imperative Programming in Sets with Atoms. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 4-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2012.4, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Imperative Programming in Sets with Atoms}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)}, pages = {4--15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-47-7}, ISSN = {1868-8969}, year = {2012}, volume = {18}, editor = {D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.4}, URN = {urn:nbn:de:0030-drops-38437}, doi = {10.4230/LIPIcs.FSTTCS.2012.4}, annote = {Keywords: Nominal sets, sets with atoms, while programs} }

Document

**Published in:** LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

We prove that, over infinite trees, satisfiability is decidable for Weak Monadic Second-Order Logic extended by the unbounding quantifier U. We develop an automaton model, prove that it is effectively equivalent to the logic, and that the automaton model has decidable emptiness.

Mikolaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 648-660, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.STACS.2012.648, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Weak MSO+U over infinite trees}}, booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)}, pages = {648--660}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-35-4}, ISSN = {1868-8969}, year = {2012}, volume = {14}, editor = {D\"{u}rr, Christoph and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.648}, URN = {urn:nbn:de:0030-drops-34279}, doi = {10.4230/LIPIcs.STACS.2012.648}, annote = {Keywords: Infinite trees, distance automata, MSO+U, profinite words} }

Document

**Published in:** LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

In this paper we work over linearly ordered data domains equipped with finitely many unary predicates and constants. We consider nondeterministic automata processing words and storing finitely many variables ranging over the domain. During a transition, these automata can compare the data values of the current configuration with those of the previous configuration using the linear order, the unary predicates and the constants.
We show that emptiness for such automata is decidable, both over finite and infinite words, under reasonable computability assumptions on the linear order.
Finally, we show how our automata model can be used for verifying properties of workflow specifications in the presence of an underlying database.

Luc Segoufin and Szymon Torunczyk. Automata based verification over linearly ordered data domains. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 81-92, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{segoufin_et_al:LIPIcs.STACS.2011.81, author = {Segoufin, Luc and Torunczyk, Szymon}, title = {{Automata based verification over linearly ordered data domains}}, booktitle = {28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)}, pages = {81--92}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-25-5}, ISSN = {1868-8969}, year = {2011}, volume = {9}, editor = {Schwentick, Thomas and D\"{u}rr, Christoph}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.81}, URN = {urn:nbn:de:0030-drops-30017}, doi = {10.4230/LIPIcs.STACS.2011.81}, annote = {Keywords: register automata, data values, linear order} }

Document

**Published in:** LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009)

We introduce a new class of automata on infinite words, called
min-automata. We prove that min-automata have the same expressive
power as weak monadic second-order logic (weak MSO) extended with a new
quantifier, the recurrence quantifier. These results are dual to a
framework presented in \cite{max-automata}, where max-automata were proved equivalent
to weak MSO extended with an unbounding
quantifier. We also present a general framework, which tries to
explain which types of automata on infinite words correspond to
extensions of weak MSO. As another example for the usefulness framework,
apart from min- and max-automata, we define an extension of weak MSO
with a quantifier that talks about ultimately periodic sets.

Mikolaj Bojanczyk and Szymon Torunczyk. Deterministic Automata and Extensions of Weak MSO. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 73-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.FSTTCS.2009.2308, author = {Bojanczyk, Mikolaj and Torunczyk, Szymon}, title = {{Deterministic Automata and Extensions of Weak MSO}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {73--84}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2308}, URN = {urn:nbn:de:0030-drops-23081}, doi = {10.4230/LIPIcs.FSTTCS.2009.2308}, annote = {Keywords: Deterministic automata, Weak MSO, min-automata, max-automata, BS-automata} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail