LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning (2022-09-21T00:00:00.000000Z)

TL;DR

Owing to the LDBA-guided exploration and LCRL model-free architecture, robust performance is observed, which also scales well when compared to standard RL approaches (whenever applicable to LTL specifications).

Abstract

LCRL is a software tool that implements model-free Reinforcement Learning (RL) algorithms over unknown Markov Decision Processes (MDPs), synthesising policies that satisfy a given linear temporal specification with maximal probability. LCRL leverages partially deterministic finite-state machines known as Limit Deterministic Buchi Automata (LDBA) to express a given linear temporal specification. A reward function for the RL algorithm is shaped on-the-fly, based on the structure of the LDBA. Theoretical guarantees under proper assumptions ensure the convergence of the RL algorithm to an optimal policy that maximises the satisfaction probability. We present case studies to demonstrate the applicability, ease of use, scalability, and performance of LCRL. Owing to the LDBA-guided exploration and LCRL model-free architecture, we observe robust performance, which also scales well when compared to standard RL approaches (whenever applicable to LTL specifications). Full instructions on how to execute all the case studies in this paper are provided on a GitHub page that accompanies the LCRL distribution www.github.com/grockious/lcrl.

Authors

Mohammadhosein Hasanbeig

1 papers

D. Kroening

1 papers

A. Abate

1 papers

TL;DR

Abstract

Authors

References46 items

COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking

Mungojerrie: Reinforcement Learning of Linear-Time Objectives

Modular Deep Reinforcement Learning for Continuous Motion Planning With Temporal Logic

Deep Reinforcement Learning with Temporal Logics

A Composable Specification Language for Reinforcement Learning Tasks

Verifiably safe exploration for end-to-end reinforcement learning

Cautious Reinforcement Learning with Logical Constraints

The probabilistic model checker Storm

DeepSynth: Program Synthesis for Automatic Task Segmentation in Deep Reinforcement Learning

Control Synthesis from Linear Temporal Logic Specifications using Model-Free Reinforcement Learning

Reinforcement Learning for Temporal Logic Control Synthesis with Probabilistic Satisfaction Guarantees

Verifiably Safe Off-Model Reinforcement Learning

Rethinking the Discount Factor in Reinforcement Learning: A Decision Theoretic Approach

Certified Reinforcement Learning with Logic Guidance

Owl: A Library for ω-Words, Automata, and LTL

Logically-Constrained Neural Fitted Q-Iteration

Model Checking

Foundations for Restraining Bolts: Reinforcement Learning with LTLf/LDLf Restraining Specifications

Using Reward Machines for High-Level Task Specification and Decomposition in Reinforcement Learning

Safe Reinforcement Learning via Formal Methods: Toward Safe Control Through Proof and Learning

Logically-Constrained Reinforcement Learning

DeepMind Control Suite

Optimal Translation of LTL to Limit Deterministic Automata

Modular Multitask Reinforcement Learning with Policy Sketches

MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata

Limit-Deterministic Büchi Automata for Linear Temporal Logic

A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications

Formal consistency checking over specifications in natural languages

FAUST 2 : Formal Abstractions of Uncountable-STate STochastic Processes

Reinforcement learning with state-dependent discount factor

The Arcade Learning Environment: An Evaluation Platform for General Agents

Markov decision processes with state-dependent discount factors and unbounded rewards/costs

PRISM 4.0: Verification of Probabilistic Real-Time Systems

Automated Identification of LTL Patterns in Natural Language Requirements

Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems

Stochastic optimal control : the discrete time case

Adaptive state space partitioning for reinforcement learning

Discounting the Distant Future: How Much Do Uncertain Rates Increase Valuations?

Safe and certified reinforcement learning with logical constraints

Towards Verifiable and Safe Model-Free Reinforcement Learning

Verifiably Safe Autonomy for Cyber-Physical Systems

Neuro-Dynamic Programming

From natural language to linear temporal logic: Aspects of specifying embedded systems in LTL

Reinforcement Learning: An Introduction

Stable Function Approximation in Dynamic Programming

Nouvelles applications des paramètres continus à la théorie des formes quadratiques. Deuxième mémoire. Recherches sur les parallélloèdres primitifs.

Field of Study

Journal Information

Name

Volume

Venue Information

Name

Type

URL

Alternate Names