Hi Yoav,
Yoav Ben Shimon yoavbenshimon@gmail.com writes:
I use the following command (LTL_FORMULA here is already translated via syfco to the required syntax): ltl2tgba -D -B -H -x sat-minimize -f LTL_FORMULA | autfilt --is-deterministic
Hum... I don't think that running
ltl2tgba -DB -x sat-minimize φ
will always give you a DBA if one exists.
I'm sure that -DB alone does not. (Since -D expresses only a preference, it's never clear when ltl2tgba to spend additional time looking for a DBA that might not exist. Maybe we need another switch.)
Adding '-x sat-minimize' will activate an extra determinization procedure based on powerset. Basically, it builds a powerset of the NBA, and attempt to determine the accepting transitions of the powerset by looking at the cycles of the NBA. See section 3.2 of "Mechanizing the Powerset Construction for Restricted Classes of ω-Automata" by Dax, Eisinger, & Klaedtke. The state-based version of this algorithm only works for a subset of recurrence formulas, and I _believe_ the transition-based version (that we do) only works with a larger subset. Additionally, because that determinization code is currently based on a cycle enumeration, it will also abort in presence of too many cycles.
I suspect this old code for attempting deterimization was written before we had a Safra-like determinization in Spot, and the code path for -x sat-minimize could now be improved. (Even enumerating cycles in the NBA to fix the acceptance of Powerset(NBA) sounds crazy to me — why aren't we looking at the product of these two?)
My aim is to fail if the result is not deterministic, since a minimal DBA is a requirement for the correctness of DBW2GR1. I'll be happy if you have any advice, especially on the use of sat-minimize: are there any parameters I should alter to get the best possible results from the sat solver? (I am aware that inherently some inputs will be difficult.) Is there any quicker way to tell if a translation to DBA is possible, perhaps separately from the minimization procedure?
I think https://spot.lre.epita.fr/hierarchy.html#org9007bec is what you want:
First, request a DPA.
ltl2tgba -DP φ
the output will always be deterministic, and it will use the minimal number of colors for that language. For any recurrence formula, the produced DPA should have an acceptance of: f, t, or Inf(0). So accept for f and t, it's already a DBA. If you Get any other acceptance, you can abort your procedure here, as no DBA exist.
Then force convert your automaton into a DBA and minimize it:
ltl2tgba -DP φ | autfilt -DB --sat-minimize
Alternatively, you can also check whether a DBA exists for φ by just checking the output of:
ltlfilt -c --recurrence -f φ
If the answer is not syntactically obvious, that will just construct the above DPA and check its acceptance condition under the hood.
Best regards, Alexandre