Reinforcement Learning for Temporal Logic Control Synthesis with\n Probabilistic Satisfaction Guarantees

2019/09/11 by Mohammadhosein Hasanbeig, Yiannis Kantaros, Hasanbeig, Mohammadhosein +9 · 8 citations
Computer Science · #Formal Methods in Verification #Advanced Software Engineering Methodologies

paper · pdf · doi:10.48550/arxiv.1909.05304

Abstract

Reinforcement Learning (RL) has emerged as an efficient method of choice for\nsolving complex sequential decision making problems in automatic control,\ncomputer science, economics, and biology. In this paper we present a model-free\nRL algorithm to synthesize control policies that maximize the probability of\nsatisfying high-level control objectives given as Linear Temporal Logic (LTL)\nformulas. Uncertainty is considered in the workspace properties, the structure\nof the workspace, and the agent actions, giving rise to a\nProbabilistically-Labeled Markov Decision Process (PL-MDP) with unknown graph\nstructure and stochastic behaviour, which is even more general case than a\nfully unknown MDP. We first translate the LTL specification into a Limit\nDeterministic Buchi Automaton (LDBA), which is then used in an on-the-fly\nproduct with the PL-MDP. Thereafter, we define a synchronous reward function\nbased on the acceptance condition of the LDBA. Finally, we show that the RL\nalgorithm delivers a policy that maximizes the satisfaction probability\nasymptotically. We provide experimental results that showcase the efficiency of\nthe proposed method.\n

Cited by

• About Time: Model-free Reinforcement Learning with Timed Reward Machines
• Automating the Refinement of Reinforcement Learning Specifications
• Predictive Safety Shield for Dyna-Q Reinforcement Learning
• ObjectAlign: Neuro-Symbolic Object Consistency Verification and Correction
• RLAF: Reinforcement Learning from Automaton Feedback
• Control Synthesis of Cyber-Physical Systems for Real-Time Specifications through Causation-Guided Reinforcement Learning
• NeuS-QA: Grounding Long-Form Video Understanding in Temporal Logic and Neuro-Symbolic Reasoning
• Physics-Informed Reward Machines

Related

• Certified Reinforcement Learning with Logic Guidance
• Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning
• Reinforcement Learning Based Temporal Logic Control with Soft Constraints Using Limit-deterministic Generalized Buchi Automata
• Logically-Constrained Reinforcement Learning
• Sample-Efficient Reinforcement Learning with Temporal Logic Objectives: Leveraging the Task Specification to Guide Exploration