Cited by 157Reinforcement Learning in Roboticssemigroups and automata theoryFormal Methods in Verification

LTL and Beyond: Formal Languages for Reward Function Specification in Reinforcement Learning

Open access
Camacho, Alberto, Toro Icarte, Rodrigo, Klassen, Toryn Q., Valenzano, Richard, McIlraith, Sheila A.·2019·Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence

Abstract

In Reinforcement Learning (RL), an agent is guided by the rewards it receives from the reward function. Unfortunately, it may take many interactions with the environment to learn from sparse rewards, and it can be challenging to specify reward functions that reflect complex reward-worthy behavior. We propose using reward machines (RMs), which are automata-based representations that expose reward function structure, as a normal form representation for reward functions. We show how specifications of reward in various formal languages, including LTL and other regular languages, can be automatically translated into RMs, easing the burden of complex reward function specification. We then show how the exposed structure of the reward function can be exploited by tailored q-learning algorithms and automated reward shaping techniques in order to improve the sample efficiency of reinforcement learning methods. Experiments show that these RM-tailored techniques significantly outperform state-of-the-art (deep) RL algorithms, solving problems that otherwise cannot reasonably be solved by existing approaches.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.24963/ijcai.2019/840

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • LTL is the natural choice for expressing instructions, goals and safety constraints in reinforcement learning and planning.

    “LTL is the natural choice for expressing instructions, goals and safety constraints in reinforcement learning and planning (Camacho et al., 2019).”

    From General agents contain world models (2025) · cites this paper as Camacho et al., 2019

    The Introduction explicitly says that no single specification language is compelling across the diversity of reinforcement-learning applications and reward structures, pointing also to the diversity of goal languages in planning. Section 5.1 shows that LTL can express temporally extended behavior, including safety properties, but does not present it as the natural choice over other languages. (LLM, conf=0.86)

    Checked by a reasoning model — may be wrong.

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

No references could be resolved yet.

