Termination of just/fair computations in term rewriting

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 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 proof method for proving fair-termination that can be automated and can be supported by current termination tools. We illustrate this proof method with some concrete examples and briefly comment on future extensions. (c) 2008 Published by Elsevier Inc.