PUBLIC VIVA-VOCE NOTIFICATION
11.30 am, Seminar Hall
Analysis of Automata-theoretic Models of Concurrent Recursive Programs
Prakash Saivasan
Chennai Mathematical Institute.
13-05-16

---

Abstract

This thesis addresses algorithmic problems on multi-pushdown systems (MPDS) and concurrent networks of pushdown systems. Such systems are formal models of communicating multi-threaded recursive programs. The results proved in the thesis include:

1) Exponential-time completeness for linear-time model checking of scope bounded MPDS. 2) A new model called Adjacent Ordered MPDS (AOMPDS) for which reachability and linear-time properties are decidable in exponential time. 3) A detailed analysis of loop accelerations in conjunction with bounded context executions for MPDS. 4) The stage bounding restriction for concurrent PDSs communicating via shared memory. A nondeterministic exponential-time solution to the reachability problem for systems consisting of one pushdown and any number of counters A super primitive-recursive lower-bound for 2 pushdown systems (where the decidability is still open) and undecidability for any system with more than 2 pushdowns. Regular representations of abstractions (upward and downward closures) of PDAs and one counter automata (OCA) play a key role in the decidability. 5) Polynomial-time algorithms for downward and upward closures of OCAs (for PDAs an exponential lower bound is already known). A sub-exponential algorithm for computing an NFA Parikh-equivalent to any OCA. 6) A simplified proof of the decidability of parity games over bounded-phase MPDS (with non-elementary complexity). A non-elementary lower bound for deciding such games.