### 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.

### License

GNU Lesser General Public License (LGPL)

### Topics

- Computer science/Algorithms/Graph

### Session Transitive-Closure

- Transitive_Closure_Impl
- Transitive_Closure_List_Impl
- RBT_Map_Set_Extension
- Transitive_Closure_RBT_Impl
- Finite_Transitive_Closure_Simprocs

### Depends on

- Collections Framework
- Executable Matrix Operations on Matrices of Arbitrary Dimensions

### Used by

- Planarity Certificates
- Network Security Policy Verification
- Knowledge-based programs

### Auto-related entries

- Executable Transitive Closures
- Deriving class instances for datatypes
- Certification Monads
- XML
- Generating linear orders for datatypes

## Cite

×

Transitive-Closure-AFP

    @article{Transitive-Closure-AFP,
      author  = {Christian Sternagel and René Thiemann},
      title   = {Executable Transitive Closures of Finite Relations},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2011},
      note    = {\url{https://isa-afp.org/entries/Transitive-Closure.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 12, 2011 : Isabelle2011-1
- Oct 11, 2011 : Isabelle2011-1
- Mar 14, 2011 : Isabelle2011