Document Open Access Logo

PDDL to DFA: A Symbolic Transformation for Effective Reasoning

Authors Giuseppe De Giacomo , Antonio Di Stasio , Gianmarco Parretti

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2025.7.pdf
  • Filesize: 0.91 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Planning and scheduling
  • Theory of computation → Logic and verification
  • Computing methodologies → Symbolic and algebraic manipulation
Keywords
  • Fully Observable Nondeterministic Planning
  • Linear Temporal Logics on finite traces
  • Reactive Synthesis
  • DFA

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

ltl_f reactive synthesis under environment specifications, which concerns the automated generation of strategies enforcing logical specifications, has emerged as a powerful technique for developing autonomous AI systems. It shares many similarities with Fully Observable Nondeterministic (fond) planning. In particular, nondeterministic domains can be expressed as ltl_f environment specifications. However, this is not needed since nondeterministic domains can be transformed into deterministic finite-state automata (dfa) to be used directly in the synthesis process. In this paper, we present a practical symbolic technique for translating domains expressed in Planning Domain Definition Language (pddl) into dfas. The technique allows for the integration of the planning domain, reduced to dfa in a symbolic form, into current symbolic ltl_f synthesis tools. We implemented our technique in a new tool, pddl2dfa, and applied it to solve fond planning by using state-of-the-art reactive synthesis techniques in a tool called syft4fond. Our empirical results confirm the effectiveness of our approach.

Cite As Get BibTex

Giuseppe De Giacomo, Antonio Di Stasio, and Gianmarco Parretti. PDDL to DFA: A Symbolic Transformation for Effective Reasoning. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 7:1-7:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TIME.2025.7

Author Details

Giuseppe De Giacomo
  • University of Oxford, UK
Antonio Di Stasio
  • City St George’s, University of London, UK
Gianmarco Parretti
  • La Sapienza University of Rome, Italy

Supplementary Materials

