NFT - Equivalence Checking

[koniksedy]

We need to implement a proper algorithm for equivalence checking of two NFTs. The existing implementation transforms NFT into an NFA by unwinding jump transitions. And then tests those NFAs using nfa-equivalence checking. However, there is a noticeable number of cases when this approach returns false instead of true.

The existence of a proper implementation would simplify the debugging of algorithms operating on NFT. It is impossible to debug algorithms operating and changing NFTs by only looking at their output. We need to be able to detect deviations from a correct NFT during the algorithm's execution. This is not possible with the existing equivalence checking algorithm.

Examples:

The following examples show two equivalent NFTs that are not recognized as such by the equivalence checking algorithm. Even the use of nft::remove_epsilon does not help, as it only removes epsilon transitions between zero-level states.

[vhavlena]

What do you mean by equivalence checking algorithm? The problem is afaik undecidable. Do you think about some approximations?

[Adda0]

You are right that the problem is undecidable for general transducers, but we can do:

1. Approximations for general transducers,
2. Checking equivalence for specific restricted transducer types where the problem becomes decidable, e.g., single-value (one input leads to at most one output) or functional transducers, etc.

[vhavlena]

Great! Sounds interesting. It could/should be connected with a detection whether a NFT is k-valued (or another relevant properties).