We start with some notation and definitions. Given a finite set of
states, we write for the set of finite sequences of states over
, and for the set of possibly infinite state sequences.
Where `' stands for a possibly infinite state sequence in
and is a natural number, by `' we mean the
state of index in , by `' we mean the prefix
of .
denotes the concatenation of and
.

**Subsections**

Sylvie Thiebaux
2006-01-20