Document Open Access Logo

Giving Instructions in Linear Temporal Logic

Authors Julian Gutierrez , Sarit Kraus , Giuseppe Perelli , Michael Wooldridge

PDF
Thumbnail PDF

File

LIPIcs.TIME.2022.15.pdf
  • Filesize: 0.76 MB
  • 14 pages

Document Identifiers

Author Details

Julian Gutierrez
  • Monash University, Melbourne, Australia
Sarit Kraus
  • Bar-Ilan University, Ramat-Gan, Israel
Giuseppe Perelli
  • Sapienza University of Rome, Italy
Michael Wooldridge
  • University of Oxford, UK

Funding

  • Perelli, Giuseppe: Giuseppe Perelli is partially supported by the ERC Advanced Grant WhiteMech (No. 834228), by the EU ICT-48 2020 project TAILOR (No. 952215), and by the Sapienza University project "BeGood" (No. AR22117A2DC7CD60).
  • Wooldridge, Michael: Michael Wooldridge was supported by the UKRI under grant (grant EP/ W002949/1).

Cite AsGet BibTex

Julian Gutierrez, Sarit Kraus, Giuseppe Perelli, and Michael Wooldridge. Giving Instructions in Linear Temporal Logic. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TIME.2022.15

Abstract

Our aim is to develop a formal semantics for giving instructions to taskable agents, to investigate the complexity of decision problems relating to these semantics, and to explore the issues that these semantics raise. In the setting we consider, agents are given instructions in the form of Linear Temporal Logic (LTL) formulae; the intuitive interpretation of such an instruction is that the agent should act in such a way as to ensure the formula is satisfied. At the same time, agents are assumed to have inviolable and immutable background safety requirements, also specified as LTL formulae. Finally, the actions performed by an agent are assumed to have costs, and agents must act within a limited budget. For this setting, we present a range of interpretations of an instruction to achieve an LTL task Υ, intuitively ranging from "try to do this but only if you can do so with everything else remaining unchanged" up to "drop everything and get this done." For each case we present a formal pre-/post-condition semantics, and investigate the computational issues that they raise.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automated reasoning
Keywords
  • Linear Temporal Logic
  • Synthesis
  • Game theory
  • Multi-Agent Systems

Metrics

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

