Conveners
Track B: Automata and Games
- Rupak Majumdar (Session Chair)
Track B: Decision Procedures
- Sylvain Schmitz (Session Chair)
Track B: Logic and Graph Structure Theory
- Martin Grohe (Session Chair)
Track B: Models of Systems
- Anca Muscholl (Session Chair)
Track B: Verification and Testing
- Dmitry Chistikov (Session Chair)
Track B: Complexity and Logic
- James Worrell (Session Chair)
George Kenison, Joris Nieuwveld, Joël Ouaknine, and James Worrell
Abstract: It is a longstanding open problem whether there is an algorithm to decide the Positivity Problem for linear recurrence sequences (LRS) over the integers, namely whether given such a sequence, all its terms are non-negative. Decidability is known for LRS of order $5$ or less, i.e., for those sequences in which every...
Bartosz Bednarczyk, Ian Pratt-Hartmann, and Daumantas Kojelis
Abstract: We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas.
The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment.
We show that the adjacent fragment has the finite model...
Michael Benedikt, Dmitry Chistikov, and Alessio Mansutti
Abstract: We investigate expansions of Presburger arithmetic (PA), i.e.,
the theory of the integers with addition and order, with additional
structure related to exponentiation: either a function that takes a
number to the power of 2, or a predicate P for the powers of 2.
The latter theory, denoted as PA(Pow), was introduced by...
Jan Dreier, Nikolas Mählmann, Sebastian Siebertz, and Szymon Toruńczyk
Abstract: 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...
Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokołowski and Szymon Toruńczyk
Abstract: A class of graphs $C$ is monadically stable if for every unary expansion $\widehat{C}$ of $C$, one cannot encode - using first-order transductions - arbitrarily long linear orders in graphs from $\widehat{C}$. It is...
Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski and Szymon Toruńczyk
Abstract: 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 $\mathcal{C}$, and using a first-order formula $\varphi$ with parameters we are able to define, in every...
Fabian Birkmann, Stefan Milius, and Henning Urbat
Abstract: We propose a novel topological perspective on data languages recognizable by orbit-finite nominal monoids. For this purpose we introduce pro-orbit-finite nominal topological spaces, which for bounded support size coincide with nominal Stone spaces and are shown to be dually equivalent to a subcategory of nominal boolean algebras....
Thomas Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç
Abstract: The operator precedence languages (OPLs) represent the largest known subclass of the context-free languages which enjoys all desirable closure and decidability properties. This includes the decidability of language inclusion, which is the ultimate verification problem. Operator precedence grammars, automata, and...
Harry Vinall-Smeeth and Christoph Berkholz
Abstract: The task of computing homomorphisms between two finite relational
structures A and B is a well-studied question with
numerous applications. Since the set Hom(A,B) of all
homomorphisms may be very large having a method of representing it in
a succinct way, especially one which enables us to perform efficient
enumeration and counting,...
Diptarka Chakraborty, Sourav Chakraborty, Gunjan Kumar and Kuldeep Meel
Abstract: Given a Boolean formula $\phi$ over $n$ variables, the problem of model counting is to compute the number of solutions of $\phi$. Model counting is a fundamental problem in computer science with wide-ranging applications in domains such as quantified information leakage, probabilistic reasoning, network...