Speaker: Madhusudan Parthasarathy , University of Pennsylvania, Philadelphia
Games for Verification and Control of Reactive Systems
Abstract: Reactive systems are systems that continuously and dynamically interact with their environment. The system and the environment can be viewed as two players playing a game. While the environment tries to give adversarial inputs to the system, the system tries to "play" in such a way so as to meet its requirement specification. Viewing reactive systems as games has met with success in various problems in formal methods. In this talk, we present two recent results that exploit this connection. In the first part of the talk, we look at games on recursive state machines. Recursive state machines (RSMs) naturally model the control-flow of software modules with procedure calls and returns. We consider the problem of solving multi-player games on RSMs, which has applications to verifying compatibility of software modules and can be used to formalize interfaces. The main result is that the problem of solving this game is decidable for various specification mechanisms such as reachability, safety and LTL specifications. The complexity of the procedure is linear in the the size of the RSM and exponential in the total number of values the modules can return.
In the second half of the talk, we address the synthesis problem for distributed systems. Consider n agents that interact with the environment at different speeds, and communicate with each other at various points in time. We want to automatically design strategies for each agent so that they meet a common goal. Solving such a problem has applications in distributed control (the strategies are the controllers) and in synthesizing communication protocols. The problem is in general undecidable and notoriously hard to tame to decidability. We identify three restrictions under which the problem becomes decidable. Furthermore, if any of these restrictions are dropped, we show that the problem becomes undecidable.
We conclude with some results in ongoing work on implementing game-solvers using methods that have been effective in model-checking, such as symbolic exploration using BDDs and SAT-solvers.
Short Bio: Madhusudan Parthasarathy is currently at the University of Pennsylvania doing his post-doctoral fellowship. After finishing his Bachelors in Mathematics in Loyola College, Chennai, India, he joined for a masters and doctoral program at the Institute of Mathematical Sciences, Chennai. He obtained his doctoral degree in September 2002, with a dissertation on the control and synthesis of reactive systems, under the supervision of Prof. P.S. Thiagarajan. During his doctoral program, he had been a visiting research scholar for a year at RWTH, Aachen, Germany in the group of Prof. Wolfgang Thomas. From January 2002, he has been a post-doctoral researcher at Upenn in the group of Rajeev Alur, working mainly on formal methods, games, reactive systems and scenario-based verification. His hobbies include amateur astronomy, photography and bird-watching.
Hosts: S. Purush Iyer, Computer Science, NCSU