arXiv subjects

Andreas Krebs

Publications and source records attributed to Andreas Krebs.

At least 19 recordsLinked to original sources

arXiv2026

Algebraic Decomposition Theory for Transformer Length Generalization

Transformer-based language models are known to sometimes generalize to sequences longer than seen during training, but we lack a precise characterization of which tasks admit length generalization. It is not even known which regular languages transformers length-generalize on -- and this is a foundational class of languages. Our contributions are to establish the first complete characterization of which regular languages transformers length-generalize on and provide a decision algorithm running in polynomial time in the size of the language's syntactic monoid. These results rely on an effective characterization of the regular languages in C-RASP, a recently-established formalism that expresses which languages transformers length-generalize on. This characterization is challenging because classical tools like Krohn-Rhodes decomposition theory for finite semigroups are insufficient for C-RASP. Firstly, the basic building blocks of Krohn-Rhodes theory -- flip-flop and simple groups -- are not expressible in C-RASP. Secondly, the basic building block of C-RASP (unbounded counting) is not expressible by the finite semigroups of Krohn-Rhodes theory. Thus, length generalization on regular languages is controlled by an algebraic property that is invisible to classical finite decomposition theory. We generalize classical decomposition theory from finite semigroups to the infinite additive group on the integers, allowing us to characterize C-RASP in terms of iterated wreath products of the integers and derive a provable polynomial-time decision algorithm for regular language membership. Experiments across a broad test suite of regular languages confirm that our theory captures transformers' length-generalization behavior more accurately than existing classifications.

cs.FL↗

arXiv2025

When Symmetry Yields NP-Hardness: Affine ML-SAT on S5 Frames

Hemaspaandra~et~al.~[JCSS 2010] conjectured that satisfiability for multi-modal logic restricted to the connectives XOR and 1, over frame classes T, S4, and S5, is solvable in polynomial time. We refute this for S5 frames, by proving NP-hardness.

cs.LO↗

arXiv2025

A Formal Framework for Understanding Length Generalization in Transformers

A major challenge for transformers is generalizing to sequences longer than those observed during training. While previous works have empirically shown that transformers can either succeed or fail at length generalization depending on the task, theoretical understanding of this phenomenon remains limited. In this work, we introduce a rigorous theoretical framework to analyze length generalization in causal transformers with learnable absolute positional encodings. In particular, we characterize those functions that are identifiable in the limit from sufficiently long inputs with absolute positional encodings under an idealized inference scheme using a norm-based regularizer. This enables us to prove the possibility of length generalization for a rich family of problems. We experimentally validate the theory as a predictor of success and failure of length generalization across a range of algorithmic and formal language tasks. Our theory not only explains a broad set of empirical observations but also opens the way to provably predicting length generalization capabilities in transformers.

cs.LG↗

arXiv2024

Synchronous Team Semantics for Temporal Logics

We present team semantics for two of the most important linear and branching time specification languages, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). With team semantics, LTL is able to express hyperproperties, which have in the last decade been identified as a key concept in the verification of information flow properties. We study basic properties of the logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of the basic logic react to adding additional atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL with team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties. For CTL with team semantics, we investigate the computational complexity of the satisfiability and model checking problem. The satisfiability problem is shown to be EXPTIME-complete while we show that model checking is PSPACE-complete.

cs.LO↗

arXiv2022

Regular languages defined by first-order formulas without quantifier alternation

We give a simple new proof that regular languages defined by first-order sentences with no quantifier alteration can be defined by such sentences in which only regular atomic formulas appear. Earlier proofs of this fact relied on arguments from circuit complexity or algebra. Our proof is much more elementary, and uses only the most basic facts about finite automata.

cs.LO↗

arXiv2020

Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership

We study two extensions of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, "the letter $a$ appears between positions $x$ and $y$" and "the factor $u$ appears between positions $x$ and $y$". These are, in a sense, the simplest properties that are not expressible using only two variables. We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We give effective conditions, in terms of the syntactic monoid of a regular language, for a property to be expressible in these logics. This algebraic analysis allows us to prove, among other things, that our new logics have strictly less expressive power than full first-order logic FO[<]. Our proofs required the development of novel techniques concerning factorizations of words.

cs.LO↗

arXiv2019

Wreath Products of Distributive Forest Algebras

