Séminaire PANAME' Agents
Model Checking Abilities of Agents: A Closer Look
Friday, March 23, 2007Jüergen DIX (Clausthal University, Allemagne)
Alternating-time temporal logic (acro{atl}) is a logic for reasoning about open computational systems and multi-agent systems. It is well known that acro{atl} model checking is linear in the size of the model. We point out, however, that the size of an acro{atl} model is usually exponential in the number of agents. When the size of models is defined in terms of states and agents rather than transitions, it turns out that the problem is (1) Delthree-complete for concurrent game structures, and (2) Deltwo-complete for alternating transition systems. In the second part, we study the model checking complexity for formulae of acro{atl} with imperfect information (acro{atl$_{ir}$}). We show that the problem is Deltwo-complete in the number of transitions and the length of the formula (thereby closing a gap in previous work of Schobbens [Schobbens04ATL]. Then, we take a closer look and use the same fine structure complexity measure as we did for acro{atl} with perfect information. We get the surprising result that checking formulae of acro{atl$_{ir}$} is also Delthree-complete in the general case, and Sigtwo-complete for Positive acro{atl$_{ir}$}''. Thus, model checking agents' abilities for both perfect and imperfect information systems belongs to the same complexity class when a finer-grained analysis is used. (joint work with Woitek Jamroga)
More details here …
yasmine.charif (at) nulllip6.fr