For a detailed description of Petri Nets and their properties see, for example, [12].
Notice that we can represent a PN structure as a weighted bipartite
graph where the two classes of nodes are the places (usually
represented with circles) and transitions (usually represented with
bars). Then, the functions I and O define the set of edges, with
their respective weights, between the nodes. Furthermore, we can
represent this structure by means of a place-transition incidence
matrix, provided there are no self-loops; i.e. as long as no place
(transition) is both input and output of the same transition (place).
We will denote this incidence matrix by 
.
Figure 12 in Section 6.3 shows a Petri Net model for the Two-Pusher example.
We do not present here any formal methods to synthesize the plant model of a complex DES using Petri Nets. These are generally limited in the literature. However, we can refer the reader to [9] and [28] for some of these formalisms.
