Events

Upcoming events

The fine-grained complexity of NFA intersection emptiness

Neha Rino University of Warwick
12 Sep 2025, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
SWS Colloquium
Given some integer k, intersection emptiness of k Nondeterministic Finite Automata (NFA k-IE) is a fundamental problem in automata theory, with applications across Computer science from Arithmetic theories and model checking to graph database queries. In this talk, I will discuss some results regarding the fine-grained complexity of NFA k-IE. Informally, what I mean by fine-grained complexity is that we want to know (upto logarithmic factors) the runtime complexity of our algorithms, and argue why they cannot be improved by relating it to the state of the art in solving long-standing hard problems like SAT. ...
Given some integer k, intersection emptiness of k Nondeterministic Finite Automata (NFA k-IE) is a fundamental problem in automata theory, with applications across Computer science from Arithmetic theories and model checking to graph database queries. In this talk, I will discuss some results regarding the fine-grained complexity of NFA k-IE. Informally, what I mean by fine-grained complexity is that we want to know (upto logarithmic factors) the runtime complexity of our algorithms, and argue why they cannot be improved by relating it to the state of the art in solving long-standing hard problems like SAT.

I will demonstrate (what we believe to be) a new algorithm for solving NFA k-IE. If all the NFAs have n states and m transitions, our algorithm runs in time O(n^{k-1}m), compared to the O(m^k) runtime of the classic Cartesian product approach. I will also present a matching lower bound subject to the Combinatorial k-Clique hypothesis, and a barrier to tight SETH-based lower bounds. This is joint work with Dmitry Chistikov, at the University of Warwick, UK.
Read more

Recent events

Permissive Assumptions in Logical Controller Synthesis for Cyber-Physical Systems

Satya Prakash Nayak Max Planck Institute for Software Systems
09 Sep 2025, 1:00 pm - 2:00 pm
Kaiserslautern building G26, room 111
SWS Student Defense Talks - Thesis Proposal
The automatic construction of correct-by-design systems has emerged as a central challenge in cyber-physical systems (CPS). As CPS combine discrete logical decision-making with continuous physical processes, their correctness requires reasoning both about logical specifications and real-time physical behavior. A common approach is to abstract the physical dynamics into a discrete plant model and synthesize a logical controller for this plant that ensures the specification. Such approaches often rely on a set of assumptions about how the system interacts with its environment. ...
The automatic construction of correct-by-design systems has emerged as a central challenge in cyber-physical systems (CPS). As CPS combine discrete logical decision-making with continuous physical processes, their correctness requires reasoning both about logical specifications and real-time physical behavior. A common approach is to abstract the physical dynamics into a discrete plant model and synthesize a logical controller for this plant that ensures the specification. Such approaches often rely on a set of assumptions about how the system interacts with its environment. However, these assumptions are typically overly restrictive and fail to capture the full range of behaviors that the environment can exhibit, leading to conservative or inflexible controllers. This thesis addresses these limitations by proposing frameworks for synthesizing controllers under more permissive assumptions.

The first part of the thesis considers permissiveness in the interactions between multiple discrete logical components, where assumptions restrict the behavior of other components. We propose new methods to compute permissive assumptions that capture all cooperative behavior of other components. Building on this, we propose a negotiation-based approach to compute assume-guarantee contracts between components, allowing components to retain flexibility while ensuring correctness in a distributed setting.

The second part of the thesis addresses permissiveness in the interaction between high-level logic and low-level physical dynamics, where assumptions on the plant model restrict the behavior of the physical environment. We develop a new class of assumptions that capture richer behaviors of low-level controllers, enabling logical controllers to adapt seamlessly to changes by the external environment. To ensure scalability for large plant models, we propose a universal controller framework where controller decisions are conditioned on future branching-time properties of the plant model, learned from a small set of representative plant models. Finally, we introduce a robust semantics for branching-time temporal logics that allows reasoning under uncertainty or partial violations of assumptions without increasing computational complexity.
Read more

Algorithmic Problems for Linear Recurrence Sequences

Joris Nieuwveld Max Planck Institute for Software Systems
05 Sep 2025, 3:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Thesis Defense
Linear recurrence sequences (LRS) are among the most fundamental and easily definable classes of number sequences, encompassing many classical sequences such as polynomials, powers of two, and the Fibonacci numbers. They also describe the dynamics of iterated linear maps and arise naturally in numerous contexts within computer science, mathematics, and other quantitive sciences. However, despite their simplicity, many easy-to-state decision problems for LRS have stubbornly remained open for decades despite considerable and sustained attention. Chief among these are the Skolem problem and the Positivity problem, ...
Linear recurrence sequences (LRS) are among the most fundamental and easily definable classes of number sequences, encompassing many classical sequences such as polynomials, powers of two, and the Fibonacci numbers. They also describe the dynamics of iterated linear maps and arise naturally in numerous contexts within computer science, mathematics, and other quantitive sciences. However, despite their simplicity, many easy-to-state decision problems for LRS have stubbornly remained open for decades despite considerable and sustained attention. Chief among these are the Skolem problem and the Positivity problem, which ask to determine, for a given LRS, whether it contains a zero term and whether it contains only positive terms, respectively. For both problems, decidability is currently open, i.e., whether they are algorithmically solvable.

In this thesis, we present the following results. For the Skolem problem, we introduce an algorithm for simple LRS whose correctness is unconditional but whose termination relies on two classical, widely-believed number-theoretic conjectures. This algorithm is implementable in practice, and we report on experimental results. For the Positivity problem, we introduce the notion of reversible LRS, which enables us to carve out a large decidable class of sequences. We also examine various expansions of classical logics by predicates obtained from LRS. In particular, we study expansions of monadic second-order logic of the natural numbers with order and present major advances over the seminal results of Büchi, Elgot, and Rabin from the early 1960s. Finally, we investigate fragments of Presburger arithmetic, where, among others, we establish the decidability of the existential fragment of Presburger arithmetic expanded with powers of 2 and 3.
Read more

Supporting Human-Human Communication: Towards a Proactive AI Paradigm

Christian Danescu-Niculescu-Mizil Cornell University
(hosted by Krishna Gummadi)
05 Sep 2025, 1:30 pm - 2:30 pm
Kaiserslautern building G26, room 607
AICS Distinguished Speaker Colloquium
Recent years have seen a gold rush towards replacing people with AI agents in communication: they can serve as your therapist, your tutor, your financial advisor, your interviewer. In this talk I will propose a contrasting vision: one where AI is used for supporting humans in their communication while preserving their agency. Achieving this vision requires moving beyond the current transactional paradigm embodied by current generative AI systems, which are designed to fulfill the immediate goals of a single person, ...
Recent years have seen a gold rush towards replacing people with AI agents in communication: they can serve as your therapist, your tutor, your financial advisor, your interviewer. In this talk I will propose a contrasting vision: one where AI is used for supporting humans in their communication while preserving their agency. Achieving this vision requires moving beyond the current transactional paradigm embodied by current generative AI systems, which are designed to fulfill the immediate goals of a single person, such as answering a question, solving a math problem, booking a flight, or (repeatedly) replying in character. To meaningfully support human-human communication without disrupting or supplanting it, an AI system must instead follow a proactive paradigm: it needs to decide when to intervene to offer support as the interaction unfolds, rather than wait to explicitly be prompted as AI agents and chatbots do today. In this talk I will present initial progress on AI technologies that enable such a proactive mode of operation, and demonstrate communication support tools that embody it.
Read more

Archive