open

Formal Verification of Open Multi-Agent Systems

We introduce a semantics to reason about MAS in which an arbitrarily large number of agents may join and leave at run-time.