X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism
Linear temporal logic (LTL) provides expressive means to specify temporally extended goals as well as preferences. Recent research has focussed on compilation techniques, i.e., methods to alter the domain ensuring that every solution adheres to the temporally extended goals. This requires either new...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Asociación Española para la Inteligencia Artificial
2018-09-01
|
| Series: | Inteligencia Artificial |
| Subjects: | |
| Online Access: | https://journal.iberamia.org/index.php/intartif/article/view/226 |
| _version_ | 1828947847479820288 |
|---|---|
| author | Gregor Behnke Susanne Biundo |
| author_facet | Gregor Behnke Susanne Biundo |
| author_sort | Gregor Behnke |
| collection | DOAJ |
| description | Linear temporal logic (LTL) provides expressive means to specify temporally extended goals as well as preferences.
Recent research has focussed on compilation techniques, i.e., methods to alter the domain ensuring that every solution adheres to the temporally extended goals.
This requires either new actions or an construction that is exponential in the size of the formula.
A translation into boolean satisfiability (SAT) on the other hand requires neither.
So far only one such encoding exists, which is based on the parallel $\exists$-step encoding for classical planning.
We show a connection between it and recently developed compilation techniques for LTL, which may be exploited in the future.
The major drawback of the encoding is that it is limited to LTL without the X operator.
We show how to integrate X and describe two new encodings, which allow for more parallelism than the original encoding.
An empirical evaluation shows that the new encodings outperform the current state-of-the-art encoding. |
| first_indexed | 2024-12-14T05:36:49Z |
| format | Article |
| id | doaj.art-a7d6b9f1f3ca4ffc9d5da89b2b0b5f61 |
| institution | Directory Open Access Journal |
| issn | 1137-3601 1988-3064 |
| language | English |
| last_indexed | 2024-12-14T05:36:49Z |
| publishDate | 2018-09-01 |
| publisher | Asociación Española para la Inteligencia Artificial |
| record_format | Article |
| series | Inteligencia Artificial |
| spelling | doaj.art-a7d6b9f1f3ca4ffc9d5da89b2b0b5f612022-12-21T23:15:09ZengAsociación Española para la Inteligencia ArtificialInteligencia Artificial1137-36011988-30642018-09-01216210.4114/intartif.vol21iss62pp75-90226X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more ParallelismGregor Behnke0Susanne Biundo1Ulm UniversityUlm UniversityLinear temporal logic (LTL) provides expressive means to specify temporally extended goals as well as preferences. Recent research has focussed on compilation techniques, i.e., methods to alter the domain ensuring that every solution adheres to the temporally extended goals. This requires either new actions or an construction that is exponential in the size of the formula. A translation into boolean satisfiability (SAT) on the other hand requires neither. So far only one such encoding exists, which is based on the parallel $\exists$-step encoding for classical planning. We show a connection between it and recently developed compilation techniques for LTL, which may be exploited in the future. The major drawback of the encoding is that it is limited to LTL without the X operator. We show how to integrate X and describe two new encodings, which allow for more parallelism than the original encoding. An empirical evaluation shows that the new encodings outperform the current state-of-the-art encoding.https://journal.iberamia.org/index.php/intartif/article/view/226Temporally Extended GoalsPlanning as SATLinear Temporal Logic |
| spellingShingle | Gregor Behnke Susanne Biundo X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism Inteligencia Artificial Temporally Extended Goals Planning as SAT Linear Temporal Logic |
| title | X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism |
| title_full | X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism |
| title_fullStr | X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism |
| title_full_unstemmed | X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism |
| title_short | X and more Parallelism. Integrating LTL-Next into SAT-based Planning with Trajectory Constraints while Allowing for even more Parallelism |
| title_sort | x and more parallelism integrating ltl next into sat based planning with trajectory constraints while allowing for even more parallelism |
| topic | Temporally Extended Goals Planning as SAT Linear Temporal Logic |
| url | https://journal.iberamia.org/index.php/intartif/article/view/226 |
| work_keys_str_mv | AT gregorbehnke xandmoreparallelismintegratingltlnextintosatbasedplanningwithtrajectoryconstraintswhileallowingforevenmoreparallelism AT susannebiundo xandmoreparallelismintegratingltlnextintosatbasedplanningwithtrajectoryconstraintswhileallowingforevenmoreparallelism |