Hi Mitch:

from the Allen/Garlan paper we have:

A process is deadlock-free if for all (t, ref) in failures(C) such that ref = 
alphabet(C), then last(t) = SUCCESS.

t is a set of traces.

You suggest:

AG(no_next_state => finished)

For all paths, the following holds globally: no_next_state => finished

How do we assign the atomic proposition "no_next_state" based
on a static analysis of the graph and the formulas?

A theme in this area seems to be to translate from 
a restricted CSP (with Boolean variables and signals only)
to CTL by explicitly dealing with all the
possible interleavings. Do you know of paper which talks about translating
from a restricted CSP to CTL?

-- Karl

>From wand@ccs.neu.edu Mon Mar 30 16:19:52 1998
>From: Mitchell Wand <wand@ccs.neu.edu>
>To: Karl Lieberherr <lieber@ccs.neu.edu>
>Cc: wand@ccs.neu.edu, jayantha@ccs.neu.edu
>Subject: deadlock
>
>KL> Hi Mitch:
>KL> you mentioned that we can translate coordinators into CTL formulas
>KL> which express deadlock freeness. How do we exclude deadlock
>KL> with a CTL formula? Do you know of a paper which does that?
>KL> The original Clarke/Emerson paper talks about mutual exclusion and fairness
>KL> but not deadlock.
>
>KL> -- Karl
>
>X False represents the proposition that we are currently at a deadlock (ie no
>next step), since it asserts that after the next step, false is true.
>
>Or you could say  (X False => finished)  "if there is no next step, we must
>be at a place where "finished" is true.
>
>Then something like A(X False => finished) asserts that at every reachable
>state, if there is no next step, then we must be finished.  [the A might not
>be quite right, I don't have a CTL reference close at hand].
>
>--Mitch 
>