In the last decade, multi-agent systems have both become widely applied and also
increasingly complex. The applications include the use of agents as automous decision
makers in often safety-critical, dangerous, or high impact scenarios (traffic
control, autonomous satellites, computational markets). The complexity arises from
the fact that not only do we expect the agent to make decisions in situations that are
not anticipated at forehand, the agent also interacts with other complex agents, with
humans, organisations, and it lives in a dynamic environment (activators of an agent
can fail, communication is prone to error, human response may be ambiguous, rules
of an organisation may leave behaviour open or over-constrained, and environments
may change ‘spontaneously’ or as a result of other agents acting upon it).
Taking these two facts together call for a rigorous Specification and Verification
of Multi-Agent Systems. Since intelligent agents are computational systems, it is no
wonder that this activity builds upon and extends concepts and ideas of specifying
and verifying computer-based systems in general. For one, an axiom is that the
tools are mainly logical, or in any case formal. But although traditional techniques
of specification and verification go a long way when reasoning about the correctness
of a single agent, there are additional questions already to be asked at this level: do
we ‘only’ require the agent to behave well under a pre-defined set of inputs, or do
we want to allow for (partially) undefined scenarios? And do we care about the ‘correctness’
of an agent’s beliefs, desires and intentions during a computation? How do
we want to guarantee that the agent ‘knows what he is doing’, has ‘reasonable desires’
and ‘only drops an intention if it(s goal) is fulfilled, or cannot be reasonably
be fulfilled any longer’? And a predecessor of this ‘how to guarantee’ question is
equally important: what do we exactly mean by those requirements?
