Towards a Parallel Search Engine for Planning Systems Based on Linear Time Logic

A planning problem can be entirely encoded as a set of linear temporal logic (LTL) formulae, in such a way that planning is reduced to model search. In order for this approach to be effective, it is important to enhance the performances of LTL provers. In this work, we study a parallel algorithm for LTL model search, based on the tableaux calculus. In paritcular, the approach presented here is based on the “divide et impera” approach: a task in tableaux construction is identified that can be split into smaller homogeneous processes. The parallelization acts during the construction of each time state: the set of formulas to be expanded is split into k disjoint subsets (where k is the number of processes), the k tableaux expansions are carried out in parallel, and the k results are suitably combined. First promising experimental results are also presented: they are based on the algorithm implementation on a cluster of non homogeneous machines.