Abstract: 
We provide a generic worklist algorithm to compute the
(reflexive)transitive closure of relations where only successors of newly
detected states are generated.
In contrast to our previous work, the relations do not have to be finite,
but each element must only have finitely many (indirect) successors.
Moreover, a subsumption relation can be used instead of pure equality.
An executable variant of the algorithm is available where the generic operations
are instantiated with list operations.
This formalization was performed as part of the IsaFoR/CeTA project,
and it has been used to certify sizechange
termination proofs where large transitive closures have to be computed.

BibTeX: 
@article{TransitiveClosureIIAFP,
author = {RenĂ© Thiemann},
title = {Executable Transitive Closures},
journal = {Archive of Formal Proofs},
month = feb,
year = 2012,
note = {\url{http://isaafp.org/entries/TransitiveClosureII.html},
Formal proof development},
ISSN = {2150914x},
}
