I've seen that the preferred way to specify the semantics of a concurrent language is to use a process calculus (e.g. pi calculus, join calculus). But in the paper presenting the F# asynchronous programming model the authors have a different approach: they first perform a CPS conversion to a core language, and then, define the semantics in terms of a transition system in which states are tuples of the form (A, Q, P), where A is the set of active computations, Q is the set of queued computations, and P is the set of pending computations--i.e. Waiting for an event. Each computation is of the form e@ctx, where ctx is a label corresponding to a synchronization context. Finally, they give transition rules for reduction (which uses the reduction rule of the core language), suspension of computations waiting on events, activation of computations (i.e. moving computations from Q to A), and event signaling.
I was wondering if this is an acceptable (i.e. accurate enough) way of specifying the semantics of a concurrent language.
EDIT: can anyone point me to papers that use a similar approach to the one taken in the F# paper?