  We consider parameterized concurrent systems consisting of a finite but
unknown number of components, obtained by replicating a given set of finite
state automata. Components communicate by executing atomic interactions whose
participants update their states simultaneously. We introduce an interaction
logic to specify both the type of interactions (e.g.\ rendez-vous, broadcast)
and the topology of the system (e.g.\ pipeline, ring). The logic can be easily
embedded in monadic second order logic of finitely many successors, and is
therefore decidable.
  Proving safety properties of such a parameterized system, like deadlock
freedom or mutual exclusion, requires to infer an inductive invariant that
contains all reachable states of all system instances, and no unsafe state. We
present a method to automatically synthesize inductive invariants directly from
the formula describing the interactions, without costly fixed point iterations.
We experimentally prove that this invariant is strong enough to verify safety
properties of a large number of systems including textbook examples (dining
philosophers, synchronization schemes), classical mutual exclusion algorithms,
cache-coherence protocols and self-stabilization algorithms, for an arbitrary
number of components.
