BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/1469
DTSTAMP:20240829T094125Z
SUMMARY:Presburger Arithmetic : Quantifier Elimination and Some Application
 s
DESCRIPTION:Speaker: Khushraj Madnani (Max Planck Institute for Software Sy
 stems\, Germany)\n\nAbstract: \nIn 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 el
 iminating a block of existentially quantified variables necessarily requir
 es doubly exponential time. Our recent work refutes this by introducing a 
 novel procedure which accomplishes quantifier elimination in singly expone
 ntial time. The core of our approach is a small model property for paramet
 ric integer programming\, which extends the seminal results of von zur Gat
 hen and Sieveking on small integer points within convex polytopes. Additio
 nally\, if time permits\, I will discuss a compelling application of Presb
 urger Arithmetic in proving a dichotomy related to the reachability proble
 m 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 n
 umber of reversals is uniformly bounded by a constant across all runs\, or
  (ii) the number of reversals grows at least logarithmically with the leng
 th of the run. Moreover\, reachability is undecidable for counter machines
  where the number of reversals grows logarithmically. This result indicate
 s that\, vis-à-vis counter machines\, classical reversal bounding encompa
 sses all the decidable cases within the broader framework of infrequent re
 versals.\nShort Bio:\nKhushraj 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 o
 f Computation group. His research interests is boradly within the domain o
 f 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 th
 e Indian Institute of Technology (IIT) Bombay\, Mumbai\, India\, under the
  guidance of Prof. S. Krishna and Prof. Paritosh K. Pandya where he defend
 ed his thesis titled "On Decidable Extensions of Metric Temporal Logic". 
 Before joining the Max-Planck Institute\, Khushraj was a postdoctoral rese
 archer at the Delft Center for Systems and Control (DCSC) within the Facul
 ty of Mechanical Engineering at Delft University of Technology\, The Nethe
 rlands. He also served as a visiting postdoctoral fellow at the Tata Insti
 tute of Fundamental Research (TIFR) in Mumbai\, India.\n
URL:https://www.tcs.tifr.res.in/web/events/1469
DTSTART;TZID=Asia/Kolkata:20240905T113000
DTEND;TZID=Asia/Kolkata:20240905T123000
LOCATION:A-201 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR