Algorithms to synthesize optimal plans satisfying temporal logic constraints

Question

I know how NuSMV can be applied on a model to check if certain temporal logic statements are satisfied, particularly LTL. I also know of the LTL to BA conversion routines available online.

I am concerned with specific types of temporal logic constraints such as:

1. this task can begin after this task
2. this task can happen only in this time interval

I think this falls in LTL, STL domain. I am mostly interested in generating motion and task plans based on temporal logic constraints. NuSMV only seems to check the validity of certain statements on a model. I am more interested in software tool or codes that can lead to optimal plan synthesis based on my specification of LTL etc.?

I know there are research papers that solve this problem. But i do not know the theory of LTL, BA, etc. in depth so it is difficult to understand what these papers are doing and then recreate the process. Can someone tell some seminal papers or simply written paper easy to understand that explain how to build such algorithms. Even relevant sections of book are useful. Most books on model checking solve the inverse that is given a model does it satisfy this LTL constraint? I am interested in creating a model that satisfies a given LTL, STL constraint etc.? This technology is lying around so if someone can even suggest me some source codes that tackle such problems that will be even more helpful. I am not keen on understanding the theory if possible and would be happy to use someone else's software to develop plans and test them.

Answer 1

Maybe take a look at http://www.syntcomp.org/

This is a competition of tools solving the LTL synthesis problem (and some related problems).

Answer 2

It might be worthwhile to check out (PPDL-like) planning using temporal goals. Given a current world/state, a bunch of world/state-modifying actions, and a goal formula (with temporal constraints), such a planner will expand the search space using the actions, until a satisfying world/state is found.

If you want optimality, look for all such plans and choose the shortest one, for example. However, bear in mind that the problem is PSpace-complete and therefore problematic when viewed as an optimisation problem as opposed to simply a decision problem (see also http://solver.planning.domains/ for an example of such a planner or https://en.wikipedia.org/wiki/Planning_Domain_Definition_Language for a more generic overview on PDDL - the de facto standard planning language in this domain).