Controller Synthesis for Omega-Regular and Steady-State Specifications

Alvaro Velasquez, Ismail Alkhouri, Andre Beckus +2

Given a Markov decision process (MDP) and a linear-time ($\omega$-regular or LTL) specification, the controller synthesis problem aims to compute the optimal policy that satisfies the s…