Optimization procedures in affine model checking

Symbolic model checking is based on a compact representation of sets of states and transition relations. At present there are three basic approaches of symbolic model checking: BDD-methods, bounded model checking using SAT-solvers, and various algebraic techniques, for example, constraint based model checking and regular model checking. In this paper we suggest improved algorithms for an algebraic data representation, namely, optimization algorithms for affine data structures.