Library hknt
Basic definitions, facts about continuous functions
Bisimulation proof method for DFA
DFA
Bisimulations
Up to equivalence (Hopcroft and Karp)
Extending the above techniques to NFA
NFA
Powerset construction
Up to congruence (HKC)
Up to congruence and language equivalence (HKC')
Computing the congruence closure by rewriting
Coinductive presentation of the antichain algorithms
Simulations
Theory of simulations up to
Simulations up to upward closure (AC)
Simulations up to upward closure and similarity (AC')
Relationship between AC and HKC
HKC can mimick AC
AC can mimick HKC on inclusion of disjoint automata
Relationship between AC' and HKC'
HKC' can mimick AC'
This page has been generated by
coqdoc