Syntax and Semantics of Petri Nets