Alladi Ramakrishnan Hall

On the Decidability and Complexity of the Theory of Presburger Arithmetic

Koduri Siddharth Choudary

IMSc

We consider the first order theory over Natural numbers with addition and order relations known as Presburger Arithmetic. We discuss a known decision procedure called Quantifier Elimination and its complexity. Further, we look at specific subclasses of this theory by imposing conditions on the Quantifier prefixes (such as fixing the number of alternations between universal and existential quantifiers or fixing the maximum length of a quantifier block without alternations, etc.) to give a more precise complexity bounds for these subclasses. Finally as an application, we consider the reachability problem in some classes of reversal bounded systems and give a reduction to Presburger Arithmetic.

This will be Siddharth's MSc Thesis defence. The talk will be in hybrid mode. The zoom link for the event will be as follows


zoom.us/j/91317891238

Meeting ID: 913 1789 1238
Passcode: 672510