On some analysis properties of colored Petri net using underlying net

Petri net is an effective tool to model and evaluate concurrent systems. Colored Petri net has been proposed to model large scale systems more effectively. Among analysis tools for colored Petri nets, such as reachability tree, to net invariants, to unfolded equivalent noncolored net, we use underlying noncolored Petri net. This method requires restriction on binding of the arc expression. In this report, some analysis properties of colored Petri net are studied using its underlying noncolored net. Sufficient conditions for boundedness and persistency are derived. Some restrictions on structure and binding are used to obtain a necessary condition for liveness.