alternate encoding options for HOA labels
Currently the Boolean functions that label ω-automata are stored as BDDs, but when printed in the HOA or Dot formats, they are printed as irredundant sums of products. When an automaton uses a lot of atomic propositions, those ISOPs can be very large. @pierreganty has an example automaton with 19 atomic propositions and 200 edges that takes 200MB in HOA.
We should investigate other encoding options, both to shorten the HOA files, but also to shorten the displayed labels when the automaton is rendered via the Dot format. Some ideas:
- attempt to use CNF
- attempt to use if-then-else form to match the BDD encoding. We thought about adding a
ite
operator in HOA but never did it. Currently we have to rewriteite(a,b,c)
as(a&b)|(!a&c)
so this might not be very effective. - in a DNF/CNF output, attempt to factorize multiple clauses (e.g.,
a&b&c&d | b&c&d&e
→b&c&d&(a|e)
) - attempt all the above, recursively
I have found some related approach in DOI:10.1109/iscas.2000.856325.
Another idea is to leverage the Alias:
headers of HOA and create one alias per BDD node is that appear more than once in the set of labels of the automaton. That won't help the Dot output.