[Spot] Unambiguous refinements of collections of BDDs

Alexandre Duret-Lutz adl at lrde.epita.fr
Mon Aug 2 11:48:55 CEST 2021


Hi Michaël,

Michaël Cadilhac <michael at 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.)

*Alexandre Duret-Lutz*
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/x-org
Size: 1858 bytes
Desc: not available
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20210802/67c13879/attachment.bin>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lrde.epita.fr/pipermail/spot/attachments/20210802/67c13879/attachment.htm>


More information about the Spot mailing list