# Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

## Séminaires passés

### Tableau-based decision procedure for the logic of strategic ability in multi-agent systems ATL

Date
Le mardi 01 juillet 2008 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Valentin Goranko (University of the Witwatersrand, South Africa)

The Alternating-time Temporal Logic (ATL), introduced by Alur, Henzinger, and Kupferman, is a logic for reasoning about strategic abilities of agents and coalitions in multi-agent systems, in which one can express statements, such as: "The agent (or, coalition of agents) A has a strategy such that, if A follows that strategy then, no matter what other agents do, the objective $\phi$ will be achieved", there the objective is itself a formula of ATL prefixed by a temporal operator such as nexttime', until', or `always in the future'.

Testing satisfiability in ATL has been proved decidable (ExpTime complete), by using alternating tree automata and by small model property, but both methods have some practical deficiencies and are not suitable for manual application.

In this talk I will give a concise introduction to ATL and then will present a recently developed decision procedure for testing satisfiability in ATL based on sound, complete, and terminating incremental tableaux. This decision procedure runs in the theoretically prescribed time complexity, i.e., ExpTime, but in most practical cases is much more efficient, and is suitable for both manual and computerized application.

(Joint work with Dmitry Shkatov, Univ. of the Witwatersrand)

## À propos du LSV

### Agenda des séminaires

mar. 19 février

Les séminaires précédents