I've started to read about process calculi (such as CSP and π-calculus). It seems to me that they are extremely general and can represent pretty much any concurrent system, many of which will be unable to "make progress".
I wondered if there were much more restrictive formalisms for describing concurrent processes? Perhaps something close to formal languages augmented with a parallel composition (a kind of tensor product of the joined languages) might work quite well? Maybe, in particular a Parsing expression grammar.
Process calculi seem to generally have a concept of channels on which synchronous messages are exchanged. The set of allowable messages are known as the alphabet of a process, and it seems analogous to the symbol set of a formal language (you'd need to augment the symbols with a send and a receive label).
The possible traces of a process calculus would be analogous to the possible strings of a language.
So, the actual questions: is there something like this in the research literature? Thanks!