  We propose an automated method for computing inductive invariants applied to
check deadlock-freedom for parametric component-based systems. The method
generalizes the approach for computing structural trap invariants from bounded
to parametric systems with general architectures. It symbolically extracts trap
invariants from a monadic interaction formula characterizing the system
architecture. The paper presents the theoretical foundations of the method
including new results for the first order monadic logic and proves its
soundness. It also provides preliminary illustrations on examples.