References

  1. Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, and Sasha Rubin. Planning and synthesis under assumptions. CoRR, abs/1807.06777, 2018. URL: https://arxiv.org/abs/1807.06777.
  2. Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, and Sasha Rubin. Planning under LTL environment specifications. In ICAPS, pages 31-39, 2019. URL: https://ojs.aaai.org/index.php/ICAPS/article/view/3457.
  3. Benjamin Aminof, Giuseppe De Giacomo, Gianmarco Parretti, and Sasha Rubin. Effective approach to ltlf best-effort synthesis in multi-tier environments. In IJCAI, 2024. Google Scholar
  4. Benjamin Aminof, Giuseppe De Giacomo, and Sasha Rubin. Best-effort synthesis: Doing your best is not harder than giving up. In IJCAI, pages 1766-1772, 2021. URL: https://doi.org/10.24963/IJCAI.2021/243.
  5. Benjamin Aminof, Giuseppe De Giacomo, and Sasha Rubin. Reactive synthesis of dominant strategies. In AAAI, pages 6228-6235. AAAI Press, 2023. URL: https://doi.org/10.1609/AAAI.V37I5.25767.
  6. Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, and Sasha Rubin. Planning under LTL environment specifications. In ICAPS, pages 31-39. AAAI Press, 2019. URL: https://ojs.aaai.org/index.php/ICAPS/article/view/3457.
  7. Krzysztof R. Apt and Erich Grädel, editors. Lectures in Game Theory for Computer Scientists. Cambridge University Press, 2011. Google Scholar
  8. Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  9. Suguman Bansal, Giuseppe De Giacomo, Antonio Di Stasio, Yong Li, Moshe Y. Vardi, and Shufang Zhu. Compositional safety LTL synthesis. In VSTTE, volume 13800 of Lecture Notes in Computer Science, pages 1-19. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-25803-9_1.
  10. Suguman Bansal, Yong Li, Lucas M. Tabajara, and Moshe Y. Vardi. Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In AAAI, pages 9766-9774, 2020. URL: https://doi.org/10.1609/AAAI.V34I06.6528.
  11. Suguman Bansal, Yong Li, Lucas M. Tabajara, and Moshe Y. Vardi. Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In AAAI, pages 9766-9774, 2020. URL: https://doi.org/10.1609/AAAI.V34I06.6528.
  12. Avrim Blum and Merrick L. Furst. Fast planning through planning graph analysis. Artif. Intell., 90(1-2):281-300, 1997. URL: https://doi.org/10.1016/S0004-3702(96)00047-1.
  13. Randal E. Bryant. Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Comput. Surv., 24(3):293-318, 1992. URL: https://doi.org/10.1145/136035.136043.
  14. Alberto Camacho, Meghyn Bienvenu, and Sheila A. McIlraith. Finite LTL synthesis with environment assumptions and quality measures. In KR, pages 454-463. AAAI Press, 2018. URL: https://aaai.org/ocs/index.php/KR/KR18/paper/view/18072.
  15. Alberto Camacho, Meghyn Bienvenu, and Sheila A McIlraith. Towards a unified view of AI planning and reactive synthesis. In ICAPS, pages 58-67, 2019. URL: https://ojs.aaai.org/index.php/ICAPS/article/view/3460.
  16. Alonzo Church. Logic, arithmetic and automata. In Proc. International Congress of Mathematicians, 1963. Google Scholar
  17. Alessandro Cimatti, Marco Pistore, Marco Roveri, and Paolo Traverso. Weak, strong, and strong cyclic planning via symbolic model checking. Artificial Intelligence, 147:35-84, 2003. URL: https://doi.org/10.1016/S0004-3702(02)00374-0.
  18. Alessandro Cimatti, Marco Roveri, and Paolo Traverso. Strong Planning in Non-Deterministic Domains Via Model Checking. In AIPS, pages 36-43. AAAI, 1998. URL: http://www.aaai.org/Library/AIPS/1998/aips98-005.php.
  19. Giuseppe De Giacomo, Antonio Di Stasio, Francesco Fuggitti, and Sasha Rubin. Pure-past linear temporal and dynamic logic on finite traces. In IJCAI, pages 4959-4965, 2020. URL: https://doi.org/10.24963/IJCAI.2020/690.
  20. Giuseppe De Giacomo, Antonio Di Stasio, Moshe Y Vardi, and Shufang Zhu. Two-stage technique for LTL_f synthesis under LTL assumptions. In KR, pages 304-314, 2020. URL: https://doi.org/10.24963/KR.2020/31.
  21. Giuseppe De Giacomo and Marco Favorito. Compositional approach to translate LTL_f/LDL_f into deterministic finite automata. In ICAPS, pages 122-130, 2021. URL: https://ojs.aaai.org/index.php/ICAPS/article/view/15954.
  22. Giuseppe De Giacomo and Yves Lespérance. The nondeterministic situation calculus. In KR, pages 216-226, 2021. URL: https://doi.org/10.24963/KR.2021/21.
  23. Giuseppe De Giacomo, Gianmarco Parretti, and Shufang Zhu. LTL_f best-effort synthesis in nondeterministic planning domains. In ECAI, pages 533-540, 2023. URL: https://doi.org/10.3233/FAIA230313.
  24. Giuseppe De Giacomo, Gianmarco Parretti, and Shufang Zhu. Symbolic LTL_f best-effort synthesis. In EUMAS, pages 228-243, 2023. Google Scholar
  25. Giuseppe De Giacomo and Sasha Rubin. Automata-theoretic foundations of FOND planning for LTL_f and LDL_f goals. In IJCAI, pages 4729-4735, 2018. URL: https://doi.org/10.24963/IJCAI.2018/657.
  26. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI, pages 854-860, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
  27. Giuseppe De Giacomo and Moshe Y. Vardi. Synthesis for LTL and LDL on finite traces. In IJCAI, pages 1558-1564, 2015. URL: http://ijcai.org/Abstract/15/223.
  28. Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi. BDD-based Boolean functional synthesis. In CAV, pages 402-421, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_22.
  29. Hector Geffner and Blai Bonet. A Concise Introduction to Models and Methods for Automated Planning. Morgan & Claypool, 2013. Google Scholar
  30. Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, and Shufang Zhu. Finite-trace and generalized-reactivity specifications in temporal synthesis. Formal Methods Syst. Des., 61(2):139-163, 2022. URL: https://doi.org/10.1007/S10703-023-00413-2.
  31. Patrik Haslum, Nir Lipovetzky, Daniele Magazzeni, and Christian Muise. An Introduction to the Planning Domain Definition Language. Morgan & Claypool, 2019. Google Scholar
  32. Christian Muise, Sheila A McIlraith, and J Christopher Beck. Improved non-deterministic planning by exploiting state relevance. In ICAPS, 2012. Google Scholar
  33. Gianmarco Parretti. Syft4Fond. Software (visited on 2025-09-18). URL: https://github.com/GianmarcoDIAG/syft4fond
    full metadata available at: https://doi.org/10.4230/artifacts.24786
  34. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, pages 179-190, 1989. Google Scholar
  35. Amir Pnueli. The Temporal Logic of Programs. In FOCS, pages 46-57, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  36. Fabio Somenzi. CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder, 2016. Google Scholar
  37. Shufang Zhu and Marco Favorito. Lydiasyft: A compositional symbolic synthesis framework for ltl_f specifications. In TACAS 2025, pages 295-302, 2025. URL: https://doi.org/10.1007/978-3-031-90643-5_15.
  38. Shufang Zhu and Giuseppe De Giacomo. Act for your duties but maintain your rights. In KR, 2022. Google Scholar
  39. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. Symbolic LTL_f synthesis. In IJCAI, pages 1362-1369, 2017. URL: https://doi.org/10.24963/IJCAI.2017/189.
  40. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. Symbolic LTL_f synthesis. In IJCAI, pages 1362-1369, 2017. URL: https://doi.org/10.24963/IJCAI.2017/189.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact