# How do process calculi, CSP, Promela, … compare?

In protocol analysis, formal verification is a very important tool. What are the major differences between CSP,Promela,... and their pro's and con's for what specific usage cases? What do you think about graphical representations of communicating systems (gCSP, v-Promela,...)? What other lesser known/used process calculi do you recommend?

-