Preprint, the final publication will be available at www.springerlink.comInternational audienceMatrix models are ubiquitous for constraint problems. Many such problems have a matrix of variablesM, with the same constraint C defined by a finitestate automaton A on each row ofMand a global cardinality constraint gcc on each column of M. We give two methods for deriving, by double counting, necessary conditions on the cardinality variables of the gcc constraints from the automaton A. The first method yields linear necessary conditions and simple arithmetic constraints. The second method introduces the cardinality automaton, which abstracts the overall behaviour of all the row automata and can be encoded by a set of linear constraints. We also ...