Abstract. The authors describe an algorithm for transformation of colored Petri nets with qualitative tokens into colored Petri net with quantitative tokens preserving boundedness, mutual exclusion, and liveness properties. This transformation allows an invariance method to be applied to colored Petri nets, which uses Truncated Set of Solutions finding algorithm for Petri net state equations expressed through systems of linear homogenous Diophantine equations. To show the algorithm’s efficiency, it is applied to the colored Petri net modeling the operation of a grid system. Equivalence of net models is tested by constructing and analyzing equal finite-state automata.

Keywords: colored Petri nets, Diophantine equations, finite-state machines, grid structure.