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. Key words: Concurrent programming, fairness, term rewriting, program analysis, termination.

• Type: Journal
• Year: 2008
• Where: IANDC
• Authors: Salvador Lucas, José Meseguer
• Keywords: Concurrent System, IANDC 2008, Ordinary Termination Problems, Termination Technology