Linear Logic Flavoured Composition of Petri Nets

TLA+ is first-order temporal logic, where you can write formulas describing how the state of a system evolves over time. If you have a concurrent process, you can describe it as a state machine, and then write TLA+ formulas to describe the evolution of the system state as the system reacts to events and evolves through time.

In contrast, Petri nets are not a logic. They are a generalisation of finite state machines tuned for describing concurrent processes. In Petri nets, the state is decomposed into a set of "places", and you mark the places with "tokens" to indicate what the current state of the system is. Depending on the state, different state transitions are enabled or not. The variant of state machines that Petri nets correspond to are called "vector addition systems with states" -- basically finite state machines plus a finite number of integer-valued registers. (However, the post this article links to describes a restriction of Petri nets where the markings are 0-1, which makes them exactly the same as FSMs.)

Since the logic of TLA+ describes infinite-state systems, if you want, you can represent Petri nets pretty directly as a set of integer-valued variables and then just write TLA+ formulas about them.

However, the main interest in Petri nets comes from the two facts that (a) they do a good job of describing concurrent systems (you can mix state- and event-based descriptions easily), and (b) are very well-behaved algebraically -- there is a wide variety of constructions which build bigger Petri nets out of smaller ones, which preserve various good properties of the smaller ones. (This latter thing is in fact what the linked post is doing.)