rank-based complementation and elevator automata
This could be the subject of an internship.
This paper defines a class of "elevator" automata (transition-based NBA where SCC are either deterministic or inherently weak) for which the rank-based conmplementation can be simplified. I'd like to have an implementation of that, as well as an implementation of Schewe's rank-based complementation (for the non-elevator case).