I am actively looking for prospective Master’s and PhD students interested in joint research on the complexity and decidability of logics. Drop me a line if you are interested (some modest scholarships are available).
We study the finite satisfiability problem for the two-variable fragment of first-order logic over two-dimensional structures. Beyond the standard vocabulary, we allow one predicate interpreted as a linear order and another predicate interpreted as a successor relation, not necessarily from the same linear order.
We prove that the problem is NExpTime-complete, resolving a question left open by Manuel and Zeume. The upper bound relies on the exponential-size model property of the logic, established via the circular witnessing scheme of Grädel, Kolaitis, and Vardi.
We also establish the computational complexity of deciding both order-invariance and order-successor-invariance for the two-variable fragment. The first result significantly simplifies the recent work of Bednarczyk and Grange, while the second one answers a question left open by Zeume and Harwath.
BSc thesis
On the Complexity of Forward Guarded Fragment with Constants
We define and investigate the FGFc,≈ fragment of first-order logic. We prove that its satisfiability problem is NExpTime-complete by establishing lower and upper bounds. For the first bound, we perform a polynomial reduction from the Torus Tiling Problem by constructing a way to interpret grids and tilings in a first-order structure using FGFc,≈-sentences. To achieve an upper bound, we define the notion of FGFc,≈-types and modify Bednarczyk and Jaakkola's construction of unravelling. We bound the number of FGF- and GF-types. We provide a sketch of the proof that we can bound the number of types in general. Then we use a theorem by Fiuk to find an exponentially big model of any given FGFc,≈-sentence.
BEng thesis
An application for visualizing games on finite graphs, with particular emphasis on Ehrenfeucht–Fraïssé games
The goal of this thesis was to analyze and understand the Ehrenfeucht–Fraïssé game and its variation, the Pebble game. To achieve this goal, a web application was implemented. It allows users to visualize and play the aforementioned games. It is possible to choose the game and the opponent: a human or a simple AI. Three methods of data input are supported: graphs used in the games can be generated randomly, given in JSON format, or drawn manually.
Propositional Dynamic Logic (PDL), known in the Description Logic community as ALCreg, is a well-established modal logic of programs. To increase its expressive power, several extensions have been proposed. One such extension is the loop operator, which expresses that an element can reach itself via a path defined by a regular expression. Although the satisfiability problem for LoopPDL is well understood, the decidability of its finite satisfiability problem has remained open for over 40 years. We present a solution for a simple fragment with loops restricted to atomic roles and their transitive closures.
MSc thesis
Decidability of satisfiability for non-regular extensions of PDL
Propositional dynamic logic (PDL) is an expressive logic for reasoning about program behaviour. It was first introduced by Fischer and Ladner [FL79]. Extensions of PDL were studied for example by Löding et al. [LLS07], who added modalities indexed by languages recognizable by visibly pushdown automata (Vpa) moving the expressivity of logic beyond regular languages. We provide a deep analysis of their automata-based approach to satisfiability problem and apply it to multi-pushdown languages (i.e. recognizable via automata equipped with finitely many stacks) by extracting sufficient characteristics of a subclass of multi-pushdown languages that imply decidability of the resulting logic. We then prove that the class of n-ordered visibly pushdown languages (n-OVPL) possesses some of these characteristics, and discuss the others.
BSc thesis
Temporal Reasoning Through the Lens of Conjunctive Grammars
This thesis describes the implementation of an algorithm for parsing conjunctive grammars over a one-letter alphabet. This algorithm was presented in 2012 by A. Okhotin and C. Reitwießner. It has one major restriction: it only works for grammars in Binary Normal Form. This approach is compared with an alternative general-purpose parsing algorithm that works for grammars in arbitrary form. The primary motivation for implementing the algorithm and exploring the structure of conjunctive grammars is the recent result of C. Bourgaux, A. Gnatenko and M. Thomazo from 2025, which shows the reduction from temporal atomic query answering in TEL future logic to parsing unary conjunctive grammars. This work was partially supported by the Austrian Science Fund through the FWF Project Ontegra [10.55776/PIN8884924].
20251 thesis
MSc thesis
Towards Finite Controllability of Forward Sets of Existential Rules
This thesis introduces a new class of existential rules, called forward TGDs, defined by the requirement that variables in the rules can be ordered so that every atom uses a contiguous subsequence of that order. We then prove that every knowledge-base consisting of forward TGDs over a binary schema is finitely controllable. This means that if some possibly infinite model of such knowledge-base does not satisfy a query, then there is a finite model which does not satisfy this query as well.
20242 theses
BSc thesis
Finite Model Property for Hybrid Graded Mu-calculus
Mu-calculus is a robust modal logic used in computer science for expressing and analyzing properties of transition systems. It extends basic modal logic by introducing fixed point operators, which allow for the expression of complex recursive properties in a compact and rigorous manner. The goal of this thesis is to explore the model-theoretic properties of mu-calculus extended with nominals (constants) and graded modalities (counting)—features commonly found in expressive ontology languages like OWL2 by W3C. We demonstrate that the resulting logic, known as hybrid graded mu-calculus, possesses the finite model property (FMP), meaning that every satisfiable formula in this logic can be satisfied in a finite Kripke structure. Our proof is based on a detailed examination of the existing FMP proof for hybrid mu-calculus by Tamura, highlighting how his construction can be adapted to accommodate graded modalities. Additionally, we provide a complete proof of the correspondence between (hybrid) graded mu-calculus and parity games, a result initially announced by Kupferman, Vardi, and Sattler in 2002 but never proven in full detail.
MSc thesis
A Constructive Proof of a Van Benthem Theorem for the Forward Guarded Fragment of First-Order Logic
Benno Fünfstück
Abstract
The forward guarded fragment (FGF) is a recently introduced decidable fragment of first-order logic (FO) whose satisfiability problem is only ExpTime-complete. FGF derives from the guarded fragment (GF) by adding a restriction on the order in which variables may appear in formulae, similar to the fluted fragment by Purdy. FGF is a higher-arity generalization of multi-modal logic with global modalities, but in contrast to GF, it does not capture logics with inverse modalities. In total analogy to the classic van Benthem characterization of modal logic, we show that FGF is exactly the fragment of FO which consists of formulae that are invariant under a suitable notion of bisimulation for FGF. Crucially, we employ techniques by Martin Otto originally designed for modal logic which also work if we restrict the class of models under consideration to finite models only. In the process, we develop a new notion of unraveling for FGF, which produces tree-like models that satisfy the same FGF formulae as the original model. The new notion of unraveling is closely linked to a notion of unraveling for GF and is interesting on its own. As an application for our van Benthem style characterization, we show that whether a given GF formula has an equivalent formula in FGF is decidable.
The Guarded Fragment is a decidable fragment of first-order logic. We are concerned with a further restriction of the Guarded Fragment, called the Forward Guarded Fragment, in which variables appear in atoms only in the order of quantification. The Guarded Fragment can be decided with the resolution method in doubly exponential time. We show that the resolution method for the Guarded Fragment can be used to decide Forward Guarded Fragment in single exponential time and we provide the implementation.
BEng thesis
E-learning platform supporting studying for the Matura exam in Computer Science
Julita Osman, Aleksandra Stępniewska & Nikola Wrona
In this paper, we describe the concept and implementation of an online educational platform that offers materials designed to prepare for the matura exam in information technology at an extended level. We observed a shortage of similar sources of knowledge, which is confirmed by the statistics provided by the Central Examination Commission every year. These statistics show that not only still a very small percentage of high school graduates decide to take the extended matura exam in computer science, but also their results are not very high. It is our ambition to contribute to change in this state of affairs. The platform’s course is divided into four parts: theory, Excel, Access and Python-based programming. Sound knowledge in each of these sections is crucial to get a high score in the high school graduation exam. For this reason, special emphasis was placed on a thorough study of each topic that may appear in the matura exam. The main goal was to build a platform that would help both students who are starting from scratch and those who have had the opportunity to study at school in preparation for the matura exam, regardless of the teaching level. All sections' topics are covered in detail and enriched by graphics to make learning more interesting and easier. In addition, each part has a section devoted to solving matura exam tasks and exercises for students to do on their own. This will allow the student to check whether he or she has already mastered a given range of material and will help to consolidate the acquired knowledge. Each topic in the programming part includes a list of tasks and their model solution. Additionally, the learning of this material is supported by a programming environment and a checker based on it, which is available on the site. The entire platform is written in React, one of the most popular and efficient frameworks for developing front-end applications. Its flexibility is a fast and efficient means for interactive and modern user experience. In addition, React is supported by a large community of developers, so as to provide access to a wide range of tools and libraries, which facilitate the development of functional and attractive websites.
20224 theses
MSc thesis
Categorical semantics for model comparison games for description logics
A categorical approach to study model comparison games in terms of comonads was recently initiated by Abramsky et al. In this work, we analyse games that appear naturally in the context of description logics and supplement them with suitable game comonads. More precisely, we consider expressive sublogics of ALC Self IbO, namely, the logics that extend ALC with any combination of inverses, nominals, safe boolean roles combinations, and Self operator. Our construction augments and modifies the so-called modal comonad by Abramsky and Shah. The approach that we took heavily relies on the use of relative comonads, which we leverage to encapsulate additional capabilities within the bisimulation games in a compositional manner.
Großer Beleg
Interpolation for the Two-Variable Guarded Fragment with Counting
Johannes Tantow
Abstract
The main theorem of the project is the proof that the two-variable guarded fragment with counting quantifiers enjoys the Craig Interpolation Property.
BSc thesis
Presburger Tree Automata With Applications to Logics With Expressive Counting
We introduce two versions of Presburger Automata with the Büchi acceptance condition, working over infinite, finite-branching trees. These automata, in addition to the classical ones, allow nodes for checking linear inequalities over labels of their children. We establish tight NP and ExpTime bounds on the complexity of the non-emptiness problem for the presented machines. We demonstrate the usefulness of our automata models by polynomially encoding the two-variable guarded fragment extended with Presburger constraints, improving the existing triply-exponential upper bound to a single exponential. This bachelor's thesis is based on joint work with Bartosz Bednarczyk, published at WOLLIC 2022.
BSc thesis
On Several Equivalent Characterisations of the Variety R
One of the celebrated results in automata theory is that the notion of regularity in formal languages is robust in a very strong sense. More precisely, several equivalent characterisations of regular languages were given. It turns out that regular languages are precisely the languages recognisable by finite automata, finite monoids, regular expressions, and definable in the monadic second order logic. Similar characterisations are also known for the first-order definable languages, e.g. these are the languages recognisable by finite aperiodic monoids. Inspired by the algebraic approach to formal languages, we aim at describing the connection between languages recognizable by finite monoids from the variety R, and the suitable restrictions of first-order logic, regular expressions, finite automata, temporal logics and more.
20212 theses
BSc thesis
Statistical constructions in decidable fragments of First-Order Logic
In this thesis we consider first order logic extended with percentage quantifiers, allowing us to express statistical properties. Such quantifiers are defined under two different semantics: global and local. We show undecidability of the satisfiability problem for the extended two-variable fragment FO2 under both semantics, two-variable guarded fragment GF2 under the global semantics, as well as the three-variable guarded fragment GF3 (and hence the full GF) under the local semantics of percentage counting. We supplement our results with decidability status of the two-variable guarded fragment GF2 with local percentage counting and monadic fragment with global percentage counting.
MSc thesis
The complexity of the satisfiability problem for Modal Logics with Data over Heaps
Modal Logic with Data has been introduced by D. Baelde, S. Lunel and S. Schmitz for reasoning on simplified representation of XML trees. In this thesis we propose a variant of this logic interpreted over heaps with data, which we call Modal Logic with Data over Heaps. Our logic is more expansive than the logic from Modal Logic with Data: it allows for unbounded number of data values, inverse modalities and their transitive closures. We investigate the complexity of two selected fragments of the logic. The first fragment is a fragment with standard modalities and their inverses, but without their transitive closures. We prove it to be PSpace-complete. The PSpace-hardness goes by a reduction from standard modal logic. The PSpace upper bound is shown by a reduction to graded modal logic with inverse. In the second fragment under consideration the structures are accessed by the transitive closures of the inverse modalities but the basic modalities are not employed. The crux of the proof is showing the polynomial-depth model property of the logic. We first prove that every satisfiable formula has a model being a single tree and a loop. We then polynomially bound the size of the loop and the depth of the tree. Finally, we exponentially bound the branching factor of the tree. This leads to an NPSpace = PSpace algorithm for satisfiability testing. The PSpace-hardness is inherited from standard modal logic. We therefore obtain PSpace-completeness of the satisfiability problem.
Theses defended at the University of Wrocław between 2021 and 2023 officially list another supervisor, as I was not yet formally eligible to act as one at the time. In practice, I supervised these theses in full.