| dc.description.abstract | Collective adaptive systems may be broadly defined as en sembles of autonomous agents, whose interaction may lead to the emer gence of global features and patterns. Formal verification may provide
strong guarantees about the emergence of these features, but may suffer
from scalability issues caused by state space explosion. Compositional
verification techniques, whereby the state space of a system is generated
by combining (an abstraction of) those of its components, have shown
to be a promising countermeasure to the state space explosion problem.
Therefore, in this work we apply these techniques to the problem of
verifying collective adaptive systems with stigmergic interaction. Specif ically, we automatically encode these systems into networks of LNT pro cesses, apply a static value analysis to prune the state space of individual
agents, and then reuse compositional verification procedures provided by
the CADP toolbox. We demonstrate the effectiveness of our approach by
verifying a collection of representative systems. | sv |
