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.
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)