We are a student-run initiative at the Max Planck Institute for Software Systems that invites PhD students from the areas of logic, automata theory, games and related fields to present their research at our institute and optionally stay for a brief research visit.

Our goal is to give students an opportunity to showcase their work, to allow them to connect with each other and to provide fertile environment for collaborations.

Please take a look at our upcoming and previous talk. An iCal file of all talks that can be imported in your calendar program of choice can be found here.

We are happy to present Łukasz Kamiński’s talk titled “On decision problems in Petri nets with data”.

Abstract

Petri nets with equality data is an extension of plain Petri nets where tokens carry values from an infinite data domain, and executability of transitions is conditioned by equalities between data values. The most fundamental decision problem for Petri nets, the reachability problem, asks, given a net together with source and target configurations, if there is a run from source to target. The decidability status of this problem for equality data still remains an intriguing open question. On the other hand, the coverability problem (where we ask if there is a run from source to a configuration that possibly extends target by some extra tokens) is decidable for equality data. The reachability is also decidable if we consider only reversible Petri nets. Furthermore, it was shown recently that the bi-reachability, a decision problem that is sandwiched between reachability and the two latter problems, is decidable.

One can also consider more complicated data domains, for instance ordered data. In this case reachability is undecidable, reachability in the reversible case and coverability are decidable and the decidability status of bi-reachability is an open question.

In this talk I will define Petri nets with data and discuss decision problems in this model.

Bio

Łukasz is a second year PhD student at the University of Warsaw and works under supervision of Sławek Lasota. His research concerns mainly vector addition systems and orbit-finite structures. He enjoys automata theory and logic in general.

We are happy to present Dominik Klumpp’s talk titled “How Commutativity Simplifies Proofs of Concurrent Programs”.

Abstract

To verify concurrent programs with unbounded loops, algorithmic verifiers must infer inductive invariants that show correctness for all infinitely many possible executions of the program. Due to the many possible interleavings of the program’s threads, such invariants are often complex (requiring non-linear arithmetic, quantifiers, or reasoning with ghost variables) and out-of-reach for most invariant inference algorithms.

In this talk, I present a series of works investigating how the notion of commutativity simplifies proofs of concurrent programs and thereby empowers algorithic verification. The idea of commutativity is based on the observation that some program statements can be reordered without affecting the outcome of an execution, and hence it suffices to verify a suitably-chosen subset of interleavings (rather than all interleavings) to conclude correctness of an entire concurrent program. We will see how commutativity-based combinatorial algorithms interact with symbolic reasoning over variables with infinite domains, and how commutativity can both extend the theoretical expressiveness and contribute to the practical success of verification approaches.

Bio

Dominik Klumpp is a PhD candidate at the University of Freiburg. He received a BSc degree in Computer Science from the University of Augsburg and a MSc degree in Software Engineering as part of a joint programme by the Technical University of Munich, LMU Munich and the University of Augsburg. For his Master thesis, he visited the group of Prof. Franck Cassez at Macquarie University, Sydney, for six months to work on provably correct control flow reconstruction from assembler code.

During his PhD at the University of Freiburg, advised by Prof. Andreas Podelski, he has focused on automated verification of concurrent programs using techniques based on the principles of commutativity and partial order reduction. His automated verification tool Ultimate GemCutter has scored top rankings in the “ConcurrencySafety” category of the International Competitions on Software Verification (SV-COMP) 2022-2025.

We are happy to present Ehsan Goharshady’s talk titled “From Termination to LTL: A template-based approach”.

Abstract

The termination problem, also known as the halting problem, is known to be undecidable. This has motivated computer scientists to study proof rules for termination of restricted classes of programs. One such technique is ranking function generation, where we try to calculate an upper-bound on the number of steps the program takes to terminate from each configuration. In this talk, I briefly introduce how such ranking functions can be generated and how they can be extended to proof rules for verification of more general classes of specifications.

Bio

Ehsan Goharshady is a third-year PhD student at ISTA in Krishnendu Chatterjee’s group. He joined ISTA in 2022 after completing his bachelor’s in pure mathematics and computer science in Iran. His main interests are verification and analysis of non-deterministic and probabilistic imperative programs, model checking robust MDPs and solving bidding games.

We are happy to present Aditya Prakash’s talk titled “The 2-Token Theorem”.

Abstract

A nondeterministic parity automaton is said to be history deterministic if there is a resolver that capable of resolving the nondeterminism while reading an input word, based on the prefix read so far. The exact complexity of deciding history determinism for parity automata has remained open since 2006, with the problem only being known to be solvable in polynomial time for Büchi and coBüchi automata, until very recently.

In this talk, I will present some recent progress on this problem, where we extend this polynomial-time decidability procedure to parity automata with a fixed number of priorities. This is achieved by positively resolving the 2-token conjecture of Bagnol and Kuperberg, which had remained open since 2018. This talk is based on joint work with Karoliina Lehtinen that will appear in STOC 2025.

