Computer-aided Verification, Game Theory

Krishnendu Chatterjee's main research interest is in the theoretical foundations of formal verification and game theory. His current research focuses on stochastic game theory, probabilistic model checking, logic and automata theory, and quantitative theories of verification. In addition, the group is also interested in algorithms for developing robust reputation and trust management systems for Wikipedia.

Contact
Krishnendu Chatterjee
Institute of Science and Technology Austria (IST Austria)
Am Campus 1
A – 3400 Klosterneuburg

Phone: +43 (0)2243 9000-3201
E-mail: krishnendu.chatterjee@remove-this.ist.ac.at

CV & publication list

Chatterjee Group website

Assistant
Elisabeth Hacker

Phone: +43 (0)2243 9000-1015
E-mail: elisabeth.hacker@remove-this.ist.ac.at

Team

Selected Projects

- Game theory in verification
This project involves the algorithmic analysis of various forms of games played on graphs.  Automatically obtaining correct systems from specifications (synthesis) as well as many important questions in computer science can be analyzed effectively in the broad framework of games on graphs. In this project we work on theoretical aspects for the better understanding of games, developing new algorithms, as well as practical applications of game solving. The results present the theoretical foundations for the formal verification of systems. Last year we obtained several important results: for example, we have established optimal complexity results for one-player stochastic games with partial information, and improved the algorithms related to probabilistic verification and we now have the fastest algorithms for the verification of probabilistic systems with omega-regular specifications.

- Quantitative verification
The classical Boolean theory of verification has a wide range of applications. However, there are a lot of applications where a more quantitative approach is necessary. For example in the case of embedded systems, along with the Boolean specification, a quantitative specification related to resource constraints must be satisfied. In this work we have been developing a framework to specify quantitative properties, answer the quantitative questions related to the classical Boolean theory of verification. The results of this project are useful for the design of correct and robust systems, and present a new theoretical framework for the formal verification of systems. Last year we have obtained results that show that there exists a class of quantitative specification language that is robust and also decidable.

- Reputation and trust management systems
In this work we study how to design robust algorithms for automatically computing the reputation of authors and the trust of text of an article in Wikipedia. Our algorithms are based on the content evolution of Wikipedia articles, and are completely automatic. The algorithms we have developed are now implemented and soon our results will be available as a tool that can be used in Wikipedia.

- Software
Several new efficient algorithms that we have developed have also been implemented by us to obtain research tools like ALPAGA and GIST for the study of graphs games.

Selected Publications

  • Chatterjee K., Henzinger, M. 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. Symposium on Discrete Algorithms
  • Chatterjee K. 2007. Concurrent games with tail objectives. Theoretical Computer Science 388:181-198.3.
  • Chatterjee K. 2005. Two-player non-zero sum omega-regular games. Concurrency Theory pp. 413-427.


Career
2009 Assistant Professor, IST Austria
2008–2009 Postdoc, University of California, Santa Cruz, USA
2007 PhD, University of California, Berkeley, USA

Selected Distinctions
2008 Ackerman Award, best thesis worldwide in Computer Science Logic
2007 David J. Sakrison Prize, best thesis in EECS, University of California, Berkeley, USA
2001 President of India Gold Medal, best IIT student of the year

To top