2
$\begingroup$

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).

enter image description here

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?

Improve this question
$\endgroup$
0

2 Answers 2

Reset to default
0
$\begingroup$

The obvious naive approach is to enumerate all $n!$ permutations, and for each, check whether it meets the LTL spec. The latter check can be done in a standard way. So, the running time of this naive approach is approximately $\Theta(n!)$.

In the worst case, any algorithm might need to take at least this much time. For instance, if the LTL spec allows all schedules, then you'll have to output all $n!$ permutations, so it takes $\Omega(n!)$ time even just to write them down on the output.

You could ask for an output-sensitive algorithm: e.g., one whose running time is $O(k \text{poly}(n))$, where $k$ is the number of legal schedules that meet the LTL spec. Unfortunately, even this does not appear to be achievable in the worst case, as the problem is NP-hard. In particular, even checking whether there exists a legal schedule is NP-hard, by reduction from Hamiltonian cycle. In particular, given a graph $G$ on $n$ vertices, treat each vertex as a task; you can construct a LTL spec that captures the requirement that the sequence of tasks form a valid path through the graph; and then there exists a valid schedule (permutation of the tasks that meets the LTL spec) iff the graph has a Hamiltonian cycle. So, if we could detect the existence of a legal schedule, we could solve the Hamiltonian cycle problem, which is NP-hard. Obviously, enumerating all legal schedules is at least as hard as detecting whether any legal schedule exists.

These hardness results imply that there is no algorithm that will be efficient in all cases. You'll have to settle for an algorithm that is sometimes efficient, or a heuristic.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Could you give a brief explanation as to how to check if a task sequence satisfies LTL spec in linear or polynomial time in the number of tasks? $\endgroup$
    – user_1_1_1
    Jul 25, 2018 at 21:35
  • $\begingroup$ @user_1_1_1, checking whether a specific string satisfies a LTL spec (or, equivalently, checking whether a string is accepted by a particular Buchi automaton) is a standard task and any good model checking textbook should describe how to do that. I suggest doing some research, and if you still can't find any resource that describes it, ask a new question and show what research you've done. $\endgroup$
    – D.W. ♦
    Jul 25, 2018 at 21:40
2
$\begingroup$

I would interpret your problem as follows:

Given a non-deterministic Büchi automaton representing some language $L$, you want to enumerate all shortest good prefixes of $L$ such that in every character of the good prefix, only at most one atomic proposition has a $\mathbf{true}$ value.

A good prefix of $L$ is a finite word such that every infinite extension of it is in $L$. I call a good prefix a shortest good prefix if and only if every prefix of the prefix is not a good prefix. A schedule is typically finite even though LTL and Büchi automaton "talk" about infinite executions. Hence this interpretation of your problem.

Note that this is actually a difficult problem -- take for example two Buchi automata for the languages []<>p and <>[]!p -- you can take their disjunction by merging the state sets and having two initial states. You do not see syntactically that every word is a good prefix.

The best way to enumerate good prefixes would thus be to construct a deterministic automaton over infinite words, such as a deterministic Rabin automaton, and enumerating all paths to a strongly connected component in which every state represents the universal language.

Enumerating the paths can be done by a simple depth first search, where you do not abort the search after you found a path to a state with the universal language. Whenever you found a path to such a component, you print it out, and return to the next recursive step. Along the way, you ignore characters with more than one proposition set.

Now in practice, you may have a good luck using LTL-to-Buchi converters. They typically do not guarantee that they find all simplifications of the LTL formula, but enumerating paths to accepting states may do the trick. Note that for non-deterministic automata, you can get duplicate schedules. If you use modern tools for LTL-to-deterministic-automaton translation (such as Rabinizer), they should also make sure that states belowing to a strongly connected component for the universal language are self-looping on all characters, which makes them easy to detect. But I don't think they guarantee this.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Your answer is very helpful but it is general and abstract so difficult for a non-expert to make immediate use of it. Could you take the problem above involving tasks A and B and then using Rabin automata or any other of your liking, show the exact numerical steps briefly? Specifically, could you give the graph over which if I am doing DFS I get the path A->B $\endgroup$
    – user_1_1_1
    Jul 24, 2018 at 19:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.