Time+Place: Tuesday 29/11/2016 14:30 Room 337-8 Taub Bld.
Title: From Reachability to Temporal Specifications in Game Theory
Speaker: Orna Kupferman - COLLOQUIUM LECTURE http://www.cs.huji.ac.il/~ornak/
Affiliation: School of Computer Science and Engineering, Hebrew University
Host: Yuval Filmus


Multi-agents games are extensively used for modeling settings in which different 
entities share resources. For example, the setting in which entities need to 
route messages in a network is modeled by network-formation games: the network 
is modeled by a graph, and each agent has to select a path satisfying his
reachability objective. In practice, the objectives of the entities are often 
more involved than reachability. The need to specify and reason about rich
specifications has been extensively studied in the context of verification and 
synthesis of reactive systems. The talk describes a lifting of ideas from formal
methods to multi-agent games. For example, in network-formation games with regular 
objectives, the edges of the graph are labeled by alphabet letters and the objective 
of each player is a regular language over the alphabet of labels. Thus, beyond reachability, 
a player may restrict attention to paths that satisfy certain properties, referring, 
for example, to the providers of the traversed edges, the actions associated with them, 
their quality of service, security, etc.  

The talk assumes no previous knowledge in game theory or formal methods. We will introduce 
the basic concepts and problems, describe how their extension to games with more expressive 
specification of objectives poses new challenges, and study the resulting games.

Joint work with Guy Avni and Tami Tamir.

Short Bio:

Orna Kupferman is a professor in the School for Computer Science and Engineering 
at The Hebrew University. She researches the theoretical aspects of formal verification. 
Prof. Kupferman graduated from The Technion in 1995 and joined The Hebrew University in 1998. 
She was a visiting researcher in Bell Laboratories, UC Berkeley, Microsoft Research, 
Cadence Berkeley Labs, and Rice University. 

Refreshments will be served from 14:15
Lecture starts at 14:30