Petit nets in general are a great tool for managing concurrency. My university’s concurrent programming course used a fairly limited tool called LTSA to model concurrent systems, and that was a great little tool for designing and reasoning about concurrent systems.

Biggest limitation was the lack of code gen - it can prove things about a concurrent system (completion, deadlock feee, global operation ordering etc) but that was only accurate if the coded implementation had identical semantics.