Model-Checking Iterated Games

Title: Model-Checking Iterated Games

Speaker: Farn Wang (National Taiwan University)

Time: 14:30, 11 July 2013

Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

We propose a logic for the definition of the collaborative power of groups of agents to enforce different temporal objectives. The resulting temporal cooperation logic (TCL) extends ATL by allowing  for successive definition of strategies for agents and agencies.

Different to previous logics with similar aims, our extension cuts  a fine line between extending the power and maintaining a low

complexity: model checking TCL sentences is EXPTIME complete in the logic, and NL complete in the model. This advancement over

nonelementary logics is bought by disallowing a too close entanglement between the cooperation and competition. We show how allowing such an

entanglement immediately leads to a nonelementary complexity. We have implemented a model checker for the logic and shown

the feasibility of model checking on a few benchmarks.

Professor Farn Wang received his Bachelor Degree in Electrical Engineering from National Taiwan University in 1982. In 1984, he received a Master of

Science degree in Computer Engineering from National Chiao-Tung University in 1984. He then received a Ph.D. degree in Computer Sciences from  the University of Texas at Austin in 1993. He was with Institute of

Information Science, Academia Sinica from 1993 to 2003. He joined the Department of Electrical Engineering, National Taiwan University in 2003

and is now a full professor there.

Professor Wang is interested at the theory and application of the verification technology. He has implemented several tools for model-checking dense-time systems. He is also a steering committee member of the the ATVA international symposium. He is now interested at

model-checking game systems and probabilistic systems and testing of complicate software systems.