Realizable Abstractions: Near-Optimal Hierarchical Reinforcement Learning
Extracted source text · arXiv 2512.04958
% NOTE: 10 pages (9 is better) of main content + bib + appendix
% US letter size
\pdfpagewidth=8.5in
\pdfpageheight=11in
\documentclass{article}
\usepackage{iclr25_sty/iclr2025_conference,times}
\usepackage[utf8]{inputenc} % allow utf-8 input
\usepackage[T1]{fontenc} % use 8-bit T1 fonts
\usepackage{microtype} % microtypography
\usepackage{nicefrac} % compact symbols for 1/2, etc.
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{bbm}
\usepackage{thm-restate}
\usepackage{booktabs} % professional-quality tables
\usepackage[inline]{enumitem}
\usepackage{comment}
\usepackage{xparse}
\usepackage{xcolor} % colors
\usepackage{tikz}
\usepackage{titletoc}
\usepackage[algoruled, vlined, shortend, linesnumbered]{algorithm2e}
\usepackage{url} % simple URL typesetting
\usepackage[hidelinks]{hyperref} % hyperlinks
\usepackage{cleveref} % pass capitalise option if you prefer to say Figure 1, instead of figure 1
% TODO: comment these lines when ready for submission.
% Todonote
\usepackage{todonotes}
\newcommand{\TodonotesColor}{brown!50!lightgray}
\setuptodonotes{%
bordercolor=\TodonotesColor,
backgroundcolor=white,
}
\newcommand{\Todonotes}[2][]{%
\todo[inline, caption={}, #1]{\begin{minipage}{\textwidth}\raggedright #2\end{minipage}}}
\newcommand{\Note}[2][]{\Todonotes[#1]{Note: #2}}
\newcommand{\Todo}[2][]{\Todonotes[#1]{To do: #2}}
\newcommand{\Strongnote}[1]{\Note[backgroundcolor=\TodonotesColor, bordercolor=white]{#1}}
\newcommand{\Strongtodo}[1]{\Todo[backgroundcolor=\TodonotesColor, bordercolor=white]{#1}}
\newcommand{\Side}[2][]{\todo[#1, size=scriptsize, linecolor=lightgray!40!brown]{#2}}
% Algorithms
\DontPrintSemicolon
\SetDataSty{textit}
\SetFuncSty{textsc}
\SetProcNameSty{textsc}
\SetProcArgSty{textit}
\newcommand\mycommentstyle[1]{\texttt{\color{gray}\footnotesize{#1}}}
\SetCommentSty{mycommentstyle}
\SetKwInOut{KwIns}{inputs}
\SetKwProg{CustomFn}{Function}{}{}
\SetKw{Break}{break}
\SetKw{KAnd}{and}
\SetKw{KGoto}{go--to}
\SetKwBlock{Repeat}{repeat}{end}
\SetKwIF{With}{}{Else}{with}{do}{}{else}{end}
\SetKwIF{If}{ElseIf}{Else}{if}{then}{else if}{else}{end}
\SetKwData{DEnough}{found}
\SetKwFunction{FStep}{Step}
\SetKwFunction{FReset}{Reset}
\SetKwFunction{FValueIteration}{ValueIteration}
\SetKwFunction{FAbstractOneR}{AbstractOneR}
\SetKwFunction{FRollout}{Rollout}
\SetKwFunction{FRealizer}{Realizer}
\SetKwFunction{FGet}{Get}
% Math
\allowdisplaybreaks % allows to split math with many rows. Use \\* to avoid page breaking
% Imports
\input{aliases}
\input{tikz-tools}
\input{colors}
% Enunciati
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\newtheorem{example}{Example}
\newtheorem{assumption}{Assumption}
\newtheorem{condition}{Condition}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\crefname{theorem}{Theorem}{Theorems}
\crefname{lemma}{Lemma}{Lemmas}
\crefname{proposition}{Proposition}{Propositions}
\crefname{corollary}{Corollary}{Corollaries}
\crefname{definition}{Definition}{Definitions}
\crefname{example}{Example}{Examples}
\crefname{assumption}{Assumption}{Assumptions}
\crefname{condition}{Condition}{Conditions}
\crefname{remark}{Remark}{Remarks}
\crefname{figure}{Figure}{Figures}
\crefname{appendix}{Appendix}{Appendices}
\newcommand\nodisplayskiphere{\vskip-\topsep}
\title{Realizable Abstractions: Near-Optimal\\ Hierarchical Reinforcement Learning}
\author{Roberto Cipollone \textsuperscript{1}, Luca Iocchi \textsuperscript{1}, Matteo Leonetti \textsuperscript{2}\\
\textsuperscript{1} Sapienza University of Rome\\
\textsuperscript{2} King’s College London\\
\texttt{\{cipollone,iocchi\}@diag.uniroma1.it}\\
\texttt{matteo.leonetti@kcl.ac.uk}
}
\iclrfinalcopy
\begin{document}
\maketitle
\begin{abstract}
% Why HRL is important
The main focus of Hierarchical Reinforcement Learning (HRL) is studying how large Markov Decision Processes (MDPs) can be more efficiently solved when addressed in a modular way, by combining partial solutions computed for smaller subtasks.
Despite their very intuitive role for learning, most notions of MDP abstractions proposed in the HRL literature have limited expressive power or do not possess formal efficiency guarantees.
% What do we do
This work addresses these fundamental issues by defining Realizable Abstractions, a new relation between generic low-level MDPs and their associated high-level decision processes.
The notion we propose avoids non-Markovianity issues and has desirable near-optimality guarantees.
Indeed, we show that any abstract policy for Realizable Abstractions can be translated into near-optimal policies for the low-level MDP, through a suitable composition of options.
As demonstrated in the paper, these options can be expressed as solutions of specific constrained MDPs.
Based on these findings, we propose \Ouralg, a new HRL algorithm that returns compositional and near-optimal low-level policies, taking advantage of the Realizable Abstraction given in the input.
We show that \Ouralg\ is Probably Approximately Correct, it converges in a polynomial number of samples, and it is robust to inaccuracies in the abstraction.
\end{abstract}
\section{Introduction}
% What is HRL
Hierarchical Reinforcement Learning (HRL) is the study of abstractions of decision processes
and how they can be used to improve the efficiency and compositionality of RL algorithms \citep{barto_2003_RecentAdvancesHierarchical,abel_2018_StateAbstractionsLifelong}.
To pursue these objectives, most HRL methods augment the low-level
Markov Decision Process (MDP) \citep{puterman_1994_MarkovDecisionProcesses}
with some form of abstraction, often a simplified state representation or a high-level policy.
As was immediately identified \citep{dayan_1992_FeudalReinforcementLearning},
compositionality is arguably one of the most important features for HRL algorithms,
as it is commonly associated with increased efficiency \citep{wen_2020_EfficiencyHierarchicalReinforcement} and policy reuse for downstream tasks \citep{brunskill_2014_PACinspiredOptionDiscovery,abel_2018_StateAbstractionsLifelong,tasse_2020_BooleanTaskAlgebraa,tasse_2022_GeneralisationLifelongReinforcement}.
% What is the problem with HRL
There is a common intuition that drives many authors in HRL.
That is, abstract states correspond to sets of ground states, and abstract actions correspond to sequences of ground actions.
This was evident since the early work in HRL \citep{dayan_1992_FeudalReinforcementLearning},
and was largely derived from hierarchical planning.
However, the main question that still remains unanswered is
\emph{which sequence of ground actions should each abstract action correspond to?}
The answer to this question also requires the identification of a suitable state abstraction.
The resulting notion of MDP abstraction has a strong impact on the applicability and the guarantees of the associated HRL methods.
There is no shared consensus on what ``MDP abstractions'' should refer to.
In the literature, the term is loosely used to refer to a variety of concepts, including
state partitions \citep{abel_2020_ValuePreservingStateAction,wen_2020_EfficiencyHierarchicalReinforcement},
bottleneck states \citep{jothimurugan_2021_AbstractValueIteration},
subtasks \citep{nachum_2018_DataefficientHierarchicalReinforcement,jothimurugan_2021_CompositionalReinforcementLearning},
options \citep{precup_1997_MultitimeModelsTemporally,khetarpal_2020_OptionsInterestTemporal},
entire MDPs \citep{ravindran_2002_ModelMinimizationHierarchical,cipollone_2023_ExploitingMultipleAbstractions},
or even the natural language \citep{jiang_2019_LanguageAbstractionHierarchical}.
In addition,
most HRL methods have been validated only experimentally
\citep{nachum_2018_DataefficientHierarchicalReinforcement,jinnai_2020_ExplorationReinforcementLearning,jothimurugan_2021_AbstractValueIteration,lee_2021_AIPlanningAnnotation,lee_2022_DHRLGraphbasedApproacha},
leading to a limited theoretical understanding of general abstractions and their use in RL.
%
Some notable exceptions \citep{brunskill_2014_PACinspiredOptionDiscovery,fruit_2017_RegretMinimizationMDPs,fruit_2017_ExplorationexploitationMDPsOptions,wen_2020_EfficiencyHierarchicalReinforcement}
give formal definitions of state and temporal abstractions, and provide formal near-optimality and efficiency guarantees.
However, they do not define a high-level decision process, enforcing requirements that are often impractical on the ground MDP directly.
% What do we do: Realizable abstractions
In this work, we propose a new formal definition of MDP abstractions, based on a high-level decision process.
This definition enables algorithms, such as the one proposed in this paper, that do not require specific knowledge about the ground MDP.
In particular, we identify a new relation that links generic low-level MDPs to their high-level representations,
and we use a second-order MDP as the high-level decision process in order to overcome non-Markovian dependencies.
As we show, the abstractions we propose are widely applicable,
do not incur the non-Markovian effects that are often found in HRL \citep{bai_2016_MarkovianStateAction,nachum_2018_DataefficientHierarchicalReinforcement,jothimurugan_2021_AbstractValueIteration},
and provide near-optimality guarantees for their associated low-level policies.
Such near-optimal policies only result from the compositions of smaller options, without any global constraint.
Due to this feature, we call them \emph{Realizable Abstractions}.
An important feature of our work is also that we do not restrict the cardinality of the state and action spaces for the ground MDP that does not need to be finite.
Instead, we require that the abstract decision process has finite state and action sets,
so that we can compute an exact tabular representation of the abstract value function.
% Algoritmic contribution
We also address the associated algorithmic question of how to learn the ground options that \emph{realize} each high-level behavior.
As we show, the realization problem, that is, the problem of learning suitable options from experience, can be cast as a Constrained MDP (CMDP) \citep{altman_1999_ConstrainedMarkovDecision} and solved with off-the-shelf online RL algorithms for CMDPs~\citep{zhang_2020_FirstOrderConstrained,ding_2022_ConvergenceSampleComplexity}.
Based on these principles, we develop a new algorithm,
called \emph{\Ouralg} (for ``Realizable Abstractions RL''),
which learns compositional policies for the ground MDP and it is Probably Approximately Correct (PAC) \citep{fiechter_1994_EfficientReinforcementLearning}.
An additional novelty of this work is that the proposed algorithm iteratively refines the high-level decision process given in input by sampling in the ground MDP and it exploits the solution obtained from the current abstraction to drive exploration in the ground MDP.
\paragraph{Summary of contributions}
The contributions of this work are theoretical and algorithmic.
We propose \emph{Realizable Abstractions} (\cref{def:realizability}),
we show a formal relation between the abstract and the ground values (\cref{th:realizab-abstraction-value,th:realizab-optimal-value}),
and we provide original insights on the conditions that must be met to reduce the effective horizon in the abstraction (\cref{th:admissible-implies-good-gamma}).
%Realizable Abstractions are general and can capture a variety of state-action abstractions,
%including very coarse partitioning of states and lossless transformations, such as MDP homomorphisms (\cref{th:realizable-homomorphisms}).
%As we show, the solution of any Realizable Abstraction corresponds to a near-optimal policy in the ground MDP which can be expressed as a simple composition of locally defined options (\cref{th:realizab-abstraction-value,th:realizab-optimal-value}).
%
Regarding the algorithmic contributions,
\Ouralg\ is sample efficient, PAC, and robust with respect to approximately realizable abstractions and overly optimistic abstract rewards (\cref{th:algorithm-sample-complexity}).
\subsection*{Related work}
% NOTE: after acc make paragraph
\textbf{State-action abstractions}\,\,
Similarly to \citet{abel_2020_TheoryAbstractionReinforcement},
we organize most of the work in HRL in two groups: state abstractions,
which primarily focus on simplified state representations, and action abstractions, which focus on high-level actions and temporal abstractions.
From the first group, we mention the MDP homomorphisms \citep{ravindran_2002_ModelMinimizationHierarchical,ravindran_2004_ApproximateHomomorphismsFramework}, stochastic bisimulation \citep{givan_2003_EquivalenceNotionsModel,ferns_2004_MetricsFiniteMarkov} and the irrelevance criteria listed in \citet{li_2006_UnifiedTheoryState}.
These are all related to the language of MDP abstractions used here.
However, the limited expressive power of these early works mainly captures specific projections of state features or symmetries in MDP dynamics.
As we discuss in \cref{sec:app:homomorphism},
our framework extends both MDP homomorphisms and stochastic bisimulations of \citet{givan_2003_EquivalenceNotionsModel}.
%
In the second group, the \emph{options} framework \citep{precup_1997_MultitimeModelsTemporally,sutton_1998_IntraoptionLearningTemporally,sutton_1999_MDPsSemiMDPsFramework}
is one of the first to successfully achieve temporal abstraction in MDPs.
Options are partial policies, which can be interpreted as abstract actions, and can be fully learned from experience \citep{bacon_2017_OptioncriticArchitecture,machado_2017_LaplacianFrameworkOption,khetarpal_2020_OptionsInterestTemporal}.
Thanks to these properties, many works implemented HRL principles within the theory of options,
such as the automatic discovery of landmarks and sub-goals
\citep{simsek_2004_UsingRelativeNovelty,castro_2011_AutomaticConstructionTemporally,kulkarni_2016_HierarchicalDeepReinforcement,nachum_2018_DataefficientHierarchicalReinforcement,jinnai_2019_DiscoveringOptionsExploration,ramesh_2019_SuccessorOptionsOption,jinnai_2020_ExplorationReinforcementLearning,jiang_2022_LearningOptionsCompressiona,lee_2022_DHRLGraphbasedApproacha}.
Nonetheless, since the state space is usually not affected by the use of options, the lack of a simplified state representation limits the reuse of previously acquired skills.
%
The study of abstractions that involve both states and actions is the most natural progression for HRL research.
Nonetheless, many works in this direction \citep{ravindran_2003_RelativizedOptionsChoosing,abel_2020_ValuePreservingStateAction,abel_2020_TheoryAbstractionReinforcement,jothimurugan_2021_AbstractValueIteration,wen_2020_EfficiencyHierarchicalReinforcement,infante_2022_GloballyOptimalHierarchical} only consider a ground MDP and a partition of the state space, without any explicit dynamics at the abstract level.
The main difficulty in defining abstract dynamics comes from the non-Markovian and non-stationary effects that often arise in HRL \citep{jothimurugan_2021_AbstractValueIteration,gurtler_2021_HierarchicalReinforcementLearning}.
This works overcomes these issues and defines MDP abstractions as distinct decision process with independent reward and transition dynamics.
\textbf{HRL theory}\,\,
The theoretical work on HRL is still less developed compared to the empirical studies.
%Nevertheless, we recall a few excellent works.
The first PAC analysis for RL in the presence of options is by \citet{brunskill_2014_PACinspiredOptionDiscovery}.
Later, \citet{fruit_2017_ExplorationexploitationMDPsOptions} and \citet{fruit_2017_RegretMinimizationMDPs}
strongly contributed to the characterization of the conditions that cause options to be beneficial (or harmful) for learning,
such as the near-optimality of options and the reduction in the MDP diameter.
Both of these findings are consistent with our results.
Lastly, \citet{wen_2020_EfficiencyHierarchicalReinforcement} developed PEP, an HRL algorithm, and derived its regret guarantee.
Similarly to our algorithm, PEP learns low-level policies in a compositional way.
However, our algorithm does not receive the ``exit profiles'' in input, which are unlikely to be known in practice.
\textbf{Compositional HRL and logic composition}\,\,
Logical descriptions and planning domains can also be used to subdivide complex dynamics into smaller subtasks.
This approach can be seen as a state-action abstraction with associated semantic labels and has been explored in various forms
\citep{dietterich_2000_HierarchicalReinforcementLearning,konidaris_2018_SkillsSymbolsLearning,illanes_2020_SymbolicPlansHighlevel,jothimurugan_2021_CompositionalReinforcementLearning,lee_2022_AIPlanningAnnotation},
even in purely logical settings \citep{banihashemi_2017_AbstractionSituationCalculus}.
The main strength of logical abstractions is their suitability for compositionality and skill reuse
\citep{andreas_2017_ModularMultitaskReinforcement,jothimurugan_2021_CompositionalReinforcementLearning,neary_2022_VerifiableCompositionalReinforcement}.
However, because of the difficulty of aligning logical representations with stochastic environments and discounted values, most methods do not come with significant near-optimality guarantees for the low-level domain.
\textbf{Other algorithms}\,\,
Regarding the algorithmic contribution, \Ouralg\ is capable of correcting and adapting to very inaccurate abstract rewards.
This feature has been heavily inspired by RL algorithms for multi-fidelity simulators
\citep{cutler_2014_ReinforcementLearningMultifidelity,kandasamy_2016_MultifidelityMultiarmedBandit}.
However, the algorithm cannot update the input mapping function.
Unlike other works \citep{jonsson_2006_CausalGraphBased,allen_2021_LearningMarkovState,steccanella_2022_StateRepresentationLearning},
learning such a state partition remains outside the scope of this work.
\section{Preliminaries}
\paragraph{Notation}
% Sets and sequences
With the juxtaposition of sets, as in $\Set{X} \Set{Y}$ and $\Set{X}^k$, we denote the abbreviation of their Cartesian product.
Similarly, $xy \in \Set{X} \Set{Y}$ is preferred to $(x, y)$, when not ambiguous.
Sequences, which we write as $x_{i:j}$, are elements of $\Set{X}^{j-i+1}$.
% Probabilities
The set of probability distributions on a set $\Set{X}$ is written as $\Distribution{\Set{X}}$.
For $x \in \Set{X}$, we use $\Det{x} \in \Distribution{\Set{X}}$ for the deterministic probability distribution on~$x$.
For finite~$\Set{X}$, this is $\Det{x}(x') \coloneqq \Indicator(x' = x)$.
% Other text
The indicator function $\Indicator(\Formula)$ evaluates to~$1$ if the condition~$\Formula$ is true, $0$~otherwise.
We write $[n]$ for $\{1, \dots, n\}$.
For any surjective function $\Mapping: \States \to \Abst\States$ and $\Abst{s} \in \Abst\States$,
we define $\Block{\Abst{s}}_\Mapping \coloneqq \{s \in \States \Given \Mapping(s) = \Abst{s}\}$,
also written $\Block{\Abst{s}}$, whenever the function is clear from context.
\paragraph{Decision Processes}
A $k$-order Markov Decision Process ($k$-MDP) is a tuple $\MDP = \Tuple{\States, \Actions, T, R, \gamma }$,
where $\States$ is a set of states, $\Actions$ is a set of actions,
$0 < \gamma < 1$ is the discount factor,
$T: \States^k \times \Actions \to \Distribution{\States}$ is the transition function,
and $R: \States^k \times \Actions \to [0, 1]$ is the reward function.
To generate the next state or reward, each function receives the last $k$~states in the trajectory.
In particular, at each time step~$h$, $R(s_{h-k:h-1}, a_{h})$ returns the immediate expected reward~$r_{h}$.
We denote the initial distribution of~$s_0$ with $\StartDistrib \coloneqq T(s\StartSym^k, a)$,
for any $a \in \Actions$, where $s\StartSym \in \States$ is some distinguished dummy state in~$\States$.
We write the cardinalities of $\States, \Actions$ as $S, A$.
In addition, an MDP is a 1-MDP, for which we can simply write $r_h \sim R(s_{h-1}, a_h)$ and $s_h \sim T(s_{h-1}, a_h)$ \citep{puterman_1994_MarkovDecisionProcesses}.
% NOTE: after accept
In any $k$-MDP, the value of a policy~$\Policy$ in some states $s_{0:k-1} \in \States^k$, written $V^\Policy(s_{0:k-1})$, is the expected sum of future discounted rewards,
when starting from~$s_{0:k-1}$, and selecting actions based on~$\Policy$.
The function $Q^\Policy(s_{0:k-1}, a_k)$ is the value of $\Policy$ when the first action after $s_{0:k-1}$ is set to~$a_k$.
Without referring to any state,
the value of a policy~$\Policy$ from the initial distribution~$\StartDistrib$ is
$V_\StartDistrib^\Policy \coloneqq V^\Policy(s\StartSym^k) = \Expected_{s_0 \sim \StartDistrib}[V^\Policy(s\StartSym^{k-1} s_0)]$.
Every $k$-MDP admits an optimal policy, $\Policy^* \coloneqq \argmax_{\Policy} V_\StartDistrib^{\Policy}$,
which is deterministic and Markovian in~$\States^{k}$.
Thus, we often consider the set of policies $\Policies \coloneqq \States^{k} \to \Actions$.
The we often write $V^{\Policy^*}$ as $V^*$.
Near-optimal policies are defined as follows.
For $\PAccuracy > 0$, a policy~$\Policy$ is $\PAccuracy$-optimal if $V^*_\StartDistrib - V^\Policy_\StartDistrib \le \PAccuracy$.
Generally speaking, Reinforcement Learning (RL) is the problem of learning a (near-)optimal policy in an MDP with unknown~$T$ and~$R$.
\paragraph{Constrained MDPs}
A \emph{Constrained MDP} (CMDP) \citep{ross_1985_ConstrainedMarkovDecision,altman_1999_ConstrainedMarkovDecision}
is defined as a tuple $\MDP = \Tuple{\States, \Actions, T, R,\allowbreak \{R_i\}_{i \in [m]}, \{l_i\}_{i \in [m]}, \gamma}$,
where $\Tuple{\States, \Actions, T, R, \gamma}$ forms an MDP and each
$R_i: \States \times \Actions \to [0, 1]$ is an auxiliary reward function with an associated $l_i \in [0,1]$.
Given a CMDP~$\MDP$, let $V^\Policy_{\StartDistrib,i}$ be the value of~$\Policy$ in the MDP $\Tuple{\States, \Actions, T, R_i, \gamma}$.
Then, the set of feasible policies for~$\MDP$ is $\Feasible\Policies \subseteq \Policies$ with
\begin{equation}
\Feasible\Policies \coloneqq \{ \Policy \in \Policies \mid V^\Policy_{\StartDistrib,i} \ge l_i \text{ for each } i \in [m] \}
\end{equation}
The optimal policy of a CMDP is defined as $\argmax_{\Policy \in \Feasible\Policies} V^\Policy$.
Near-optimal policies are defined as usual.
Extending this relaxation to constraints, we also define the set of $\PMaxViolation$-feasible policies as:
$\Feasible[,\PMaxViolation]{\Policies} \coloneqq \{ \Policy \in \Policies \mid V^\Policy_{\StartDistrib,i} \ge l_i - \PMaxViolation \text{ for each } i \in [m] \}$.
% NOTE: after acceptance
To capture negative cost functions, some works do not restrict auxiliary rewards to the $[0,1]$ range.
However, this will be enough for our purposes.
\paragraph{Occupancy measures}
% NOTE: after acc
%These are important quantities for MDPs and will be used thoroughly.
In any MDP, the state occupancy measure of a policy~$\Policy$,
is the normalized discounted probability of reaching some~$s$, when starting from some previous state $s\Prev$, and selecting actions with~$\Policy$.
That is, $\OccupancyS(s \Given s\Prev) \coloneqq (1 - \gamma) \sum_{t=0}^\infty \gamma^t\, \Pr(s_t = s \Given s_0 = s\Prev, \Policy)$.
Similarly, the state-action occupancy is $\OccupancySA(sa \Given s\Prev) \coloneqq \OccupancyS(s \Given s\Prev)\, \Policy(a \Given s)$.
The value function of any policy can be expressed as a scalar product between $\OccupancySA$ and the reward function.
Using the vector notation, this is
$V^\Policy(s) = \langle \OccupancySA(s), R \rangle / (1-\gamma)$,
and from the initial distribution, $V_\StartDistrib^\Policy = \langle V^\Policy, \StartDistrib \rangle$.
Often, we will simply write both distributions as~$d^\Policy$.
For simplicity, the notation we use is specific to discrete distributions.
However, values and occupancy measures remain well defined for continuous state and action spaces if probability densities are used.
\paragraph{Options}
An \emph{option} is a temporally extended action \citep{sutton_1998_IntraoptionLearningTemporally}.
In this paper, an option is defined as $o = \Tuple{\Set{I}_o, \Policy_o, \beta_o}$,
where $\Set{I}_o \subseteq \States^2$ is an initiation set composed of pairs of states,
$\Policy_o \in \Policies$ is the policy that $o$ executes
and $\beta_o: \States \to \{0, 1\}$ is a termination condition.
An option is applicable at some $a_{t-1} r_{t-1} s_{t-1} a_t r_t s_t$ if $s_{t-1} s_t \in \Set{I}_o$.
With respect to the classic definition \citep{sutton_1998_IntraoptionLearningTemporally}, we have extended the initiation sets to pairs, instead of single states.
% NOTE: after acceptance
%Note that this is still an option for MDPs, because the policy remains Markovian, only the initiation set is generalized.
%
In this work, we focus on a specific class of options, called $\Mapping$-relative options
\citep{abel_2020_ValuePreservingStateAction}.
For clarity, we recall that $\Block{\cdot}_\Mapping$ and $\Block{\cdot}$ denote the inverse image of~$\Mapping$.
Given some surjective $\Mapping: \States \to \Abst\States$,
an option $o = \Tuple{\Set{I}_o, \Policy_o, \beta_o}$ is said to be \emph{$\Mapping$-relative}
if there exists two $\Abst{s}_p, \Abst{s} \in \Abst{\States}$ such that
$\Set{I}_o = \Block{\Abst{s}_p}_\Mapping \times \Block{\Abst{s}}_\Mapping$,
$\beta_o(s) = \Indicator(s \not\in \Block{\Abst{s}}_\Mapping)$,
and $\Policy_o \in \Policies_{\Abst{s}}$,
where $\Policies_{\Abst{s}} \coloneqq \Block{\Abst{s}}_\Mapping \to \Actions$
is the set of policies defined for the block.
In essence, $\Mapping$-relative options always start in some block and terminate as soon as the block changes.
Any set of options $\Options$ is $\Mapping$-relative iff all of its options are.
In the remainder of this paper, we only consider sets $\Mapping$-relative options.
Regarding the notation, we use $\Options_{\Abst{s}_p \Abst{s}}$ for the set of all options starting in $\Block{\Abst{s}_p} \Block{\Abst{s}}$,
and $\Options_{\Abst{s}} \coloneqq \cup_{\Abst{s}_p} \Options_{\Abst{s}_p \Abst{s}}$
for all options in one block.
Finally, we call \emph{policy of options} any set~$\Options$ that contains a single $\Mapping$-relative option for each pair $\Abst{s}_p \Abst{s}$.
We use this name because $\Options$ can be fully treated as a policy for the ground MDP.
$V^{\Options}$ is the value of the policy that always executes the only applicable option in~$\Options$ until each option terminates.
\section{Realizable Abstractions}
\label{sec:ra}
% General idea
This section defines Realizable Abstractions and studies the properties they satisfy.
To explain the main intuitions behind our abstractions, we use the running example of \cref{fig:grid-example} (left), which represents a ground MDP~$\MDP$, with a simple grid world dynamics.
In this work, an MDP abstraction is a pair $\Tuple{\Abst\MDP, \Mapping}$,
where $\Abst\MDP$ is a decision process over states~$\Abst\States$,
and $\Mapping: \States \to \Abst\States$ is the state mapping function.
In the example, $\Abst\States = \{\Abst{s}_1, \Abst{s}_2, \Abst{s}_3\}$.
The association of abstract states with ground blocks in the partition is intuitive, as shown by the colors in the example.
Actions and ground options, on the other hand, are much less trivial to associate.
In this work, with Realizable Abstractions, we encode the following intuition:
if an abstract transition $(\Abst{s}_1, \Abst{a}, \Abst{s}_3)$ has a high probability of occurring from~$\Abst{s}_1$ in the abstract model~$\Abst\MDP$,
then there must exist a $\Mapping$-relative option that moves the agent from block $\Block{\Abst{s}_1}$ to block $\Block{\Abst{s}_3}$ in the ground MDP,
with high probability and in a few steps.
In other words, we choose to interpret abstract transitions as representations of what is possible to replicate, we say ``realize'', in the ground MDP.
Both conditions above, in terms of probability and time, are equally important and consistent with the meaning of discounted values in MDPs.
Here, we choose $\Mapping$-relative options because they only terminate after leaving each block.
In the example, no direct transition is possible between $\Block{\Abst{s}_2}$ and $\Block{\Abst{s}_3}$.
So, we should have $\Pr(\Abst{s}_3 \Given \Abst{s}_2, \Abst{a}, \Abst\MDP) = 0$, for any~$\Abst{a}$.
Instead, selecting an appropriate value for $\Pr(\Abst{s}_3 \Given \Abst{s}_1, \Abst{a}, \Abst\MDP)$ is much more complex, as it strongly depends on the initial state of the option in the gray block.
This is at the heart of non-Markovianity in HRL.
In this work, we address this issue through a careful treatment of entry states and allowing abstractions to model second-order dependencies.
This allows us to condition the probability of the transition $({\Abst{s}_1},{\Abst{a}},{\Abst{s}_3})$ on the previous abstract state visited, which might be $\Abst{s}_2$ or $\Abst{s}_3$ in the example.
This modeling advantage motivates our choice of abstract second-order abstract MDPs.
\begin{figure}
\centering
\begin{tikzpicture}
\node (grid) [tight] {\includegraphics[width=5cm]{./imgs/grid2.pdf}};
\begin{tikzimgrelative}{grid}
\node (as1) [circle, fill=grid2-gray!70!white, inner sep=2.5pt] at ($(6.5/17, 6.5/9)$) {$\Abst{s}_1$};
\node (as2) [circle, fill=grid2-green!70!white, inner sep=2.5pt] at ($(3.5/17, 1.5/9)$) {$\Abst{s}_2$};
\node (as3) [circle, fill=grid2-yellow!70!white, inner sep=2.5pt] at ($(12.5/17, 1/9)$) {$\Abst{s}_3$};
\begin{scope}[font=\scriptsize\sffamily, gray]
\node at ($(2.5/17,3.5/9)$) {x};
\node at ($(3.5/17,3.5/9)$) {x};
\node at ($(4.5/17,3.5/9)$) {x};
\node at ($(13.5/17,2.5/9)$) {x};
\node at ($(14.5/17,2.5/9)$) {x};
\node at ($(2.5/17,4.5/9)$) {e};
\node at ($(3.5/17,4.5/9)$) {e};
\node at ($(4.5/17,4.5/9)$) {e};
\end{scope}
\end{tikzimgrelative}
\end{tikzpicture}
\hspace{3em}
\begin{tikzpicture}
\node (grid) [tight] {\includegraphics[width=5cm]{./imgs/grid2-bad.pdf}};
\begin{tikzimgrelative}{grid}
\node (as1) [circle, fill=grid2-gray!70!white, inner sep=2.5pt] at ($(6.5/17, 6.5/9)$) {$\Abst{s}_1$};
\node (as2) [circle, fill=grid2-green!70!white, inner sep=2.5pt] at ($(3.5/17, 1.5/9)$) {$\Abst{s}_2$};
\node (as3) [circle, fill=grid2-yellow!70!white, inner sep=2.5pt] at ($(12.5/17, 1/9)$) {$\Abst{s}_3$};
\begin{scope}[darkgray]
\node at ($(2.5/17,4.5/9)$) {$s_1$};
\node at ($(4.5/17,4.5/9)$) {$s_2$};
\end{scope}
\end{tikzimgrelative}
\end{tikzpicture}
\caption{(left) The running example. The ground MDP is a grid world domain and $\Abst\States = \{\Abst{s}_1, \Abst{s}_2, \Abst{s}_3\}$.
Each \textsf{\textcolor{gray}{\footnotesize e}} is an entry in $\Entries_{\Abst{s}_2 \Abst{s}_1}$
and each \textsf{\textcolor{gray}{\footnotesize x}} is an exit in $\Exits_{\Abst{s}_1}$.
(right) A different ground MDP.}
\label{fig:grid-example}
\end{figure}
% General abstractions
We now proceed to formalize all the previous intuitions.
In this work, the abstraction of an MDP~$\MDP$ is a pair $\Tuple{\Abst\MDP, \Mapping}$,
where $\Abst\MDP$ is a 2-MDP $\Abst\MDP = \Tuple{\Abst\States, \Abst\Actions, \Abst{T}, \Abst{R}, \gamma}$
with finite states and actions spaces,
and $\Mapping: \States \to \Abst\States$ is a surjective function.
Our formal statements will also be valid when $\Abst\MDP$ is an MDP, since it can also be regarded as a 2-MDP with restricted dynamics.
%
% Entries and exits
For each two distinct abstract states $\Abst{s}_p, \Abst{s} \in \Abst{\States}$,
we define the set of \emph{entry states}~$\Entries_{\Abst{s}_p \Abst{s}}$ as
the set of ground states in~$\Block{\Abst{s}}$,
at which it is possible to enter~$\Block{\Abst{s}}$ from~$\Block{\Abst{s}_p}$.
Also, the \emph{exit states}~$\Exits_{\Abst{s}}$ contains all ground states outside the block~$\Block{\Abst{s}}$ that are reachable in one transition.
In \cref{fig:grid-example}~(left), each entry in $\Entries_{\Abst{s}_2 \Abst{s}_1}$ is marked with an~\textsf{\textcolor{gray}{\footnotesize e}},
and each exit in $\Exits_{\Abst{s}_1}$ is marked with an~\textsf{\textcolor{gray}{\footnotesize x}}.
More generally,
% NOTE: after acceptance make display
$\Entries_{\Abst{s}_p \Abst{s}} \coloneqq \{s \in \Block{\Abst{s}} \mid \exists s_p \in \Block{\Abst{s}_p}, \exists a \in \Actions,\, T(s \Given s_p, a) > 0 \}$ and
$\Exits_{\Abst{s}} \coloneqq \cup_{\Abst{s}' \neq \Abst{s}} \Entries_{\Abst{s} \Abst{s}'}$.
Exit and entry states are an intuitive way to discuss the boundaries of contiguous state partitions and are often found in the HRL literature
\citep{wen_2020_EfficiencyHierarchicalReinforcement,infante_2022_GloballyOptimalHierarchical}.
There is one last possibility of entering a block, that is, through the initial distribution~$\StartDistrib$.
However, this specific case is also captured by $\Entries_{\Abst{s}\StartSym \Abst{s}}$.
The previous abstract state carries fundamental information to characterize entry states,
while knowledge of abstract states further back are not nearly as crucial and would make the model significantly more cumbersome.
For this reason, we only need to use 2-MDPs to represent the abstract MDP, without the need of $k$-MDPs with $k>2$.
% NOTE: after acceptance
%In this regard, we assume that the start states are properly mapped as $\Block{\Abst{s}\StartSym}_\Mapping = \{s\StartSym\}$.
%
% Block
A careful treatment of exits and entries is essential, as it allows us to develop a truly compositional approach where each block is treated separately.
For this purpose, associated with each abstract state, we define the \emph{block MDP}
as the portion of the original MDP that is restricted to a single block, its exit states and a new absorbing state.
\begin{definition}
Given an MDP $\MDP$ and ${\Mapping: \States \to \Abst\States}$,
we define the \emph{block MDP} of some $\Abst{s} \in \Abst\States$ as
$\MDP_{\Abst{s}} = \Tuple{\States_{\Abst{s}}, \Actions, T_{\Abst{s}}, R_{\Abst{s}}, \gamma }$,
with states $\States_{\Abst{s}} \coloneqq \Block{\Abst{s}} \cup \Exits_{\Abst{s}} \cup \{\SinkS\}$, where $\SinkS$ is a new absorbing state;
the transition function is $T_{\Abst{s}}(s, a) \coloneqq T(s, a)$ if $s \in \Block{\Abst{s}}$ and $T(s, a) \coloneqq \Det{\SinkS}$, otherwise, which is a deterministic transition to~$\SinkS$;
the reward function is $R_{\Abst{s}}(s, a) \coloneqq R(s, a)$ if $s \in \Block{\Abst{s}}$ and $0$ otherwise.
\end{definition}
Therefore, the dynamics of each block MDP remains unchanged while in the relevant block,
but is modified to reach the aborbing state with a null reward, from the exits.
With respect to analogous definitions from the literature \citep{fruit_2017_RegretMinimizationMDPs},
our exit states are \emph{not} absorbing.
This small change is essential to preserve the original occupancy distributions at the exits.
% External
Now, since any $\Mapping$-relative option is a complete policy for the block MDP of~$\Abst{s}$,
we will use $d^o_{\Abst{s}}$ to denote the state occupancy measure for policy $\Policy_o$ in~$\MDP_{\Abst{s}}$.
Since abstract transitions should only reflect the ``external'' behavior of the options at the level of blocks, regardless of the specific ground paths followed, we marginalize the occupancy measure with respect to the exit blocks.
More precisely, we define the \emph{block occupancy} measure of $\Abst{s}$ and $o \in \Options_{\Abst{s}}$ at some $s \in \Block{\Abst{s}}$ as the probability distribution $h_{\Abst{s}}^o(s) \in \Distribution{\Abst{\States} \cup \{\SinkS\}}$, with
$h_{\Abst{s}}^o(\Abst{s}' \Given s) \coloneqq \sum_{s' \in \Block{\Abst{s}'}} d^o_{\Abst{s}}(s' \Given s)$,
if $\Abst{s}' \neq \SinkS$, and $h_{\Abst{s}}^o(\SinkS \Given s) \coloneqq d^o_{\Abst{s}}(\SinkS \Given s)$, otherwise.
% Interpret the ground items
Block occupancies are perfect candidates for relating the abstract transitions to the options in the ground MDP.
Similarly, abstract rewards will be related to the total return accumulated within the block.
This second term is exactly captured by $V^o_{\Abst{s}}(s)$, the value of the option~$o$ in the block MDP of~$\Abst{s}$.
% Introduce abstract, computed quantities
These two elements, $h^o_{\Abst{s}}$ and $V^o_{\Abst{s}}$,
that are relative to the ground MDP,
will be related to analogous quantities in the abstraction.
Specifically, this work identifies that these quantities should be compared with the probability of the associated abstract transitions and the associated abstract rewards.
% NOTE: after acceptance
%Specifically, this work identifies that the ground block occupancies should be compared with the discounted probability of reaching other abstract states in the abstraction.
%Similarly, the ground block value should be related to the total reward accumulated in the corresponding abstract state.
% TODO: define these better to explain them from what they represent
Expanding these terms for 2-MDPs in any $\Abst{s}_p, \Abst{s}, \Abst{s}' \in \Abst\States$ and $\Abst{a} \in \Abst\Actions$, with $\Abst{s} \neq \Abst{s}'$,
these are:
\begin{align}
&\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') \coloneqq (1 - \gamma) (\Abst\gamma\, \Abst{T}(\Abst{s}' \Given \Abst{s}_p \Abst{s}, \Abst{a} ) + \Abst\gamma^2\, \Abst{T}_{\Abst{s}_p \Abst{s} \Abst{a}}\, \Abst{T}(\Abst{s}' \Given \Abst{s}\Abst{s}, \Abst{a})) \label{eq:computed-option-occupancy}\\*
&\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \coloneqq \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) + \Abst\gamma\, \Abst{T}_{\Abst{s}_p \Abst{s} \Abst{a}}\, \Abst{R}(\Abst{s}\Abst{s}, \Abst{a}) \label{eq:computed-option-value}
\end{align}
with $\Abst{T}_{\Abst{s}_p \Abst{s} \Abst{a}} = \frac{\Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})}$.
Their structure is mainly motivated by the fact that these expressions sum over an indefinite number of self-loops in~$\Abst{s}$ before transitioning to a different state in the 2-MDP.
Equation \ref{eq:computed-option-occupancy} encodes the discounted cumulative probability of visiting $\Abst{s}'$ immediately after $\Abst{s}$ in the abstract model, which is $\sum_{t=0}^\infty \gamma^t \Pr(\Abst{s}_t = \Abst{s}' \Given \Abst{s}_{0:t-1} = \Abst{s}, \Abst{a}_{1:t} = \Abst{a}, \Abst{s}_{-1} = \Abst{s}_p, \Abst\MDP )$. This expression is similar to what the occupancy measure captures in the ground MDP, with the difference that the action becomes an option and, instead of a single state, $\Abst{s}$ is associated with all states in the block $\Block{\Abst{s}}$. Expanding the probability above leads to Equation \ref{eq:computed-option-occupancy}. In particular, $\Abst{T}_{\Abst{s}_p \Abst{s} \Abst{a}}$ is the result of the geometric series $\Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a} ) \sum_t \gamma^t \Abst{T}(\Abst{s} \Given \Abst{s} \Abst{s}, \Abst{a} ) $ that accounts for an indefinite number of self loops in $\Abst{s}$.
Analogously, Equation \ref{eq:computed-option-value} is the discounted cumulative return accumulated in $\Abst{s}$. All self loops in $\Abst{s}$
contribute with a reward of $\Abst{R}(\Abst{s}\Abst{s}, \Abst{a})$, which explains the second term in the sum. The first term is the reward achieved after the first transition in $\Abst{s}$.
Note that if the abstraction is a standard 1-MDP, then $\Abst{R}(\Abst{s}\Abst{s}, \Abst{a}) = \Abst{R}(\Abst{s}_p\Abst{s}, \Abst{a})$ and $\Abst{T}(\Abst{s}' \Given \Abst{s}_p \Abst{s}, \Abst{a}) = \Abst{T}(\Abst{s}' \Given \Abst{s} \Abst{s}, \Abst{a})$ the expressions simplify to:
\begin{align}
&\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') \coloneqq \frac{(1 - \gamma)\, \Abst\gamma\, \Abst{T}(\Abst{s}' \Given \Abst{s}, \Abst{a} )}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}, \Abst{a})} &
&\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \coloneqq \frac{\Abst{R}(\Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}, \Abst{a})} \label{eq:computed-option-mdp}
\end{align}
which does not depend on $\Abst{s}_p$.
% Realizable
\paragraph{Realizable Abstractions}
Using the concepts above, we are now ready to provide a complete description of our MDP abstractions.
We say that an abstract action is \emph{realizable}
if the behavior described by the abstract transitions and rewards can be replicated (realized) in the ground MDP.
% NOTE: after acceptance
%More precisely, realizable actions can be associated with options in the ground MDP which attain the required occupancy and value.
\begin{definition}\label{def:realizability}
Given an MDP~$\MDP$ and an abstraction~$\Tuple{\Abst\MDP, \Mapping}$,
any abstract tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$
is said $(\PRealizableR, \PRealizableT)$-\emph{realizable}
if there exists a $\Mapping$-relative option~$o \in \Options_{\Abst{s}_p \Abst{s}}$, such that
\begin{align}
(1 - \gamma) (\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - V^o_{\Abst{s}}(s)) &\le \PRealizableR \label{eq:realizabilityR}\\*
\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') - h^{o}_{\Abst{s}}(\Abst{s}' \Given s) &\le \PRealizableT \label{eq:realizabilityT}
\end{align}
for all $\Abst{s}' \neq \Abst{s}$ and $s \in \Entries_{\Abst{s}_p \Abst{s}}$.
The option~$o$ is called $(\PRealizableR, \PRealizableT)$-\emph{realization} of $(\Abst{s}_p \Abst{s}, \Abst{a})$.
An abstraction $\Tuple{\Abst\MDP, \Mapping}$ is said $(\PRealizableR, \PRealizableT)$-realizable in~$\MDP$
if any $(\Abst{s}_p \Abst{s}, \Abst{a}) \in \Abst{\States}^2 \times \Abst\Actions$
with $\Abst{s}_p \neq \Abst{s}$ also is.
A $(0,0)$-realizable abstraction is \emph{perfectly realizable}.
\end{definition}
% Bounded optimism
This definition essentially requires that the desired block occupancy and value, computed from the abstraction,
should be similar to the ones that are possible in the ground MDP from each entry state.
The case $\Abst{s}_p \neq \Abst{s}$ is the most important.
The case $\Abst{s}_p = \Abst{s} = s\StartSym$ is only needed to require similar starting distributions at the two levels.
% NOTE: after acceptance
%The importance of entry states comes from the fact that quantifying over all $s \in \Block{\Abst{s}}$ would make \cref{def:realizability} hard to satisfy for large state partitions.
We observe that if the abstraction is an MDP, as is often the case in the literature \citep{li_2006_UnifiedTheoryState,ravindran_2002_ModelMinimizationHierarchical},
\cref{eq:computed-option-occupancy,eq:computed-option-value} simplify and our definition can still be applied.
Finally, we note that the scale factor of $(1-\gamma)$ was added to~\eqref{eq:realizabilityR} to obtain two parameters $\PRealizableR$ and $\PRealizableT$ in the same range of $[0, 1]$,
although the appropriate magnitude for such values should scale with $(1-\gamma)$.
%
Any given $\PRealizableR$ and $\PRealizableT$ put a restriction not only on the abstract decision process but also on the possible mapping functions.
Indeed, some partitions may not admit any dynamics that satisfies \cref{def:realizability} over the induced abstract states.
% NOTE: after acceptance
%especially if some entry state can achieve very different transition probabilities or rewards.
Consider, for example, the ground MDP and the partition of \cref{fig:grid-example}~(right).
If the grid world is deterministic, there exists an option~$o$ for which
$h^o_{\Abst{s}_1}(\Abst{s}_3 \Given s_2) = \gamma^{11} \approx 0.57$,
but, due to the higher number of steps required from~$s_1$,
$h^o_{\Abst{s}_1}(\Abst{s}_3 \Given s_1) = \gamma^{21} \approx 0.34$.
Let $\gamma=0.95$ and $\Abst{\MDP}$ be so that, for some~$\Abst{a}$,
$\tilde{h}_{\Abst{s}_2 \Abst{s}_1 \Abst{a}}(\Abst{s}_3) = 0.6$.
Then, due to the very diverse behaviors from $s_1$ and~$s_2$, the tuple $(\Abst{s}_2 \Abst{s}_1 \Abst{a})$ is not realizable with $\PRealizableT = 0.09$ in \cref{fig:grid-example}~(right),
while it is in the MDP of \cref{fig:grid-example} (left).
% NOTE: after acceptance
%Similar counterexamples can also be constructed for rewards.
% Any def is good. Is our abstraction better?
% NOTE: after acceptance
%We have now defined realizable MDP abstractions and described their meaning.
%However, the HRL literature already includes many notions of abstractions.
%A new definition is only valuable if it is applicable, which we have discussed already,
%and if it possesses strong properties.
%In this section, we show that any abstract policy for a realizable abstraction can be
%transformed into a near-optimal policy for the ground MDP in a purely compositional way.
The most important feature of our abstractions is that
any policy for a Realizable Abstraction can be associated with a near-optimal policy for the ground MDP, which can be expressed as a simple composition of $\Mapping$-relative options.
% Realizations
Indeed, if some abstraction $\Tuple{\Abst\MDP, \Mapping}$ is $(\PRealizableR, \PRealizableT)$-realizable,
then it is possible to associate to each tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$ the option that realizes it.
In the following,
we say that some policy of options~$\Options$ is the \emph{realization} of some abstract policy~$\Abst\Policy$,
if $\Options$ contains the realization of every tuple $(\Abst{s}_p \Abst{s}, \Abst\Policy(\Abst{s}_p \Abst{s}))$.
We can finally state the main property below. Its proof is in the appendix.
\begin{restatable}{theorem}{realizableabstvalue}\label{th:realizab-abstraction-value}
Let $\Tuple{\Abst\MDP, \Mapping}$ be an $(\PRealizableR, \PRealizableT)$-realizable abstraction of an MDP~$\MDP$.
Then, if $\Options$ is the realization of some abstract policy $\Abst{\Policy}$,
then, for any $\Abst{s}_p \in \Abst\States$, $s \in \Exits_{\Abst{s}_p}$, $\Abst{s} = \Mapping(s)$,
\begin{equation}\label{eq:realizab-abstraction-value}
\Abst{V}^{\Abst\Policy}(\Abst{s}_p \Abst{s}) - V^{\Options}(s) \le \frac{\PRealizableR}{(1 - \gamma)^2} + \frac{\PRealizableT\, \abs{\Abst{\States}}}{(1 - \gamma)^2 (1 - \Abst\gamma)}
\end{equation}
Moreover, if the marginal initial distributions correspond,
$\forall \Abst{s}.\, \Abst\StartDistrib(\Abst{s}) = \sum_{s \in \Block{\Abst{s}}} \StartDistrib(s)$,
the same bound also holds for $\Abst{V}^{\Abst\Policy}_{\Abst{\StartDistrib}} - V^{\Options}_\StartDistrib$.
\end{restatable}
% Immediate meaning and different DP
For simplicity, in the following statements, we will assume that
$\forall \Abst{s}.\, \Abst\StartDistrib(\Abst{s}) = \sum_{s \in \Block{\Abst{s}}} \StartDistrib(s)$
holds true for realizable abstractions.
The bound in \cref{th:realizab-abstraction-value} relates the value of~$\Abst\Policy$ in the abstract~$\Abst\MDP$ with
the value of the realization~$\Options$ in the ground~$\MDP$.
Essentially, this theorem proves that $(\PRealizableR,\PRealizableT)$-realizability is sufficient to
have formal guarantees on the minimal value achieved by the realization.
% NOTE: after acceptance
%The importance of \cref{th:realizab-abstraction-value} comes from the fact that realizations can be computed in a compositional way,
%because there is no global optimization involved in computing the ground policy of options.
%Indeed, for an option to be part of the realization, it suffices that it satisfies the constraints in \cref{eq:realizabilityT,eq:realizabilityR}.
%Since these constraints are expressed in terms of the block MDP,
%their computation is completely independent of all the other blocks and options.
Importantly, such a value can be achieved by a composition of options
that are only characterized by local constraints on the individual block MDPs.
In this light, the value loss in \eqref{eq:realizab-abstraction-value} is the maximum cost to be paid for finding a policy
as a union of shorter policies, without any global optimization.
% How large
To evaluate the scale of the bound, we note that $\PRealizableT$ and $\PRealizableR$ are in $[0, 1]$,
and that $\Abst\gamma \le \gamma$.
Also, the size of abstract state space~$\Abst{S} \coloneqq \abs{\Abst\States}$ is always finite,
and the size of the ground state space, which is usually very large or infinite, does not appear.
\cref{th:realizab-abstraction-value} does not yet imply near-optimality of~$\Options$ in~$\MDP$,
because pessimistic abstractions with null target occupancies and block values would also satisfy \cref{def:realizability}, trivially.
Thus, in addition to realizability, we require that abstractions should be always optimistic, in the following sense.
% NOTE: after acceptance
%Thus, taking inspiration from search heuristics, we say that admissible abstractions should be always optimistic.
\begin{definition}\label{def:admissibility}
An abstraction $\Tuple{\Abst\MDP, \Mapping}$ of an MDP~$\MDP$ is \emph{admissible} if
for any $\Abst{s}_p, \Abst{s}$ with $\Abst{s}_p \neq \Abst{s}$
and option~$o \in \Options_{\Abst{s}_p \Abst{s}}$,
there exists an abstract action $\Abst{a} \in \Abst\Actions$, such that
$\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') \ge h^{o}_{\Abst{s}}(\Abst{s}' \Given s)$ and
$\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge V^o_{\Abst{s}}(s)$,
for all $\Abst{s}' \neq \Abst{s}$ and $s \in \Entries_{\Abst{s}_p \Abst{s}}$.
\end{definition}
As we show below, admissible abstractions provide optimistic estimates of ground values.
Together with \cref{th:realizab-abstraction-value}, this property allows us
to guarantee the near-optimality of the realizations in~$\MDP$.
\begin{restatable}{proposition}{admissiblevalues}\label{th:admissible-values}
Let $\Tuple{\Abst\MDP, \Mapping}$ be an admissible abstraction of an MDP~$\MDP$.
Then, for any ground policy~$\Policy$, there exists an abstract policy~$\Abst\Policy$,
such that $\Abst{V}^{\Abst\Policy}(\Abst{s}_p \Abst{s}) \ge V^{\Policy}(s)$,
at any $\Abst{s}_p \in \Abst\States$, $s \in \Exits_{\Abst{s}_p}$, $\Abst{s} = \Mapping(s)$,
and $\Abst{V}^{\Abst\Policy}_{\Abst\StartDistrib} \ge V^{\Policy}_\StartDistrib$.
\end{restatable}
\begin{restatable}{corollary}{realizaboptimalvalue}\label{th:realizab-optimal-value}
Any realization of the optimal policy of an admissible and $(\PRealizableR, \PRealizableT)$-realizable abstraction is $\PAccuracy$-optimal, for
$\PAccuracy = \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2(1 - \Abst\gamma)}$,
\end{restatable}
% TODO: continue here checking
% Information content
%Realizable abstractions are flexible representations because they can encode a variable amount of information content.
%If the ground domain is a goal MDP with a single initial state, we might consider two extremes.
%On the one hand, the abstraction might be composed of just two abstract states: a goal and a non-goal state.
%Although this might be an admissible and perfectly realizable abstraction, for a suitable transition function, it provides no information content.
%Realizing the only option would be as complex as solving the entire MDP.
%On the other extreme, any MDP~$\MDP$ can be also abstracted by itself as $\Tuple{\MDP, \Identity}$,
%where $\Identity: x \mapsto x$ is the identity function.
%Clearly, many intermediate state partitions are also possible, although some will not be perfectly realizable.
Realizable Abstractions are flexible representations that can capture both very coarse state partitions and much more fine-grained subdivisions.
For example, on one extreme, we verify that any MDP~$\MDP$ can be abstracted by itself as $\Tuple{\MDP, \Identity}$, where $\Identity: x \mapsto x$ is the identity function.
\begin{restatable}{proposition}{selfexactabstraction}\label{th:self-abstractions}
Any MDP~$\MDP$ admits $\Tuple{\MDP, \Identity}$ as an admissible and perfectly realizable abstraction.
\end{restatable}
% TODO: also say that optimistic rewards make it just realizable
Although our abstractions are able to represent compressions along the time dimension,
they are not restricted to those.
As a special case, they can capture any MDP homomorphism \citep{ravindran_2002_ModelMinimizationHierarchical,ravindran_2004_ApproximateHomomorphismsFramework}
and any stochastic bisimulation \citep{givan_2003_EquivalenceNotionsModel}.
These two formalisms have equivalent expressive power \citet[Theorem~6]{ravindran_2004_AlgebraicApproachAbstraction} and
their compression takes place only with respect to parallel symmetries of the state space.
We report the main results for MDP homomorphisms here.
The relevant definitions and proofs are deferred to \cref{sec:app:homomorphism}.
\begin{restatable}{proposition}{realizablehomomorph}\label{th:realizable-homomorphisms}
If $\Tuple{f, \{g_s\}_{s \in \States}}$ is an MDP homomorphism from~$\MDP$ to~$\Abst\MDP$,
then $\Tuple{\Abst\MDP, f}$ is an admissible and perfectly realizable abstraction of~$\MDP$.
\end{restatable}
\begin{restatable}{proposition}{realizablehomomorphback}\label{th:realizable-homomorphisms-back}
There exists an MDP~$\MDP$ and an admissible and perfectly realizable abstraction $\Tuple{\Abst\MDP, \Mapping}$
for which no surjections $\{g_s\}_{s \in \States}$ exist such that $\Tuple{\Mapping, \{g_s\}_{s \in \States}}$
is an MDP homomorphism from~$\MDP$ to~$\Abst\MDP$.
\end{restatable}
% TODO: add a sentence: the same is true for bisimulation
\paragraph{Reducing the effective horizon}
A reduction in the effective planning horizon, which scales with $(1-\gamma)^{-1}$ for the ground MDP, can have a very strong impact on learning.
As we already know, $\Abst\gamma \le \gamma$.
Moreover, this inequality can become strict for Realizable Abstractions, as long as the two discount factors satisfy \cref{def:realizability}.
However, to make the relation between $\gamma$ and $\Abst\gamma$ more explicit, we prove the following proposition.
\begin{restatable}{proposition}{admissibleimpliesgoodgamma}\label{th:admissible-implies-good-gamma}
If $\Tuple{\Abst\MDP, \Mapping}$ is an admissible abstraction for an MDP~$\MDP$,
then, for any tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$ with $\Abst{s}_p \neq \Abst{s}$,
option $o \in \Options_{\Abst{s}_p \Abst{s}}$,
and $s \in \Entries_{\Abst{s}_p \Abst{s}}$,
it holds
$h^o_{\Abst{s}}(\Abst{s} \Given s) \ge (1-\Abst\gamma) \max\{1, V^o_{\Abst{s}}\}$.
% NOTE: after acceptance
% \begin{align}
% &h^o_{\Abst{s}}(\Abst{s} \Given s) \ge 1-\Abst\gamma \label{eq:abst-gamma-h} \\*
% &V^o_{\Abst{s}} \le h^o_{\Abst{s}}(\Abst{s} \Given s) / (1-\Abst\gamma) \label{eq:abst-gamma-V}
% \end{align}
\end{restatable}
This statement is composed of two results,
$h^o_{\Abst{s}}(\Abst{s} \Given s) \ge 1-\Abst\gamma$,
which only constrains the occupancy,
and $V^o_{\Abst{s}} \le h^o_{\Abst{s}}(\Abst{s} \Given s) / (1-\Abst\gamma)$ which also involves value.
These inequalities encode the necessary conditions for reducing the effective horizon in the abstraction.
The first inequality says that $\Abst\gamma$ can only be low if the occupancy in every block is high.
In particular, if there exists an option~$o$ that leaves some $\Block{\Abst{s}}$ in one step,
then $h^o_{\Abst{s}}(\Abst{s} \Given s) = 1-\gamma$ and $\Abst\gamma = \gamma$ is the only feasible choice.
The second says that $\Abst\gamma$ can only be low if $V^o_{\Abst{s}}$ is also low with respect to $h^o_{\Abst{s}}$.
In particular, if $o$ collects in $\Block{\Abst{s}}$ a reward of 1 at each step,
then $V^o_{\Abst{s}} = h^o_{\Abst{s}}(\Abst{s} \Given s) / (1-\gamma)$ and $\Abst\gamma = \gamma$ is the only feasible choice.
This allows us to conclude that a time compression in the abstraction is possible only if:
\begin{enumerate*}[label=(\roman*)]
\item the changes between blocks occur at some lower timescale;
\item rewards are temporally sparse.
\end{enumerate*}
This confirms some common intuitions among the HRL literature, while it shows that sparse rewards are also important.
% NOTE: after acceptance
%In fact, if either of the conditions above are not verified, no time compression is possible.
%Importantly, $\Abst\gamma \coloneqq \gamma$ is always a feasible choice.
\paragraph{Learning realizations}
% NOTE: after acceptance
%Realizable abstractions have very desirable properties for HRL, including compositionality and near-optimality.
To conclude this section,
we now study how each realizing option can be learned from experience.
Although the constraints in \cref{def:realizability} could be direcly used,
here we propose a slight relaxation that is more suitable for online learning.
Specifically, instead of quantifying for each entry state $\Entries_{\Abst{s}_p \Abst{s}}$ of the block,
we consider some initial distribution $\nu \in \Distribution{\Entries_{\Abst{s}_p \Abst{s}}}$.
% NOTE: after accept
%This distribution allows us to marginalize with respect to initial states.
%and express realizability without mentioning individual ground states.
\begin{definition}
Given an MDP~$\MDP$ and an abstraction~$\Tuple{\Abst\MDP, \Mapping}$,
an abstract tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$, with $\Abst{s}_p \neq \Abst{s}$,
is $(\PRealizableR, \PRealizableT)$-\emph{realizable from} a distribution
$\nu \in \Distribution{\Entries_{\Abst{s}_p \Abst{s}}}$,
if there exists a $\Mapping$-relative option~$o \in \Options_{\Abst{s}_p \Abst{s}}$, such that
$\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') - h^{o}_{\nu}(\Abst{s}') \le \PRealizableT$
and $(1 - \gamma) (\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - V^o_{\nu}) \le \PRealizableR$,
for all $\Abst{s}' \neq \Abst{s}$,
where $h^{o}_{\nu}(\Abst{s}') \coloneqq \sum_{s} h^o_{\Abst{s}}(\Abst{s}' \Given s)\, \nu(s)$ and
$V^{o}_{\nu} \coloneqq \sum_{s} V^o_{\Abst{s}}(s)\, \nu(s)$.
The option~$o$ is the realization of $(\Abst{s}_p \Abst{s}, \Abst{a})$ from~$\nu$.
\label{def:realizability-from}
\end{definition}
Being a relaxed definition,
every realization is a realization from any distribution, but not vice versa.
However, given some policy of options~$\Options$,
if each $o \in \Options$ is a $(\PRealizableR, \PRealizableT)$-realization of a tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$ from some~$\nu$, and $\nu$ is the entry distribution of $\Block{\Abst{s}}$ from~$\Block{\Abst{s}_p}$ given~$\Options$,
then, $\Abst{V}^{\Abst\Policy}_{\Abst{\StartDistrib}} - V^{\Options}_\StartDistrib$
still satisfy the bound in \cref{th:realizab-abstraction-value}.
The advantage is that, due to marginalization, the terms $h^o_\nu$ and $V^o_\nu$ are no longer dependent on ground states.
This means that realizability from distribution consists exactly of $\abs{\Abst\States}$ constraints,
of which $\abs{\Abst\States}-1$ come from the block occupancies and one from the value.
In this work, we identify two techniques for learning realizations: by solving Constrained MDPs, or by Linear Programming.
The Linear Programming formulation provides insteresting insights and is discussed in \cref{sec:app:lp}.
However, realizing with Constrained MDPs is the preferred approach, and it is the one discussed here.
%
Unlike standard RL, CMDPs allow the encoding of both soft and hard constraints.
This field has received attention because of its relevance for RL and the encoding of hard constraints in safety-critical systems.
By expressing the realizability problem as a CMDP, we do not restrict ourselves to a specific technique.
Rather, we could realize abstract actions with any online RL algorithm for CMDPs.
This is especially relevant since the ground MDP may be non-tabular.
% NOTE: after acc
%in general, thus preventing the application of the most standard techniques.
Fortunately, there are many general RL algorithms for CMDPs already available
\citep{achiam_2017_ConstrainedPolicyOptimization,zhang_2020_FirstOrderConstrained,ding_2020_NaturalPolicyGradient,ding_2022_ConvergenceSampleComplexity,ding_2023_LastiterateConvergentPolicy,wachi_2024_SurveyConstraintFormulations}.
%NOTE: after acc
%and more are expected to be developed in the near future due to the relevance of this framework.
Among all $\Abst{S}$ constraints of \cref{def:realizability-from},
we choose to represent the $\Abst{S}-1$ inequalities for the target occupancies as hard constraints
and the single inequality for the value as a soft constraint.
By assuming the realizability of each abstract tuple,
% NOTE: after acc
%Since we will assume that each $(\Abst{s}_p \Abst{s}, \Abst{a})$ is indeed $(\PRealizableR, \PRealizableT)$-realizable,
the option $o^* \in \Options_{\Abst{s}_p \Abst{s}}$, obtained as the maximization of the soft objective~$V^o_\nu$,
will satisfy all the $\Abst{S}$ original constraints.
To express the hard constraints, we observe that
$h^{o}_{\nu}(\Abst{s}') = \sum_{s, s' \in \States} d^o_{\Abst{s}}(s' \Given s)\, \Indicator(s' \in \Block{\Abst{s}'})\, \nu(s) = (1-\gamma)\, V^o_{\nu,\Abst{s}'}$,
% NOTE: after accept make dismplay math
%\begin{align}\label{eq:realize-cmdp-reduction-constraints}
% h^{o}_{\nu}(\Abst{s}') =
% \sum_{s \in \States} h^o_{\Abst{s}}(\Abst{s}' \Given s)\, \nu(s) =
% \sum_{s, s' \in \States} d^o_{\Abst{s}}(s' \Given s)\, \Indicator(s' \in \Block{\Abst{s}'})\, \nu(s) =
% (1-\gamma)\, V^o_{\nu,\Abst{s}'}
%\end{align}
where $V^o_{\nu,\Abst{s}'}$ is the value function of~$o$ in the MDP
$\Tuple{\States_{\Abst{s}}, \Actions, T_{\Abst{s}}, R'_{\Abst{s}'}, \gamma }$, with
$R'_{\Abst{s}'}(s, a) \coloneqq \Indicator(s \in \Block{\Abst{s}'})$.
The only difference from this MDP and the block MDP $\MDP_{\Abst{s}}$ is that a reward of 1 is placed in~$\Block{\Abst{s}'}$, while every other internal reward is~0.
This means that we can reformulate the problem of realizing any tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$ in~$\MDP$ as:
\begin{equation}\label{eq:realize-cmdp-reduction}
\argmax_{\Policy \in \Policies} V^\Policy_{\nu} \qquad s.t. \quad V^\Policy_{\nu,\Abst{s}'} \ge \frac{\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') - \PRealizableT}{1 - \gamma} \quad \forall \Abst{s}' \neq \Abst{s}
\end{equation}
In other words, this is a CMDP with auxiliary reward functions~$R'_{\Abst{s}'}$ and associated lower limits $l_{\Abst{s}'} \coloneqq (\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') - \PRealizableT) / (1 - \gamma)$.
Its solution can be seen as a $\Mapping$-relative option for~$\MDP$.
% NOTE after acc
%The output is a policy for the block MDP~$\MDP_{\Abst{s}}$, which can be equivalently seen as a $\Mapping$-relative option for the full MDP~$\MDP$.
\section{\Ouralg: a new HRL algorithm}
\label{sec:algorithm}
\begin{algorithm}[t]
\caption{\Ouralg}
\label{alg:main}
%
\KwIns{\,MDP simulator $\MDP$, abstraction $\Tuple{\Abst\MDP, \Mapping}$, and parameters $\PRealizableR$, $\PRealizableT$, $\POptionSubopt$.}
\BlankLine
\ForEach{$(\Abst{s}_p \Abst{s}, \Abst{a})$}{
$\Algorithm(\Abst{s}_1 \Abst{s}_2, \Abst{a}_1) \gets \FRealizer(\MDP, \Block{\Abst{s}}, \tilde{h}_{s_p s a}, \PRealizableT)$ \tcp*{Online RL algorithm for CMDPs}
$\Realization(\Abst{s}_1 \Abst{s}_2, \Abst{a}_1) \gets \Const{null}$ \tcp*{policy of options}
}
$s_p \gets s\StartSym$;\, $s \gets \MDP.\FReset()$ \;
\Repeat{
$\Abst\Policy \gets \FValueIteration(\Abst\MDP, \frac{1}{1-\gamma} \log \frac{2}{(1-\gamma) \PAccuracy})$ \label{alg:main-vi}\;
\Repeat{
$\Abst{s}_p \Abst{s} \gets \Mapping(s_p)\, \Mapping(s)$ \label{alg:main-exploit-start}\;
$\Abst{a} \gets \Abst\Policy(\Abst{s}_p \Abst{s})$\;
\uIf{$\Realization(\Abst{s}_p \Abst{s}, \Abst{a})$ is not null}{
$s_p s \gets \FRollout(\MDP, \Realization(\Abst{s}_p \Abst{s}, \Abst{a}))$ \label{alg:main-exploit} \tcp*{until $s \in \Exits_{\Abst{s}}$}
}
\Else{
$s_p s \gets \Algorithm(\Abst{s}_p \Abst{s}, \Abst{a}).\FRollout()$ \label{alg:main-explore} \tcp*{until $s \in \Exits_{\Abst{s}}$}
\If(\label{alg:line:main-new-option}){$\Algorithm(\Abst{s}_p \Abst{s}, \Abst{a}).\DEnough$}{
$\Realization(\Abst{s}_p \Abst{s}, \Abst{a}), \Est{V} \gets \Algorithm(\Abst{s}_p \Abst{s}, \Abst{a}).\FGet()$ \label{alg:line:main-return-option}\;
$\Est{V}_{\text{opt}} \gets \min \{ \Est{V} + \frac{\PRealizableR}{1 - \gamma} + \POptionSubopt,\, \frac{1}{1-\gamma} \}$\;
\If(\label{alg:line:main-update-block}){$\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} > \Est{V}_{\text{opt}}$}{
$\Abst\MDP \gets \FAbstractOneR(\Abst\MDP, (\Abst{s}_p \Abst{s}, \Abst{a}), \Est{V}_{\text{opt}})$\;
$s_p s \gets \FRollout(\MDP)$ \tcp*{conclude episode}
\Break\;
}
}
$s_p s \gets \FRollout(\MDP)$ \tcp*{conclude episode}
}
}
}
%
%\vspace{1ex} % NOTE: after accept
\CustomFn{\FAbstractOneR{$\Abst\MDP$, $(\Abst{s}_p \Abst{s}, \Abst{a})$, ${V}$}}{
\lForEach{$\Abst{s}_p' \notin \{\Abst{s}_p, \Abst{s}\}$}{
$V^-_{\Abst{s}_p' \Abst{s} \Abst{a}} \gets \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}}$
}
$\Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) \gets \max\{0, \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) + {V} - \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \}$\;
\lIf{$\Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) = 0$}{
$\Abst{R}(\Abst{s} \Abst{s}, \Abst{a}) \gets {V} \left( \frac{\Abst\gamma \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst\gamma \Abst{T}(\Abst{s} \Given \Abst{s} \Abst{s}, \Abst{a})} \right)^{-1}$ \label{alg:line:abstractoner-after-ss}
}
\lForEach{$\Abst{s}_p' \notin \{\Abst{s}_p, \Abst{s}\}$}{
$\Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) \gets \min\{1, \Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + V^-_{\Abst{s}_p' \Abst{s} \Abst{a}} - \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} \}$ \label{alg:line:abstractoner-other-sp}
}
%\KwRet $\Abst\MDP$\;
}
\end{algorithm}
Taking advantage of the properties of Realizable Abstractions, in this section, we develop a new sample efficient HRL algorithm called \emph{RARL} (Realizable Abstractions RL).
The algorithm learns a ground policy of options in a compositional way.
Moreover, in case the rewards of the abstraction given in input are strongly overestimated,
\Ouralg\ can correct them and update the abstraction accordingly.
The complete procedure is shown in \cref{alg:main}.
In input, we assume that some abstraction $\Tuple{\Abst\MDP, \Mapping}$ is given but it is m,
the algorithm only accesses the ground MDP~$\MDP$ through online simulations.
The appropriate values for the other input parameters will be described later in \cref{as:good-initial-abstraction,as:good-realizer}.
Initially, for each abstract tuple, \Ouralg\ instantiates one individual online RL algorithm for CMDPs.
% NOTE: after acc
%These will be used to optimize the problem in Eq.~\eqref{eq:realize-cmdp-reduction} with online samples.
The dictionary~$O$, which contains all the realizing options, is initially empty.
At convergence,
after all relevant tuples have been realized,
the algorithm repeatedly executes the lines \ref{alg:main-exploit-start}--\ref{alg:main-exploit}.
In this exploitation phase,
the abstract policy is responsible for selecting the option to execute.
During the exploration phase, instead, the algorithm reaches some block for which no option is already known.
In this case, the online CMDP solver has full control over the samples collected in block~$\Block{s}$ (line~\ref{alg:main-explore}).
When the CMDP solver finds a near-optimal option for the block (\cref{alg:line:main-new-option}), as in \cref{as:good-realizer},
the option is returned, along with its associated value (\cref{alg:line:main-return-option}).
These are the estimated $\Policy$ and $V^\Policy_\nu$ of Eq.~\eqref{eq:realize-cmdp-reduction}.
Importantly, each tuple is realized at most once.
Then, whenever the block value of the realization is below some threshold (line~\ref{alg:line:main-update-block}),
the algorithm calls \FAbstractOneR, which updates the rewards of $\Abst\MDP$ to correct for this mismatch.
In this case, the break statement triggers a new re-planning in $\Abst\MDP$ with Value Iteration,
which is executed for the number of iterations specified in input.
%When exploring, since realizing options are not known, little guarantees can be made.
%Thus, we discard all the following samples for that episode.
\paragraph{Sample complexity}
In this conclusive section, we provide formal guarantees on the sampe efficiency of \Ouralg.
% NOTE: after acceptance
%We first define how we measure sample complexity.
%Let $\Policy_t$ be the policy that some algorithm~$\Algorithm$ executes in episode~$t$.
%For some $\PAccuracy > 0$, the sample complexity of $\Algorithm$ is defined as the total number of episodes~$t$ in which $\Policy_t$ is not $\PAccuracy$-optimal, meaning
%$N_\PAccuracy \coloneqq \abs{\{t \in \Naturals_+: V^* - V^{\Policy_t} > \PAccuracy\}}$.
%This is analogous to the sample complexity of exploration of \citet{kakade_2003_SampleComplexityReinforcement}, expressed over episodes.
%
%An RL algorithm $\Algorithm$ is PAC if,
%for any unknown MDP~$\MDP$ and positive parameters $\PAccuracy$ and~$\PConfidence$,
%with probability exceeding $1-\PConfidence$,
%the sample complexity~$N_\PAccuracy$ of~$\Algorithm$ is less than some polynomial in the relevant quantities.
%%
%The notion just presented captures the sample complexity for the outer RL algorithm,
%which continues running indefinitely in the MDP.
%On the other hand, we define sample complexity for CMDPs as the number of samples required to find near-optimal policies.
%
Since the algorithm is modular and depends on the specific CMDP algorithm adopted,
we first characterize PAC online algorithms for CMDPs.
An RL algorithm $\Algorithm$ is PAC-Safe if, for any unknown CMDP~$\MDP$
and positive parameters $\PMaxViolation, \POptionSubopt$ and $\PConfidence$, whenever $\Feasible\Policies$ is not empty,
with probability exceeding $1 - \PConfidence$,
$\Algorithm$ returns some $\POptionSubopt$-optimal and $\PMaxViolation$-feasible policy in~$\Feasible[,\PMaxViolation]\Policies$.
Moreover, the number of episodes collected from~$\MDP$
must be less than some polynomial in the relevant quantities.
\begin{assumption}[PAC-Safe algorithms]\label{as:good-realizer}
\FRealizer is a PAC-Safe online RL algorithm with parameters $\POptionSubopt, \PMaxViolation$ and confidence ${1 - \PConfidence/(2\Abst{S}^2 \Abst{A})}$,
where $\POptionSubopt$ is the input of \Ouralg.
\end{assumption}
%Before stating the main result, we list all assumptions.
%The first one simply characterizes the CMDP solvers, which should possess formal guarantees in order to obtain guarantees for the global algorithm.
The second assumption ensures that the input abstraction is admissible,
and the transition function $\Abst{T}$ is $\PRealizableT$-realizable.
The same is not assumed for rewards, which can be severely overestimated by~$\Abst\MDP$.
\begin{assumption}[Optimism of $\Abst\MDP$]\label{as:good-initial-abstraction}
Let $\Tuple{\Abst\MDP, \Mapping}$ and $\PRealizableT, \PRealizableR$ be the inputs of \Ouralg.
We assume that $\Tuple{\Abst\MDP, \Mapping}$ is admissible and that there exists some admissible
$(\PRealizableR, \PRealizableT)$-realizable abstraction $\Tuple{\Abst{\MDP}^*, \Mapping}$,
in which $\Abst{\MDP}^*$ only differs from $\Abst\MDP$ by its reward function
and $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge \tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}}$ for all $\Abst{s}_p, \Abst{s}, \Abst{a}$.
\end{assumption}
% TODO: say that M^* is unknown!
The main intuition that we use to prove the sample complexity is that,
although sampling occurs in $\MDP$, all decisions of \Ouralg\ take place at the level of blocks and high-level states.
This allows us to use $\Abst\MDP$ as a proxy to refer to the returns that are possible in~$\MDP$.
Moreover, thanks to the admissibility ensured by \cref{as:good-initial-abstraction},
we can show that \Ouralg\ is optimistic in the face of uncertainty,
% NOTE: after accept
%similarly to other PAC algorithms, such as \textsc{R-Max} \citep{brafman_2003_RMaxGeneralPolynomial},
because the overestimated rewards of $\Abst\MDP$ play the role of exploration bonuses for tuples that have not yet been realized.
%
%Then, we can define the set of ``known'' abstract tuples as those for which the algorithm has found a realizing option:
%$\Known_t \coloneqq \{(\Abst{s}_p \Abst{s}, \Abst{a}) \Given O_t(\Abst{s}_p \Abst{s}, \Abst{a}) \text{ is not null}\}$.
%
% NOTE: after accept
%To discuss the third and last assumption, we observe that the algorithm does not try to realize consecutive blocks in the same episode.
%In other words, the control is passed to some \FRealizer in line~\ref{alg:main-explore}
%only if an option for block $\Block{\Abst{s}_p}$ has been found already.
%This property ensures that the entry distribution associated with each $\Entries_{\Abst{s}_p \Abst{s}}$ remains mostly fixed.
%Specifically, if the algorithm reaches \cref{alg:main-explore} in episode~$t$,
%then, the entry distribution equals $\nu_{t,\Abst{s}_p \Abst{s}} \coloneqq \Pr(s \Given s_p \in \Block{\Abst{s}_p}, s \in \Block{\Abst{s}}, O_t)$.
%Unfortunately, this distribution is not completely fixed over time,
%and, at some $t' > t$, $\nu_{t',\Abst{s}_p \Abst{s}}$ might be different from $\nu_{t,\Abst{s}_p \Abst{s}}$,
%because, in addition to the options that are present in $O_t$, new options for $(\Abst{s}_p \Abst{s}, \Abst{a})$ might be available in $O_{t'}$ for $\Block{\Abst{s}_p}$ or the preceding blocks.
%This is a quite nuanced dependency, and it only arises when learning realizations from specific entry distributions, instead of all entry states.
%We omit the treatment of this marginal issue here.
Finally, to discuss the third and last assumption,
we consider each $\nu_{t,\Abst{s}_p \Abst{s}}$, that represents the entry distribution for block~$\Block{\Abst{s}}$ from~$\Block{\Abst{s}_p}$ at episode~$t$.
Due to the way the algorithm is constructed,
these distributions can remain mostly fixed, and they only depend on the available options in~$O$ at the beginning of episode~$t$ (let $O_t$ represent this set).
Still, since the addition of new options might change such distributions, we assume that the old realizations remain valid in the future, as follows.
\begin{assumption}\label{as:new-options-dont-hurt-initiation}
During any execution of $\Ouralg$,
if $O_t(\Abst{s}_p \Abst{s}, \Abst{a})$ is an $(\PRealizableR, \PRealizableT)$-realization of
$(\Abst{s}_p \Abst{s}, \Abst{a})$ in $\Abst{\MDP}^*$ from $\nu_{t,\Abst{s}_p \Abst{s}}$,
then the same is true from $\nu_{t',\Abst{s}_p \Abst{s}}$, for any $t' > t$.
\end{assumption}
This is a quite nuanced dependency, and it only arises when learning realizations from specific entry distributions, instead of all entry states.
We omit the treatment of this marginal issue here.
We can finally state our bound, which limits the sample complexity of exploration \citep{kakade_2003_SampleComplexityReinforcement} of \Ouralg.
\begin{restatable}{theorem}{samplecomplexity}\label{th:algorithm-sample-complexity}
Under \cref{as:good-initial-abstraction,as:good-realizer,as:new-options-dont-hurt-initiation},
and any positive inputs $\PAccuracy, \PConfidence$,
with probability exceeding $1 - \PConfidence$,
\Ouralg\ is $\PAccuracy'$-optimal with
% NOTE: after acc make display
$\PAccuracy' = \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + \frac{3 \PAccuracy}{1-\gamma}$
on all but the following number of episodes
$\frac{2 \Abst{S}^2 \Abst{A}}{\PAccuracy} \left( \RealizerComplexity(\POptionSubopt, \PMaxViolation)\,\Abst{S}^2 + \log \frac{2S^2A}{\PConfidence} \right)$,
where $\RealizerComplexity(\POptionSubopt, \PMaxViolation)$ is the sample complexity of the realization algorithm.
\end{restatable}
% TODO: explain what this becomes for MDPs
% TODO: check why \Optionsubopt and max violation do not appear in \PAccuracy'
Thanks to the compositional property of Realizable Abstractions,
the sample complexity of each CMDP learner, which is $\RealizerComplexity(\POptionSubopt, \PMaxViolation)$, only contributes linearly to the bound, with the number of tuples to realize.
This number, which we bound with $\Abst{S}^2 \Abst{A}$, may be often much smaller because not all tuples are relevant for near-optimal behavior.
For example, \citet{wen_2020_EfficiencyHierarchicalReinforcement} shows that HRL has an advantage over \emph{flat} RL when the subMDPs can be grouped into $K$~equivalence classes
and $K \ll \Abst{S}$.
The same argument can be applied here.
When two block MDPs are equivalent, they can be regarded as one,
the collected samples can be shared, and the resulting options can be used in both blocks.
Therefore, the above bound can also be written with a multiplying factor of $\Abst{S} \Abst{A} K$ instead of $\Abst{S}^2 \Abst{A}$.
\section{Conclusion}
This work answers one important open question for HRL regarding how to relate the abstract actions with the ground options.
The answer is \emph{to relate the probability of abstract transitions with the probability of the temporally-extended transitions that can be obtained with options in the ground MDP}.
More specifically, this is given by the Realizable Abstractions, described in this paper.
This notion also implies suitable state abstractions that formally guarantee near-optimal and sample efficient solutions of the ground MDP.
In future work, the sample complexity of \cref{th:algorithm-sample-complexity} could be expressed as an instance-dependent bound.
This would highlight when HRL can be more efficient than standard RL, in presence of accurate abstractions, even without relying on equivalence classes.
%\Ouralg\ could be generalized for correcting for strongly inaccurate transitions.
% NOTE: after acc maybe say
%Compositionality is essential for lifelong learning}
% NOTE: After acceptance. acknowledgments before references in ack environment, only in camera ready
\small
\bibliographystyle{iclr25_sty/iclr2025_conference}
\bibliography{bib}
\normalsize
\clearpage
\appendix
\section*{Appendices}
\startcontents[appendix]
\printcontents[appendix]{l}{1}{}
\vspace{5ex}
\section{Properties of Realizable Abstractions}
\realizableabstvalue*
\begin{proof}
To relate the value functions of different decision processes, we inductively define a sequence of functions $V_0, V_1, \dots $
as $V_0(s_p s) \coloneqq 0$, and, if $k \in \Naturals_+$,
\begin{equation}
V_k(s_p s) \coloneqq \Expected \left[ g^o + \gamma^j\, V_{k-1}(s_{j-1} s_j) \Given s_p s, o \in \Options \cap \Options_{\Mapping(s_p) \Mapping(s)} \right]
\end{equation}
where $g^o$ is the cumulative discounted return of the option~$o$ and $j$~its random duration.
In practice, $V_k$ is the value of executing $k$~consecutive options, then computing the value on the abstraction.
Analogously, we also define $\Abst{V}_0, \Abst{V}_1, \dots$ for the abstraction as $\Abst{V}_0(\Abst{s}_p \Abst{s}) \coloneqq 0$ and
\begin{equation}
\Abst{V}_k(\Abst{s}_p \Abst{s}) \coloneqq \Expected \left[ \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) + \Abst\gamma\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}') \Given \Abst{s}_p \Abst{s}, \Abst{a} \sim \Abst\Policy) \right]
\end{equation}
We observe that $\Abst{V}^{\Abst\Policy}(\Abst{s}_p \Abst{s}) = \lim_{k \to \infty} \Abst{V}_k(\Abst{s}_p \Abst{s})$ and
$V^\Policy(s) = V^{\Options}(s) = \lim_{k \to \infty} V_k(s_p s)$.
Now, with an inductive proof, we show that,
for every $k \in \Naturals$, $\Abst{s}_p \in \Abst{\States}$, $s_p \in \Block{\Abst{s}_p}$, $s \in \Exits_{\Abst{s}_p}$,
\begin{equation}
\Abst{V}_k(\Abst{s}_p \Abst{s}) - V_k(s_p s) \le \sum_{i = 0}^k \gamma^i\, \frac{\PRealizableR\, (1 - \Abst\gamma) + \PRealizableT\, \Abst{S}}{(1-\gamma)(1 - \Abst\gamma)}
\end{equation}
where, for this derivation, we are using the syntactic abbreviation $\Abst{s} \coloneqq \Mapping(s)$ and $\Abst{S} \coloneqq \abs{\Abst{\States}}$.
For the base case, $k=0$ and $V_0(s_p s) = \Abst{V}_k(\Abst{s}_p \Abst{s})$.
Now, for the inductive step, we apply \cref{th:next-occupancy-2mdp} and \cref{th:multistep-value} to the two value functions, respectively.
We also use $\Abst{T}_{\Abst{s}_3 | \Abst{s}_1 \Abst{s}_2}$ and $\Abst{R}_{\Abst{s}_1 \Abst{s}_2}$, the same abbreviations of \cref{th:next-occupancy-2mdp}. Then,
\begin{align}
& \Abst{V}_k(\Abst{s}_p \Abst{s}) - V_k(s_p s) =\\
&= \Abst{R}_{\Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}}\, \Abst{R}_{\Abst{s}\Abst{s}}
+ \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \left( \Abst{\gamma}\, \Abst{T}_{\Abst{s}' \Given \Abst{s}_p \Abst{s}} +
\frac{\Abst{\gamma}^2\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}\, \Abst{T}_{\Abst{s}' \Given \Abst{s} \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}} \right)\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}') \notag\\
&\qquad - \sum_{s' \in \States_{\Abst{s}}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, (\Indicator(s' \in \Block{\Abst{s}})\, R(s', o(s')) + \Indicator(s' \in \Exits_{\Abst{s}})\, V_{k-1}(s')) \\
&= \Abst{R}_{\Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}}\, \Abst{R}_{\Abst{s}\Abst{s}}
- \sum_{s' \in \Block{\Abst{s}}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, R(s', o(s')) \notag\\
&\qquad + \hspace{-2mm}\sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \left( \Abst{\gamma}\, \Abst{T}_{\Abst{s}' \Given \Abst{s}_p \Abst{s}} +
\frac{\Abst{\gamma}^2\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}\, \Abst{T}_{\Abst{s}' \Given \Abst{s} \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}} \right)\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}')
- \sum_{s' \in \Exits_{\Abst{s}}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, V_{k-1}(s')
\intertext{If $V^o_{\Abst{s}}$ is the value function of~$o$ in the block-restricted MDP~$\MDP_{\Abst{s}}$,}
&= \Abst{R}_{\Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}}\, \Abst{R}_{\Abst{s}\Abst{s}}
- V^o_{\Abst{s}}(s) \notag\\
&\hspace{-1ex} + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \Biggl(
\left( \Abst{\gamma}\, \Abst{T}_{\Abst{s}' \Given \Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}^2\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}\, \Abst{T}_{\Abst{s}' \Given \Abst{s} \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}} \right)\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}')
- \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, V_{k-1}(s') \Biggr) \\
\intertext{using the fact that $s' \in \Entries_{\Abst{s} \Abst{s}'}$, and $\Tuple{\Abst\MDP, \Mapping}$ is an $(\PRealizableR, \PRealizableT)$-realizable abstraction,}
&\le \frac{\PRealizableR}{1-\gamma} + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \Biggl(
\left( \Abst{\gamma}\, \Abst{T}_{\Abst{s}' \Given \Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}^2\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}\, \Abst{T}_{\Abst{s}' \Given \Abst{s} \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}} \right)\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}')
- \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, V_{k-1}(s') \Biggr) \\
\intertext{Now, we add and subtract
$\sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}')$,}
&= \frac{\PRealizableR}{1-\gamma} + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \Biggl(
\sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}')
- \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, V_{k-1}(s') \Biggr) \notag\\
&\qquad + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \Biggl(
\left( \Abst{\gamma}\, \Abst{T}_{\Abst{s}' \Given \Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}^2\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}\, \Abst{T}_{\Abst{s}' \Given \Abst{s} \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}} \right)\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}')
- \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}') \Biggr) \\
&= \frac{\PRealizableR}{1-\gamma} + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}}
\frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, \bigl(\Abst{V}_{k-1}(\Abst{s} \Abst{s}') - V_{k-1}(s') \bigr)\notag\\
&\qquad + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \Abst{V}_{k-1}(\Abst{s} \Abst{s}') \Biggl(
\left( \Abst{\gamma}\, \Abst{T}_{\Abst{s}' \Given \Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}^2\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}\, \Abst{T}_{\Abst{s}' \Given \Abst{s} \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}} \right)
- \frac{h^{o}_{\Abst{s}}(\Abst{s}' \Given s)}{1-\gamma} \Biggr)\\
\intertext{applying the inductive hypothesis to the first line and the definition of an $(\PRealizableR, \PRealizableT)$-realizable abstraction to the second line,}
&\le \frac{\PRealizableR}{1-\gamma}
+ \sum_{s' \in \Exits_{\Abst{s}}} \frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, \sum_{i = 0}^{k-1} \gamma^i\, \frac{\PRealizableR\, (1 - \Abst\gamma) + \PRealizableT\, \Abst{S}}{(1-\gamma)(1 - \Abst\gamma)}
+ \frac{\PRealizableT\, \Abst{S}}{(1-\gamma)(1 - \Abst\gamma)}
\label{eq:realized-value-inductive-occupancy}
\end{align}
It only remains to quantify $\sum_{s' \in \Exits_{\Abst{s}}} d^{o}_{\Abst{s}}(s' \Given s)$.
To do this, we apply \cref{th:occupancy-at-exits} which gives,
\begin{equation}
\sum_{s' \in \Exits_{\Abst{s}}} d^{o}_{\Abst{s}}(s' \Given s) = (1 - h^{o}_{\Abst{s}}(\Abst{s} \Given s))\, (1 - \gamma)
\end{equation}
However, since the option starts in $s \in \Block{\Abst{s}}$, the occupancy $h^{o}_{\Abst{s}}(\Abst{s} \Given s)$ cannot be less than $(1 - \gamma)$.
This allows us to complete the inequality and obtain
\begin{align}
\Abst{V}_k(\Abst{s}_p \Abst{s}) - V_k(s_p s)
&\le \frac{\PRealizableR\, (1 - \Abst\gamma) + \PRealizableT\, \Abst{S}}{(1-\gamma)(1 - \Abst\gamma)} + \gamma \sum_{i = 0}^{k-1} \gamma^i\, \frac{\PRealizableR\, (1 - \Abst\gamma) + \PRealizableT\, \Abst{S}}{(1-\gamma)(1 - \Abst\gamma)}\\
&= \sum_{i = 0}^{k} \gamma^i\, \frac{\PRealizableR\, (1 - \Abst\gamma) + \PRealizableT\, \Abst{S}}{(1-\gamma)(1 - \Abst\gamma)}
\end{align}
This concludes the inductive step.
To verify \cref{eq:realizab-abstraction-value},
We observe that $\Abst{V}^{\Abst\Policy}(\Abst{s}_p \Abst{s}) = \lim_{k \to \infty} \Abst{V}_k(\Abst{s}_p \Abst{s})$ and
$V^\Policy(s) = V^{\Options}(s) = \lim_{k \to \infty} V_k(s_p s)$.
We conclude by verifying the statement for the values from the respective initial distributions.
\begin{align}
& \Abst{V}_{\Abst\StartDistrib}^{\Abst\Policy} - V_\StartDistrib^{\Options}
= \sum_{\Abst{s} \in \Abst\States} \Abst\StartDistrib(\Abst{s})\, \Abst{V}^{\Abst\Policy}(\Abst{s}\StartSym \Abst{s}) - \sum_{s \in \States} \StartDistrib(s)\, V^{\Options}(s) \label{eq:admissible-values-init1}\\
&= \sum_{\Abst{s} \in \Abst\States} \Abst\StartDistrib(\Abst{s})\, \Abst{V}^{\Abst\Policy}(\Abst{s}\StartSym \Abst{s})
- \sum_{\Abst{s} \in \Abst\States} \sum_{s \in \Block{\Abst{s}}} \StartDistrib(s)\, \Abst{V}^{\Abst\Policy}(\Abst{s}\StartSym \Abst{s})\notag\\*
&\qquad + \sum_{\Abst{s} \in \Abst\States} \sum_{s \in \Block{\Abst{s}}} \StartDistrib(s)\, \Abst{V}^{\Abst\Policy}(\Abst{s}\StartSym \Abst{s})
- \sum_{s \in \States} \StartDistrib(s)\, V^{\Options}(s)\\
&= \sum_{\Abst{s} \in \Abst\States} \Abst{V}^{\Abst\Policy}(\Abst{s}\StartSym \Abst{s})\, (\Abst\StartDistrib(\Abst{s})\, - \sum_{s \in \Block{\Abst{s}}} \StartDistrib(s) )
+ \sum_{s \in \States} \StartDistrib(s)\, (\Abst{V}^{\Abst\Policy}(\Abst{s}\StartSym \Mapping(s)) - V^{\Options}(s)) \label{eq:admissible-values-init2}
\end{align}
Using the assumption on initial distributions and the derivation above we obtain the second result.
\end{proof}
\admissiblevalues*
\begin{proof}
To start, we observe that any ground policy~$\Policy$ can be equivalently represented as a unique policy of options~$\Options$.
Therefore, to relate the values in the two decision processes, we inductively define a sequence of functions $V_0, V_1, \dots $
as $V_0(s_p s) \coloneqq 0$, and, if $k \in \Naturals_+$,
\begin{equation}
V_k(s_p s) \coloneqq \Expected \left[ g^o + \gamma^j\, V_{k-1}(s_{j-1} s_j) \Given s_p s, o \in \Options \cap \Options_{\Mapping(s_p) \Mapping(s)} \right]
\end{equation}
where $g^o$ is the cumulative discounted return of the option~$o$ and $j$~its random duration.
In practice, $V_k$ is the value of executing $k$~consecutive options, then collecting null rewards.
Analogously, for some $\Abst\Policy$, we also define $\Abst{V}_0, \Abst{V}_1, \dots$ for the abstraction as $\Abst{V}_0(\Abst{s}_p \Abst{s}) \coloneqq 0$ and
\begin{equation}
\Abst{V}_k(\Abst{s}_p \Abst{s}) \coloneqq \Expected \left[ \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) + \Abst\gamma\, \Abst{V}_{k-1}(\Abst{s} \Abst{s}') \Given \Abst{s}_p \Abst{s}, \Abst{a} \sim \Abst\Policy) \right]
\end{equation}
We observe that $\Abst{V}^{\Abst\Policy}(\Abst{s}_p \Abst{s}) = \lim_{k \to \infty} \Abst{V}_k(\Abst{s}_p \Abst{s})$ and
$V^\Policy(s) = V^{\Options}(s) = \lim_{k \to \infty} V_k(s_p s)$.
Thus, to prove the result, it suffices to show that, for some $\Abst\Policy$, $\Abst{V}_k(\Abst{s}_p \Abst{s}) \ge V_k(s_p s)$, for all $k \in \Naturals$
and every $\Abst{s}_p \in \Abst\States$, $s_p \in \Block{\Abst{s}_p}$, $s \in \Exits_{\Abst{s}_p}$, $\Abst{s} = \Mapping(s)$.
We first define $\Abst\Policy$, then prove the result by induction.
For any $\Abst{s}_p \Abst{s}$, we define the abstract policy $\Abst\Policy(\Abst{s}_p \Abst{s}) \coloneqq \Abst{a}$,
where $\Abst{a}$ is any action satisfying
$\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') \ge h^{o}_{\Abst{s}}(\Abst{s}' \Given s)$ and
$\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge V^o_{\Abst{s}}(s)$,
for all $\Abst{s}' \neq \Abst{s}$ and $s \in \Entries_{\Abst{s}_p \Abst{s}}$,
with $o$ being the only option in~$\Options \cap \Options_{\Abst{s}_p \Abst{s}}$.
These abstract actions exist because it is assumed that $\Tuple{\Abst\MDP, \Mapping}$ is admissible.
The rest of the proof is inductive.
For $k=0$, the base case trivially holds because $\Abst{V}_k \equiv V_k$.
For $k>0$,
we compute $\Abst{V}_k(\Abst{s}_p \Abst{s}) - V_k(s_p s)$ and expand it as in the proof of \cref{th:realizab-abstraction-value}.
This can be done by respecting all equalities up until
\begin{align}
\begin{split}
\MoveEqLeft \Abst{V}_k(\Abst{s}_p \Abst{s}) - V_k(s_p s) = \\
&= \Abst{R}_{\Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}}\, \Abst{R}_{\Abst{s}\Abst{s}} - V^o_{\Abst{s}}(s) \\
&\qquad + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}}
\frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, \bigl(\Abst{V}^{\Abst{\Policy}}(\Abst{s} \Abst{s}') - V_{k-1}(s') \bigr)\\
&\qquad + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \Abst{V}^{\Abst{\Policy}}(\Abst{s} \Abst{s}') \Biggl(
\left( \Abst{\gamma}\, \Abst{T}_{\Abst{s}' \Given \Abst{s}_p \Abst{s}} + \frac{\Abst{\gamma}^2\, \Abst{T}_{\Abst{s} \Given \Abst{s}_p \Abst{s}}\, \Abst{T}_{\Abst{s}' \Given \Abst{s} \Abst{s}}}{1 - \Abst{\gamma}\, \Abst{T}_{\Abst{s} \Given \Abst{s} \Abst{s}}} \right)
- \frac{h^{o}_{\Abst{s}}(\Abst{s}' \Given s)}{1-\gamma} \Biggr)
\end{split}\\
\begin{split}
&= \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - V^o_{\Abst{s}}(s) \\
&\qquad + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \sum_{s' \in \Entries_{\Abst{s} \Abst{s}'}}
\frac{d^{o}_{\Abst{s}}(s' \Given s)}{1-\gamma}\, \bigl(\Abst{V}^{\Abst{\Policy}}(\Abst{s} \Abst{s}') - V_{k-1}(s') \bigr)\\
&\qquad + \sum_{\Abst{s}' \in \Abst{\States} \setminus \{\Abst{s}\}} \Abst{V}^{\Abst{\Policy}}(\Abst{s} \Abst{s}')
\left( \frac{\tilde{h}_{\Abst{s}_p' \Abst{s} \Abst{a}}(\Abst{s}')}{1-\gamma} - \frac{h^{o}_{\Abst{s}}(\Abst{s}' \Given s)}{1-\gamma} \right)
\end{split}
\end{align}
Using both the definition of $\Abst{a}$, which is admissible for~$o$ and the inductive hypothesis,
we can confirm that all three terms are positive.
Finally, using a similar expansion as \cref{eq:admissible-values-init1,eq:admissible-values-init2},
we can verify that the same is also true for the respective initial distributions.
\end{proof}
\realizaboptimalvalue*
\begin{proof}
Let $\Options$ be an $(\PRealizableR, \PRealizableT)$-realization of the optimal abstract policy $\Abst{\Policy}^*$.
Then, using \cref{th:admissible-values} for the first inequality and \cref{th:realizab-abstraction-value} for the last:
\begin{equation}
V^*_\StartDistrib \le \Abst{V}^{\Abst{\Policy}}_{\Abst\StartDistrib} \le \Abst{V}^{\Abst{\Policy}^*}_{\Abst\StartDistrib} \le V^\Options_\StartDistrib + \PAccuracy
\end{equation}
\end{proof}
\begin{lemma}\label{th:next-occupancy-2mdp}
In any 2-MDP~$\MDP$ and deterministic policy~$\Policy$, for any two states $s_p, s \in \States$,
\begin{equation}
V^\Policy(s_p s) =
R_{s_p s} + \frac{\gamma\, T_{s|s_p s}}{1 - \gamma\, T_{s|ss}}\, R_{ss}
+ \sum_{s' \in \States \setminus \{s\}} \left( \gamma\, T_{s'|s_p s} +
\frac{\gamma^2\, T_{s|s_p s}\, T_{s'|ss}}{1 - \gamma\, T_{s|ss}} \right)\, V^\Policy(s s')
\end{equation}
where $T_{s_3|s_1 s_2} \coloneqq T(s_3 \Given s_1 s_2, \Policy(s_1 s_2))$ and $R_{s_1 s_2} \coloneqq R(s_1 s_2, \Policy(s_1 s_2))$.
\end{lemma}
\begin{proof}
We use the abbreviations $T_{s_1|s_1 s_2}$ and $R_{s_1 s_2}$ to avoid excessive verbosity. Then,
\begin{align}
& V^\Policy(s_p s) = \sum_{s' \in \States} T_{s'|s_p s}\, (R_{s_p s} + \gamma\, V^\Policy(s s')) \\
&= R_{s_p s} + \sum_{s' \in \States \setminus \{s\}} T_{s'|s_p s}\, \gamma\, V^\Policy(s s') + T_{s|s_p s}\, \gamma\, V^\Policy(s s) \\
&= R_{s_p s} + \sum_{s' \in \States \setminus \{s\}} T_{s'|s_p s}\, \gamma\, V^\Policy(s s') + T_{s|s_p s}\, \gamma\, R_{ss}\\
&\qquad + T_{s|s_p s}\, \gamma\, T_{s|ss}\, \gamma\, V^\Policy(ss) + T_{s|s_p s}\, \gamma\, \sum_{s' \in \States \setminus \{s\}} T_{s'|s_p s}\, \gamma\, V^\Policy(s s') \\
&= R_{s_p s} + \gamma\, T_{s|s_p s}\, R_{ss} \sum_{t=0}^\infty \gamma^t\, T_{s|ss}^t \notag\\
&\qquad + \sum_{s' \in \States \setminus \{s\}} \gamma\, T_{s'|s_p s}\, V^\Policy(s s') +
\gamma\, T_{s|s_p s} \sum_{s' \in \States \setminus \{s\}} \gamma\, T_{s'|ss}\, V^\Policy(s s') \sum_{t=0}^\infty \gamma^t\, T_{s|ss}^t \\
&= R_{s_p s} + \frac{\gamma\, T_{s|s_p s}}{1 - \gamma\, T_{s|ss}}\, R_{ss}
+ \sum_{s' \in \States \setminus \{s\}} \left( \gamma\, T_{s'|s_p s} +
\frac{\gamma^2\, T_{s|s_p s}\, T_{s'|ss}}{1 - \gamma\, T_{s|ss}} \right)\, V^\Policy(s s')
\end{align}
\end{proof}
\begin{lemma}\label{th:multistep-value}
Consider any MDP~$\MDP$ and surjective function $\Mapping: \States \to \Abst\States$.
Then, from any state $s \in \States$,
the value of any deterministic $\Mapping$-relative option $o \in \Options_{\Mapping(s)}$ and policy~$\Policy$ is
\begin{equation}
{Q}^\Policy(s, o) = \sum_{s' \in \States} \frac{d^o_{\Mapping(s)}(s' \Given s)}{1 - \gamma} \bigl(\Indicator(s' \in \Block{\Mapping(s)})\, R(s', o(s')) + \Indicator(s' \in \Exits_{\Mapping(s)})\, V^\Policy(s')\bigr)
\end{equation}
where $d^o_{\Mapping(s)}$ is the state occupancy measure of~$\Policy_o$ in the block-restricted MDP~$\MDP_{\Mapping(s)}$.
\end{lemma}
\begin{proof}
Let $\Blocksteps{\Abst{s}}{t} \coloneqq \Block{\Abst{s}}^{t-1} \times (\States \setminus \Block{\Abst{s}})$
be the set that includes all trajectories leaving the block in exactly $t$ transitions.
We also abbreviate $\Abst{s} \coloneqq \Mapping(s)$. Then,
\begin{align}
& {Q}^\Policy(s, o)
= R(s, o(s)) + \gamma \Expected_{s'}[\Indicator(s' \in \Block{\Abst{s}})\, {Q}^\Policy(s', o) + \Indicator(s' \not\in \Block{\Abst{s}})\, {V}^\Policy(s'))] \\
&= R(s, o(s)) + \gamma \sum_{s' \in \Block{\Abst{s}}} T(s' \Given s, o(s))\, {Q}^\Policy(s', o)
+ \gamma \sum_{s' \not\in \Block{\Abst{s}}} T(s' \Given s, o(s))\, {V}^\Policy(s') \\
&= \sum_{t = 0}^\infty \gamma^t\, \sum_{s_{1:t} \in \Block{\Abst{s}}^t} \Pr(s_{1:t} \Given s_0=s, o, \MDP)\, R(s_t, o(s_t))\notag\\
&\qquad + \sum_{t = 1}^\infty \gamma^t\, \sum_{s_{1:t} \in \Blocksteps{\Abst{s}}{t}} \Pr(s_{1:t} \Given s_0=s, o, \MDP)\, V^\Policy(s_{t})\\
&= \sum_{t = 0}^\infty \gamma^t\, \sum_{s_{1:t} \in \Block{\Abst{s}}^t} \Pr(s_{1:t} \Given s_0=s, o, \MDP_{\Abst{s}})\, R_{\Abst{s}}(s_t, o(s_t))\notag\\
&\qquad + \sum_{t = 1}^\infty \gamma^t\, \sum_{s_{1:t} \in \Blocksteps{\Abst{s}}{t}} \Pr(s_{1:t} \Given s_0=s, o, \MDP_{\Abst{s}})\, V^\Policy(s_{t})
\end{align}
In the last equation, all probabilities are computed on the block-restricted MDP $\MDP_{\Abst{s}}$.
This is equivalent, since all probabilities of transitions from $\Block{\Abst{s}}$ are preserved.
Since every trajectory that leaves the block may only reach $\SinkS$, without further rewards in $\MDP_{\Abst{s}}$, we can simplify as follows.
\begin{align}
\MoveEqLeft {Q}^\Policy(s, o)
= \sum_{t = 0}^\infty \gamma^t\, \sum_{s_{1:t} \in \States_{\Abst{s}}^t} \Pr(s_{1:t} \Given s_0=s, o, \MDP_{\Abst{s}})\, R_{\Abst{s}}(s_t, o(s_t))\notag\\
&\qquad + \sum_{t = 1}^\infty \gamma^t\, \sum_{s' \in \Exits_{\Abst{s}}} \Pr(s_{t} = s' \Given s_0=s, o, \MDP_{\Abst{s}})\, V^\Policy(s')\\
&= \Expected \left[ \sum_{t = 0}^\infty \gamma^t\, r_t \Given s, o, \MDP_{\Abst{s}} \right]\notag\\
&\qquad + \sum_{s' \in \States} \sum_{t = 1}^\infty \gamma^t\, \Pr(s_{t} = s' \Given s_0=s, o, \MDP_{\Abst{s}})\, \Indicator(s' \in \Exits_{\Abst{s}})\, V^\Policy(s')\\
&= V^{o}_{\Abst{s}}(s) + \sum_{s' \in \States} \sum_{t = 0}^\infty \gamma^t\, \Pr(s_{t} = s' \Given s_0=s, o, \MDP_{\Abst{s}})\, \Indicator(s' \in \Exits_{\Abst{s}})\, V^\Policy(s')\\
&= (1 - \gamma)^{-1} \sum_{s' \in \Block{\Abst{s}}} d^o_{\Abst{s}}(s' \Given s)\, R(s', o(s'))\notag\\
&\qquad + (1 - \gamma)^{-1} \sum_{s' \in \States} d^o_{\Abst{s}}(s' \Given s)\, \Indicator(s' \in \Exits_{\Abst{s}})\, V^\Policy(s')\\
&= \sum_{s' \in \States} (1 - \gamma)^{-1}\, d^o_{\Abst{s}}(s' \Given s)\, (\Indicator(s' \in \Block{\Abst{s}})\, R(s', o(s')) + \Indicator(s' \in \Exits_{\Abst{s}})\, V^\Policy(s'))
\end{align}
\end{proof}
\begin{lemma}\label{th:occupancy-at-exits}
Let $\MDP_{\Abst{s}}$ be any block MDP, computed from some MDP $\MDP$, mapping function $\Mapping$ and abstract state $\Abst{s}$.
Then, for any option $o \in \Options_{\Abst{s}}$ and $s \in \Block{\Abst{s}}$, it holds:
\begin{align}
d^o_{\Abst{s}}(\SinkS \Given s) &= ( 1 - h^{o}_{\Abst{s}}(\Abst{s} \Given s))\, \gamma \label{eq:occupancy-at-sink}\\*
\sum_{s' \in \Exits_{\Abst{s}}} d^{o}_{\Abst{s}}(s' \Given s) &= (1 - h^{o}_{\Abst{s}}(\Abst{s} \Given s))\, (1 - \gamma) \label{eq:occupancy-at-exits}
\end{align}
\end{lemma}
\begin{proof}
In a block MDP, we remind that the occupancy measure is spread between the block $\Block{\Abst{s}}$, the exits and the sink state~$\SinkS$.
In other words,
\begin{equation}\label{eq:exit-occupancy-expression}
\sum_{s' \in \Exits_{\Abst{s}}} d^{o}_{\Abst{s}}(s' \Given s) = 1 - \sum_{s' \in \Block{\Abst{s}}} d^{o}_{\Abst{s}}(s' \Given s) - d^{o}_{\Abst{s}}(\SinkS \Given s) =
1 - h^{o}_{\Abst{s}}(\Abst{s} \Given s) - d^{o}_{\Abst{s}}(\SinkS \Given s)
\end{equation}
From the definition of occupancy, we also know that
\begin{align}
d^o_{\Abst{s}}(\SinkS \Given s) &= (1 - \gamma) \sum_{t = 0}^\infty \gamma^t\, \Pr(s_t = \SinkS \Given s_0 = s, o, \MDP_{\Abst{s}})\\
&= (1 - \gamma) \sum_{t = 1}^\infty \gamma^t\, \Pr(s_t = \SinkS \Given s_0 = s, o, \MDP_{\Abst{s}})\\
&= (1 - \gamma) \sum_{t = 1}^\infty \gamma^t\, \Pr(s_{t-1} \in \Exits_{\Abst{s}} \cup \{\SinkS\} \Given s_0 = s, o, \MDP_{\Abst{s}})\\
&= \gamma\, (1 - \gamma) \sum_{t = 0}^\infty \gamma^t\, \Pr(s_{t} \in \Exits_{\Abst{s}} \cup \{\SinkS\} \Given s_0 = s, o, \MDP_{\Abst{s}})\\
&= \gamma\, \left( \sum_{s' \in \Exits_{\Abst{s}}} d^{o}_{\Abst{s}}(s' \Given s) + d^{o}_{\Abst{s}}(\SinkS \Given s) \right) \label{eq:sink-occupancy-expression}
\end{align}
Substituting \cref{eq:exit-occupancy-expression} into \cref{eq:sink-occupancy-expression} gives the result.
\end{proof}
\selfexactabstraction*
\begin{proof}
The ground domain is $\MDP = \Tuple{\States, \Actions, T, R, \gamma}$
and the abstraction is $\Tuple{\MDP, \Identity}$.
We will first show that this is a perfectly realizable abstraction.
The identity function induces the naive partitioning, in which each state is in a separate block: $\Block{s}_\Identity = \{s\}$.
Also, if we just consider deterministic $\Identity$-relative options, we see that these are simple repetitions of the same action for the same state.
We can now compute the un-normalized block occupancy measure at any state $s \in \States$ and deterministic $o \in \Options_s$.
Then, for $s' \neq s$,
\begin{align}
\frac{h_{\Identity(s)}^o(s' \Given s)}{1 - \gamma}
&= \sum_{s' \in \Block{\Identity(s')}} \sum_{t = 0}^\infty \gamma^t\, \Pr(s_t = s' \Given s_0 = s, o, \MDP_{\Identity(s)})\\
&= \sum_{t = 1}^\infty \gamma^t\, \Pr(s_{0:t-1} \in \Block{s}^t, s_t = s' \Given s_0 = s, o, \MDP_{s})\\
&= \sum_{t = 1}^\infty \gamma^t\, T(s \Given s, o(s))^{t-1}\, T(s' \Given s, o(s))\\
&= \frac{\gamma\, T(s' \Given s, o(s))}{1 - \gamma\, T(s \Given s, o(s))}
\end{align}
Now we compute un-normalized \cref{eq:computed-option-occupancy} for~$\MDP$.
Importantly, since $T(s_p s, a) = T(s s, a)$, we can just write $T(s, a)$:
\begin{align}
\frac{\tilde{h}_{{s}_p {s} {a}}({s}')}{1-\gamma}
= \gamma\, T(s' \Given s, a) + \frac{\gamma^2\, T(s \Given s, a)\, T(s' \Given s, a)}{1 - \gamma\, T(s \Given s, a)}
= \frac{\gamma\, T(s' \Given s, a)}{1 - \gamma\, T(s \Given s, a)}
\label{eq:self-abstractions-2mdp}
\end{align}
This proves that $\Policy_o(s) = a$ is a perfect realization of~$a$ with respect to \cref{eq:realizabilityT}.
We now consider rewards.
The term $V_s^o(s)$, appearing in \cref{eq:realizabilityR}, is the cumulative return obtained by repeating action~$a$
(since it is the only reward in $\MDP_s$).
\begin{align}
V_s^o(s) &= \sum_{t = 0}^\infty \gamma^t\, \Pr(s_t = s \Given s_0 = s, a, \MDP_{\Abst{s}})\, R(s, a)\\
&= \sum_{t = 0}^\infty \gamma^t\, T(s \Given s, a)^{t-1}\, R(s, a)\\
&= \frac{\gamma\, R(s, a)}{1 - \gamma\, T(s \Given s, a)}
\end{align}
Following a similar procedure of \cref{eq:self-abstractions-2mdp}, we also verify \cref{eq:realizabilityR}.
We have just verified perfect realizability only using equality relations.
Therefore, it is proven that admissibility is also satisfied.
\end{proof}
\admissibleimpliesgoodgamma*
\begin{proof}
Let us fix any $\Abst{s}_p, \Abst{s} \in \Abst\States$, with $\Abst{s}_p \neq \Abst{s}$,
an option $o \in \Options_{\Abst{s}_p \Abst{s}}$, and an $s \in \Entries_{\Abst{s}_p \Abst{s}}$.
Since the abstraction is admissible, we know there exists an~$\Abst{a}$, such that
$\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') \ge h^{o}_{\Abst{s}}(\Abst{s}' \Given s)$ and
$\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge V^o_{\Abst{s}}(s)$,
at any $\Abst{s}' \neq \Abst{s}$.
Using the abbreviation $\Abst{T}_{\Abst{s}_3|\Abst{s}_1 \Abst{s}_2} \coloneqq \Abst{T}(\Abst{s}_3 \Given \Abst{s}_1 \Abst{s}_2, \Abst{a})$,
we expand the first inequality with~\eqref{eq:computed-option-occupancy},
\begin{align}
&h^{o}_{\Abst{s}}(\Abst{s}' \Given s) \le (1 - \gamma) \left( \Abst\gamma \Abst{T}_{\Abst{s}' | \Abst{s}_p \Abst{s}}
+ \Abst\gamma^2 \frac{ \Abst{T}_{\Abst{s}' | \Abst{s}\Abst{s}} \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}}}{1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}} \right) \\
\iff\,\, & \frac{h^{o}_{\Abst{s}}(\Abst{s}' \Given s)}{(1 - \gamma)} \le
\frac{ \Abst\gamma \Abst{T}_{\Abst{s}' | \Abst{s}_p \Abst{s}}
- \Abst\gamma^2 \Abst{T}_{\Abst{s}' | \Abst{s}_p \Abst{s}} \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}
+ \Abst\gamma^2 \Abst{T}_{\Abst{s}' | \Abst{s}\Abst{s}} \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}}}{1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}} \\
\intertext{by summing all such inequalities over $\Abst{s}' \neq \Abst{s}$, and using \cref{eq:occupancy-at-exits} for the left-hand side, we obtain}
\implies\,\, & 1 - h^{o}_{\Abst{s}}(\Abst{s} \Given s) \le
\frac{ \Abst\gamma (1 - \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}})
- \Abst\gamma^2 \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}} (1 - \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}})
+ \Abst\gamma^2 \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}} (1 - \Abst{T}_{\Abst{s} | \Abst{s}\Abst{s}})}{1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}} \\
\iff\,\, & 1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}} - h^{o}_{\Abst{s}}(\Abst{s} \Given s) (1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}) \le
\Abst\gamma - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}}
- \Abst\gamma^2 \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}
+ \Abst\gamma^2 \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}} \\
\iff\,\, & h^{o}_{\Abst{s}}(\Abst{s} \Given s) (1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}) \ge
(1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}) - \Abst\gamma (1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}})
+ \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}} (1 - \Abst\gamma) \\
\iff\,\, & h^{o}_{\Abst{s}}(\Abst{s} \Given s) \ge
1 - \Abst\gamma
+ \frac{\Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}} (1 - \Abst\gamma)}{1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}} \label{eq:admissible-implies-proof1} \\
\implies\,\, & h^{o}_{\Abst{s}}(\Abst{s} \Given s) \ge
1 - \Abst\gamma
\end{align}
For the second statement, we expand $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge V^o_{\Abst{s}}(s)$,
\begin{align}
&V^o_{\Abst{s}}(s) \le \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) + \Abst\gamma \Abst{R}(\Abst{s}\Abst{s}, \Abst{a}) \frac{ \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}}}{1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}} \\
\implies\,\, & V^o_{\Abst{s}}(s) \le 1 + \frac{ \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}}}{1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}} \\
\iff\,\, & (1 - \Abst\gamma) V^o_{\Abst{s}}(s) \le (1 - \Abst\gamma) + \frac{ \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s}_p \Abst{s}} (1 - \Abst\gamma)}{1 - \Abst\gamma \Abst{T}_{\Abst{s} | \Abst{s} \Abst{s}}} \\
\intertext{using \eqref{eq:admissible-implies-proof1},}
\implies\,\, & V^o_{\Abst{s}}(s) \le h^{o}_{\Abst{s}}(\Abst{s} \Given s) / (1 - \Abst\gamma)
\end{align}
\end{proof}
\section{Connection with MDP Homomorphisms and bisimulation}
\label{sec:app:homomorphism}
In this section,
we relate our new concept of realizable abstractions with two existing formal definitions of MDP abstractions,
namely, MDP homomorphisms \citep{ravindran_2002_ModelMinimizationHierarchical} and stochastic bisimulation \citep{givan_2003_EquivalenceNotionsModel}.
As we demonstrate in this section,
both MDP homomorphisms and stochastic bisimulation are strictly less expressive (meaning, their assumptions are strictly more stringent)
than realizable abstractions.
As we show below, any MDP abstraction obtained via an homomorphisms or a stochastic bisimulation is also an admissible and perfectly realizable abstraction.
On the other hand, there exists MDP-abstraction pairs, $\MDP$ and $\Tuple{\Abst\MDP, \Mapping}$, that
satisfy the realizability assumptions but no associated MDP homomorphisms or bisimulation exists for the two.
% TODO: write this in main body
In an effort to make both MDP homomorphisms and stochastic bisimulation more widely applicable,
they have been generalized to approximate the strict relations,
respectively in \citet{ravindran_2004_ApproximateHomomorphismsFramework} and \citet{ferns_2004_MetricsFiniteMarkov}.
Nonetheless, they only allow small variations around the strict equality, similarly to what we have done in this paper for realizable abstractions,
but they cannot capture very different relations from their original definition.
Therefore, we will relate the strict relations of the various formalisms: admissible and perfectly realizable abstractions, MDP homomorphisms, and stochastic bisimulation.
\paragraph{MDP homomorphisms}
MDP homomorphisms are a classic formalism for MDP minimization \citep{ravindran_2002_ModelMinimizationHierarchical}.
A homomorphism from an MDP $\MDP = \Tuple{\States, \Actions, T, R, \gamma}$
to another $\Abst\MDP = \Tuple{\Abst\States, \Abst\Actions, \Abst{T}, \Abst{R}, \gamma}$
is a pair $\Tuple{f, \{g_s\}_{s \in \States}}$,
with a function $f: \States \to \Abst\States$
and surjections $g_s: \Actions \to \Abst\Actions$, satisfying
\begin{align}
\Abst{T}(f(s') \Given f(s), g_s(a)) &= \sum_{s'' \in \Block{f(s')}} T(s'' \Given s, a)
\label{eq:hom-transition}\\
\Abst{R}(f(s), g_s(a)) &= R(s, a)
\label{eq:hom-reward}
\end{align}
for all ${s, s' \in \States}$, ${a \in \Actions}$.
For simplicity, here we assumed that all actions are applicable in any state.
MDP homomorphisms can also be generalized to be approximate as shown in \citet{ravindran_2004_ApproximateHomomorphismsFramework}.
\realizablehomomorph*
\begin{proof}
If the ground domain is $\MDP = \Tuple{\States, \Actions, T, R, \gamma}$,
we choose as abstraction $\Tuple{\Abst\MDP, f}$.
We compute the un-normalized block occupancy measure at any state $s \in \States$ and deterministic option $o \in \Options_{f(s)}$.
We also assume that~$o$ selects the same action for every $\Block{f(s)}$.
Then, for $\Abst{s}' \neq f(s)$,
\begin{align}
\MoveEqLeft \frac{h_{f(s)}^o(\Abst{s}' \Given s)}{1 - \gamma}
= \sum_{s' \in \Block{\Abst{s}'}} \sum_{t = 0}^\infty \gamma^t\, \Pr(s_t = s' \Given s_0 = s, o, \MDP_{f(s)})\\
&= \sum_{s' \in \Block{\Abst{s}'}} \sum_{t = 1}^\infty \gamma^t\, \Pr(s_{0:t-1} \in \Block{f(s)}^t, s_t = s' \Given s_0 = s, o, \MDP_{f(s)})\\
&= \sum_{t = 1}^\infty \gamma^t \sum_{s_{0:t-1} \in \Block{f(s)}^t} \sum_{s' \in \Block{\Abst{s}'}} \Pr(s_{0:t-1}, s_t = s' \Given s_0 = s, o, \MDP_{f(s)})\\
\intertext{Now, summing from $s'$ to $s_{t-1}$ back to $s_0$ and substituting \cref{eq:hom-transition},}
&= \sum_{t = 1}^\infty \gamma^t\, \Abst{T}(f(s) \Given f(s)\, g_s(o(s))^{t-1}\, \Abst{T}(\Abst{s}' \Given f(s)\, g_s(o(s)))\\
&= \frac{\gamma\, \Abst{T}(\Abst{s}' \Given f(s)\, g_s(o(s)))}{1 - \gamma\, \Abst{T}(f(s) \Given f(s)\, g_s(o(s)))}
\end{align}
Now we compute un-normalized \cref{eq:computed-option-occupancy} for~$\MDP$.
As in \cref{eq:self-abstractions-2mdp}, since $\Abst{T}(\Abst{s}_p \Abst{s}, \Abst{a}) = T(\Abst{s} \Abst{s}, \Abst{a})$, we can just write $T(\Abst{s}, \Abst{a})$ and:
\begin{align}
\frac{\tilde{h}_{{\Abst{s}}_p {\Abst{s}} {\Abst{a}}}({\Abst{s}}')}{1-\gamma}
= \frac{\gamma\, \Abst{T}(\Abst{s}' \Given \Abst{s}\, \Abst{a})}{1 - \gamma\, \Abst{T}(\Abst{s} \Given \Abst{s}\, \Abst{a})}
\end{align}
This proves that $\Policy_o(s) \in g_s^{-1}(\Abst{a})$ is a perfect realization of~$\Abst{a}$ with respect to \cref{eq:realizabilityT}.
We now consider rewards.
The term $V_{f(s)}^o(s)$, appearing in \cref{eq:realizabilityR}, is
\begin{align}
V_{f(s)}^o(s)
&= \sum_{t = 0}^\infty \gamma^t \sum_{s_{0:t} \in \Block{f(s)}^{t+1}} \Pr(s_{0:t} \Given s_0 = s, o, \MDP_{f(s)})\, R(s, a)\\
&= \sum_{t = 0}^\infty \gamma^t\, \Abst{T}(f(s) \Given f(s)\, o(a))^{t}\, \Abst{R}(f(s)\, o(a))\\
&= \frac{\gamma\, \Abst{R}(f(s)\, o(a))}{1 - \gamma\, \Abst{T}(f(s) \Given f(s)\, o(a))}
\end{align}
By comparison with $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}}$ in \cref{eq:realizabilityR},
the same choice $\Policy_o(s) \in g_s^{-1}(\Abst{a})$ also satisfies the second constraint.
\end{proof}
\realizablehomomorphback*
\begin{figure}
\centering
\begin{tikzpicture}
\matrix [column sep=1cm] {
\node (s0) [state, initial, label=below:$s_0$] {}; \&
\node (s1) [state, label=below:$s_1$] {}; \&
\node (s2) [state, label=below:$s_2$, label=above:$+1$, fill=lightgray] {}; \\
};
\draw [->] (s0) -- (s1);
\draw [->] (s1) -- (s2);
\draw [->] (s2) edge [loop right] (s2);
\end{tikzpicture}
\qquad
\begin{tikzpicture}
\matrix [column sep=1cm] {
\node (s0) [state, initial, label=below:$\Abst{s}_0$] {}; \&
\node (s1) [state, label=below:$\Abst{s}_2$, label=above:$+1$, fill=lightgray] {}; \\
};
\draw [->] (s0) -- (s1);
\draw [->] (s0) edge [loop above] (s1);
\draw [->] (s1) edge [loop right] (s2);
\end{tikzpicture}
\caption{The ground MDP (left) and the abstract MDP (right)
used in the proof of \cref{th:realizable-homomorphisms-back}.}
\label{fig:mdp-row}
\end{figure}
\begin{proof}
Consider the MDP in \cref{fig:mdp-row}.
This is a very simple MDP $\MDP = \Tuple{\States, \Actions, T, R, \gamma}$
with three states $\States = \{s_0, s_1, s_2\}$, an action $\Actions = \{a_0\}$,
deterministic transitions as indicated by the figure,
and a reward of $+1$ in state~$s_2$, zero otherwise.
The state mapping function is constructed as $\Mapping(s_0) = \Mapping(s_1) = \Abst{s}_0$ and $\Mapping(s_2) = \Abst{s}_1$.
The abstract MDP is $\Abst\MDP = \Tuple{\{\Abst{s}_0, \Abst{s}_1\}, \{\Abst{a}_0\}, \Abst{T}, \Abst{R}, \gamma}$,
where the reward function returns $+1$ in state $\Abst{s}_1$, zero otherwise,
and the transition function $\Abst{T}$ only allows the transitions indicated by the arrows.
The exact values for the stochastic transitions in $\Abst{s}_0$ are
$\Abst{T}(\Abst{s}_1 \Given \Abst{s}_0, \Abst{a}_0) \coloneqq \gamma / (1 + \gamma)$ and
$\Abst{T}(\Abst{s}_0 \Given \Abst{s}_0, \Abst{a}_0) \coloneqq 1 / (1 + \gamma)$.
We now show that $\Tuple{\Abst\MDP, \Mapping}$ is admissible and perfectly realizable.
Let us remind that $\Abst{s}\StartSym$ is the dummy state symbol that represents the beginning of an episode in the abstract MDP.
Then, we apply the equations in~\eqref{eq:computed-option-mdp} to get:
\begin{align}
\tilde{h}_{\Abst{s}\StartSym \Abst{s}_0 \Abst{a}_0}(\Abst{s}_1)
&= \frac{(1 - \gamma)\, \gamma\, \Abst{T}(\Abst{s}_1 \Given \Abst{s}_0, \Abst{a}_0 )}{1 - \gamma\, \Abst{T}(\Abst{s}_0 \Given \Abst{s}_0, \Abst{a}_0)}
= \frac{(1 - \gamma)\, \gamma^2 / (1 + \gamma)}{1 - \gamma / (1 + \gamma)}
= (1 - \gamma)\, \gamma^2 \\
\tilde{V}_{\Abst{s}\StartSym \Abst{s}_0 \Abst{a}_0} &= \frac{\Abst{R}(\Abst{s}_0, \Abst{a}_0)}{1 - \gamma\, \Abst{T}(\Abst{s}_0 \Given \Abst{s}_0, \Abst{a}_0)} = 0 \\
\tilde{V}_{\Abst{s}_0 \Abst{s}_1 \Abst{a}_0} &= \frac{\Abst{R}(\Abst{s}_1, \Abst{a}_0)}{1 - \gamma\, \Abst{T}(\Abst{s}_1 \Given \Abst{s}_1, \Abst{a}_0)} = \frac{1}{1-\gamma}
\end{align}
With one action, there is only one option~$o$ for each block that achieve a value of 0\ in $\Block{s_0}$, since all rewards in $s_0, s_1$ are null,
and a value of $1/(1-\gamma)$ in $\Block{\Abst{s}_1}$, since the rewards from $s_2$ are 1 for an infinite number of steps.
Lastly, the block occupancy measure $h_{\Abst{s}_0}^o(\Abst{s}_1 \Given s_0)$ is also $(1 - \gamma) \gamma^2$ because it can only reach $s_2$ after exactly two steps.
Since the terms satisfy these equalities, the abstraction is both admissible and perfectly realizable.
To conclude the proof, we show that the state abstraction function $\Mapping$ prevents the existence of an MDP homomorphism from~$\MDP$ to~$\Abst\MDP$.
Simply, in the abstraction above, the ground states $s_0$ and $s_1$ both belong to the same block.
However, this fact contradicts \eqref{eq:hom-transition}, because:
\begin{equation}
\sum_{s \in \Block{\Mapping(s_2)}} T(s \Given s_0, a_0) = T(s_2 \Given s_0, a_0) = 0 \neq
1 = T(s_2 \Given s_1, a_0) = \sum_{s \in \Block{\Mapping(s_2)}} T(s \Given s_1, a_0)
\end{equation}
Since $\Mapping(s_0) = \Mapping(s_1)$, the transition function defined in \cref{eq:hom-transition} is undefined for any $g_s: \Actions \to \Abst\Actions$.
\end{proof}
We now turn our attention to stochastic bisimulation.
As we will see, the same results above still hold because their expressive power is equivalent to MDP homomorphisms.
\paragraph{Stochastic bisimulation}
Stochastic bisimulation \citep{givan_2003_EquivalenceNotionsModel} is a technique for state minimization in MDPs,
inspired by the bisimulation relations for transition systems and concurrent processes.
Given an MDP~$\MDP$, it allows to define another MDP, that we write as $\Abst\MDP$,
in which one or more states are grouped together if they are in the bisimilarity relation.
In this section, we study this relation and we formally verify that bisimulation is strictly less expressive (meaning, more stringent),
than the realizability condition that this paper proposes.
We first introduce some required notation.
Given a binary relation $E \subseteq \States \times \States'$, we write $(s, s') \in E$ if any two $s, s' \in \States$ are in the relation.
If every $s \in \States$ and $s' \in \States'$ appears in some pair in $E$,
we define $E|\States$ to be the partition of~$\States$ obtained by grouping all states that are reachable
under the reflexive, symmetric, and transitive closure of~$E$.
In this section, for $s \in \States$, we write $\Block{s}_{E|\States}$ to denote the set in the partition $E|\States$ to which $s$ belongs.
$E|\States'$ and $\Block{s'}_{E|\States'}$ are defined analogously.
A \emph{stochastic bisimulation} \citep{givan_2003_EquivalenceNotionsModel}
over two MDPs $\MDP = \Tuple{\States, \Actions, T, R, \gamma}$ and $\MDP' = \Tuple{\States', \Actions, T', R', \gamma}$ with the same action space,
is any relation $Z \in \States \times \States'$ that satisfies, for any $s \in \States, s' \in \States', a \in \Actions$:
\begin{enumerate}
\item $s$ appears in $E$ and $s'$ appears in $E$;
\item If $(s, s') \in E$, then $R(s, a) = R(s', a)$;
\item If $(s, s') \in E$, then for any $(s_n, s_n') \in E$,
\begin{equation}
\sum_{s_v \in \Block{s_n}_{E|\States}} T(s, a, s_v) = \sum_{s_v' \in \Block{s_n'}_{E|\States'}} T'(s', a, s_v')
\end{equation}
\end{enumerate}
Despite the different formalisms, stochastic bisimulations over MDPs and MDP homomorphisms have exactly the same expressive power.
As proven by the following theorem, an MDP homomorphism exists if and only if
This has been proven in a theorem that we report below.
\begin{restatable}{proposition}{homomorphismsandbisimilarity}
\citep[Corollary of Theorem~6]{ravindran_2004_AlgebraicApproachAbstraction}
Let $\Tuple{f, \{g_s\}_{s \in \States}}$ be an MDP homomorphism from an MDP~$\MDP$ to an MDP~$\Abst\MDP$.
The relation $E \subseteq \States \times \Abst\States$, defined by $(s, \Abst{s}) \in E$ if and only if $\Mapping(s) = \Abst{s}$,
is a stochastic bisimulation.
\end{restatable}
This exact statement means that the existence of an MDP homomorphism guarantees the existence of a stochastic bisimulation.
The opposite implication can be also obtained as a result of Theorem~6 from \citet{ravindran_2004_AlgebraicApproachAbstraction}.
Specifically, if $E$ is a maximal stochastic bisimulation from $\MDP$ to $\Abst\MDP$, then there exits an MDP homomorphism between the two.
\section{Realizing with Linear Programming}
\label{sec:app:lp}
For this alternative approach, we show that the realizability problem can be formulated as a linear program, which may be addressed with primal-dual techniques.
This may come as little surprise, since the Lagrangian formulation is one of the possible solution methods for constrained optimization problems such as CMDPs.
However, we present these two techniques separately because some CMDP methods may be more closely related to Deep RL algorithms,
and they can be quite different from online stochastic optimization algorithms for linear programs.
In addition, primal-dual techniques have been studied independently of CMDPs and are often developed as solution methods for unconstrained RL.
Recent research focuses on finding near-optimal policies for non-tabular MDPs, both in the presence of generative simulators and online RL
\citep{defarias_2003_LinearProgrammingApproach,mahadevan_2014_ProximalReinforcementLearning,chen_2016_StochasticPrimaldualMethods,tiapkin_2022_PrimaldualStochasticMirror,gabbianelli_2023_OfflinePrimaldualReinforcement,neu_2023_EfficientGlobalPlanning}.
The advantage of online optimization is that the typically large linear programs would not be stored explicitly.
This is still an open field of study and, similarly to the CMDP formulation above,
the formulation we propose here may be solved with any feasible algorithm for this setting.
The linear programming (LP) formulation of optimal planning in MDPs
dates back to \citet{puterman_1994_MarkovDecisionProcesses,bertsekas_1995_DynamicProgrammingOptimal}.
We first show this classic formulation here and then add the additional constraints.
Using vector notation for functions and distributions, we interpret the rewards as a vector
$R \in \Reals^{SA}$ and the initial distribution as $\nu \in \Reals^S$.
Transitions are written as a matrix $P \in \Reals^{SA \times S}$ where $P(sa, s') \coloneqq T(s' \Given s, a)$.
Let $E \in \Reals^{SA \times S}$ with $E(s a, s') \coloneqq \Indicator(s = s')$,
be a matrix that copies elements for each action.
Then, the planning problem in MDPs is expressed as:
\begin{equation}\label{eq:primal}
\begin{gathered}
\max_{b \in \Reals^{SA}:\, b \ge 0}\quad {b}^T {R} \\
\begin{aligned}
\textup{s.t.}\quad E^T b - \gamma\, P^T b = (1 - \gamma)\, \nu
\end{aligned}
\end{gathered}
\end{equation}
The constraint expressed here is the Bellman flow equation on the state-action occupancy distribution.
At the optimum, the solution $b^*$ is the discounted state-action occupancy measure of the optimal policy,
and we have $E^T b^* = d^{\Policy^*}_\nu$.
In addition, the objective is the scaled optimal value $V^* = \langle b^*, R \rangle / (1 - \gamma)$.
The dual linear program is
\begin{equation}\label{eq:dual}
\begin{gathered}
\min_{V \in \Reals^{S}}\quad (1 - \gamma)\, \nu^T V \\
\begin{aligned}
\textup{s.t.}\quad E\, V - \gamma\, P\, V \ge R
\end{aligned}
\end{gathered}
\end{equation}
and the optimum of this problem is $V^*$, the value of the optimal policy.
Solving either the primal or the dual problem is equivalent to solving the given MDP.
The references cited above are only some of the works that adopt this linear formulation to find the optimal policy.
For generalizing to non-tabular MDPs, the linear formulation is often expressed in feature space \citep{defarias_2003_LinearProgrammingApproach}.
Here, we work with the tabular equations shown above for simplicity.
The LP formulation just presented can now be applied to each block MDP and modified to introduce the additional constraints.
Similarly to our choice for CMDPs, we only express the constraint on occupancy distributions.
Due to the equality constraint in \eqref{eq:primal}, the vector~$b$ is forced to be a state-action occupancy distribution.
Thus, all $\Abst{S}-1$ constraints from \eqref{def:realizability-from} can be written in the primal program as
$B^T b \ge \tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}} - \PRealizableT$, where
$B \in \Reals^{SA \times (\Abst{S}-1)}$ is the matrix that sums all occupancies across states and actions for one block as
$B^T(\Abst{s}, sa) \coloneqq \Indicator(\Abst{s} = \Mapping(s))$.
The linear program becomes
\begin{equation}
\begin{gathered}
\max_{b \in \Reals^{SA}:\, b \ge 0}\quad b^T R \\
\begin{aligned}
\textup{s.t.}\quad E^T b - \gamma\, P^T b &= (1 - \gamma)\, \nu\\
-B^T b &\le \PRealizableT - \tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}
\end{aligned}
\end{gathered}
\end{equation}
Computing the dual of this program we have:
\begin{equation}
\begin{gathered}
\min_{V \in \Reals^{S},\, y \in \Reals^{\Abst{S}-1},\, y \ge 0}\quad
\begin{pmatrix} (1 - \gamma)\, \nu \\ \PRealizableT - \tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}} \end{pmatrix}^T
\begin{pmatrix} V \\ y\end{pmatrix}\\
\begin{aligned}
\textup{s.t.}\quad
\begin{pmatrix} E - \gamma P & -B \end{pmatrix}
\begin{pmatrix} V\\y \end{pmatrix}
\ge R
\end{aligned}
\end{gathered}
\label{eq:dual-with-constrainedT}
\end{equation}
We do not need to encode the second constraint on rewards because it will be satisfied by the optimum, provided that $(\Abst{s}_p \Abst{s}, \Abst{a})$ is realizable.
The dual vector~$y$ gives interesting insights about how this formulation works.
Looking at the constraint in \eqref{eq:dual-with-constrainedT},
we see that the variables~$y$ play the role of artificial terminal values that are placed at exit states.
In other words, these variables are excess values that are needed to incentivize an increased state occupancy at exit states.
This is consistent with the classic interpretation of slack variables in dual programs.
From an HRL perspective, on the other hand, each entry of~$y$ is related to the terminal value associated with neighboring blocks.
This is what causes the optimization problem to shift from pure maximization of the internal block value $V^o_\nu$,
towards a compromise between the current block and other, more rewarding, blocks.
Therefore, if the optimal vector $y^*$ was known in advance,
the realizability problem of each abstract state and action could be solved simply by setting the rewards of the block MDP as
\begin{equation}
R_{\Abst{s}}(s, a) \coloneqq
\begin{cases}
R(s, a) & \text{if $s \in \Block{\Abst{s}}$}\\
y^*(\Mapping(s)) & \text{if $s \in \Exits_{\Abst{s}}$}\\
0 & \text{if $s = \SinkS$}
\end{cases}
\end{equation}
and optimizing the classic RL objective over $\MDP_{\Abst{s}}$ with any (Deep) RL technique.
With this interpretation, we can recognize that $y^*$ is related to what \citet{wen_2020_EfficiencyHierarchicalReinforcement} called ``exit profiles''.
The main difference is that, unlike exit profiles, the values~$y^*$ are homogeneous within blocks and are not assumed to be known in advance.
\section{Sample complexity of \protect\Ouralg}
In this section, we use $O_t$, $\Abst{\MDP}_t$ and $\Abst{\Policy}_t$ to denote, respectively,
the state of the variables $O$, $\Abst\MDP$ and $\Abst\Policy$ in \cref{alg:main}, at the beginning of episode~$t \in \Naturals_+$.
Moreover, we represent the set of ``known'' tuples, which have been realized already, as
$\Known_t \coloneqq \{(\Abst{s}_p \Abst{s}, \Abst{a}) \Given O_t(\Abst{s}_p \Abst{s}, \Abst{a}) \text{ is not null}\}$.
The structure of this section is the following.
The main sample complexity theorem comes first, and the other lemmas follow below.
\Cref{th:abstractoner-any-option} proves that \FAbstractOneR updates the rewards of $\Abst{\MDP}_t$ in such a way as to obtain the intended targets $\tilde{V}$ for the block values.
\Cref{th:abstractoner-best-option} proves that, when called with a near-optimal realization,
any update made by \FAbstractOneR to the abstract MDP preserves optimism and all the previous realizations.
\Cref{th:algorithm-finds-realizations} proves that, with high probability, any option in $O_t$ is a realization for $\Abst{\MDP}_t$.
Finally, \cref{th:algorithm-sample-complexity} combines these results to obtain the global sample complexity.
\samplecomplexity*
\begin{proof}
In this proof, $O_t$, $\Abst{\MDP}_t$ and $\Abst{\Policy}_t$ respectively denote the state of the variables $O$, $\Abst\MDP$ and $\Abst\Policy$ in \cref{alg:main} at the beginning of episode~$t \in \Naturals_+$.
The algorithm runs \FValueIteration\ at the first episode and each time the abstraction is updated.
According to \cref{th:vi-iterations}, for any $\PAccuracyV > 0$,
after $\frac{1}{1-\gamma} \log \frac{2}{(1-\gamma)^2 \PAccuracyV}$ value iteration updates,
the output $\Abst{\Policy}_t$ is always an $\PAccuracyV$-optimal policy for $\Abst{\MDP}_t$ in all states,
which we write $\Abst{V}^{\Abst{\Policy}^*}_{t}(\Abst{s}) - \Abst{V}^{\Abst{\Policy}_t}_{t}(\Abst{s}) \le \PAccuracyV$
or $\Abst{V}^{\Abst{\Policy}^*}_{t}(\Abst{s}) - \PAccuracyV \le \Abst{V}^{\Abst{\Policy}_t}_{t}(\Abst{s})$,
for all $\Abst{s}$.
Now, for any $\PAccuracyH > 0$, to be set later,
we define the abstract effective horizon as $\Abst{H} \coloneqq \frac{1}{1-\Abst{\gamma}} \log \frac{1}{\PAccuracyH (1 - \Abst{\gamma})}$.
Then, using \cref{th:truncate-horizon-values},
we obtain $\Abst{V}^{\Abst{\Policy}_t}_{t}(\Abst{s}) \le \Abst{V}^{\Abst{\Policy}_t}_{t,\Abst{H}}(\Abst{s}) + \PAccuracyH$,
where $\Abst{V}^{\Abst{\Policy}_t}_{t,\Abst{H}}(\Abst{s})$ is the expected sum of the first $H$ discounted rewards collected in $\Abst{\MDP}_t$ using $\Abst{\Policy}_t$.
So far, the chain of inequalities has led to the following.
\begin{equation}
\Abst{V}^{\Abst{\Policy}^*}_{t}(\Abst{s}) \le \Abst{V}^{\Abst{\Policy}_t}_{t,\Abst{H}}(\Abst{s}) + \PAccuracyH + \PAccuracyV
\end{equation}
The same inequality is also true from any initial distribution.
In particular, we choose the marginal distribution $\Abst{s} \sim \Abst\StartDistrib \coloneqq \Pr(\Mapping(s) \Given \StartDistrib)$,
where $\StartDistrib$ is the initial distribution in~$\MDP$.
We write this as
\begin{equation}\label{eq:sample-complexity-1}
\Abst{V}^{\Abst{\Policy}^*}_{t,\Abst\StartDistrib} \le \Abst{V}^{\Abst{\Policy}_t}_{t,\Abst{H},\Abst\StartDistrib} + \PAccuracyH + \PAccuracyV
\end{equation}
Let us define the set of known tuples as $\Known_t \coloneqq \{(\Abst{s}_p \Abst{s}, \Abst{a}) \Given O_t(\Abst{s}_p \Abst{s}, \Abst{a}) \text{ is not null}\}$,
which contains the set of all tuples for which an option has been learnt.
For each $t \in \Naturals_+$, we define the ``escape event'' $E_t$ as the event that
the execution of the algorithm encounters some tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$ which is not in $\Known_t$,
in the first $\Abst{H}$ blocks of episode~$t$.
This happens if the algorithm reaches the else branch in episode~$t$ after at most $\Abst{H}$ iterations in episode~$t$.
We first consider the case in which $E_t$ does not happen in some episode~$t$.
Since \cref{as:good-initial-abstraction,as:good-realizer,as:new-options-dont-hurt-initiation} are satisfied,
we can apply \cref{th:algorithm-finds-realizations}.
This implies that $\Abst{\MDP}_t$ is optimistic and admissible and,
for each of the first $\Abst{H}$ abstract tuples encountered in that episode,
there exists an associated option in $O_t$ which is a $(\PRealizableR', \PRealizableT')$-realization.
Now, we can apply the second statement of \cref{th:realizab-abstraction-value}
and obtain that the algorithm is executing a policy of options $\Options_t$ that satisfies
\begin{equation}\label{eq:sample-complexity-0}
\Abst{V}^{\Abst\Policy}_{t,\Abst{H},\Abst{\StartDistrib}} - V^{\Options_t}_{\Abst{H},\StartDistrib} \le \frac{\PRealizableR (1-\Abst{\gamma}) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)}
\end{equation}
\Cref{th:realizab-abstraction-value} is stated for value functions over infinite horizons,
but it is applied here to value functions truncated after $\Abst{H}$ blocks.
This is necessary, since $\Options_t$ may not be a fully realized policy of options,
and options are guaranteed to be realizations only for the first $\Abst{H}$ blocks.
On the other hand, the results of \cref{th:realizab-abstraction-value} still follow for the truncated value functions,
because its proof has been written for the finite-horizon variants that tend to infinity for the finite horizon case.
%
Then, since $V^{\Options_t}_{\Abst{H},\StartDistrib} \le V^{\Options_t}_{\StartDistrib}$,
we can combine the inequalities \eqref{eq:sample-complexity-0} and \eqref{eq:sample-complexity-1} and obtain
\begin{equation}
\Abst{V}^{\Abst{\Policy}^*}_{t,\Abst\StartDistrib} \le V^{\Options_t}_\StartDistrib + \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + \PAccuracyH + \PAccuracyV
\end{equation}
Now, using the fact that $\Tuple{\Abst{\MDP}_t, \Mapping}$ is admissible for~$\MDP$,
we can apply the second half of \cref{th:admissible-values} for the ground policy $\Policy^*$,
knowing that the abstract policy $\Abst{\Policy}^*$ satisfies it, and obtain
$V^*_\StartDistrib \le \Abst{V}^{\Abst{\Policy}^*}_{t,\Abst\StartDistrib}$.
From which,
\begin{equation}\label{eq:sample-complexity-2}
V^*_\StartDistrib - V^{\Options_t}_\StartDistrib \le \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + \PAccuracyH + \PAccuracyV
\end{equation}
This proves that the algorithm is near-optimal for every episode~$t$ in which $E_t$ did not occur.
Note that reducing the term $\PAccuracyV$ only increases the computational complexity, not the number of samples used.
In this proof, we will pick $\PAccuracyV \coloneqq \PAccuracyH$, for simplicity.
At the end of the proof, this choice will match what is found in the main algorithm.
For the episodes in which the escape event $E_t$ does happen, instead,
we do not make any guarantee on $V_\StartDistrib^{\Policy_t}$, which might be zero.
Here $\Policy_t$ represents the low-level policy used by the algorithm in episode~$t$.
Let $\neg E_t$ be the negation of the escape event.
Accounting for both cases, without conditioning on $E_t$, the value of the algorithm in episode~$t$ is
\begin{align}
&V_\StartDistrib^{\Policy_t} = \Expected\left[\sum_{i=1}^\infty \gamma^{i-1} r_i \Given \MDP, \Policy_t\right]\\
&\ge \Pr(\neg E_t) \Expected\left[\sum_{i=1}^\infty \gamma^{i-1} r_i \Given \MDP, \Policy_t, \neg E_t \right]\\
\intertext{using \eqref{eq:sample-complexity-2},}
&\ge \Pr(\neg E_t) \left( V^*_\StartDistrib - \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} - 2\PAccuracyH \right)\\
&= V^*_\StartDistrib - \Pr(E_t) V^*_\StartDistrib - (1 - \Pr(E_t))\left(\frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + 2\PAccuracyH \right)
\end{align}
Then,
\begin{align}
V^*_\StartDistrib - V_\StartDistrib^{\Policy_t} &\le \Pr(E_t) V^*_\StartDistrib + (1 - \Pr(E_t))\left(\frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + 2\PAccuracyH \right)\\
&\le \frac{\Pr(E_t)}{1-\gamma} + \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + 2\PAccuracyH
\end{align}
Let $\PAccuracyH' \coloneqq \PAccuracyH (1-\gamma)$,
\begin{align}
V^*_\StartDistrib - V_\StartDistrib^{\Policy_t} &\le \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + \frac{\Pr(E_t)}{1-\gamma} + \frac{2\PAccuracyH'}{1-\gamma}
\end{align}
If $\Pr(E_t) \le \PAccuracyH'$, then the algorithm is near-optimal in episode~$t$, with
\begin{align}
V^*_\StartDistrib - V_\StartDistrib^{\Policy_t} &\le \frac{\PRealizableR (1-\Abst\gamma) + \PRealizableT \Abst{S}}{(1 - \gamma)^2 (1 - \Abst\gamma)} + \frac{3\PAccuracyH'}{1-\gamma}
\end{align}
Now consider any episode~$t$ in which $\Pr(E_t) > \PAccuracyH'$.
We follow a similar reasoning to the proof of theorem~10 in \citet{strehl_2009_ReinforcementLearningFinite}.
The event $E_t$ can be modeled with a Bernoulli random variable $X_t$ with $\Expected[X_t] > \PAccuracyH'$.
We observe that the probability of this event stays constant even in episodes that follow, until some new option is added,
because both the abstract policy and the set of options used remain constant for the known tuples.
In other words, $X_t, X_{t+1}, \dots, X_{t'}$ is a sequence of independent and identically distributed Bernoulli RVs,
where $t'$ is the first episode in which $\Known_{t'-1} \neq \Known_{t'}$ (a new tuple becomes known).
Thanks to our choices,
the sum $\sum_{i = t, \dots, t'-1} X_i$ represents the number of times that
a new trajectory is collected and it contributes to the realization of some $(\Abst{s}_p \Abst{s}, \Abst{a})$ before a new update occurs.
By \cref{as:good-realizer} and the guarantees of PAC-Safe algorithms,
the realizer only requires a number of trajectories that is some polynomial in
$(\abs\States, \abs\Actions, 1/\POptionSubopt, \log(2 \Abst{S}^2 \Abst{A}/\PConfidence), 1/\PMaxViolation, 1/(1-\gamma))$.
Let $\RealizerComplexity(\POptionSubopt, \PMaxViolation)$ be such polynomial.
We now estimate the number of exits required before some tuple becomes known.
To do this, we ensure that $\sum_{i = t, \dots, t-1'} X_i \ge \RealizerComplexity(\POptionSubopt, \PMaxViolation) \Abst{S}^2$ with high probability, through an application of \cref{th:concentration-ineq-bernoullis}.
This implies that, for any $\PConfidenceE > 0$, if
\begin{equation}\label{eq:sample-complexity-3}
t' - t \ge \frac{2}{\PAccuracyH'} \left( \RealizerComplexity(\POptionSubopt, \PMaxViolation) \Abst{S}^2 + \log \frac{1}{\PConfidenceE} \right) \eqqcolon \Delta
\end{equation}
then, $\sum_{i = t, \dots, t'-1} X_i \ge \RealizerComplexity(\POptionSubopt, \PMaxViolation) \Abst{S}^2$,
with probability at least $1 - \PConfidenceE$.
Therefore, with probability $1 - \PConfidenceE$,
there exists some tuple $(\Abst{s}_p \Abst{s}, \Abst{\Policy}_t(\Abst{s}_p \Abst{s}))$ that was encountered
at least $\RealizerComplexity(\POptionSubopt, \PMaxViolation)$ times from $t$~to~$t'-1$,
and, with the same probability, $\Delta$ is the maximum sample complexity for learning a new option.
Concluding,
since the maximum number of options to realize is at most $S^2 A$,
we multiply the bound above for each tuple,
and apply the union bound with $\PConfidenceE \coloneqq \PConfidence / (2 S^2 A)$ to verify that the event
$\sum_{i} X_i \ge \RealizerComplexity(\POptionSubopt, \PMaxViolation)\, \Abst{S}^2$
holds with probability $1 - \PConfidence/2$ for all tuples.
This gives a total sample complexity of
\begin{equation}
\frac{2 \Abst{S}^2 \Abst{A}}{\PAccuracyH'} \left( \RealizerComplexity(\POptionSubopt, \PMaxViolation)\, \Abst{S}^2 + \log \frac{2S^2A}{\PConfidence} \right)
\end{equation}
With a further application of the union bound, we guarantee that this sample complexity and the statement of \cref{th:algorithm-finds-realizations} jointly hold with probability $1-\PConfidence$.
To select the appropriate accuracy, we choose $\PAccuracyH \coloneqq \PAccuracy/(1-\gamma)$,
which gives $\PAccuracyH' = \PAccuracy$.
\end{proof}
\begin{lemma}\label{th:algorithm-finds-realizations}
Under \cref{as:good-initial-abstraction,as:good-realizer,as:new-options-dont-hurt-initiation},
and any positive inputs $\PAccuracy, \PConfidence$,
it holds, with probability $1 - \PConfidence$,
that for every $t \in \Naturals_+$, $\Abst{\MDP}_t$ is optimistic (according to \cref{cond:good-transitions-and-mapping}), and,
for every $(\Abst{s}_p \Abst{s}, \Abst{a}) \in \Known_t$,
$O_t(\Abst{s}_p \Abst{s}, \Abst{a})$ is an $(\PRealizableR', \PRealizableT')$-realization
of $(\Abst{s}_p \Abst{s}, \Abst{a})$ from $\nu_{t,\Abst{s}_p \Abst{s}}$ in~$\Abst{\MDP}_t$,
where
$\PRealizableR' \coloneqq \PRealizableR + \POptionSubopt (1 - \gamma)$ and
$\PRealizableT' \coloneqq \PRealizableT + \PMaxViolation (1 - \gamma)$.
\end{lemma}
\begin{proof}
As assumed by \cref{as:good-realizer},
each instance of \FRealizer is a PAC-Safe RL algorithm with maximum failure probability of
$\PConfidence/(2 \Abst{S}^2 \Abst{A})$.
Since there are less than $\Abst{S}^2 \Abst{A}$ instances of \FRealizer,
and each of them only returns the option at most once,
by the union bound, the probability that any of the instances fail during the execution of \Ouralg\ is at most~$\PConfidence/2$.
Taking into account this failure probability,
we condition the rest of the proof on the event that none of the instances in~$\Algorithm$ fail.
The proof is by induction.
Since $\Abst{\MDP}_1$ is the input of the algorithm,
it is optimistic, according to \cref{as:good-initial-abstraction}.
Also, since $\Known_1$ is empty, the second half of the statement trivially holds.
%
The inductive step will occupy most of the remaining proof.
For any episode $t \ge 1$, assume that $\Abst{\MDP}_t$ is optimistic and,
for every $(\Abst{s}_p \Abst{s}, \Abst{a}) \in \Known_t$,
$O_t(\Abst{s}_p \Abst{s}, \Abst{a})$ is an $(\PRealizableR', \PRealizableT')$-realization
of $(\Abst{s}_p \Abst{s}, \Abst{a})$ from $\nu_{t,\Abst{s}_p \Abst{s}}$ in~$\Abst{\MDP}_t$.
Now, if the algorithm does not enter the block in \cref{alg:line:main-new-option} during episode~$t$,
which can only happen at most once in any episode,
then $\Known_{t+1} = \Known_t$, $O_{t+1} = O_t$ and $\Abst{\MDP}_{t+1} = \Abst{\MDP}_t$.
Therefore, the inductive step is verified for this case.
We now consider the case in which the algorithm does enter the block in \cref{alg:line:main-new-option}.
In this case, a single tuple is added, $\Known_{t+1} = \Known_t \cup \{(\Abst{s}_p \Abst{s}, \Abst{a})\}$,
with its associated option $\Est{o} \coloneqq O_{t+1}(\Abst{s}_p \Abst{s}, \Abst{a})$.
Therefore, we proceed to prove that $\Est{o}$ is an $(\PRealizableR', \PRealizableT')$-realization
of $(\Abst{s}_p \Abst{s}, \Abst{a})$ from $\nu_{t+1,\Abst{s}_p \Abst{s}}$ in~$\Abst{\MDP}_{t}$.
We will link this result to $\Abst{\MDP}_{t+1}$ later in the proof.
Consider $\Algorithm(\Abst{s}_p \Abst{s}, \Abst{a})$, the instance of \FRealizer associated with the newly added tuple.
Copying from \eqref{eq:realize-cmdp-reduction}, and accounting for $\Feasible[,\PMaxViolation]\Policies$,
we observe that the realizer algorithm is solving the following problem:
\begin{equation}\label{eq:realize-cmdp-reduction-relaxed}
\argmax_{o \in \Options_{\Abst{s}_p \Abst{s}}} V^o_{\nu} \qquad s.t. \quad V^o_{\nu,\Abst{s}'} \ge \frac{\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') - \PRealizableT}{1 - \gamma} - \PMaxViolation \quad \forall \Abst{s}' \neq \Abst{s}
\end{equation}
Here, $\nu$ should be intended as $\nu_{t,\Abst{s}_p \Abst{s}} = \Pr(s \Given s_p \in \Block{\Abst{s}_p}, s \in \Block{\Abst{s}}, O_t)$.
In other words, this is the entry distribution caused by the options available at episode~$t$.
Let $o^*$ be the optimal solution of the original optimization problem~\eqref{eq:realize-cmdp-reduction},
and $o^{\PMaxViolation*}$ be the optimal solution of the relaxed problem in~\eqref{eq:realize-cmdp-reduction-relaxed}.
Note that these options always exist, due to \cref{as:good-initial-abstraction}.
In fact, the feasible sets $\Feasible\Policies$ and $\Feasible[,\PMaxViolation]\Policies$ cannot be empty,
because $\Abst{\MDP}^*$ only differs from $\Abst{\MDP}_t$ with respect to the reward function,
and the constraint set only depends on transition probabilities.
Then, by the guarantees of PAC-Safe algorithms,
the instance of $\FRealizer$ returns an option $\Est{o}$ which satisfies all the constraints above and, for the objective,
it holds $V^{o^{\PMaxViolation*}}_{\nu} - V^{\Est{o}}_{\nu} \le \POptionSubopt$.
Now, since $\Feasible\Policies \subseteq \Feasible[,\PMaxViolation]\Policies$,
it holds $V^{o^*}_{\nu} \le V^{o^{\PMaxViolation*}}_{\nu}$,
which implies $V^{o^*}_{\nu} - V^{\Est{o}}_{\nu} \le \POptionSubopt$.
%
Next, we consider the abstraction $\Abst{\MDP}^*$, which is referenced by \cref{as:good-initial-abstraction}.
This unknown 2-MDP is admissible and $(\PRealizableR, \PRealizableT)$-realizable.
Since $o^*$ is an optimal solution of the original realization problem,
by \cref{as:good-initial-abstraction},
we have $\tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}} - V^{o^*}_{\nu} \le \PRealizableR / (1 - \gamma)$,
where the left-most term is $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}}$, computed in~$\Abst{\MDP}^*$.
This means that, in the inequalities above, we can lower bound $V^{o^*}_{\nu}$ by $\tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}} - \PRealizableR / (1 - \gamma)$
and obtain $(1 - \gamma) (\tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}} - V^{\Est{o}}_{\nu}) \le \PRealizableR + \POptionSubopt (1 - \gamma) \eqqcolon \PRealizableR'$.
Regarding the constraints, as we showed in the paragraph before the expression \eqref{eq:realize-cmdp-reduction},
as solution of the relaxed problem \eqref{eq:realize-cmdp-reduction-relaxed} satisfies
$\tilde{h}_{\Abst{s}_p \Abst{s} \Abst{a}}(\Abst{s}') - h^{\Est{o}}_{\nu}(\Abst{s}') \le \PRealizableT + \PMaxViolation (1 - \gamma)$.
Together, the two inequalities above prove that the output of $\Algorithm(\Abst{s}_p \Abst{s}, \Abst{a})$ is a $(\PRealizableR', \PRealizableT')$-realization
of $(\Abst{s}_p \Abst{s}, \Abst{a})$ from~$\nu$ in $\Abst{\MDP}^*$, for
$\PRealizableR' \coloneqq \PRealizableR + \POptionSubopt (1 - \gamma)$ and
$\PRealizableT' \coloneqq \PRealizableT + \PMaxViolation (1 - \gamma)$.
%
Now, according to \cref{as:new-options-dont-hurt-initiation},
this statement will be true not only from $\nu_{t,\Abst{s}_p \Abst{s}}$ but from any future initial distribution
that is caused by the addition of new options in~$O_t$.
So, we will simply say that $\Est{o}$ is an $(\PRealizableR', \PRealizableT')$-realization in $\Abst{\MDP}^*$.
We now distinguish two cases.
If the algorithm does not enter the block in \cref{alg:line:main-update-block} in episode~$t$,
then $\Abst{\MDP}_{t+1} = \Abst{\MDP}_t$.
This means that $\Abst{\MDP}_{t+1}$ is optimistic, by inductive hypothesis,
and $\Est{o}$ is an $(\PRealizableR', \PRealizableT')$-realization in $\Abst{\MDP}_{t+1}$.
Indeed, the failed if-statement ensures that
$(1 - \gamma)(\tilde{V}_{t,\Abst{s}_p \Abst{s} \Abst{a}} - V^{\Est{o}}_\nu) \le \PRealizableR'$.
Since $\Abst{\MDP}^*$ and $\Abst{\MDP}_t$ have the same transition function,
this proves that $O_t(\Abst{s}_p \Abst{s}, \Abst{a})$ is an $(\PRealizableR', \PRealizableT')$-realization in~$\Abst{\MDP}_t$.
All the other options in $O_t$ remain valid realizations after the addition of $\Est{o}$ thanks to \cref{as:new-options-dont-hurt-initiation}
and the fact that no other $\tilde{V}$ is modified during this iteration.
The last case to consider is when the algorithm enters \cref{alg:line:main-update-block} in episode~$t$.
In this case, the abstraction gets updated with \FAbstractOneR.
For characterizing its output, we verify if the preconditions of \cref{th:abstractoner-best-option} are satisfied.
First, \cref{cond:good-transitions-and-mapping} is satisfied by $\Abst{\MDP}_t$ due to the inductive hypothesis.
Second, as option we consider $\Est{o}$, which we already know from above that is an $(\PRealizableR', \PRealizableT')$-realization in $\Abst{\MDP}^*$.
So, we can apply \cref{th:abstractoner-best-option} to obtain:
\begin{enumerate}[label=\roman*)]
\item $\Abst{\MDP}_{t+1}$ is a valid 2-MDP;
\item $\Est{o}$ is an $(\PRealizableR', \PRealizableT')$-realization for $\Abst{\MDP}_{t+1}$;
\item $\Abst{\MDP}_{t+1}$ is optimistic;
\item For all $\Abst{s}_p' \notin \{\Abst{s}, \Abst{s}_p\}$ such that $(\Abst{s}_p' \Abst{s} \Abst{a}) \in \Known_t$,
it holds that $O_{t+1}(\Abst{s}_p' \Abst{s}, \Abst{a})$ is an $(\PRealizableR', \PRealizableT')$-realization in $\Abst{\MDP}_{t+1}$.
\end{enumerate}
For the fourth point, we also used the inductive hypothesis and \cref{as:new-options-dont-hurt-initiation}.
Any tuple that does not involve $\Abst{s}, \Abst{a}$ is not affected by the updated rewards.
Therefore, together with the second and fourth point above, we obtain that $O_{t+1}$ verifies the inductive step.
This concludes the proof.
\end{proof}
\begin{condition}[optimism of $\Abst\MDP$]\label{cond:good-transitions-and-mapping}
Given positive $\PRealizableT$ and $\PRealizableR$,
there exists some admissible $(\PRealizableR, \PRealizableT)$-realizable abstraction
$\Tuple{\Abst{\MDP}^*, \Mapping}$, in which $\Abst{\MDP}^*$ only differs from $\Abst\MDP$ by its reward function
and $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge \tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}}$ for all $\Abst{s}_p, \Abst{s}, \Abst{a}$.
\end{condition}
\begin{lemma}\label{th:abstractoner-best-option}
Consider an MDP~$\MDP$, an abstraction $\Tuple{\Abst\MDP, \Mapping}$ satisfying \cref{cond:good-transitions-and-mapping},
any tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$, and some option $o \in \Options_{\Abst{s}_p \Abst{s}}$
that is an $(\PRealizableR, \PRealizableT)$-realization of $(\Abst{s}_p \Abst{s}, \Abst{a})$ in $\Abst{\MDP}^*$ from some $\nu \in \Distribution{\Entries_{\Abst{s}_p \Abst{s}}}$.
Also, let $V \coloneqq \min\{V^o_\nu + \PRealizableR/(1-\gamma), 1/(1-\gamma)\}$ and
$\Abst\MDP' \coloneqq \FAbstractOneR(\Abst\MDP, {(\Abst{s}_p \Abst{s}, \Abst{a})}, V)$.
If $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge V$, then, it holds:
\begin{enumerate}
\item $\Abst\MDP'$ is a valid 2-MDP;
\item $\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}} = V$;
\item $\Abst{\MDP}'$ satisfies \cref{cond:good-transitions-and-mapping} (optimism);
\item For any $\Abst{s}_p' \notin \{ \Abst{s}, \Abst{s}_p \}$,
if $o'$ is an $(\PRealizableR, \PRealizableT)$-realization
of $(\Abst{s}_p' \Abst{s} \Abst{a})$ in~$\Abst{\MDP}$
from some $\nu' \in \Distribution{\Entries_{\Abst{s}_p' \Abst{s}}}$,
then, the same is true in~$\Abst{\MDP}'$.
\end{enumerate}
\end{lemma}
\begin{proof}
The first two points of the statements are direct consequences of \cref{th:abstractoner-any-option}.
In fact, the assumptions taken by this statement subsume those of \cref{th:abstractoner-any-option}.
The third statement says that the transition function of $\Abst{\MDP}'$ and $\Abst{\MDP}^*$ coincide
and that optimism is preserved from $\Abst\MDP$ to~$\Abst\MDP'$.
The first half is immediate to prove because transitions are not modified by \FAbstractOneR.
On the other hand, the rest of the statement is proven by contradiction, by assuming that $\Abst{\MDP}'$ is not optimistic.
% Admissibility in logic terms (not used anymore in this proof but left here for reference)
% !(∀abst_states ∀option ∃action ∀starting_state ∀dest_block admissibility)
% ∃abst_states ∃option ∀action ∃starting_state ∃dest_block !admissibility
In other words, we assume that there exist some $\Abst{s}_p', \Abst{s}', \Abst{a}'$,
such that $\tilde{V}'_{\Abst{s}_p' \Abst{s}' \Abst{a}'} < \tilde{V}^*_{\Abst{s}_p' \Abst{s}' \Abst{a}'}$.
Let us fix $\Abst{s}_p', \Abst{s}', \Abst{a}'$ according to the statement above.
For the optimism of $\Abst\MDP$, it follows that
$\tilde{V}_{\Abst{s}_p' \Abst{s}' \Abst{a}'} \ge \tilde{V}^*_{\Abst{s}_p' \Abst{s}' \Abst{a}'}$.
However, due to how $\FAbstractOneR$ is defined,
it is possible that $\tilde{V}'_{\Abst{s}_p' \Abst{s}' \Abst{a}'} \neq \tilde{V}_{\Abst{s}_p' \Abst{s}' \Abst{a}'}$
only if $\Abst{s}' = \Abst{s}$ and $\Abst{a}' = \Abst{a}$, which are part of the tuple given in input to the function.
Now, let us assume $\Abst{s}_p' = \Abst{s}_p$.
We see that:
\begin{align}
\tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}} &> \tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}} & \text{\small (initial assumption)}\\
&= \min\{V^o_\nu + \PRealizableR/(1-\gamma), 1/(1-\gamma)\} & \text{\small (point two)}\\
&\ge \min\{\tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}}, 1/(1-\gamma)\} & \text{\small ($o$ is an $\PRealizableR$-realization in $\Abst{\MDP}^*$)} \\
&\ge \tilde{V}^*_{\Abst{s}_p \Abst{s} \Abst{a}}
\end{align}
which is a contradiction.
Then, necessarily $\Abst{s}_p' \neq \Abst{s}_p$.
From here, starting from the usual initial assumption,
\begin{align}
& \tilde{V}^*_{\Abst{s}_p' \Abst{s} \Abst{a}} > \Abst{R}'(\Abst{s}'_p \Abst{s}, \Abst{a}) + \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}'_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})}\\
& = \min\{1, \Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} - V^+_{\Abst{s}_p' \Abst{s} \Abst{a}} \} + \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}'_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})}
\end{align}
Where $\min\{1, \Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} - V^+_{\Abst{s}_p' \Abst{s} \Abst{a}} \}$
is the assignment made in \cref{alg:line:abstractoner-other-sp},
and $V^+_{\Abst{s}_p' \Abst{s} \Abst{a}}$ is $\tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}}$,
computed in the MDP obtained after the assignments above \cref{alg:line:abstractoner-other-sp}.
From here, we continue considering the case $\Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} - V^+_{\Abst{s}_p' \Abst{s} \Abst{a}} \le 1$:
\begin{align}
\tilde{V}^*_{\Abst{s}_p' \Abst{s} \Abst{a}} > \Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} - V^+_{\Abst{s}_p' \Abst{s} \Abst{a}} + \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}'_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})} \label{eq:abstractoner-proof-cases1}
\end{align}
Expanding $V^+_{\Abst{s}_p' \Abst{s} \Abst{a}}$, the whole right-hand term simplifies to $\tilde{V}_{\Abst{s}'_p \Abst{s} \Abst{a}}$.
However, $\tilde{V}^*_{\Abst{s}_p' \Abst{s} \Abst{a}} > \tilde{V}_{\Abst{s}'_p \Abst{s} \Abst{a}}$
contradicts the fact that $\Abst\MDP$ is optimistic.
Finally, we consider the case
$\Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} - V^+_{\Abst{s}_p' \Abst{s} \Abst{a}} > 1$.
Then,
\begin{align}
\tilde{V}^*_{\Abst{s}_p' \Abst{s} \Abst{a}} &> 1 + \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}'_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})} \\
&\ge \Abst{R}^*(\Abst{s}_p' \Abst{s}, \Abst{a}) + \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}'_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})}
\end{align}
Now, we argue that $\Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \ge \Abst{R}^*(\Abst{s}\Abst{s}, \Abst{a})$.
In fact, under the case we were considering,
it is also true that $\tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} > V^+_{\Abst{s}_p' \Abst{s} \Abst{a}}$,
which means that the reward function at $(\Abst{s}\Abst{s}, \Abst{a})$ has been modified by the algorithm.
In turn, this only happens when $\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) = 0$,
which means that only $\Abst{R}'(\Abst{s} \Abst{s}, \Abst{a})$ contributes to $\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}}$.
However, since we know by statement~2 that $\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}} = \min\{V^o_\nu + \PRealizableR/(1-\gamma), 1/(1-\gamma)\}$,
if it was the case that $\Abst{R}^*(\Abst{s}\Abst{s}, \Abst{a}) > \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a})$,
then, the rewards of $(\Abst{s}_p \Abst{s}, \Abst{a})$ would not be $\PRealizableR$-realizable in $\Abst{\MDP}^*$ with~$o$, as we assumed
(for instance, we can consider the case $V^o_\nu = 0$, $\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}} = \PRealizableR/(1-\gamma)$).
Thus, we established that $\Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \ge \Abst{R}^*(\Abst{s}\Abst{s}, \Abst{a})$,
and we conclude the chain of inequalities above:
\begin{align}
\tilde{V}^*_{\Abst{s}_p' \Abst{s} \Abst{a}} > \Abst{R}^*(\Abst{s}_p' \Abst{s}, \Abst{a}) + \frac{\Abst\gamma \Abst{R}^*(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}'_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})}
= \tilde{V}^*_{\Abst{s}_p' \Abst{s} \Abst{a}}
\end{align}
This contradiction concludes the proof for point~3.
For the fourth and final result, it suffices to show that $\tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} \ge \tilde{V}'_{\Abst{s}_p' \Abst{s} \Abst{a}}$,
as this would imply $V^{o'}_{\nu'} + \PRealizableR/(1-\gamma) \ge \tilde{V}'_{\Abst{s}_p' \Abst{s} \Abst{a}}$, which expresses realizability in $\Abst{\MDP}'$.
We distinguish two cases.
If $\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) > 0$,
\cref{alg:line:abstractoner-after-ss} does not execute and it holds that
$\Abst{R}'(\Abst{s} \Abst{s}, \Abst{a}) = \Abst{R}(\Abst{s} \Abst{s}, \Abst{a})$ and
$\tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} = V^+_{\Abst{s}_p' \Abst{s} \Abst{a}}$.
The latter expression also implies that $\Abst{R}'(\Abst{s}_p' \Abst{s}, \Abst{a}) = \Abst{R}(\Abst{s}_p' \Abst{s}, \Abst{a})$.
Thus, it is verified that $\tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} = \tilde{V}'_{\Abst{s}_p' \Abst{s} \Abst{a}}$.
Finally, we consider the remaining case, $\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) = 0$.
\begin{align}
&\Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) + {V} - \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \le 0 \\
&V \le \frac{\Abst\gamma \Abst{R}(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})} \\
&V\, \left( \frac{\Abst\gamma \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})} \right)^{-1} \le \Abst{R}(\Abst{s}\Abst{s}, \Abst{a})
\end{align}
and, $\Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \le \Abst{R}(\Abst{s}\Abst{s}, \Abst{a})$.
Therefore,
\begin{align}
\tilde{V}'_{\Abst{s}_p' \Abst{s} \Abst{a}} &= \min\{1, \Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + V^-_{\Abst{s}_p' \Abst{s} \Abst{a}} - \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} \}
+ \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}_p' \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})} \\
&\le V^-_{\Abst{s}_p' \Abst{s} \Abst{a}} \\
&= \Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a})
+ \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}_p' \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})} \\
&\le \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}}
\end{align}
\end{proof}
\begin{lemma}\label{th:abstractoner-any-option}
Consider any MDP~$\MDP$, any abstraction $\Tuple{\Abst\MDP, \Mapping}$,
any abstract tuple $(\Abst{s}_p \Abst{s}, \Abst{a})$ and any $V \in [0, 1/(1-\gamma)]$.
If $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge V$, then
$\Abst\MDP' \coloneqq \FAbstractOneR(\Abst\MDP, {(\Abst{s}_p \Abst{s}, \Abst{a})}, V)$
is a valid 2-MDP and $\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}} = V$.
\end{lemma}
\begin{proof}
First we check that $\Abst\MDP'$ is a valid 2-MDP after the execution of \FAbstractOneR.
To verify this, we already know that $\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) \ge 0$.
However, $\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) \le 1$ is also true, since
we assumed that $\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} \ge V$.
For $\Abst{R}'(\Abst{s} \Abst{s}, \Abst{a})$, we should only verify the case
$\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) = 0$.
In turn, this only happens if
$\Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) \le \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - V$,
that is
$V \le \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a})$.
Then,
\begin{align}
\Abst{R}'(\Abst{s} \Abst{s}, \Abst{a}) &= V \left( \frac{\Abst\gamma \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst\gamma \Abst{T}(\Abst{s} \Given \Abst{s} \Abst{s}, \Abst{a})} \right)^{-1}\\
&\le (\tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a})) \left( \frac{\Abst\gamma \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst\gamma \Abst{T}(\Abst{s} \Given \Abst{s} \Abst{s}, \Abst{a})} \right)^{-1}\\
&= \Abst{R}(\Abst{s} \Abst{s}, \Abst{a})
\end{align}
which proves $\Abst{R}'(\Abst{s} \Abst{s}, \Abst{a}) \in [0, 1]$.
Finally, for any $\Abst{s}'_p \notin \{\Abst{s}, \Abst{s}_p\}$,
we write \cref{alg:line:abstractoner-other-sp} as:
\begin{align}
\Abst{R}'(\Abst{s}'_p \Abst{s}, \Abst{a}) = \min\{1, \Abst{R}(\Abst{s}'_p \Abst{s}, \Abst{a}) + \tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} - V^+_{\Abst{s}_p' \Abst{s} \Abst{a}} \}
\end{align}
where $V^+_{\Abst{s}_p' \Abst{s} \Abst{a}}$ is $\tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}}$,
computed in the MDP obtained after the assignments above \cref{alg:line:abstractoner-other-sp}.
We have already verified that
$\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) \le \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a})$ and
$\Abst{R}'(\Abst{s} \Abst{s}, \Abst{a}) \le \Abst{R}(\Abst{s} \Abst{s}, \Abst{a})$.
This implies that $\tilde{V}_{\Abst{s}_p' \Abst{s} \Abst{a}} - V^+_{\Abst{s}_p' \Abst{s} \Abst{a}}$ is positive and $\Abst{R}'(\Abst{s}'_p \Abst{s}, \Abst{a}) \in [0, 1]$.
Now we verify the second point of the statement by
substituting the definition of $\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}}$ for~$\Abst\MDP'$.
We consider two cases.
If $\Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) > \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - V$,
\begin{align}
\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}} &=
\Abst{R}'(\Abst{s}_p \Abst{s}, \Abst{a}) + \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})}\\
&= \Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) + V - \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} + \frac{\Abst\gamma \Abst{R}(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})}\\
&= V
\end{align}
On the other hand, if $\Abst{R}(\Abst{s}_p \Abst{s}, \Abst{a}) \le \tilde{V}_{\Abst{s}_p \Abst{s} \Abst{a}} - V$,
\begin{align}
\tilde{V}'_{\Abst{s}_p \Abst{s} \Abst{a}} &=
0 + \frac{\Abst\gamma \Abst{R}'(\Abst{s}\Abst{s}, \Abst{a}) \Abst{T}(\Abst{s} \Given \Abst{s}_p \Abst{s}, \Abst{a})}{1 - \Abst{\gamma}\, \Abst{T}(\Abst{s} \Given \Abst{s}\Abst{s}, \Abst{a})} = V
\end{align}
\end{proof}
\subsection*{Other lemmas}
As shown in \citet{agarwal_2021_ReinforcementLearningTheory}, the $\gamma$-contraction property, together with \citet[Corollary 2]{singh_1994_UpperBoundLoss}, gives the following.
\begin{lemma}\label{th:vi-iterations}
Let $Q\AtIter{k}$ be the Q-function obtained after~$k$ \FValueIteration updates,
and let $\Policy\AtIter{k}$ be the greedy policy for $Q\AtIter{k}$.
If $k \ge \frac{\log \frac{2}{(1-\gamma)^2 \PAccuracy}}{1-\gamma}$, then $V^*(s) - V^{\Policy\AtIter{k}}(s) \le \PAccuracy$ for each $s \in \States$.
\end{lemma}
The following statement was expressed for MDPs in \citet{kearns_2002_NearoptimalReinforcementLearning}.
However, its proof only relies on geometric discounting.
So, it can also be applied to any decision process and $k$-MDP.
\begin{lemma}[\citet{kearns_2002_NearoptimalReinforcementLearning}]\label{th:truncate-horizon-values}
In any decision process~$\MDP$ and policy~$\Policy$,
if $H = \frac{1}{1-\gamma} \log \frac{1}{\PAccuracy (1 - \gamma)}$,
then, in any state~$s$, $V^\Policy(s) \le V_H^\Policy(s) + \PAccuracy$,
where $V_H^\Policy$ is the expected sum of the first~$H$ discounted rewards.
\end{lemma}
Finally, we adopt the following concentration inequality from \citet[Corollary~2]{li_2009_UnifyingFrameworkComputational}.
\begin{lemma}[\citet{li_2009_UnifyingFrameworkComputational}]\label{th:concentration-ineq-bernoullis}
Let $X_1, \dots, X_m$ be a sequence of $m$ independent Bernoulli RVs, with $\Pr(X_i) \ge a$, for all~$i$,
for some constant~$a > 0$.
Then, for any~$k \in \Naturals$ and $\PConfidence > 0$,
with probability at least $1 - \PConfidence$,
$\sum_{i = 1, \dots, m} X_i \ge k$, provided that
\begin{equation}
m \ge \frac{2}{a} \left( k + \log \frac{1}{\PConfidence} \right)
\end{equation}
\end{lemma}
\end{document}
%% Abbreviations
% General math
\renewcommand{\Pr}{\mathbb{P}}
\DeclarePairedDelimiter{\abs}{\lvert}{\rvert}
\DeclarePairedDelimiter{\Abs}{\Big\lvert}{\Big\rvert}
\DeclarePairedDelimiter{\norm}{\lVert}{\rVert}
\DeclarePairedDelimiter{\Norm}{\Big\lVert}{\Big\rVert}
\renewcommand{\impliedby}{\Leftarrow}
\renewcommand{\implies}{\Rightarrow}
\renewcommand{\iff}{\Leftrightarrow}
\DeclareMathOperator*{\infimum}{inf}
\DeclareMathOperator*{\supremum}{sup}
\DeclareMathOperator*{\argmax}{arg\,max}
\DeclareMathOperator*{\argmin}{arg\,min}
\DeclareMathOperator{\clip}{clip}
\DeclareMathOperator{\Expected}{\mathbb{E}}
\DeclareMathOperator{\var}{var}
\DeclareMathOperator{\mode}{mode}
\DeclareMathOperator{\cov}{cov}
\DeclareMathOperator{\corr}{corr}
\DeclareMathOperator{\Ber}{Ber}
\DeclareMathOperator{\Bin}{Bin}
\DeclareMathOperator{\Multin}{Mu}
\DeclareMathOperator{\Cat}{Cat}
\DeclareMathOperator{\Poi}{Poi}
\DeclareMathOperator{\Exp}{Exp}
\DeclareMathOperator{\Lapl}{Lap}
\DeclareMathOperator{\Ga}{Ga}
\DeclareMathOperator{\Be}{Beta}
\DeclareMathOperator{\Dir}{Dir}
\DeclareMathOperator{\Unif}{Unif}
\DeclareMathOperator{\sigm}{sigm}
\DeclareMathOperator{\diag}{diag}
\DeclareMathOperator{\sign}{sign}
\DeclareMathOperator{\Supp}{supp} % Support of a distribution
\newcommand{\Reals}{\mathbb{R}}
\newcommand{\Bools}{\mathbb{B}}
\newcommand{\Naturals}{\mathbb{N}}
\newcommand{\Given}{\mid}
\newcommand{\Det}[1]{\delta_{#1}} % Deterministic distribution
\newcommand{\Indicator}{\mathbb{I}}
\newcommand{\Identity}{\mathrm{I}}
\newcommand{\Arrow}[3]{\ensuremath{#1\overset{#2}{\longrightarrow}#3}}
\DeclarePairedDelimiterX{\DivergencePar}[2]{(}{)}{%
#1\;\delimsize\|\;#2%
}
\newcommand{\Dkl}{D_{KL}\DivergencePar}
% Convention for each group
\newcommand{\Const}[1]{\mathit{#1}}
\newcommand{\Est}[1]{\hat{#1}}
\newcommand{\Approx}[1]{\tilde{#1}}
\newcommand{\Set}[1]{\mathcal{#1}}
\newcommand{\Distribution}[1]{\Delta(#1)}
\newcommand{\Tuple}[1]{\langle #1 \rangle}
\newcommand{\Model}[1]{\mathbf{#1}}
\newcommand{\Nonmark}[1]{\bar{#1}}
%% Topic specific names
% Sets
\newcommand{\States}{\Set{S}}
\newcommand{\Actions}{\Set{A}}
\newcommand{\Observations}{\Set{O}}
\newcommand{\Rewards}{\Set{R}}
\newcommand{\Policies}{\Pi}
\newcommand{\Finals}{\Set{F}}
\newcommand{\Options}{\Omega}
\newcommand{\Goals}{\Set{G}}
\newcommand{\Entries}{\Set{E}}
\newcommand{\Exits}{\Set{X}}
\newcommand{\Known}{\Set{K}}
% Models
\newcommand{\MDP}{\Model{M}}
\newcommand{\DP}{\Model{D}}
% Functions
\newcommand{\Policy}{\pi}
\newcommand{\StartDistrib}{\mu} % initial observation distribution
\NewDocumentCommand{\OccupancyS}{O{\Policy}O{}}{d^{#1}_{\mathsf{s}#2}} % State occupancy (policy as optional arg)
\NewDocumentCommand{\OccupancySA}{O{\Policy}O{}}{d^{#1}_{\mathsf{sa}#2}} % State-action occupancy (policy as optional arg)
\newcommand{\Mapping}{\phi} % state compression function
\newcommand{\Block}[1]{\lfloor\hskip-1pt#1\hskip-1pt\rfloor} % block of ground states
\newcommand{\Potential}{\Phi} % potential function used in RS
\newcommand{\Algorithm}{\mathfrak{A}} % learning algorithm
\newcommand{\Realization}{O}
% Modifiers
\newcommand{\AtIter}[1]{^{(#1)}}
\newcommand{\Sample}[1]{_{#1}}
\newcommand{\Prev}{_p} % Previous
\newcommand{\Abst}[1]{\bar{#1}}
\newcommand{\SinkSym}{_\bot}
\newcommand{\StartSym}{_\star}
\newcommand{\Feasible}[2][]{#2_{\mathsf{c}#1}}
% Others
\newcommand{\Formula}{\varphi}
\newcommand{\Rewardsum}{g}
\newcommand{\Emptystr}{\lambda}
\newcommand{\Toblock}[2]{#1, s_{#1+1} \in \Block{#2}} % Terminate to block #2 after #1 steps
\newcommand{\Tostate}[2]{#1, s_{#1+1} = #2} % Terminate to state #2 after #1 steps
\newcommand{\Transitiontup}[2]{{#1} \leadsto {#2}} % Transition from state to state
\newcommand{\SinkS}{s_\bot}
\newcommand{\StopSymbol}{o_\bot} % string or episode stop symbol
\newcommand{\Blocksteps}[2]{\Block{#1}^{({#2})}} % Set represening t-1 steps inside the block, then outside
\newcommand{\RealizerComplexity}{f_\mathsf{r}} % Sample complexity of the realization algorithm
\newcommand{\Ouralg}{RARL}
% Parameters
\newcommand{\PConfidence}{\delta}
\newcommand{\PAccuracy}{\varepsilon}
\newcommand{\PRealizableR}{\alpha} % realizability assumption on rewards
\newcommand{\PRealizableT}{\beta} % realizability assumption on transitions
\newcommand{\PMaxViolation}{\eta} % maximum constraint violation
\newcommand{\POptionSubopt}{\zeta} % suboptimality of realizations
\newcommand{\PInitialSim}{\xi} % Similar initial distributions
\newcommand{\PAccuracyH}{\PAccuracy_\mathsf{h}}
\newcommand{\PAccuracyV}{\PAccuracy_\mathsf{v}}
\newcommand{\PConfidenceE}{\PConfidence_\mathsf{e}}
% Tikz
\usetikzlibrary{arrows}
\usetikzlibrary{arrows.spaced}
\usetikzlibrary{automata}
\usetikzlibrary{fit}
\usetikzlibrary{positioning}
\usetikzlibrary{calc}
\usetikzlibrary{graphs}
\usetikzlibrary{graphs.standard}
\usetikzlibrary{matrix}
\usetikzlibrary{intersections}
\usetikzlibrary{shapes.geometric}
\usetikzlibrary{shapes.symbols}
\usetikzlibrary{decorations.pathreplacing}
\usetikzlibrary{patterns}
\usetikzlibrary{shadings}
\usetikzlibrary{quotes}
%\usetikzlibrary{graphdrawing}
\usetikzlibrary{backgrounds}
\usetikzlibrary{scopes}
\pgfdeclarelayer{below}
\pgfdeclarelayer{beloww}
\pgfsetlayers{beloww,below,main}
\tikzset{
>=stealth',
ampersand replacement=\&,
font=\footnotesize,
every node/.style={align=center},
lightshadow/.style={fill=lightgray!30},
every loop/.style={min distance=5mm},
loop below left/.style={every loop, out=210,in=240},
loop above right/.style={every loop, out=30,in=60},
loop below right/.style={every loop, out=300,in=330},
loop above left/.style={every loop, out=110,in=150},
%
node/.style={shape=circle, fill=white, thick, draw, minimum size=2.5mm, inner sep=0},
observed node/.style={node, fill=lightgray},
block/.style={
rounded corners=4pt, draw, fill=white, inner sep=6pt, outer sep=0pt},
box/.style={rounded corners=4pt, inner sep=1.8ex, draw=#1!50,
fill=#1!20},
dot/.style={fill, circle, inner sep=0.7pt},
image/.style={inner sep=0pt, outer sep=3pt},
tight/.style={inner sep=0pt, outer sep=0pt},
state/.style={state without output, fill=white, inner sep=0pt, minimum size=8pt},
%
flow/.style={->, thick, >=spaced stealth'},
arrow/.style={->, semithick},
pin line/.style={-, very thin, draw=gray},
label text/.style={draw=none, font=\scriptsize, inner sep=1pt},
% Overlays
invisible/.style={opacity=0, text opacity=0},
alt/.code args={<#1>#2#3}{%
\alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}}
},
visible on/.style={alt={#1{}{invisible}}},
keys on/.style args={<#1>#2}{alt=<#1>{#2}{}},
}
\newcommand{\tikzmarkme}[1]{\tikz[remember picture]\coordinate(#1);}
\newcommand{\tikzmarkword}[2]{\!%
\begin{tikzpicture}[remember picture, baseline=(#2.base)]
\node (#2) [inner sep=1pt, outer sep=0pt] {\normalsize{}#1};
\end{tikzpicture}\!%
}
\newenvironment{tikzimgrelative}[1]%
{\begin{scope}[shift=(#1.north west),x={(#1.north east)},y={(#1.south west)}]}%
{\end{scope}}
\newenvironment{tikzimgabsolute}[1]%
{\begin{scope}[shift=(#1.north west),y={($(#1.north west)+(0,-1)$)}]}%
{\end{scope}}
% 3-room grid
\definecolor{grid2-green}{HTML}{aade87}
\definecolor{grid2-gray}{HTML}{e6e6e6}
\definecolor{grid2-yellow}{HTML}{ffe680}