## 2 Background
### Coloured Petri Nets (CPNs)
#### 2.1.1 CPN Tools  
CPN Tools [13] is the main tool used to design coloured Petri nets. Each place has a name, a colour set and an initial marking. The name identifies the place, the colour set determines the types of tokens that can be stored, and the place may also have an initial value. This initial value is used to start the CPN model. Figure 1(a) illustrates a place (_place01_) containing one token set to zero. Outside the place there are an initial marking (set to 0) and a colour set (_INT_).  
Figure 1(b) shows an arc with a single annotation that is a variable (\(i\)) of the same type of the input place colour. Figure 1(c) illustrates a transition containing: identification (_trans01_), guard, time and code. The guard (\([i=0]\)) is a Boolean expression and must be true to enable the transition. When the  
Figure 1: (**a**) place and token, (**b**) arc and (**c**) transition representations in CPN Tools.  
transition is fired, the time fragment (@+_I_) adds a certain amount of time in the CPN model and the code assigned to the transitions must be executed. The code is divided into three parts: _input_, _output_ and _action_. The _action_ contains the CPN ML code to perform some activity that processes the input (_input_) and returns a value (_output_).  
Hierarchical CPN aims to represent CPN models at different abstraction levels that that may be connected to each other. This feature is very useful for building large models (e.g., to represent an application). In practice, this feature enables us to divide the model into multiple modules, where each module has a CPN. In addition, it allows the reuse of modules, which reduces the size of the model. These independent models (called sub modules) are represented by a substitution transitions in the main module. These modules are connected through places and the connections always involve only two places: one in the sub modules (called _port_) and another in the super modules (called _socket_). A _socket_ passes a token to its respective _port_, and _vice-versa_. There are three kinds of ports: input, output, and I/O. An input port receives a token from the socket; an output port sends a token to the super modules and I/O port can both send and receive tokens.  
The CPN Tools has an important mechanism to periodically extract information about marking of places and occurring biding elements: Monitor. A monitor may be used to observe, inspect, stop, control or modify the simulation of a CPN model. In practice, the monitor can observe and take appropriate actions based on the observations. There is support for four kinds of monitors, namely breakpoint (to stop a simulation), data collector (to extract numerical data from a net), write-in-files (to update files during simulations) and user-defined (used to any purpose).  
State space models, such as Petri nets, aim at automatic analysis and verification of the behavior of systems. The basic analysis methods build the system's state space considering all state transitions (reachability graph). This process can be fully automated. Unfortunately, such methods suffer from a problem that is fundamental that led many to believe that state space methods would never work well enough for large systems. Nevertheless, the great rewards of the state space models have stimulated researchers to undertake studies to lessen the problem [14]. There are many strategies and methods to tackle this problem, among them, it should be highlighted approaches that exploits structural attributes of the model [10, 11], reductions in the reachability graph and at the net level [15], exploration of symmetries within the reachability graph [9], the adoption of partial state space generation methods [16, 17], and simulation [6, 18, 19]. Simulation itself may be understood as a partial state space generation methods, since it stops generating new states when a criterion is reached. This particular work extensively uses reductions at the net level and adopts stochastic simulation as the fundamental strategy for conducting the evaluation.