The model-checking algorithm of the VFSM Validator is based
on the algorithms presented in "Memory-Efficient Algorithms
for the Verification of Temporal Properties", by
Courcoubetis, Vardi, Wolper, and Yannakakis, Formal Methods
in System Design, 1: 275-288 (1992).  We did not find the
proof of Algorithm A especially clear, so we have attempted
to improve on it.  Michael Benedikt and I worked on and
discussed versions of the proof; the following is my own
version.  In other words, Michael is not responsible for
errors in what follows!

----

We define depth-first search (DFS) as a recursive
algorithm on a labelled transition system.

dfs(s) =
   mark s			
   (t1,...,tn) = successors(s)
   for i from 1 to n
      if t_i is not marked
         dfs(t_i)
   return			

We write 's?' for the point in a DFS at which a call
to dfs(s) occurs, and 's!' for the point at which the
return from dfs(s) occurs.  Since dfs(s) is only
called if state s is unmarked, and s is marked
as the first step in dfs(s), we know that there can
be at most one s? and one s! for each state s, and
that s? must appear before s!.

The following simple property holds directly by definition
of DFS.

Prop. 1: Suppose t? appears between s? and s!.  Then
  a)  t! appears before s!, and
  b)  t is reachable from s

Lemma 0: Suppose there exists a path p from s to t in an
LTS, and that s is the first state marked on the path.
Then t! appears before s!

Proof.  By induction on the length of p.

Base case: path p is a single edge from s to t

Consider the point at which s is marked in the DFS.  Before
returning dfs(s) will examine node t to see if it is marked.
There are two cases.  If t is not marked then dfs(t) will be
called, and it must return before dfs(s) returns, so t!
appears before s!.  If t is marked, then dfs(t) was called
by another successor of s and returned, so t! occurs before
s!.

Induction case: the length of path p is n > 1.

Consider the first node u that is marked along p after s.
There are two cases.  In the first case node u is t.  
Since n > 1 we know there exists another node v along
the path from s to t.

    s ..... v ..... u=t

We have that: s? appears before t? (by assumption),
t? appears before v? (since t is the first node along
the path to be marked after s), v? appears before v!
(a basic property of DFS), and v! appears before s!
(by application of the induction hypothesis to the path
from s to v).  Therefore t? appears between s? and s!,
so by Prop. 1a. t! appears before s!.

In the second case node u is some node between s and t.

    s ..... u ..... t

By induction we know that u! appears before s! in the DFS
and that t! appears before u!, so t! appears before s!.

(End of proof of Lemma 0)

Lemma 1. Suppose that fi and fj are distinct, reachable
nodes, there is a path from fi to fj, and fi! appears
before fj! in the DFS.  Then fi belongs to a nontrivial
strongly connected component.

Proof.  Suppose fi is the first node to be marked on the
path.  Then fj! appears before fi! by Lemma 0, contrary to
assumption.  So some other node s must be the first node
to be marked on the path.

We know that s? appears before fi? (since s is the first
node to be marked on the path), that fi? appears before fi! (a
basic property of DFS), and that fi! appears before fj! (by
assumption).  So by transitivity fi? appears between s? and
fj!.

Now consider whether s and fj are the same.  If so, then fi?
appears between s? and s! immediately.  If not, then fj! 
appears before s! by application of Lemma 0 to s and fj, and
again fi? appears between s? and s!.  Therefore fi is
reachable from s by Prop. 1b.  Since s is reachable from fi
by assumption, nodes fi and s belong to a nontrivial
strongly connected component.

(End of proof of Lemma 1)