Termination of just/fair computations in term rewriting

13 years 4 months ago

Download users.dsic.upv.es

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.

Salvador Lucas, José Meseguer

Real-time Traffic