Thursday, November 22, 2012
Speaker: Thomas Colcombet
Venue: IST Austria
The subject of this talk is to present regular cost functions, a quantitative extension to the notion of regular languages (of words, trees, finite or infinite) for which powerful decision procedures are available.
We will motivate this presentation starting from an open question (FOSSACS 2011) of Rabinovich and Velner concerning an extension of Church synthesis problem in which Player I is allowed, afterward, to change a bounded number of moves he played. Formally, the question is as follows: two players, I and II, which alternatively play a bit, thus producing an infinite play.This play is said n-winning if, up to modifying n of the bits player I has played so far, the play belongs to a given regularlanguage of infinite words. The problem is to decide if there is a natural number n such that Player I can guarantee n-winning.
We will see that this question is naturally (and positively) solved using regular cost functions over infinite words.