The computational complexity of scenario-based agent verification and design

We first advocate that the AUML (Agent Unified Modeling Language) notation, even in its new version, is not precise enough to adequately describe protocols. This problem was long identified by Harel and we propose to follow his solution: extend sequence diagrams with a “prechart”, i.e. single out the initiation sequence of the protocol. This new notation keeps readability and intuition, but is also technically adequate and is given a formal semantics. It actually is a form of simple temporal logics, equipped with a game-based semantics, which is appropriate for modeling agent-based systems. We then go on to study its complexity. Unsurprisingly, the version with protocol roles is undecidable. The main interesting problem is to synthesize agents that follow the protocol described. Surprisingly, it is undecidable even if we remove roles, alternatives, loops, asynchronous communication, conditions, constraints, negations (already removed in AUML). The complexity of checking whether a society of agents obeys a protocol given in this trivial notation is also surprisingly high: it is PSPACE-complete, like temporal logic, while we show that this simple language is strongly less expressive than temporal logic. Notations in-between have the expected increase in expressiveness, but no increase in complexity. This justifies the use of a language including alternatives, asynchronous communication and conditions, since it increases expressiveness with no cost in complexity.