Termination of Fair Computations in Term Rewriting
Authors
Salvador Lucas and José Meseguer
Abstract
The main goal of this paper is to apply rewriting termination technology
---enjoying a quite mature set of termination results and tools--- to the
problem of proving automatically the termination of concurrent systems under
fairness assumptions. We adopt the thesis that a concurrent system can be
naturally modeled as a rewrite system, and develop a \emph{reductionistic}
theoretical approach to systematically transform, under reasonable
assumptions, fair-termination problems into ordinary termination problems of
associated relations, to which standard rewriting termination techniques and
tools can be applied. Our theoretical results are combined into a practical
\emph{proof methodology} for proving fair-termination that can be automated
and can be supported by current termination tools. We illustrate this
methodology with some concrete examples and briefly comment on future
extensions. Keywords
Concurrent programming, fairness, term rewriting,
program analysis, termination.