Szymon Toruńczyk

Highlights Conference 2025 Conference Abstract

Monadically dependent classes and the model checking problem

• Szymon Toruńczyk

Highlights Conference 2022 Conference Abstract

Ordered Graphs of Bounded Twin-Width

• Szymon Toruńczyk

We establish a list of characterizations of bounded twin-width for hereditary classes of totally ordered graphs: as classes of at most exponential growth studied in enumerative combinatorics, as monadically NIP classes studied in model theory, as classes that do not transduce the class of all graphs studied in finite model theory, and as classes for which model checking first-order logic is fixed-parameter tractable studied in algorithmic graph theory. This has several consequences. First, it allows us to show that every hereditary class of ordered graphs either has at most exponential growth, or has at least factorial growth. This settles a question first asked by Balogh, Bollobás, and Morris [Eur. J. Comb. '06] on the growth of hereditary classes of ordered graphs, generalizing the Stanley-Wilf conjecture/Marcus-Tardos theorem. Second, it gives a fixed-parameter approximation algorithm for twin-width on ordered graphs. Third, it yields a full classification of fixed-parameter tractable first-order model checking on hereditary classes of ordered binary structures. Fourth, it provides a model-theoretic characterization of classes with bounded twin-width.

Highlights Conference 2017 Conference Abstract

On computability and tractability for infinite sets

• Szymon Toruńczyk

Abstract available in PDF.

Highlights Conference 2016 Conference Abstract

The MSO+U Theory of (N, <) Is Undecidable

• Mikołaj Bojańczyk
• Paweł Parys
• Szymon Toruńczyk

We consider the logic MSO+U, which is monadic second-order logic extended with the unbounding quantifier. The unbounding quantifier is used to say that a property of finite sets 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. This work was published on STACS 2016.

Highlights Conference 2016 Conference Abstract

Towards complexity theory with atoms

• Szymon Toruńczyk

I will discuss various classical computational problems, generalized to the setting where the instances are potentially infinite sets with atoms. In particular, we will focus on constraint satisfaction problems, such as 3-colorability, unreachability, Horn-SAT, solvability of systems of linear equations, where the instance is an infinite structure (graph, formula) built out of atoms, with a finite description. It turns out that tight classical complexity results lift to the infinite setting. Moreover, many classical algorithms can be lifted to this setting in a natural way.

Highlights Conference 2014 Conference Abstract

Descriptive Complexity and Constraint Satisfaction Problems

• Szymon Toruńczyk

We give a common generalization of two theorems from Descriptive Complexity: the Immerman-Vardi Theorem, which says that over linearly ordered structures, the logic LFP+C captures PTime and the Cai-Fürer-Immerman Theorem, which says that over all finite structures, the logic LFP+C does not capture PTime. Our generalization relies on a connection with Constraint Satisfaction Problems and recent results from CSP theory. The presented results are a consequence of the results presented in the previous talk by Joanna Ochremiak. Both talks are based on a joint paper with Bartek Klin, Sławomir Lasota and Joanna Ochremiak accepted to CSL-LICS 2014.

Highlights Conference 2013 Conference Abstract

Turing machines with atoms

• Mikołaj Bojańczyk
• Bartek Klin
• Sławomir Lasota
• Szymon Toruńczyk

We study Turing machines over sets with atoms, also known as nominal sets. Our main result is that deterministic machines are weaker than nondeterministic ones; in particular, P! =NP in sets with atoms. Our main construction is closely related to the Cai-Fuerer-Immerman graphs used in descriptive complexity theory.

Highlights Conference 2013 Conference Abstract

Verification of database driven systems via amalgamation

• Szymon Toruńczyk
• Mikołaj Bojańczyk
• Luc Segoufin

We describe a general framework for static verification of systems that base their decisions upon queries to databases. The database is specified using constraints, typically a schema, and is not modified during a run of the system. The system is equipped with a finite number of registers for storing intermediate information from the database and the specification consists of a transition table described using quantifier-free formulas that can query either the database or the registers. Our main result concerns systems querying XML databases -- modeled as data trees -- using quantifier-free formulas with predicates such as the descendant axis or comparison of data values. Our technique is based on the notion of amalgamation and is quite general. For instance it also applies to relational databases (with an optimal \pspace algorithm).