Hi Mitch:
let's discuss tomorrow in seminar.
-- Karl
>From wand@ccs.neu.edu Tue Mar 31 15:04:45 1998
>
>You asked:
>
>kl> How do we assign the atomic proposition "no_next_state" based
>kl> on a static analysis of the graph and the formulas?
>
>As I had said earlier:
>
>mw> X False represents the proposition that we are currently at a deadlock (ie
>mw> no next step), since it asserts that after the next step, false is true.
>
>kl> A theme in this area seems to be to translate from 
>kl> a restricted CSP (with Boolean variables and signals only)
>kl> to CTL by explicitly dealing with all the
>kl> possible interleavings. Do you know of paper which talks about translating
>kl> from a restricted CSP to CTL?
>
>CTL or things like are intimately connected with the logic of CCS.  There are
>some good papers by Hennessy and Milner about this.  The logic of CSP is far
>less developed. I don't know if the reason is technological or personal.
>
>--Mitch 
>