Factorization of the State Space Construction for Cyclic Systems with Data

In the context of formal modeling and verification of complex systems composed of cycling entities, we propose a method allowing to speed up the construction of state spaces exploiting symmetries. The method is suitable for systems continuously updating large data but whose transitions do not depend on the particular data values. Using a judicious ordering of operations, the method avoids non-necessary multiple treatments thus allowing to factorize a part of the computations. We prove that the method is correct and complete, and illustrate its application on a case study composed of a network of cycling timed automata extended with data.