Buchi automata in CSP and FDR

Let P be a divergence-free finite-state CSP process. 

What behavioural properties of P's infinite traces can the FDR check "C[P] is divergence free" via a finitary and distributive CSP context C?

[The restriction to distributive contexts is necessary to ensure that this condition is one of traces rather than sets of traces.]

I will show that these are precisely the sets of traces accepted by the deterministic Buchi automata.

[The proof that any such automaton is represented by a C is easy; the reverse is "interesting".]

I will also how a small modification to FDR can make it able to check for properties captured by (the negations of) arbitrary Buchi automata, and discuss such properties can fit into the CSP refinement framework.

If time permits I will also talk about fairness assumptions in the context of FDR, concentrating on its application to modelling shared variable programs.