Algorithms to synthesize optimal plans satisfying temporal logic constraints 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:


this task can begin after this task
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.
Maybe take a look at http://www.syntcomp.org/

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