Termination of fair computations in term rewriting

Salvador Lucas, José Meseguer

Research output: Contribution to journalConference articlepeer-review


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 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 proof methodology for proving fairtermination 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.

Original languageEnglish (US)
Pages (from-to)184-198
Number of pages15
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3835 LNAI
StatePublished - Jan 1 2005
Event12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005 - Montego Bay, Jamaica
Duration: Dec 2 2005Dec 6 2005


  • Concurrent programming
  • Fairness
  • Program analysis
  • Term rewriting
  • Termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Termination of fair computations in term rewriting'. Together they form a unique fingerprint.

Cite this