Research works printed but not linked: 30

  1. Jacob Andreas, Dan Klein, and Sergey Levine. Modular multitask reinforcement learning with pol- icy sketches. In ICML, pages 166-175, 2017.
  2. Bacchus et al., 1996] Fahiem Bacchus, Craig Boutilier, and Adam J. Grove. Rewarding behaviors. In AAAI, pages 1160- 1167, 1996.
  3. Bacchus et al., 1997] Fahiem Bacchus, Craig Boutilier, and Adam J. Grove. Structured solution methods for non- Markovian decision processes. In AAAI, pages 112-117, 1997.
  4. Jorge A. Baier and Sheila A. McIl- raith. Planning with temporally extended goals using heuristic search. In ICAPS, pages 342-345, 2006.
  5. Jorge A. Baier, Christian Fritz, and Sheila A. McIlraith. Exploiting procedural domain control knowledge in state-of-the-art planners. In ICAPS, pages 26- 33, 2007.
  6. Jorge A. Baier, Christian Fritz, Meghyn Bi- envenu, and Sheila McIlraith. Beyond classical planning: Procedural control knowledge and preferences in state-of-the- art planners. In AAAI, Nectar Track, pages 1509-1512, 2008.
  7. Ronen I. Brafman, Giuseppe De Gia- como, and Fabio Patrizi. LTLf/LDLf non-Markovian rewards. In AAAI, pages 1771-1778, 2018.
  8. Alberto Camacho, Oscar Chen, Scott Sanner, and Sheila A. McIlraith. Non-Markovian rewards ex- pressed in LTL: guiding search via reward shaping. In SOCS, pages 159-160, 2017.
  9. Alberto Camacho, Oscar Chen, Scott Sanner, and Sheila A. McIlraith. Non-markovian rewards expressed in LTL: Guiding search via reward shaping (ex- tended version). In GoalsRL, a workshop collocated with ICML/IJCAI/AAMAS, 2018.
  10. De Giacomo and Vardi, 2013] Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI, pages 854-860, 2013.
  11. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 -a framework for LTL and ω-automata manipulation. In ATVA, volume 9938 of LNCS, pages 122-129. Springer, October 2016.
  12. E. Allen Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, volume B, pages 995-1072. Elsevier, 1990.
  13. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979.
  14. Kupferman and Vardi, 2001] Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. Formal Meth- ods in System Design, 19(3):291-314, 2001.
  15. Leslie Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software En- gineers. Addison-Wesley, 2002.
  16. Lu et al., 2018] Tyler Lu, Dale Schuurmans, and Craig Boutilier. Non-delusional Q-learning and value-iteration. In NeurIPS, pages 9971-9981, 2018.
  17. George H Mealy. A method for synthesiz- ing sequential circuits. The Bell System Technical Journal, 34(5):1045-1079, Sep. 1955.
  18. Volodymyr Mnih, Koray Kavukcuoglu, David Silver, Andrei A. Rusu, Joel Veness, Marc G Belle- mare, Alex Graves, Martin Riedmiller, Andreas K. Fidjeland, Georg Ostrovski, et al. Human-level control through deep re- inforcement learning. Nature, 518(7540):529-533, 2015.
  19. Andrew Y. Ng, Daishi Harada, and Stuart Rus- sell. Policy invariance under reward transformations: Theory and application to reward shaping. In ICML, volume 3, pages 278-287, 1999.
  20. Tom Schaul, John Quan, Ioannis Antonoglou, and David Silver. Prioritized experience replay. arXiv preprint arXiv:1511.05952, 2015. · arXiv
  21. Shirin Sohrabi, Jorge A. Baier, and Sheila A. McIlraith. Preferred explanations: Theory and gen- eration via planning. In AAAI-11, pages 261-267, 2011.
  22. Richard S. Sutton and Andrew G. Barto. Reinforcement learning: An introduction. MIT Press, second edition, 2018.
  23. Sylvie Thiébaux, Charles Gretton, John K. Slaney, David Price, and Froduald Kabanza. Decision-theoretic planning with non-Markovian rewards. Journal of Artificial Intelligence Research, 25:17-74, 2006.
  24. Thompson, 1968] Ken Thompson. Regular expression search algorithm. Communications of the ACM, 11(6):419-422, 1968.
  25. Toro Icarte et al., 2018a] Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIl- raith. Teaching multiple tasks to an RL agent using LTL. In AAMAS, pages 452-461, 2018.
  26. Toro Icarte et al., 2018b] Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIl- raith. Using reward machines for high-level task specification and decomposition in reinforcement learning. In ICML, pages 2112-2121, 2018.
  27. Eleni Triantafillou, Jorge A. Baier, and Sheila A. McIlraith. A unifying framework for planning with LTL and regular expressions. In MOCHAP, a workshop collocated with ICAPS, pages 23-31, 2015.
  28. Van Hasselt et al., 2016] Hado Van Hasselt, Arthur Guez, and David Silver. Deep reinforcement learning with double Q- learning. In AAAI, pages 2094-2100, 2016.
  29. Christopher J. C. H. Watkins and Peter Dayan. Q-learning. Machine learning, 8(3-4):279-292, 1992.
  30. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. Symbolic LTLf synthesis. In IJCAI, pages 1362-1369, 2017.

Cited by

Sorted by citations

Authors
Camacho, A., Toro Icarte, R., Klassen, T. Q., Valenzano, R., & McIlraith, S. A.
Affiliations
  • University of Toronto (CA)
  • Department of Computer Science, University of Toronto, Toronto, Canada
  • Element AI, Toronto, Canada
Venue
Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Published
2019-08
Pages
6065-6073
OpenAlex
W2966537673
Cited by
157
References
0
Citations by year
2026: 6 · 2025: 16 · 2024: 22 · 2023: 29 · 2022: 36 · 2021: 25 · 2020: 22 · 2019: 1
FWCI
8.03
Type
conference paper
Language
en
Open access
Locations
International Joint Conference on Artificial Intelligence (publishedVersion)
Funders
  • Microsoft Research
  • Natural Sciences and Engineering Research Council of Canada
  • Comisión Nacional de Investigación Científica y Tecnológica
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Reinforcement Learning in Robotics
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › semigroups and automata theory
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
Keywords
reward machines, linear temporal logic, formal languages, reward shaping, Q-learning, sample efficiency, sparse rewards, regular languages

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review