References

  1. Jacob Andreas, Dan Klein, and Sergey Levine. Modular multitask reinforcement learning with policy sketches. In Doina Precup and Yee Whye Teh, editors, ICML, volume 70 of Proceedings of Machine Learning Research, pages 166-175. PMLR, 2017. URL: http://proceedings.mlr.press/v70/andreas17a.html.
  2. Alexandre Antunes, Lorenzo Jamone, Giovanni Saponaro, Alexandre Bernardino, and Rodrigo Ventura. From human instructions to robot actions: Formulation of goals, affordances and probabilistic planning. In 2016 IEEE International Conference on Robotics and Automation (ICRA), pages 5449-5454. IEEE, 2016. Google Scholar
  3. D. E. Appelt. Planning English Sentences. Cambridge University Press: Cambridge, England, 1985. Google Scholar
  4. J. L. Austin. How to Do Things With Words. Oxford University Press: Oxford, England, 1962. Google Scholar
  5. Fahiem Bacchus and Froduald Kabanza. Using temporal logics to express search control knowledge for planning. Artif. Intell., 116(1-2):123-191, 2000. URL: https://doi.org/10.1016/S0004-3702(99)00071-5.
  6. K. Binmore. Fun and Games: A Text on Game Theory. D. C. Heath and Company: Lexington, MA, 1992. Google Scholar
  7. Adrian Boteanu, Thomas Howard, Jacob Arkin, and Hadas Kress-Gazit. A model for verifiable grounding and execution of complex natural language instructions. In 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 2649-2654. IEEE, 2016. Google Scholar
  8. P. R. Cohen and C. R. Perrault. Elements of a plan based theory of speech acts. Cognitive Science, 3:177-212, 1979. Google Scholar
  9. E. A. Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pages 996-1072. Elsevier, 1990. Google Scholar
  10. FIPA. The foundation for intelligent physical agents, 2001. See URL: http://www.fipa.org/.
  11. Dana Fisman, Orna Kupferman, and Yoad Lustig. Rational synthesis. In TACAS, volume 6015 of LNCS, pages 190-204. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12002-2_16.
  12. John Grant, Sarit Kraus, Michael John Wooldridge, and Inon Zuckerman. Manipulating boolean games through communication. In Twenty-Second International Joint Conference on Artificial Intelligence, 2011. Google Scholar
  13. J. Gutierrez, P. Harrenstein, and M. Wooldridge. Iterated Boolean games. Information and Computation, 242:53-79, 2015. Google Scholar
  14. Julian Gutierrez, Aniello Murano, Giuseppe Perelli, Sasha Rubin, Thomas Steeples, and Michael Wooldridge. Equilibria for games with combined qualitative and quantitative objectives. Acta Informatica, pages 1-26, 2020. Google Scholar
  15. Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell., 287:103353, 2020. URL: https://doi.org/10.1016/j.artint.2020.103353.
  16. Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIlraith. Teaching multiple tasks to an RL agent using LTL. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018, pages 452-461. International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM, 2018. Google Scholar
  17. Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIlraith. Teaching multiple tasks to an RL agent using LTL. In Elisabeth André, Sven Koenig, Mehdi Dastani, and Gita Sukthankar, editors, AAMAS, pages 452-461. IFAAMAS, Richland, SC, USA / ACM, 2018. URL: http://dl.acm.org/citation.cfm?id=3237452.
  18. León Illanes, Xi Yan, Rodrigo Toro Icarte, and Sheila A McIlraith. Symbolic plans as high-level instructions for reinforcement learning. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 30, pages 540-550, 2020. Google Scholar
  19. Pat Langley, Nishant Trivedi, and Matt Banister. A command language for taskable virtual agents. In G. Michael Youngblood and Vadim Bulitko, editors, Proceedings of the Sixth AAAI Conference on Artificial Intelligence and Interactive Digital Entertainment, AIIDE 2010, October 11-13, 2010, Stanford, California, USA. The AAAI Press, 2010. URL: http://aaai.org/ocs/index.php/AIIDE/AIIDE10/paper/view/2153.
  20. S. C. Levinson. Pragmatics. Cambridge University Press: Cambridge, England, 1983. Google Scholar
  21. Nicolas Markey and Philippe Schnoebelen. Model checking a path. In Roberto M. Amadio and Denis Lugiez, editors, CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings, volume 2761 of Lecture Notes in Computer Science, pages 248-262. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45187-7_17.
  22. Pedro Henrique Martins, Luís Custódio, and Rodrigo Ventura. A deep learning approach for understanding natural language commands for mobile service robots. arXiv preprint, 2018. URL: http://arxiv.org/abs/1807.03053.
  23. J. Mayfield, Y. Labrou, and T. Finin. Evaluating KQML as an agent communication language. In M. Wooldridge, J. P. Müller, and M. Tambe, editors, Intelligent Agents II (LNAI Volume 1037), pages 347-360. Springer-Verlag: Berlin, Germany, 1996. Google Scholar
  24. Dipendra K Misra, Jaeyong Sung, Kevin Lee, and Ashutosh Saxena. Tell me dave: Context-sensitive grounding of natural language to manipulation instructions. The International Journal of Robotics Research, 35(1-3):281-300, 2016. Google Scholar
  25. A. Pnueli. The temporal logic of programs. In Proceedings of the Eighteenth IEEE Symposium on the Foundations of Computer Science (FOCS'77), pages 46-57. The Society, 1977. Google Scholar
  26. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of the Sixteenth ACM Symposium on the Principles of Programming Languages (POPL), pages 179-190, January 1989. Google Scholar
  27. A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programs (ICALP'89), pages 652-671, 1989. Google Scholar
  28. Pradip Pramanick, Hrishav Bakul Barua, and Chayan Sarkar. Decomplex: Task planning from complex natural instructions by a collocating robot. In 2020 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pages 6894-6901. IEEE, 2021. Google Scholar
  29. Vasumathi Raman, Constantine Lignos, Cameron Finucane, Kenton CT Lee, Mitchell P Marcus, and Hadas Kress-Gazit. Sorry dave, i'm afraid i can't do that: Explaining unachievable robot tasks using natural language. In Robotics: Science and Systems, volume 2, pages 2-1. Citeseer, 2013. Google Scholar
  30. J. R. Searle. Speech Acts: An Essay in the Philosophy of Language. Cambridge University Press: Cambridge, England, 1969. Google Scholar
  31. A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. Google Scholar
  32. A. Prasad Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects Comput., 6(5):495-512, 1994. URL: https://doi.org/10.1007/BF01211865.
  33. Stefanie Tellex, Nakul Gopalan, Hadas Kress-Gazit, and Cynthia Matuszek. Robots that use language. Annual Review of Control, Robotics, and Autonomous Systems, 3:25-55, 2020. Google Scholar
  34. Rodrigo Toro Icarte, Toryn Q Klassen, Richard Valenzano, and Sheila A McIlraith. Teaching multiple tasks to an rl agent using ltl. In Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, pages 452-461, 2018. Google Scholar
  35. Michael Wooldridge, Ulle Endriss, Sarit Kraus, and Jérôme Lang. Incentive engineering for boolean games. Artificial Intelligence, 195:418-439, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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