LTL-Constrained Steady-State Policy Synthesis
Decision-making policies for agents are often synthesized with the constraint that a formal specification of behaviour is satisfied. Here we focus on infinite-horizon properties. On the one hand, Linear Temporal Logic (LTL) is a popular example of a formalism for qualitative specifications. On the other hand, Steady-State Policy Synthesis (SSPS) has recently received considerable attention as it provides a more quantitative and more behavioural perspective on specifications, in terms of the frequency with which states are visited. Finally, rewards provide a classic framework for quantitative properties. In this paper, we study Markov decision processes (MDP) with the specification combining all these three types. The derived policy maximizes the reward among all policies ensuring the LTL specification with the given probability and adhering to the steady-state constraints. To this end, we provide a unified solution reducing the multi-type specification to a multi-dimensional long-run average reward. This is enabled by Limit-Deterministic B\"uchi Automata (LDBA), recently studied in the context of LTL model checking on MDP, and allows for an elegant solution through a simple linear programme. The algorithm also extends to the general $\omega$-regular properties and runs in time polynomial in the sizes of the MDP as well as the LDBA.
Code (0)
등록된 구현이 없습니다.
Tasks
Decision MakingSimilar Papers 제목 키워드 기반
Controller Synthesis for Omega-Regular and Steady-State Specifications
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 specification. More recently, proble…
Steady-State Planning in Expected Reward Multichain MDPs
The planning domain has experienced increased interest in the formal synthesis of decision-making policies. This formal synthesis typically entails finding a policy which satisfies formal specifications in the form of so…
Decision MakingSteady State Analysis of Episodic Reinforcement Learning
This paper proves that the episodic learning environment of every finite-horizon decision task has a unique steady state under any behavior policy, and that the marginal distribution of the agent's input indeed converges…
Continual Learningreinforcement-learningReinforcement LearningReinforcement Learning (RL)Approximate Optimal Filter for Linear Gaussian Time-invariant Systems
State estimation is critical to control systems, especially when the states cannot be directly measured. This paper presents an approximate optimal filter, which enables to use policy iteration technique to obtain the st…
State EstimationMULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints
We present MULTIGAIN 2.0, a major extension to the controller synthesis tool MULTIGAIN, built on top of the probabilistic model checker PRISM. This new version extends MULTIGAIN's multi-objective capabilities, by allowin…