Assume that the specification has the shape ψ = ψ₁ ∧ ψ₂ where ψ₁ and ψ₂ are output-disjoint specifications (i.e., they do not share any output). In LTL synthesis, you'd find a controller for ψ₁, and then a controller for ψ₂, and you would then combine the two controllers by simply putting them side by side. Easy peasy. As written in the [CIAA'25 paper](https://www.lrde.epita.fr/~adl/dl/duret.25.ciaa.pdf), I did the same with LTLf, only to realize yesterday that it is incorrect in this context. Because we are not working with infinite traces anymore, the two controllers should also agree on the size of the traces they accept! As an example, consider ψ₁ = X[!]X[!]X(0) (= the trace should have length three), and ψ₂ = X[!]X(0) (= length two). Specification ψ₁ and ψ₂ are realizable separately, but ψ₁ ∧ ψ₂ is clearly NOT realizable. ``` % ltlfsynt -f 'X[!]X[!]X(0) && X[!]X(0)' --verbose --real using Mealy semantics there are 2 subformulas working on subformula X[!]X(0) starting on-the-fly translation with node-based backpropagation, with BFS order, with one-step preprocess translation to MTDFA (1 roots, 0 APs) took 0.00146946 seconds MTDFA game was solved during translation working on subformula X[!]X[!]X(0) starting on-the-fly translation with node-based backpropagation, with BFS order, with one-step preprocess translation to MTDFA (1 roots, 0 APs) took 0.000966759 seconds MTDFA game was solved during translation REALIZABLE % ltlfsynt -f 'X[!]X[!]X(0) && X[!]X(0)' --verbose --real --decomp=no using Mealy semantics formula simplified to X[!](X(0) & X[!]X(0)) starting on-the-fly translation with node-based backpropagation, with BFS order, with one-step preprocess translation to MTDFA (1 roots, 0 APs) took 0.0016126 seconds MTDFA game was solved during translation UNREALIZABLE ``` I can see how to fix that in an approach that is _not_ on-the-fly: 1. build two MTDFAs A₁ and A₂ for ψ₁ and ψ₂ 2. if one of those MTDFAs is not realizable, the conjunct is not realizable 3. else combine the two MTDFAs before checking for realizability again This makes perfect sense in an approach using compositional translation. The sub-specifications do not even have to be output-disjoint anymore. This could also use Cosy's trick where, before combination, the Aᵢs are simplified by removing the parts that are surely losing. (Cosy is described in a paper by Shufang Zhu et al. to appear at ECAI'25.) But what about an on-the-fly setting? Step 1 & 2 can still be done, but then it looks very tricky to restart the on-the-fly construction of ψ₁∧ψ₂ from partial constructions for ψ₁ and ψ₂... Maybe we should instead find a way to characterize the formulas for which putting controllers side-by-side is OK. For instance if for each ψᵢ we can show that there exists some nᵢ such that L(ψᵢ) contains a word for any size ≥nᵢ, and additionally all Ψᵢ are output-disjoint, then is it ok? The benchmark I ran for the CIAA'25 paper includes some configurations with decomposition disabled. So I know that all results that where successfully computed with and without decomposition are in agreement, and it is likely that the SyntComp benchmark does not have tricky formulas that would highlight the issue. Nonetheless, the incorrect optimization helps us solve a significant additional number of cases, as highlighted in red bellow. Compare `ltlfsynt:bfs-os-nodec` with `ltlfsynt:bfs-os`.   In case we fail to make the decomposition work for on-the-fly approach, it is possible that using it in full/compositional approaches (with the fix where the automata have to be recombined) will make the result more efficient that the on-the-fly settings.