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 Aditya Prakash’s talk titled “Recognising history-deterministic parity automata”.

A nondeterministic parity automaton is history-deterministic if there is a resolver that can resolve the nondeterminism while reading a word, based on the prefix read so far. The complexity of deciding history-determinism for parity automata is a problem that has remained open since 2006 and was only known to be in PTIME for Büchi and coBüchi automata till recently. I will present some recent progress we have made on this problem where we extended the PTIME decidability procedure to parity automata with 4 priorities.

This is based on joint work with Karoliina Lehtinen.

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.