Affiliations: Department of Economics, Lancaster University, LA1 4YX
Lancaster, UK. E-mail: [email protected] | Institute of Artificial Intelligence, University of
Groningen, Grote Kruisstraat 2/1, 9712 TS Groningen, The Netherlands. E-mail:
[email protected] | Institute of Informatics, Warsaw University, Banacha
2, 02-097 Warsaw, Poland. E-mail: [email protected]
Abstract: Our previous research presents a methodology of cooperative problem
solving for beliefdesire- intention (BDI) systems, based on a complete formal
theory called TEAMLOG. This covers both a static part, defining individual,
bilateral and collective agent attitudes, and a dynamic part, describing system
reconfiguration in a dynamic, unpredictable environment. In this paper, we
investigate the complexity of the satisfiability problem of the static part of
TEAMLOG, focusing on individual and collective attitudes up to collective
intention. Our logics for teamwork are squarely multi-modal, in the sense that
different operators are combined and may interfere. One might expect that such
a combination is much more complex than the basic multi-agent logic with one
operator, but in fact we show that it is not the case: the individual part of
TEAMLOG is PSPACE-complete, just like the single modality case. The full
system, modelling a subtle interplay between individual and group attitudes,
turns out to be EXPTIME-complete, and remains so even when propositional
dynamic logic is added to it. Additionally we make a first step towards restricting the language
of TEAMLOG in order to reduce its computational complexity. We study formulas
with bounded modal depth and show that in case of the individual part of our
logics, we obtain a reduction of the complexity to NPTIME-completeness. We also
show that for group attitudes in TEAMLOG the satisfiability problem remains in
EXPTIMEhard, even when modal depth is bounded by 2. We also study the
combination of reducing modal depth and the number of propositional atoms. We
show that in both cases this allows for checking the satisfiability in linear
time.
