In this talk, we revisit the fundamental problem of quantifier elimination in Existential Presburger Arithmetic. As one of the main highlights, we challenge the long-standing claim that eliminating a block of existentially quantified variables necessarily requires doubly exponential time. Our recent work refutes this by introducing a novel procedure which accomplishes quantifier elimination in singly exponential time. The core of our approach is a small model property for parametric integer programming, which extends the seminal results of von zur Gathen and Sieveking on small integer points within convex polytopes. Additionally, if time permits, I will discuss a compelling application of Presburger Arithmetic in proving a dichotomy related to the reachability problem for counter machines with infrequent reversals. By analyzing the growth of small solutions for iterations of Presburger-definable constraints, we show that any counter machine falls into one of two categories: (i) the number of reversals is uniformly bounded by a constant across all runs, or (ii) the number of reversals grows at least logarithmically with the length of the run. Moreover, reachability is undecidable for counter machines where the number of reversals grows logarithmically. This result indicates that, vis-à-vis counter machines, classical reversal bounding encompasses all the decidable cases within the broader framework of infrequent reversals.

Short Bio:

Khushraj Madnani is a postdoctoral researcher at the Max-Planck Institute for Software Systems in Kaiserslautern, Germany,  associated with the Rigorous Software Engineering group and the Models of Computation group. His research interests is boradly within the domain of formal verification of infinite-state systems, focusing primarily on (1) automata and logics for timed systems, (2) formal logics and models of computation, and (3) network controlled cyber physical systems. Khushraj completed his Master's and Ph.D. in Computer Science and Engineering at the Indian Institute of Technology (IIT) Bombay, Mumbai, India, under the guidance of Prof. S. Krishna and Prof. Paritosh K. Pandya where he defended his thesis titled "On Decidable Extensions of Metric Temporal Logic". Before joining the Max-Planck Institute, Khushraj was a postdoctoral researcher at the Delft Center for Systems and Control (DCSC) within the Faculty of Mechanical Engineering at Delft University of Technology, The Netherlands. He also served as a visiting postdoctoral fellow at the Tata Institute of Fundamental Research (TIFR) in Mumbai, India.