Modeling Petri nets using Alloy

Petri net is a computational tool that is well-known in modeling various processes. Its formal semantics, graphical nature and expressiveness lend itself as a convenient model of computation for a wide-range of applications. On the other hand, Alloy is a declarative specification language used for expressing structural constraints and behavior in a software system. Alloy is heavily influenced by the Z notation on its mathematical aspects and Object Constraint Language on its syntax. An advantage of Alloy, however, is that its semantics bridges the gap between Z and object models, and shows how to give simple and robust meaning to widely used forms, such as navigation expressions and object model diagrams. This paper demonstrates how Petri nets and its properties and behavior can be specified using Alloy.