LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

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

Tuesday, July 01 2008 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
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)

About LSV