## 2 Technical Background and Related Work  
### Colored Petri Nets  
Colored Petri Net (CPN) is a mathematical modeling language developed by [PERSON] [4] for the design and analysis of complex systems. CPN is an extension of Petri Nets [5] which was invented by [PERSON] with the concepts of color, time and hierarchy. In a CPN, the state of a system, being modeled, is represented with an ellipse and called a place. An activity, on the other hand, is represented by a rectangle and is called a transition. A directed arc connects a place and a transition such that a set of places, transitions, and arcs form mutually disjoint sets. Unlike Petri Nets, a place in CPN holds tokens that have different types of values, which allows modeling of complex systems. CPN incorporates a mathematical formalism that allows one to verify and validate the structural and behavioral properties of the modeled system. To understand a CPN, consider a simple traffic light signal. At any given instance, the traffic light can be in one of the three states: red, orange, or green. The signal changes its state after a fixed specified time. A Colored Petri Net model of this traffic light system is shown in Figure 1. The three states of the system, red, orange, and green are represented by places R, O, and G, respectively. The actions of going from state red to orange, from state orange to state green, and from state green to state red are represented by transitions Tro, Tog, and Tgr, respectively. The temporal characteristics of the system are modeled with delays on the transitions. The value of 20 on transition Tro in Figure 2 suggests that after 20 time units the traffic light will be in the orange state. Similarly, the values of 5 and 15 on transitions Tog and Tgr reflect the time delays which the traffic light will experience to be in the green and the red state, respectively. Figure 1: CPN Model of a Traffic Light System. The presence of a single token at place R in Figure 2 shows that the traffic light is currently in the state red. In the absence of expressions on the input arcs of a transition and guard expression, a transition is said to be enabled and ready to fire when all the input places have at least a single token available in them. The firing of a transition signifies that the event represented by that transition has taken place. A transition, when fired, takes token(s) from its input place(s) and produces token(s) for the output place(s). As seen in Figure 2, transition Tro is enabled and is ready to fire. Once it fires, it consumes the token from place R and produces a token for place O as shown in Figure 3. This suggests that the traffic light has changed its state from red to orange. The token at place O shows that the traffic light is now in the state orange and it has changed its state after 20 time units. To verify if a particular property holds true in the complete state space of a model, the reachability graph of a CPN is analyzed. The nodes in the graph correspond to the reachable markings of the CPN model and its edges correspond to the transitions of the CPN model from one marking to another. Table 1 presents the fundamental properties of a CPN model that can be verified through reachability analysis along with a brief description [6]. The reachability analysis report of the traffic light signal CPN (Figure 2) is summarized in Table 2. The report was generated in CPNTools [3] which automatically analyzes the reachability graph of a CPN model. The values of 1 and 0 for the upper and lower bounds signify the maximum and the minimum number of tokens that each place will have. The absence of dead marking reflects that the traffic light system is a continuous and ongoing system. The lack of a dead transition ensures that all the features of a traffic light system are used and since all transitions are live it also ensures that all the functionalities can be used again.