Hi Mitch:

you mentioned that we can translate coordinators into CTL formulas
which express deadlock freeness. How do we exclude deadlock
with a CTL formula? Do you know of a paper which does that?
The original Clarke/Emerson paper talks about mutual exclusion and fairness
but not deadlock.

-- Karl