Séminaires
Séminaire du 19 Avril 2013
Lieu
IBISC: comment y aller
petit amphi, rez-de-chaussée du bâtiment IBGBI
Programme
14h00-15h00: Valentin Goranko, Tech. Univ. Denmark, "How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games"
Abstract: 
game theory and Logic have developed two different traditions in studying abilities of agents to achieve objectives in multi-player games. Game theory studies rational behavior of players, relevant for their achievement of quantitative objectives: optimizing payoffs (e.g., maximizing rewards or minimizing cost) or, more generally, preferences on outcomes. On the other hand, logic mainly deals with abilities of players for achieving qualitative objectives of players: reaching or maintaining game states with desired properties, e.g., winning states or safe states. Put as a slogan, the former tradition is concerned with how a player can become maximally rich, or pay the least possible price, in the game, while the latter tradition -- with how a player can achieve a state of `happiness', or avoid reaching a state of `unhappiness', in the game.
We propose a logical framework combining the two traditions by enriching concurrent game models with payoffs for the normal form games associated with the states of the model and propose a quantitative extension of the logic ATL* enabling the combination of quantitative and qualitative reasoning. Again put as a slogan, our framework enables one to reason about whether and how a player can reach or maintain a state of `happiness' while becoming or remaining maximally rich, or paying a minimal cost on the way.
In this talk I will present the framework and will give some examples. Then I will discuss the model-checking problem for the Quantitative ATL* on guarded concurrent game models with payoffs and will mention some decidability and undecidability results..
15h00-15h30 : Yves-Stan Le Cornec, Univ. Evry, "Compositional analisys of modular systems using hierarchical state space abstraction"
Abstract: State space explosion is a well known problem when dealing with model-checking of large systems. One way to address this problem is modularity: we study individually the various components of a model, and try to avoid constructing the behavior of the full system if it is not necessary.
We consider a system defined as the synchronous product of its (finite) modules and propose an approach to perform efficient model-checking of mu-calculus formulae on such a modular system. Given a formula phi, each module can be analysed separately, possibly yielding a conclusion about the truth value of phi on the global system. When no conclusion can be drawn locally, a minimal state space preserving phi is computed for the module and can be incrementally composed with others, thus enabling for hierarchical analysis of the system in a bottom-up fashion.