OFCOURSE

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).

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.

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.

TBD

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.