Bio

Aditya is a fourth-year PhD student at the University of Warwick, where he is working with Marcin Jurdzinski on automata and games, especially those on infinite words. During his PhD, his research has been focused on history-determinism, particularly on parity automata.

We are happy to present Lucie Guillou’s talk titled “Safety Analysis of Parameterized Networks with Non-Blocking Rendez-Vous and Broadcasts”.

I will present two recent joint works done with Arnaud Sangnier and Nathalie Sznajder. We study networks of processes that all execute the same finite protocol and communicate synchronously in two different ways: a process can broadcast one message to all other processes or send it to at most one other process. We study two coverability problems with a parameterised number of processes (state coverability and configuration coverability). It is already known that these problem are Ackermann-hard (and decidable) in the general case. This already holds when the processes communicate only by broadcasts. We show that when forbidding broadcasts, the two problems are EXPSPACE-complete. We also study a restriction on the protocol: a Wait-Only protocol has no state from which a process can send and receive messages. We show that without broadcasts, both problems are PTIME-complete in this restriction, and with broadcasts, state coverability is PTIME-complete and configuration coverability PSPACE-complete.

Bio

Lucie is a final-year PhD student at IRIF, in Paris, France, where she is working with Arnaud Sangnier and Tali Sznajder on distributed systems with an unbounded number of agents. Her research focuses on distributed systems with an unbounded number of agents, particularly on the complexities of certain verification problems in these networks.

We are happy to present Quentin Guilmant’s talk titled “Surreal Numbers”.

Surreal numbers form a class of number very singular in which we can embed every ordered field. In particular, transseries, studied for instance in Asymptotic Theory. Surreal numbers are in fact an even larger field which contains numbers that represent hyper exponential functions or half exponential functions (whose composition by themselves is the exponential function). It is also possible to get the derivative and the anti-derivative of surreal numbers.

Polynomial differential equations can form an analog model of computation, which has been introduced by Shanon in 1941, the general purpose analog computer (GPAC). It had been developed by Lipschitz, Pour El and more recently by Graça and Cost in 2003 to define a notion of computability on it. It has also been proven that this model is equivalent to Turing Computability in the sense of computable analysis.

In this talk, Quentin will introduce you to the wonderful world of surreal numbers and show you his work to solve polynomial differential equations whose solutions are surreal numbers. This may lead to a better understanding of asymptotics of the GPACs, and then, of GPAC-computable functions.

Bio

Quentin recently finished his PhD at the LIX (Palaiseau, France). He works on surreal number and their suspected link with computability theory. Before that he studied in the ENS Lyon where he got his Master in fundamental computer science.

We are happy to present Soumodev Mal’s talk titled “On the Satisfiability of Context-free String Constraints with Subword Ordering”.

String constraints impose constraints over variables that take strings as assignments. Given a string constraint C, the satisfiability problem asks if there is an assignment which satisfies every constraint in C. Most classes of string constraints in their full generality although have high expressive power turn out to be undecidable. Hence, a natural direction to recover decidability is to consider meaningful subclasses of such constraints. In this talk, we consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. We call this variant subword-ordering string constraints. The satisfiability problem for the variant turns out to be undecidable (even with regular membership). We consider a fragment in which the subword order constraints do not impose any cyclic dependency between variables. We show that this fragment is NEXPTIME-complete. As an important application of our result, we establish a strong connection between the acyclic fragment of the subword-ordering string constraints and acyclic lossy channel systems, an important distributed system model. This allowed us to settle the complexity of control state reachability in acyclic lossy channel pushdown systems. The problem was shown to be decidable by Atig et al. in 2008. However, no elementary upper bound was known. We show that this problem is NEXPTIME-complete.

This is a joint work with C. Aiswarya and Prakash Saivasan. Accepted at LICS’22.

Bio

Soumodev Mal is a second year PhD student at Chennai Mathematical Institute, India working under the supervision of Prof. C. Aiswarya, CMI and Prof. Prakash Saivasan, IMSc. His research interests broadly lies in Formal verification. He is currently working on verification of String Constraints.

We are happy to present Henry Sinclair-Banks’s talk titled “The Complexity of Coverability in Fixed Dimension VASS with Various Encodings “.

This presentation is about the coverability problem for Vector Addition Systems with States (VASS). We have lately shown that coverability in two-dimensional VASS with one binary encoded counter and one unary encoded counter is in NP. For contrast, coverability in two-dimensional VASS is PSPACE-complete with two binary encoded counters and NL-complete with two unary encoded counters.

Our NP upper bound is achieved using new techniques and one of these techniques is shown in this presentation. Coverability in any fixed dimension unary VASS, that is when the counter updates are encoded in unary, is long-known to be NL-complete. In this variation of the problem, the initial and target counter values are also encoded in unary, this turns out to be of great importance.

