Concurrency Algebra and Petri Nets

Concurrency Algebra is an algebraic framework for reasoning about the dynamic behavior of Petri nets. Based on a simple algebra containing concatenation, choice, and shuffle of strings, concurrency algebra uses a substitution schema determined by the structure of the given Petri net to generate new terms that denote its behavior. For non-terminating Petri nets, the behavior becomes the smallest set of strings satisfying a recursive equation over sets of strings.