Executable Transitive Closures of Finite Relations

Title:	Executable Transitive Closures of Finite Relations
Authors:	Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2011-03-14
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.
Change history:	[2014-09-04] added example simprocs in Finite_Transitive_Closure_Simprocs
BibTeX:	@article{Transitive-Closure-AFP, author = {Christian Sternagel and René Thiemann}, title = {Executable Transitive Closures of Finite Relations}, journal = {Archive of Formal Proofs}, month = mar, year = 2011, note = {\url{http://isa-afp.org/entries/Transitive-Closure.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Collections, Matrix
Used by:	KBPs, Network_Security_Policy_Verification, Planarity_Certificates
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.