Transition systems has been intensively applied to the modeling of complex systems, for example they have been used for giving semantics to synchronous languages such as Lustre or Signal, or to hybrid automata. Properties of their behavior can be verified using model checking procedures, which rely on an iterative computation of least or greatest fixed points. For instance, safety properties can be proved by a fixed point computation of the set of all the states that can access to the forbidden states and verifying that it does not contain an initial state. This approach has to face two main difficulties : the complexity of the data types domain and the termination of the iterative algorithm. They are solved by approximation heuristics such as abstract interpretations and widening operators. However, in many cases, a sharper analysis of the transition system can be exploited to speed up the calculus. Consequently, we propose an other algorithm to compute this fixed point taking advantage of the decomposition of the relation in an union of simpler relations. If the transition system is deterministic, then our algorithm computes the exact fixed point, otherwise it computes an over approximation. We have implemented this algorithm on top of a linear constraint solver over real number and applied it to the proof of a safety property of a reactive system and we compare with the model checker Hytech.