It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al.,(2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decidability of PDL. We solve this problem in the case k=2: All languages recognized by forest algebras satisfying a 2-fold iterated distributive law are in PDL. Furthermore, we show that this class is decidable. This provides a novel nontrivial decidable subclass of PDL, and demonstrates the viability of the proposed approach to deciding PDL in general.

cs.FL↗

arXiv2018

Difference hierarchies and duality with an application to formal languages

The notion of a difference hierarchy, first introduced by Hausdorff, plays an important role in many areas of mathematics, logic and theoretical computer science such as descriptive set theory, complexity theory, and the theory of regular languages and automata. From a lattice theoretic point of view, the difference hierarchy over a bounded distributive lattice stratifies the Boolean algebra generated by it according to the minimum length of difference chains required to describe the Boolean elements. While each Boolean element is given by a finite difference chain, there is no canonical such writing in general. We show that, relative to the filter completion, or equivalently, the lattice of closed upsets of the dual Priestley space, each Boolean element over the lattice has a canonical minimum length decomposition into a Hausdorff difference. As a corollary each Boolean element over a (co-)Heyting algebra has a canonical difference chain. With a further generalization of this result involving a directed family of adjunctions with meet-semilattices, we give an elementary proof of the fact that a regular language is given by a Boolean combination of purely universal sentences using arbitrary numerical predicates if and only if it is given by a Boolean combination of purely universal sentences using only regular numerical predicates.

math.GN↗

arXiv2018

Visibly Pushdown Languages and Free Profinite Algebras

We build a notion of algebraic recognition for visibly pushdown languages by finite algebraic objects. These come with a typical Eilenberg relationship, now between classes of visibly pushdown languages and classes of finite algebras. Building on that algebraic foundation, we further construct a topological object with one purpose being the possibility to derive a notion of equations, through which it is possible to prove that some given visibly pushdown language is not part of a certain class (or to even show decidability of the membership-problem of the class in some cases). In particular, we obtain a special instance of Reiterman's theorem for pseudo-varieties. These findings are then employed on two subclasses of the visibly pushdown languages, for which we derive concrete sets of equations. For some showcase languages, these equations are utilised to prove non-membership to the previously described classes.

cs.FL↗

arXiv2018

Team Semantics for the Specification and Verification of Hyperproperties

We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.

cs.LO↗

arXiv2017

Diminishable Parameterized Problems and Strict Polynomial Kernelization

Kernelization---a mathematical key concept for provably effective polynomial-time preprocessing of NP-hard problems---plays a central role in parameterized complexity and has triggered an extensive line of research. This is in part due to a lower bounds framework that allows to exclude polynomial-size kernels under the assumption of NP $\nsubseteq$ coNP$/$poly. In this paper we consider a restricted yet natural variant of kernelization, namely strict kernelization, where one is not allowed to increase the parameter of the reduced instance (the kernel) by more than an additive constant. Building on earlier work of Chen, Flum, and Müller [Theory Comput. Syst. 2011] and developing a general and remarkably simple framework, we show that a variety of FPT problems does not admit strict polynomial kernels under the weaker assumption of P $\neq$ NP. In particular, we show that various (multicolored) graph problems and Turing machine computation problems do not admit strict polynomial kernels unless P $=$ NP. To this end, a key concept we use are diminishable problems; these are parameterized problems that allow to decrease the parameter of the input instance by at least one in polynomial time, thereby outputting an equivalent problem instance. Finally, we study a relaxation of the notion of strict kernels and reveal its limitations.

cs.CC↗

arXiv2017

On the Complexity of Bounded Context Switching

Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS. The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of the memory (m) in O*(m^(cs)2^(cs)). This is achieved by creating instances of the easier problem Shuff which we solve via fast subset convolution. We also present a lower bound for BCS of the form m^o(cs / log(cs)), based on the exponential time hypothesis. Interestingly, closing the gap means settling a conjecture that has been open since FOCS'07. Further, we prove that BCS admits no polynomial kernel. Next, we introduce a measure, called scheduling dimension, that captures the complexity of schedules. We study BCS parameterized by the scheduling dimension (sdim) and show that it can be solved in O*((2m)^(4sdim)4^t)$, where t is the number of threads. We consider variants of the problem for which we obtain (matching) upper and lower bounds.

cs.FL↗

arXiv2017

Computing best discrete least-squares approximations by first-degree splines with free knots

We present an algorithm to compute best least-squares approximations of discrete real-valued functions by first-degree splines (broken lines) with free knots. We demonstrate that the algorithm delivers after a finite number of steps a (global) best approximation. The analysis is complemented by remarks on programming and by a number of numerical examples including applications from medicine (MBC, MIC).

math.NA↗

arXiv2016

Two-variable Logic with a Between Predicate

We study an extension of FO^2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, `the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables. We present several logics, both first-order and temporal, that have the same expressive power, and find matching lower and upper bounds for the complexity of satisfiability for each of these formulations. We also give an effective necessary condition, in terms of the syntactic monoid of a regular language, for a property to be expressible in this logic. We show that this condition is also sufficient for words over a two-letter alphabet. This algebraic analysis allows us us to prove, among other things, that our new logic has strictly less expressive power than full first-order logic FO[<].

cs.LO↗

arXiv2015

Using Duality in Circuit Complexity

We investigate in a method for proving separation results for abstract classes of languages. A well established method to characterize varieties of regular languages are identities. We use a recently established generalization of these identities to non-regular languages by Gehrke, Grigorieff, and Pin: so called equations, which are capable of describing arbitrary Boolean algebras of languages. While the main concern of their result is the existence of these equations, we investigate in a general method that could allow to find equations for language classes in an inductive manner. Thereto we extend an important tool -- the block product or substitution principle -- known from logic and algebra, to non-regular language classes. Furthermore, we abstract this concept by defining it directly as an operation on (non-regular) language classes. We show that this principle can be used to obtain equations for certain circuit classes, given equations for the gate types. Concretely, we demonstrate the applicability of this method by obtaining a description via equations for all languages recognized by circuit families that contain a constant number of (inner) gates, given a description of the gate types via equations.

cs.CC↗

arXiv2015

Value Automata with Filters

We propose to study value automata with filters, a natural generalization of regular cost automata to nondeterminism. Models such as weighted automata and Parikh automata appear naturally as specializations. Results on the expressiveness of this model offer a general understanding of the behavior of the models that arise as special cases. A landscape of such restrictions is drawn.

cs.FL↗

arXiv2015

The model checking fingerprints of CTL operators

The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.

cs.LO↗

arXiv2015

A Team Based Variant of CTL

We introduce two variants of computation tree logic CTL based on team semantics: an asynchronous one and a synchronous one. For both variants we investigate the computational complexity of the satisfiability as well as the model checking problem. The satisfiability problem is shown to be EXPTIME-complete. Here it does not matter which of the two semantics are considered. For model checking we prove a PSPACE-completeness for the synchronous case, and show P-completeness for the asynchronous case. Furthermore we prove several interesting fundamental properties of both semantics.

cs.LO↗