The increasing complexity of distributed applications makes their dependability a problematic issue. Model-checking is a formal method for automatically validating a system, based on an exhaustive exploration of its behaviors, but that is challenged by the combinatorial state-space explosion problem. To address this problem, we propose an approach based on automatic symmetry analysis of models and of properties expressed in Linear Temporal Logic (LTL), allowing construction of a quotient state graph that supports verification. We combine this approach with symbolic representations, thus offering an extremely compact storage solution. We define a flexible hierarchical decision diagram model, that allows to efficiently exploit a compositional description of a system. Finally, we place our techniques within a model-based rapid application development methodology, to allow their use in an industrial context.