This paper investigates a type-based framework to guarantee a basic
liveness property in the $\pi$-calculus.  The resulting liveness
property ensures that the action at a specified channel will
eventually fire, in spite of the presence of nondeterminism and
possibly diverging computation. We first integrate nontermination into
the linear $\pi$-calculus introduced in \cite{YBH01}, for which we
prove the liveness by a translation into the linear $\pi$-calculus,
preserving a specific sequence of typed actions. We then extend
the calculus with the first-order state, and prove the liveness property
via a translation into the linear $\pi$-calculus with nondeterministic
sums.  The systematic method based on techniques from term rewriting
systems and analysis of operational structures associated with
linearity leads to a clean proof of the liveness.  The liveness
property is interesting not only in its own right, but also in its
nontrivial semantic consequences, including decidability of equations
and non-interference theorems of secure functional and imperative
programming languages.