Correct-by-synthesis reinforcement learning with temporal logic constraints
Open accessAbstract
We consider a problem on the synthesis of optimal reactive controllers with an a priori unknown performance criterion while satisfying a given temporal logic specification through the interaction with an uncontrolled environment. We decouple the problem into two sub-problems. First, we extract a (maximally) permissive strategy for the system, which encodes multiple (possibly all) ways in which the system can react to the adversarial environment and satisfy the specifications. Then, we quantify the a priori unknown performance criterion as a (still unknown) reward function, and compute - by using the so-called maximin-Q learning algorithm - an optimal strategy for the system within the operating envelope allowed by the permissive strategy. We establish both correctness (with respect to the temporal logic specifications) and optimality (with respect to the a priori unknown performance criterion) of this two-step technique for a fragment of temporal logic specifications. For specifications beyond this fragment, correctness can still be preserved, but the learned strategy may be sub-optimal. We present an algorithm to the overall problem, and demonstrate its use and computational requirements on a set of robot motion planning examples.
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.
Integrity signals
Registry
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.
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?
Wen et al.'s technique does not work with function approximation, which prevents it from being used in complex scenarios.
“Unlike the approach in the paper, their technique does not work with function approximation, which prevents it from being used in complex scenarios.”
From Safe Reinforcement Learning via Shielding (2018) · cites this paper as Wen, Ehlers, and Topcu 2015
Section V (Examples; page unavailable) shows that learning time and iterations grow as the grid grows, and describes a trade-off between performance and computation cost. This supports a scalability concern, but the paper does not say that its technique cannot work with function approximation or that it cannot be used in complex scenarios. (LLM, conf=0.76)
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: 25
- A. G. Barto, R. S. Sutton, and C. W. Anderson. Neuronlike adaptive elements that can solve difficult learning control problems. IEEE Transactions on Systems, Man and Cybernetics, SMC-13(5):834-846, 1983.
- J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to safety games. RAIRO-Theoretical Informatics and Applications, 36(03):261-275, 2002.
- K. Chatterjee, T. A. Henzinger, and M. Jurdzinski. Mean-payoff parity games. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 178-187. IEEE, 2005.
- X. C. Ding, S. L. Smith, C. Belta, and D. Rus. Optimal control of markov decision processes with linear temporal logic constraints. IEEE Transactions on Automatic Control, 59(5):1244-1257, 2014.
- R. Ehlers and B. Finkbeiner. Reactive safety. In Proceedings of Symposium on Games, Automata, Logics and Formal Verification, pages 178-191, 2011.
- J. Fu and U. Topcu. Probably approximately correct mdp learning and control with temporal logic constraints. In Proceedings of Conference on Robotics: Science and Systems, 2014.
- B.-Q. Huang, G.-Y. Cao, and M. Guo. Reinforcement learning neural network to the problem of autonomous mobile robot obstacle avoidance. In Proceedings of Conference on Machine Learning and Cybernetics, volume 1, pages 85-89, 2005.
- M. Jurdziński. Small progress measures for solving parity games. In Symposium on Theoretical Aspects of Computer Science 2000, pages 290-301, 2000.
- O. Kupferman and M. Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291-314, 2001.
- M. L. Littman. Markov games as a framework for multi-agent reinforcement learning. In Proceedings of Conference on Machine Learning, volume 94, pages 157-163, 1994.
- M. L. Littman and C. Szepesvári. A generalized reinforcement- learning model: Convergence and applications. In Proceedings of Conference on Machine Learning, pages 310-318, 1996.
- Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems, 6(1):68-93, 1984.
- T. J. Perkins and A. G. Barto. Lyapunov-constrained action sets for reinforcement learning. In Proceedings of Conference on Machine Learning, volume 1, pages 409-416, 2001.
- N. Piterman, A. Pnueli, and Y. Saar. Synthesis of reactive (1) designs. In Verification, Model Checking, and Abstract Interpretation, pages 364-380. Springer, 2006.
- A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proceedings of Symposium on Principles of Programming Languages, pages 179-190, 1989.
- A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In Automata, Languages and Programming, pages 652-671. Springer, 1989.
- A. Schwartz. A reinforcement learning method for maximizing undiscounted rewards. In Proceedings of Conference on Machine Learning, volume 93, pages 298-305, 1993.
- L. S. Shapley. Stochastic games. Proceedings of the National Academy of Sciences of the United States of America, 39(10):1095-1100, 1953.
- S. Sohail and F. Somenzi. Safety first: a two-stage algorithm for the synthesis of reactive systems. International Journal on Software Tools for Technology Transfer, 15(5-6):433-454, 2013.
- R. S. Sutton. Learning to predict by the methods of temporal differences. Machine Learning, 3(1):9-44, 1988.
- R. S. Sutton and A. G. Barto. Introduction to Reinforcement Learning. MIT Press, 1998.
- G. Tesauro. TD-gammon, a self-teaching backgammon program, achieves master-level play. Neural Computation, 6(2):215-219, 1994.
- W. Thomas, T. Wilke, et al. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500. Springer Science & Business Media, 2002.
- M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency, pages 238-266. Springer, 1996.
- E. M. Wolff, U. Topcu, and R. M. Murray. Optimal control with weighted average costs and temporal logic specifications. In Proceed- ings of Conference on Robotics: Science and Systems, 2012.
Cited by
Sorted by citations
Safe Reinforcement Learning via Shielding
Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., & Topcu, U. (2018) · Proceedings of the AAAI Conference on Artificial Intelligence · doi:10.1609/aaai.v32i1.11797 · Cited by 37 · see citing works
Self-citation
- Authors
- Wen, M., Ehlers, R., & Topcu, U.
- Affiliations
- University of Pennsylvania (US)
- University of Bremen (DE)
- Venue
- 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
- Publisher
- IEEE
- Published
- 2015-09
- Pages
- 4983-4990
- ISSN
- 2153-0858 (ISSN-L)
- OpenAlex
- W2963604565
- Cited by
- 59
- References
- 0
- Citations by year
- 2025: 1 · 2024: 5 · 2023: 4 · 2022: 7 · 2021: 7 · 2020: 12 · 2019: 6 · 2018: 9 · 2017: 1 · 2016: 5 · 2015: 2
- FWCI
- 5.11
- Type
- conference paper
- Language
- en
- Open access
- green
- arxiv.org
- Locations
- IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) (publishedVersion)
- arXiv (Cornell University) (submittedVersion)
- arXiv (Cornell University)
- Funders
- National Science Foundation (1446479)
- Air Force Office of Scientific Research
- Air Force Research Laboratory
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Artificial Intelligence › Reinforcement Learning in Robotics
- Physical Sciences › Computer Science › Artificial Intelligence › Logic, Reasoning, and Knowledge
- Keywords
- reinforcement learning, temporal logic specifications, adversarial environments, robot motion planning, optimal control under uncertainty
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
