Hi Michaël,

Michaël Cadilhac <michael@cadilhac.name> writes:

In BDDs, my use case is to have C be a collection of BDDs and a BDD represent the set of its satisfying assignments.

Building an unambiguous refinement of BDDs seems an essential step in determinization: If I have a state with two outgoing transitions labeled with BDDs {F, G} such that F&G is not False, then this state is nondeterministic.  To determinize it, we will have to consider the transition labels {F&G, F&!G, !F&G}.  Note that this set refines {F, G}, since F = (F&G)|(F&!G) and similarly for G.

Yes. Unfortunately, Spot's determinization is not smart in that regard. It simply decomposes everything over the 2^AP possible minterms, and then merge the parallel edges that can be merged in the resulting automaton. As an optimization, we simply reduce AP to what's needed locally while computing successors.

If the entire set of labels of an automaton was globally decomposed as you suggest, and the automaton rewritten to use only elements of the optimal partition, then Spot's determinization would be indeed more efficient, and we would still be able to apply our optimization for stutter-invariant inputs. (That optimization requires repeatedly moving forward with the same label, so that preclude doing some "local" decomposition while computing some successors.)

I implemented it in a few different ways and would be interested in alternative implementations.

Maybe there are some in https://www.lrde.epita.fr/dload/papers/newton.17.dtd.report.pdf (disclaimer: I've only read the first two pages.)