We have recently found that if the initial and target counter values are instead encoded in binary, then coverability in four-dimensional unary VASS is NP-hard and coverability in eight-dimensional unary VASS is PSPACE-hard. These lower bounds are corollaries of recent results of the hardness of reachability in fixed dimension unary VASS, and this presentation will feature the technique used in the reductions to coverability.

Bio

Henry Sinclair-Banks is a PhD student at the University of Warwick under the supervision of Dr. Dmitry Chistikov and Dr. Marcin Jurdzinski. Within theoretical computer science, the main themes of his research are automata, complexity, and logic. More specifically, the questions he most enjoys are all about automata with counters such as vector addition systems with states and one-counter nets.

We are happy to present Moritz Lichter’s talk titled “Separating Rank Logic from Polynomial Time”.

The quest for a logic capturing polynomial time is the question whether there exists a logic that exactly defines all properties decidable in polynomial time. The most promising candidates for such a logic are Choiceless Polynomial Time (CPT) and rank logic. Rank logic extends fixed-point logic by a rank operator over prime fields. In this talk, I argue that rank logic cannot define the isomorphism problem of a variant of the so called CFI graphs. This isomorphism problem is decidable in polynomial time and actually definable in CPT. Thus, rank logic is separated from CPT and in particular from polynomial time.

Bio

Moritz completed his Bachelor in computer science at the TU Darmstadt before moving to Universität des Saarlands for his Master. Since 2017, Moritz is a PhD student supervised by Pascal Schweitzer (first at TU Kaiserslautern, then at TU Darmstadt), where his research is centered around polynomial time logic, graph isomorphism, descriptive complexity theory and computer algebra.

We are happy to present Ruiwen Dong’s talk titled “Identity Problem for Unitriangular Matrices of Dimension Four”.

The Identity Problem in semigroup algorithmic theory asks the following: Given as input a set of square matrices $G = {A_1, A_2, …, A_k}$, does the semigroup generated by G contain the identity matrix $I$? The Identity Problem has been shown to be undecidable even when restricted to matrices of low dimensions. For example, Bell et al. showed its undecidability for matrices in $SL(4, Z)$. Some decidability results for the Identity Problem include its NP-completeness for matrices in $SL(2, Z)$, as well as its PTIME decidability in the Heisenberg group $H_3$. In this talk, we show a decidability result of the Identity Problem for matrices in the group $UT(4, Z)$ of unitriangular integer matrices of dimension four. Some of the techniques used for this result may be generalized to tackle higher dimensional unipotent groups.

Bio

Ruiwen Dong is currently a PhD student in Computer Science at the University of Oxford. He obtained his MsC from Ecole Polytechnique, France, and his BsC from Peking University, China. His main areas of interests include semigroup algorithmic problems, rings and algebra, as well as symbolic computing.

We are happy to present Ritam Raha’s talk titled “One Counter Automata: Reachability and Synthesis Problems”.

One-counter automata are well studied classical model that extend classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some ω-regular property. We will discuss how these problems relate to different restricted fragments of Presburger arithmetic with divisibility. Using this connection, I will present decidability results for the above mentioned synthesis problems. I will also present polynomial-space algorithms for the special cases of the problem where parameters can only be used in counter tests. This talk is primarily based on joint work with my supervisor Guillermo Perez.

Bio

Ritam Raha is a joint PhD student at the University of Antwerp in Belgium and LaBRI, University of Bordeaux in France. He is working under the supervision of Prof. Guillermo Perez and Prof. Nathanael Fijalkow. His research mainly focuses on verification of complex systems against learnt specifications.

We are happy to present A.R. Balasubramanian’s talk titled “Complexity of Coverability in Depth-Bounded Processes”.

We are happy to present K.S. Thejaswini’s talk titled “A Technique to Speed up Some Symmetric Attractor-based Algorithms for Parity Games”.

It is well known that the classic McNaughton-Zielonka algorithm for solving parity games has excellent performance in practice, but its worst-case asymptotic complexity is worse than that of the state-of-the-art algorithms. K.S. Thejaswini will present their work which pinpoints the mechanism that is responsible for this relative underperformance and propose a new technique that eliminates it. Their new technique is based on firstly enhancing the algorithm to compute attractor decompositions’ of subgames instead of just winning strategies on them, and then on making it carefully use attractor decompositions computed in prior recursive calls. This results in a theoretical improvement in the run-time complexity of not just McNaughton and Zielonka, but these techniques also improve several other attractor-based algorithms’ theoretical run-time. We also suggest different heuristics which can further potentially enhance the practical running time of these algorithms.

Bio

K.S. Thejaswini is a third year PhD student at the university of Warwick in the UK, and her supervisor is Marcin Jurdzinksi. Her PhD is broadly on solving parity games faster and in her PhD, she aims to understand several parity games algorithms better. She enjoys working on problems from the perspective of games, but more broadly, she is interested in problems in logic, automata, and games.