Error in the product construction / word inclusion of Rabin automata
Hi,
I observed the following problem with ltlcross. This report may get a bit lengthy, so let me first explain what I did to produce the error / what datapoints I can provide and then write down my assumptions of what is happening. Most of the former is probably not actually relevant, I'm including it for completeness.
Initial Findings
I'm one of the developers of Rabinizer / owl. We received a bug report for a particular formula a & GF ((a | b) & (Ga | !GFa))
. Here, ltlcross reported an error for Rabinizer + Degeneralization, as follows.
Invocation:
ltlcross -t "build/bin/ltl2dra -i $f > %O" -f 'a & GF ((a | b) & (Ga | FG!a))'
Output:
error: P0*N0 is nonempty; both automata accept the infinite word:
a; cycle{!a & !b}
Automata (as reported by ltlcross --automata --json=output.json
)
Positive:
HOA: v1
name: "Automaton for [{<<(a & ((((a & Ga) | FGa) & (((a | Fa) & GFa) | ((b | Fb) & GFb))) | (((!a & G!a) | FG!a) & (((a | Fa) & GFa) | ((b | Fb) & GFb)))))>>}]"
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Rabin 3
Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5))
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0 "{<<(a & ((((a & Ga) | FGa) & (((a | Fa) & GFa) | ((b | Fb) & GFb))) | (((!a & G!a) | FG!a) & (((a | Fa) & GFa) | ((b | Fb) & GFb)))))>>}"
[0] 1
State: 1 "{<<((((a & Ga) | FGa) & (((a | Fa) & GFa) | ((b | Fb) & GFb))) | (((!a & G!a) | FG!a) & (((a | Fa) & GFa) | ((b | Fb) & GFb))))::[a]::[(b | Fb)]::[(a | Fa)]::[!a]>>|[0, 0]}"
[!0&!1] 1 {0 4}
[!0&1] 1 {0 3 4}
[0&!1] 1 {2 5}
[0&1] 1 {1 2 5}
--END--
Negative:
HOA: v1
name: "Automaton for [{<<(!a | ((((!a | F!a) & GF!a) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b))) & (((a | Fa) & GFa) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b)))))>>}]"
States: 4
Start: 0
AP: 2 "a" "b"
acc-name: Rabin 2
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0 "{<<(!a | ((((!a | F!a) & GF!a) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b))) & (((a | Fa) & GFa) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b)))))>>}"
[!0] 1
[0] 2
State: 1 "{<<true>>|[0]}"
[t] 1 {3}
State: 2 "{<<((((!a | F!a) & GF!a) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b))) & (((a | Fa) & GFa) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b))))::[!b]::[(!a | F!a)]::[(a | Fa)]::[!a]>>|[1, 0]}"
[0] 3 {1 2}
[!0&1] 2 {2}
[!0&!1] 2 {3}
State: 3 "{<<((((!a | F!a) & GF!a) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b))) & (((a | Fa) & GFa) | (((!a & G!a) | FG!a) & ((!b & G!b) | FG!b))))::[!b]::[(!a | F!a)]::[(a | Fa)]::[!a]>>|[0, 0]}"
[0] 3 {2}
[!0&1] 2 {2}
[!0&!1] 2 {3}
--END--
Observe that the positive automaton does not contain a; cycle{!a & !b}
, the negative one does. Also, note that with ltlcross -t ltl2tgba --no-complement -t <rabinizer>
, no errors are reported.
Digging deeper
By removing simplifications, we could reproduce the issue on smaller automata. I assume that the actual input formula (a & GF(a & Ga)
) is irrelevant for the error.
Ltlcross yields:
error: Comp(N0)*Comp(P0) is nonempty; both automata accept the infinite word:
cycle{a; !a}
The following two automata are produced:
HOA: v1
name: "Automaton for [{<<(a & ((a & Ga) | FGa) & (a | Fa) & GFa)>>}]"
States: 4
Start: 0
AP: 1 "a"
acc-name: Rabin 3
Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0 "{<<(a & ((a & Ga) | FGa) & (a | Fa) & GFa)>>}"
[!0] 1
[0] 2
State: 1 "{<<false>>}"
[t] 1
State: 2 "{<<(((a & Ga) | FGa) & (a | Fa) & GFa)::[(a | Fa)]::[a]>>|[1]}"
[!0] 3 {4}
[0] 3 {5}
State: 3 "{<<(((a & Ga) | FGa) & (a | Fa) & GFa)::[(a | Fa)]::[a]>>|[0]}"
[!0] 3 {4}
[0] 2 {5}
--END--
HOA: v1
name: "Automaton for [{<<(!a | ((!a | F!a) & GF!a) | (!a & G!a) | FG!a)>>}]"
States: 4
Start: 0
AP: 1 "a"
acc-name: Rabin 4
Acceptance: 8 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5))
| (Fin(6) & Inf(7))
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0 "{<<(!a | ((!a | F!a) & GF!a) | (!a & G!a) | FG!a)>>}"
[!0] 1
[0] 2
State: 1 "{<<true>>|[0]}"
[t] 1 {7}
State: 2 "{<<(((!a | F!a) & GF!a) | (!a & G!a) | FG!a)::[(!a | F!a)]::[!a]>>|[0, 0, 0]}"
[!0] 3 {1 3 5}
[0] 2 {2 4}
State: 3 "{<<(((!a | F!a) & GF!a) | (!a & G!a) | FG!a)::[(!a | F!a)]::[!a]>>|[0, 0, 1]}"
[!0] 2 {1 3 5}
[0] 2 {2 4}
--END--
Automaton 2 does accept cycle{a; !a}
, so there seems to be something weird going on. Moreover, when we either don't degeneralize OR further convert to parity, no error is reported. The issue also seems to be sensitive to the order of states. When reordering the states, the counterexample reported looks slightly different (cycle{a; !a; !a}
).
Summary
Since both normal product and product of complements have false positives, I assume that the problem is within the product construction of Rabin automata. Since the error does not happen for semantically equivalent but smaller formulas, I assume that the error somehow is related to superfluous Rabin pairs not being handled correctly. Note that the automata are complete.