I like the compositional approach, particularly considering that a lot of the non-reactive correct-by-construction stuff supports some sort of modularity. Many of the more practical heuristics for model checking take advantage of an iterative approach that seems something like the dual of compositional program synthesis.

But to answer your question more directly, I haven’t seen any (real) specifications at all, much less specifications of that form.

One important contribution of this paper is the extension to generalized Buechi automata as inputs while avoiding the counting construction. This improves the complexity.

You can argue about the usefulness of the compositional approach. Who has ever seen a specification in the form f1 /\ … /\ fn?