Abstract

We provide a generic work-list algorithm to compute the transitive closure
of finite relations where only successors of newly detected states are
generated. This algorithm is then instantiated for lists over arbitrary
carriers and red black trees (which are faster but require a linear order
on the carrier), respectively. Our formalization was performed as part of
the IsaFoR/CeTA project where reflexive transitive closures of large tree
automata have to be computed.

BibTeX

@incollection{CSRT-AFP11a,
  author      = "Christian Sternagel and Ren{\'e} Thiemann",
  title       = "{E}xecutable {T}ransitive {C}losures of {F}inite {R}elations",
  booktitle   = "The Archive of Formal Proofs",
  editor      = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
  publisher   = "\url{http://afp.sf.net/entries/Transitive-Closure.shtml}",
  year        = 2011,
  month       = mar,
  note        = "Formal proof development"
  ISSN        = "2150-914x",
}