How to graph search a LTL-generated Buchi automaton to generate valid execution paths

Question

I have a set of tasks, and a LTL specification that describes which orders of the tasks are legal. I want to find a way to enumerate all permutations of the tasks that meet the specification.

For example, suppose there are two tasks, A and B, and the LTL spec <>(A&<>B) is. This spec says that A should eventually be done and after A eventually B should be done. In this case, there is only one legal sequence: (A,B).

We can convert the LTL formula to a Buchi automaton, as shown above. Then since this example is so trivial, it is easy to see that the only legal sequence is A-->B.

But what if we had a more complex LTL formula? How could we enumerate all legal sequences (permutations) of the tasks that satisfy the spec? Is there an efficient algorithm to do this?