Add trim and reverse methods for NFAs

[jn1z]

Add trim and reverse methods for NFAs. (Reverse could be useful in theory for DFAs to NFAs, as well.)

I tried to make these generic, but got stuck in basically the same place as before.

[mtf90]

Just for a better understanding: Does the reversed NFA essentially represent the complement language? And is triming essentially a minimization of the NFA?

[jn1z]

Does the reversed NFA essentially represent the complement language?

Good question!
The complement language \bar{L} is separate from the reversed language L^R.
\bar{L} is recognized by just flipping the final and non-final states.
L^R requires flipping the final and initial states, and inverting all transitions.

So, for example,
L = {0, 01, 100}
L^R = {0, 10, 001}
\bar{L} = {1, 10, 011} or something like that

I'll look for a reference to add to the comments.

is triming essentially a minimization of the NFA?

Yes, it's an O(m) minimization of the NFA that removes "dead states".
Right-trim removes those that aren't reachable from the initial state(s) -- these are often removed during Subset Construction.
Left-trim removes those that don't reach the final state(s).

The "trim" terminology is mentioned here, for example: https://cs.stackexchange.com/questions/159828/

I'll look for a reference to add to the comments.

No rush on this PR especially if you've got large changes happening. BTW, I'll email you about my goals here, it might be of interest to you.

[mtf90]

Don't worry, there is always stuff to do :D. I'll manage to find some time for your contributions. I'm excited to hear about the broader picture.

The reversal part makes sense so far. I'll have to think a little bit about where to put it best (because you could also reverse a DFA for example, maybe even MealyMachines?).

As for the triming, maybe we could use some of the existing code. The Minimizer works on arbitrary UniversalGraphs which NFAs can be transformed to. Maybe something along the lines of Automata#minimize? Or does trim include some other important properties?

[jn1z]

Cool!

As for the triming, maybe we could use some of the existing code.

Yes, absolutely. trim is not sophisticated. Half of it just applies a quotient, which is already done by the Minimizer. So there could be re-use there.

The reversal part makes sense so far. I'll have to think a little bit about where to put it best (because you could also reverse a DFA for example, maybe even MealyMachines?).

I don't know much about Mealy machines. But according to this, you can't reverse a Mealy machine in general: https://cs.stackexchange.com/questions/83383/reverse-the-input-and-output-of-a-mealy-machine

[mtf90]

I don't know much about Mealy machines. But according to this, you can't reverse a Mealy machine in general: https://cs.stackexchange.com/questions/83383/reverse-the-input-and-output-of-a-mealy-machine

Yeah, reversal may introduce non-determinism. For FSAs this is not a problem, but AutomataLib currently does not support non-deterministic transducer.

[jn1z]

The Minimizer works on arbitrary UniversalGraphs which NFAs can be transformed to.

Oh... does that mean this might already support NFA reduction via "multiple-relation Paige-Tarjan" ?!
e.g., [Ilie-Yu], https://www.csd.uwo.ca/~ilie/TisF04.pdf

That would be wonderful if so -- I've had difficulty finding an implementation of that anywhere, but it should be only subtly different from Paige-Tarjan and bisimulation.

[mtf90]

I took a closer look at the referenced paper of the Minimizer class. Unfortunately, the abstract states that

We design an algorithm that minimizes irreducible deterministic local automata ...

While the implementation seems to be able to deal with non-deterministic automata (or rather graphs) as well, I observed another problem. Since the implementation works on graphs, it has no knowledge about the automaton-specific semantics and only compares structural properties of states. For example, an accepting state with no outgoing transitions and an accepting state with only rejecting sink-successors would be treated as in-equivalent. There are other cases where this behavior causes confusion. Maybe we can use your work as a kick-off to overhaul / cleanup some of the minimization interfaces and be more precise when to use what method.

As for the trimming / minimization of NFAs: the PaigeTarjanInitializers class has specific methods for minimizeDFA and minimizeMealy. Maybe it is possible to hook into existing code with a special minizeNFA initialization? Unfortunately, I have never looked into the specific algorithms in detail, so it might take me some time to get into it. If you have any ideas, feel free to go ahead.

[jn1z]

We design an algorithm that minimizes irreducible deterministic local automata ...

I'm hopeful that it didn't mention NFAs, because technically the algorithm can't "minimize" NFAs (which is NP-hard), but rather reduce them somewhat.

Also it mentions that it solves "for a sequence of partial functions", i.e., similar to a sequence of relations.

For example, an accepting state with no outgoing transitions and an accepting state with only rejecting sink-successors would be treated as in-equivalent.

I believe this is actually what's desired for Ilie-Yu NFA reduction! (In either state, any further transition is rejecting, so they're equivalent. Additionally, all sink states are equivalent to each other, i.e., at most one sink state when quotiented.)

As for the trimming / minimization of NFAs: the PaigeTarjanInitializers class has specific methods for minimizeDFA and minimizeMealy. Maybe it is possible to hook into existing code with a special minizeNFA initialization?

