A talk series on
Models of Computation and Rigorous Software Engineering



A. R. Balasubramanian

08 September 2022 - 10:00 CEST

We consider the class of depth-bounded processes in $\pi$-calculus. These processes are the most expressive fragment of $\pi$-calculus, for which verification problems are known to be decidable. The decidability of the coverability problem for this class has been achieved by means of well-quasi orders. (Meyer, IFIP TCS 2008; Wies, Zufferey and Henzinger, FoSSaCS 2010). However, the precise complexity of this problem is not known so far, with only a known EXPSPACE-lower bound. In this paper, we prove that coverability for depth-bounded processes is $\mathbf{F}{\epsilon_0}$-complete, where $\mathbf{F}{\epsilon_0}$ is a class in the fast-growing hierarchy of complexity classes. This solves an open problem mentioned by Haase, Schmitz, and Schnoebelen (LMCS, Vol 10, Issue 4) and also addresses a question raised by Wies, Zufferey and Henzinger (FoSSaCS 2010).

Click here for more details.
Ritam Raha

22 September 2022 - 10:00 CEST

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.

Ruiwen Dong

6 October 2022 - 10:00 CEST

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.



K. S. Thejaswini

25 August 2022 - 10:00 CEST

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.

Click here for more details.


OFCOURSE is the student talk series on Models of Computation and Rigorous Software Engineering at the
Max Planck Institute for Software Systems.
Run by and for PhD students, our aim is to provide a platform for PhD students to present their ongoing work, and to network with each other.
If you are interested in giving a talk, please contact one of the organisers below.