potential determinization improvement
The following example shows two equivalent input automata that differ only by the label of the transition between 0 and 1:
Here are the two automata:
b, c = spot.automata("""HOA: v1
States: 4 Start: 0 AP: 3 "c" "a" "b"
acc-name: Buchi Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0 [t] 0 [0|2] 1 [1] 2
State: 1 [!2] 1 [0&2] 1 {0} [!0&2] 3
State: 2 [!0&1] 2 [0&1] 2 {0}
State: 3 [0] 1 {0} [!0] 3
--END--
HOA: v1 States: 4 Start: 0 AP: 3 "c" "a" "b"
acc-name: Buchi Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc stutter-invariant
--BODY--
State: 0 [t] 0 [t] 1 [1] 2
State: 1 [!2] 1 [0&2] 1 {0} [!0&2] 3
State: 2 [!0&1] 2 [0&1] 2 {0}
State: 3 [0] 1 {0} [!0] 3
--END--""");
When determinizing these automata, the left automaton (b) produces an output larger than the right one (c).
This situation is adapted from a an actual case where I noticed that disabling simulation-based reduction would improve the determinized output.
% genltl --ms-phi-s=1 | bin/ltl2tgba -P -D -x simul=1 --stats=%s
7
% genltl --ms-phi-s=1 | bin/ltl2tgba -P -D -x simul=0 --stats=%s
4
What happening is that the simulation-based reduction prunes some unnecessary transitions of in the translation of the formula, remove some unnecessary transitions, leaving only b|c
in this case, while the input original translation had translations labeled by b&c
, b
, c
, and 1
.
I'm wondering if this could be improved during the determinization, maybe knowing that we are talking about a stutter-invariant property. Here the label of the transition 0→2 can also be replaced by True, resulting in a 4-state DPA output where the initial states has no loop:
Here it would be nice to detect that we can actually start the determinization in state [0]{₀[1]₀}{₁[2]₁}
or maybe even in state {₀[1]₀}{₁[2]₁}
(ignoring [0]
). Under what conditions are we allowed to do that?