partition an automaton into safety and liveness
The safety closure is what we use to build monitors, I think. We need the part building the liveness extension.
We should also provide a liveness detector, and add a safety/liveness classification in the on-line application.
See also ftp://www-cs.stanford.edu/cs/theory/amir/hierarchy.ps for some discussion of "liveness" vs. "uniform liveness". Maybe we could detect that as well.