<p>Maybe take a look at <a href="http://www.syntcomp.org/" rel="nofollow noreferrer">http://www.syntcomp.org/</a></p>

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

CC BY-SA 3.0
2017-04-25T13:05:45.247Z
2017-04-25T13:05:45.247Z
Markus
<p>It might be worthwhile to check out (PPDL-like) planning using temporal goals. Given a current <strong>world/state</strong>, a bunch of world/state-modifying <strong>actions</strong>, and a <strong>goal</strong> formula (with temporal constraints), such a planner will expand the search space using the actions, until a satisfying world/state is found.</p>

<p>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 <a href="http://solver.planning.domains/" rel="nofollow noreferrer">http://solver.planning.domains/</a> for an example of such a planner or <a href="https://en.wikipedia.org/wiki/Planning_Domain_Definition_Language" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Planning_Domain_Definition_Language</a> for a more generic overview on PDDL - the de facto standard planning language in this domain).</p>

CC BY-SA 3.0
2018-02-10T09:28:42.680Z
2018-02-10T09:28:42.680Z
nondeterministic
<p>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. </p>

<p>I am concerned with specific types of temporal logic constraints such as:</p>

<ol>
<li>this task can begin after this task</li>
<li>this task can happen only in this time interval</li>
</ol>

<p>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.?</p>

<p>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.</p>

<lo.logic><automata-theory><concurrency><model-checking><temporal-logic>
Algorithms to synthesize optimal plans satisfying temporal logic constraints
user_1_1_1
# Algorithms to synthesize optimal plans satisfying temporal logic constraints

(Asked by: username_0 on 2017-04-25)

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.

**Tags:** lo.logic, automata-theory, concurrency, model-checking, temporal-logic

---

## 2 answers

### Answer by username_1 on 2017-04-25. Score: 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 by username_2 on 2018-02-10. Score: 0

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


---

