• iteration-bisimulation-automata