I actually attempted that: https://github.com/jn1z/NFA-experiments/blob/main/NFAMinimize.java
This initializes PaigeTarjan with the expected data for an NFA. But testing appeared to show this didn't work. I fear this is due to the subtle difference of partition refinement and "multiple-relation partition refinement".

This paper says it adapted the multiple-relation version to Aldebaran (which was replaced with the somewhat-closed-source CADP): https://www.sciencedirect.com/science/article/pii/016764239090071K
"...an adapted version... computing the coarsest partition problem with respect to the family of binary relation instead of one binary relation"

I tried understanding the difference, but there's a subtlety I'm missing.

[jn1z]

As an aside, the Beal-Crochemore paper mentions that:

"We assume that the automaton is trim, i.e., each state is co-accessible: there is at least one successful path starting from this state. This assumption is important to guarantee the correctness of the algorithm."

...which means that the current Minimize implementation does a trim somewhere ?

[jn1z]

would be treated as in-equivalent.

Oh, I misread that as "equivalent". You're right, that's not what we want.

[mtf90]

I skimmed over the Beal/Crochemore paper but find it very hard to understand because it requires a lot of background knowledge about specific sub-classes of automata. I think the code is not a direct implementation of the algorithm but does some additional steps to make it more general. For example, the paper states that

In general, it is not true that a deterministic non-minimal automaton has mergeable states (see the automaton of Figure 2).

While I understand that the automaton in Fig. 2 is a non-AFT automaton, it sounds like the algorithm presented in the paper cannot minimize it. Yet, the implementation can. Furthermore, your remark

...which means that the current Minimize implementation does a trim somewhere ?

is included in the initialize method (which filters all uneachable states via a breadth-first traversal) which supports the idea of additional tweaks.

It may reasonable to try to extend it to non-deterministic automata, but I would first like to understand what your goal with this PR is. I also read the Ilie/Navarro/Yu paper and personally find the equivalence-based reduction (using PaigeTarjan like in your draft) rather elegant. However, both approaches (left-/right-equivalence) only seem to reduce but not necessarily minimize the NFA (?). Any particular reason why you are interested in this approach but not actual minimization (even though it is PSPACE complete)?

[jn1z]

it sounds like the algorithm presented in the paper cannot minimize it. Yet, the implementation can.

Strange! Actually, originally I was reading a 2008 version of the Beal-Crochemore paper:
https://hal.science/hal-00620274/document

Which appears clearer to me anyway. That's the one that mentions "trim" (the other one mentions irreducible, i.e. strongly connected, which seems like an even stronger assumption.)

(which filters all unreachable states via a breadth-first traversal)

Does that handle the co-accessible case? I think that's required by the paper (then again, the implementation may be doing something different than the algorithm).

I would first like to understand what your goal with this PR is.

I just wanted to add some functionality that I'm using locally. "reverse", in particular, seems like a generic use case.

The PR can be dropped/closed though, that's fine.

I also read the Ilie/Navarro/Yu paper and personally find the equivalence-based reduction (using PaigeTarjan like in your draft) rather elegant.

Me too -- I like that it reduces to Hopcroft in the DFA case.

I have a naive version of the NFA reduction that I can add to my repo in a bit -- it's supposedly O(mn) rather than O(m log n) and as such is too slow for some use cases.

Any particular reason why you are interested in this approach

I'm interested in making expected-case determinization faster, and in certain cases, these make determinization much faster at a small cost (think of them as "preconditioners").

For a description of the overall goal, I emailed your tu-dortmund.de account a few days ago from my gmail account -- it may have gone to spam ?

[mtf90]

Strange! Actually, originally I was reading a 2008 version of the Beal-Crochemore paper: https://hal.science/hal-00620274/document

Oh wow, the DOI link in the documentation actually links to a different paper than the link name suggests. Your version seems much more digestible. I'll read your version and update the documentation when time allows.

I just wanted to add some functionality that I'm using locally. "reverse", in particular, seems like a generic use case.
...
I have a naive version of the NFA reduction that I can add to my repo in a bit -- it's supposedly O(mn) rather than O(m log n) and as such is too slow for some use cases.

I think keeping the PR for now is fine, even if it is just for experimentation. Maybe converting it to a draft would be cleaner, though, at least until things are finalized.

I'm interested in making expected-case determinization faster, and in certain cases, these make determinization much faster at a small cost (think of them as "preconditioners").

For a description of the overall goal, I emailed your tu-dortmund.de account a few days ago from my gmail account -- it may have gone to spam ?

Unfortunately, I haven't received any mail. Maybe try re-sending it. gmail addresses shouldn't be blocked, as far as I am concerned. Otherwise, if you are comfortable with having this discussion publicly, feel free to create a thread at the discussion page.

[jn1z]

Thanks! I'll create a discussion thread about NFA reductions.

Some of the remainder of the goal is original research (and, also, not proven to be correct yet ;-) ), so not ready for a public forum.