  Reversible computation is an unconventional form of computing that extends
the standard forward-only mode of computation with the ability to execute a
sequence of operations in reverse at any point during computation. As such, in
this thesis we propose a reversible approach to Petri nets by introducing
machinery and associated operational semantics to tackle the challenges of the
main forms of reversibility. Our proposal concerns a variation of cyclic Petri
nets, called Reversing Petri Nets (RPNs) where tokens are persistent and
distinguished from each other by an identity. An immediate extension of the
original model includes allowing multiple tokens of the same base/type to occur
in a model. Specifically, we explore the individual token interpretation where
one distinguishes different tokens residing in the same place by keeping track
of where they come from. We also propose the collective token interpretation,
as the opposite approach to token ambiguity, which considers all tokens of a
certain type to be identical, disregarding their history during execution. Both
of the proposed models of RPNs (with single or multi tokens) implement the
notion of uncontrolled reversibility, meaning that it specifies how to reverse
an execution and allows to do so freely, yet it places no restrictions as to
when and whether to prefer backward execution over forward execution or vice
versa. In this respect, a further aim is to control reversibility by extending
our formal semantics where transitions are associated with conditions whose
satisfaction allows the execution of transitions in the forward/reversed
direction.
