# Fulfilling Formal Specifications ASAP by Model-free Reinforcement Learning

arXiv: https://arxiv.org/abs/2304.12508 · HTML: https://mlsanity.com/paper/2304.12508/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 52 references that are in the map.
- First posted on arXiv 25 Apr 2023.

## Builds on (most cited first, 10 of 10)

- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Soft Actor-Critic Algorithms and Applications](https://mlsanity.com/paper/1812.05905/) (2018)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [Reinforcement Learning With Temporal Logic Rewards](https://mlsanity.com/paper/1612.03471/) (2016)
- [Keeping Your Distance: Solving Sparse Reward Tasks Using Self-Balancing Shaped Rewards](https://mlsanity.com/paper/1911.01417/) (2019)
- [Probably Approximately Correct MDP Learning and Control With Temporal Logic Constraints](https://mlsanity.com/paper/1404.7073/) (2014)
- [Robust Online Monitoring of Signal Temporal Logic](https://mlsanity.com/paper/1506.08234/) (2015)
- [A Policy Search Method For Temporal Logic Specified Reinforcement Learning Tasks](https://mlsanity.com/paper/1709.09611/) (2017)
- [SABLAS: Learning Safe Control for Black-box Dynamical Systems](https://mlsanity.com/paper/2201.01918/) (2022)
- [Hierarchical Potential-based Reward Shaping from Task Specifications](https://mlsanity.com/paper/2110.02792/) (2021)

## Abstract (arXiv)

We propose a model-free reinforcement learning solution, namely the ASAP-Phi framework, to encourage an agent to fulfill a formal specification ASAP. The framework leverages a piece-wise reward function that assigns quantitative semantic reward to traces not satisfying the specification, and a high constant reward to the remaining. Then, it trains an agent with an actor-critic-based algorithm, such as soft actor-critic (SAC), or deep deterministic policy gradient (DDPG). Moreover, we prove that ASAP-Phi produces policies that prioritize fulfilling a specification ASAP. Extensive experiments are run, including ablation studies, on state-of-the-art benchmarks. Results show that our framework succeeds in finding sufficiently fast trajectories for up to 97% test cases and defeats baselines.