Abstract:
Logic-based approaches to Artificial Intelligence seem to be presently undervalued by most AI practitioners. However, we believe that mathematical logic -- while probably not the best tool for engineering -- should still be important in AI research for at least two reasons. First, mathematical models provide a conceptual apparatus for thinking about systems, that can be as well used outside mathematical logic. The second reason is that creating a formal model of a problem makes one realize many (otherwise implicit) assumptions underlying his or her approach to this problem. The assumptions are often given a simplistic treatment in the model, yet their implications are usually worth investigating even in this form. Moreover, having made them explicit, one can strive to relax some of them and still use a part of the formal and conceptual machinery -- instead of designing solutions completely ad hoc.

Model checking is an interesting idea that emerged from the research on logic in computer science. The model checking problem asks whether a particular formula holds in a particular model. This seems especially useful in the case of dynamic or temporal logics, whose models can be interpreted as game models, transition systems, control flow charts, data flow charts etc. Moreover, model checking turns out to be relatively cheap in computational terms.

It has been already proposed that the model checking of computation tree logic (CTL) formulae can be used for generating plans in deterministic as well as non-deterministic domains (Giunchiglia and Traverso, 1999; Pistore and Traverso, 2001). Alternating-time temporal logic ATL is an extension of CTL that includes notions of agents, their abilities and strategies (conditional plans) explicitly in its models. Thus, ATL seems even better suited for planning, especially in multi-agent systems, which was already suggested in (van der Hoek and Wooldridge, 2002). In this paper, we introduce a simple adaptation of the ATL model checking algorithm from (Alur et al., 2002) that -- besides checking if a goal can be achieved -- returns also an appropriate strategy to achieve it. We point out that this algorithm generalizes the well-known search algorithm of minimaxing, and that ATL models generalize turn-based transition trees from game theory. The paper ends with some suggestions that the contribution can be bilateral, and that game theory models and algorithms can improve ATL-based models of multi-agent systems as well.

Keywords: multiagent systems, planning as model checking, alternating-time temporal logic, minimaxing.

Computational Intelligence Group @ Technical University of Clausthal
Human Media Interaction Group @ University of Twente
Computer Science Group @ University of Gdansk	Last modified 2004-03-02