Chennai Mathematical Institute

Seminars




Computer Science Seminar
Date: Wednesday, 3 April 2024
Time: 3:30 to 4:30 PM
Venue: Lecture Hall 2
On the Monadic Second-Order Theory of Arithmetic Predicates

Mihir Vahanwala
MPI-SWS, Saarbrücken, Germany.
03-04-24


Abstract

Logicians, both theoretical and applied, inevitably face a compromise: the expressive power of a logic often comes at the cost of the tractability of deciding its verification problem, sometimes at the cost of decidability itself. Our work views this tradeoff optimistically: we consider the well understood MSO Theory of the Natural Numbers, and ask what expressive power we can add while retaining its decidability. Prior work has studied the effect of expanding the theory with a single unary predicate. Our work introduces a framework to show decidability of the MSO Theory of the Natural Numbers expanded with multiple unary predicates. In this talk, we illustrate our techniques by showing how to decide the theory expanded with the predicates PowerOf2, PowerOf3.

Bio: Mihir Vahanwala is a PhD student at the Max Planck Institute for Software Systems, Saarbrücken. He works in the Foundations of Algorithmic Verification Group led by Prof. Joël Ouaknine. His research interests lie in dynamical systems, logic, and concurrency. Before joining his current position, he graduated from IIT-Bombay in 2022 with a B.Tech. (with Honours) in Computer Science and Engineering.