# Controller Synthesis for Omega-Regular and Steady-State Specifications

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 41 references that are in the map.
- First posted on arXiv 5 Jun 2021.

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

- [SPOTTER: Extending Symbolic Planning Operators through Targeted Reinforcement Learning](https://mlsanity.com/paper/2012.13037/) (2020)
- [Discounting in LTL](https://mlsanity.com/paper/1406.4249/) (2014)
- [Steady-State Planning in Expected Reward Multichain MDPs](https://mlsanity.com/paper/2012.02178/) (2020)
- [LTL-Constrained Steady-State Policy Synthesis](https://mlsanity.com/paper/2105.14894/) (2021)
- [Optimal Control of MDPs with Temporal Logic Constraints](https://mlsanity.com/paper/1303.1942/) (2013)
- [Optimal Receding Horizon Control for Finite Deterministic Systems with Temporal Logic Constraints](https://mlsanity.com/paper/1303.3533/) (2013)

## Built on by (most cited first, 2 of 2)

- [MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints](https://mlsanity.com/paper/2305.16752/) (2023)
- [Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement](https://mlsanity.com/paper/2506.17792/) (2025)

## Abstract (arXiv)

Given a Markov decision process (MDP) and a linear-time (ω-regular or LTL) specification, the controller synthesis problem aims to compute the optimal policy that satisfies the specification. More recently, problems that reason over the asymptotic behavior of systems have been proposed through the lens of steady-state planning. This entails finding a control policy for an MDP such that the Markov chain induced by the solution policy satisfies a given set of constraints on its steady-state distribution. This paper studies a generalization of the controller synthesis problem for a linear-time specification under steady-state constraints on the asymptotic behavior. We present an algorithm to find a deterministic policy satisfying ω-regular and steady-state constraints by characterizing the solutions as an integer linear program, and experimentally evaluate our approach.