text:
\section{Introduction}
\label{sec:intro}

Many techniques for solving problems defined on transition systems, like SAT-based planning~\cite{kautz:selman:92} and bounded model checking~\cite{BiereCCZ99}, benefit from knowledge of {\em upper bounds} on the lengths of solution transition sequences, aka \emph{completeness thresholds}.
If $N$ is such a bound, and if a solution exists, then that solution need not comprise more than $N$ transitions.

In AI planning, upper bounds on plan lengths have two main uses related to SAT-based planning.
Firstly, like for bounded model-checking, an upper bound on plan lengths can be used as a completeness threshold, i.e. to prove a planning problem has no solution.
Secondly, it can be used to improve the ability of a SAT-based planner to find a solution.
Typically, a SAT-based planner queries a SAT solver to search for plans of increasing lengths, aka horizons, going through many unsatisfiable formulae until the given horizon is longer than the shortest possible plan.
If a horizon longer than the shortest plan were initially provided, the planner can avoid many of the costly unsatisfiable queries~\cite{DBLP:journals/aicom/GereviniSV15}.
Using plan length upper bounds as horizons in this way
was shown to increase the coverage of SAT-based planners~\cite{Rintanen:Gretton:2013,icaps2017,abdulaziz:2019}.

\citeauthor{BiereCCZ99} identified the {\em diameter} ($d$) and the \emph{recurrence diameter} ($\ensuremath{\mathit{rd}}$), which are topological properties of the state space, as completeness thresholds for bounded model-checking of safety and liveness properties, respectively.
$d$ is the longest shortest path between any two states.
$\ensuremath{\mathit{rd}}$ is the length of the longest simple path in the state space, i.e. the length of the longest path that does not traverse any state more than once.
Both, $d$ and $\ensuremath{\mathit{rd}}$, are upper bounds on the shortest plan's length, i.e. they are completeness thresholds for SAT-based planning.
Also, $d$ is a lower bound on $\ensuremath{\mathit{rd}}$ that can be exponentially smaller.

Computing $d$ or $\ensuremath{\mathit{rd}}$ for succinctly represented transition systems, such as \emph{factored systems}, is hindered by the worst-case complexity of all existing methods, which is exponential or doubly-exponential in the size of the given system, respectively.
This complexity can be alleviated by \emph{compositionally} computing upper bounds on $d$ or $\ensuremath{\mathit{rd}}$ instead of exactly computing them.
Compositional bounding methods compute an upper bound on a factored transition system's diameter by composing together values of topological properties of state spaces of abstract subsystems~\cite{baumgartner2002property,Rintanen:Gretton:2013,abdulaziz2015verified,icaps2017,abdulaziz:2019}, and they are currently the only practically viable method to compute bounds on plan lengths or the state space diameter.
Compositional approaches provide useful bounds on plan length or the diameter using potentially exponentially smaller computational effort compared to directly computing $d$ or $\ensuremath{\mathit{rd}}$, since explicit representations of only abstract subsystems have to be constructed.

In this work we study the computation of $\ensuremath{\mathit{rd}}$ for state spaces of classical planning problems, which are factored transition systems.
The longest simple path and its length are fundamental graph properties.
Thus, computing $\ensuremath{\mathit{rd}}$ for state spaces of planning problems is inherently interesting, as it might reveal interesting properties of different planning problems.
However, our goal is to devise better compositional methods to compute upper bounds on plan lengths to aid SAT-based planning.
This raises an interesting question: why should we focus on computing $\ensuremath{\mathit{rd}}$ instead of $d$?
This question is reasonable since, as stated earlier, $d$ can be computed in exponentially less time than $\ensuremath{\mathit{rd}}$, and $\ensuremath{\mathit{rd}}$ is an upper bound on $d$ that can be exponentially larger.
The reason is simple: it has been shown that $d$ cannot be bounded by diameters of \emph{projections}~\cite[Chapter 3, Theorem 1]{abdulaziz2017formally}.
Since projections are cornerstone abstractions for compositional bounding, a method to compute $d$ cannot be leveraged for compositional bounding.
On the other hand, previous authors showed that, theoretically, recurrence diameters of projections can be composed to bound the concrete system's diameter~\cite{baumgartner2002property,icaps2017}.
Here we explore the potential of this theoretical possibility: we study methods to compute $\ensuremath{\mathit{rd}}$ and the use of those methods to improve existing compositional bounding algorithms.

Our first contribution concerns the relationship between $\ensuremath{\mathit{rd}}$ and the \emph{traversal diameter} ($\ensuremath{\mathit{td}}$), which is another state space topological property.
The best existing compositional bounding method is due to \citeauthor{abdulaziz:2019}~\citeyear{abdulaziz:2019}, and it computes traversal diameters of abstractions and composes them into an upper bound on $d$ and on plan-length.
We show that $\ensuremath{\mathit{td}}$ is an upper bound on $\ensuremath{\mathit{rd}}$, and that $\ensuremath{\mathit{rd}}$ can be exponentially smaller than $\ensuremath{\mathit{td}}$.
This gives an opportunity for substantial improvements in the bounds computed by compositonal bounding methods, if recurrence diameters of abstractions are used instead of their traversal diameters.
However, the practical realisation of this improvement is contingent on whether there is an efficient method to compute $\ensuremath{\mathit{rd}}$.

Our second, and main, contribution is that we investigate practically useful methods to compute recurrence diameters of factored systems that come from planning problems.
We implement two methods to compute recurrence diameters based on the work of \citeauthor{BiereCCZ99}~\citeyear{BiereCCZ99}.
Unlike \citeauthor{BiereCCZ99}, who devised their method and tested it on model-checking problems, we test these methods on planning benchmarks and show that it is impractical for most planning problems.
We show, however, that computing the recurrence diameter within the compositional bounding method by \citeauthor{icaps2017}~\citeyear{icaps2017} leads to bounds that are, as predicted theoretically, much tighter when $\ensuremath{\mathit{rd}}$ is used instead of $\ensuremath{\mathit{td}}$.

However, a challenge is that our method to compute $\ensuremath{\mathit{rd}}$ and that of \citeauthor{BiereCCZ99} have wort-case running times that are doubly-exponential in the size of the given factored system.
This is much worse than the worst-case complexity of computing $\ensuremath{\mathit{td}}$, which is singly-exponential in the size of the factored system.
This stems from the complexity of the problem of computing $\ensuremath{\mathit{rd}}$ for succinct digraphs, which is NEXP-hard~\cite{pardalos2004note,papadimitriou1986note}.
Our third contribution is that we investigate techniques to alleviate the impact of this prohibitive worst-case running time on the overall compositional bounding algorithm by combining the computation of $\ensuremath{\mathit{rd}}$ and $\ensuremath{\mathit{td}}$.

Lastly, we experimentally show that the improved bounds lead to an improved problem coverage for state-of-the-art SAT-based planner {\sc Mp}~\cite{rintanen:12}, when the bounds are used as horizons for it.

\section{Background and Notation}
\label{sec:defs}

We consider {\em factored transition systems} which are characterised in terms of a set of {\em actions}.
From actions we can define a set of {\em valid states}, and then approach bounds by considering properties of {\em executions} of actions on valid states.
Whereas conventional expositions in the planning and model-checking literature would also define initial conditions and goal/safety criteria, here we omit those features from discussion since the
state-space topological properties we consider are independent of those features.

\begin{mydef}[States and Actions]
\label{def:stateAction}
A maplet, $\v \mapsto b$, maps a variable $\v$---i.e. a state-characterising proposition---to a Boolean $b$.
A state, $\state$, is a finite set of maplets.
We write $\ensuremath{\mathit{\mathcal{D}}}(\state)$ to denote $\{\v \mid (\v \mapsto b) \in \state\}$, the domain of $\state$.
For states $\state_1$ and $\state_2$, the union, $\state_1 \uplus \state_2$, is defined as $\{\v \mapsto b \mid $ $\v \in \ensuremath{\mathit{\mathcal{D}}}(\state_1) \cup \ensuremath{\mathit{\mathcal{D}}}(\state_2) \wedge \mbox{\upshape \textsf{if}}\; \v \in \ensuremath{\mathit{\mathcal{D}}}(\state_1) \;\mbox{\upshape \textsf{then}}\; b = \state_1(\v) \;\mbox{\upshape \textsf{else}}\; b = \state_2(\v)\}$.
Note that the state $\state_1$ takes precedence.
An action is a pair of states, $(p,e)$, where $p$ represents the \emph{preconditions} and $e$ represents the \emph{effects}.
For action $\ensuremath{\pi}=(p,e)$, the domain of that action is $\ensuremath{\mathit{\mathcal{D}}}(\ensuremath{\pi})\equiv\ensuremath{\mathit{\mathcal{D}}}(p) \cup \ensuremath{\mathit{\mathcal{D}}}(e)$.
\end{mydef}

\begin{mydef}[Execution]
\label{def:exec}
When an action \ensuremath{\pi}\ $(=(p,e))$ is executed at state $\state$, it produces a successor state $\exec{\state}{\ensuremath{\pi}}$, formally defined as
$\exec{\state}{\ensuremath{\pi}} = \mbox{\upshape \textsf{if}}\; p \nsubseteq \state\; \mbox{\upshape \textsf{then}}\; \state \;\mbox{\upshape \textsf{else}}\; e \uplus \state$.
We lift execution to lists of actions $\ensuremath{\vec{{\act}}}$, so $\exec{\state}{\ensuremath{\vec{{\act}}}}$ denotes the state resulting from successively applying each action from $\ensuremath{\vec{{\act}}}$ in turn, starting at $\state$.
\end{mydef} We give examples of states and actions using sets of literals, where we denote the maplet $a\mapsto \top$ with the literal $a$ and $a\mapsto \bot$ with the literal $\overline{a}$.
For example, $(\{a,\overline{b}\}, \{c\})$ is an action that if executed in a state where $a$ is true and $b$ is false, it sets $c$ to true.
$\ensuremath{\mathit{\mathcal{D}}}((\{a,\overline{b}\}, \{c\})) = \{a,b,c\}$.
We also give examples of sequences, which we denote by the square brackets, e.g. $[a,b,c]$.

\begin{mydef}[Factored Transition System]
\label{def:actoredTransitionSystem}
A set of actions $\delta$ constitutes a factored transition system.
$\ensuremath{\mathit{\mathcal{D}}}(\delta)$ denotes the domain of $\delta$, which is the union of the domains of all the actions in $\delta$.
Let $\mbox{\upshape \textsf{set}}(\ensuremath{\vec{{\act}}})$ be the set of elements in $\ensuremath{\vec{{\act}}}$.
The set of valid action sequences, $\ases{\delta}$, is $\{\ensuremath{\vec{{\act}}} \mid\; \mbox{\upshape \textsf{set}}(\ensuremath{\vec{{\act}}}) \subseteq \delta\}$.
The set of valid states, $\ensuremath{\mathbb{U}}(\delta)$,  is $\{\state \mid \ensuremath{\mathit{\mathcal{D}}}(\state) = \ensuremath{\mathit{\mathcal{D}}} (\delta)\}$.
$\graph(\delta)$ denotes the set of pairs
$\{(\state, \exec{\state}{\ensuremath{\pi}})\mid \state \in \ensuremath{\mathbb{U}}(\delta), \ensuremath{\pi} \in \delta\}$, which is all non self-looping transitions in the state space of $\delta$.
\end{mydef}
 {\makeatletter
\def\old@comma{,}
\catcode`\,=13
\def,{\ifmmode\old@comma\discretionary{}{}{}\else\old@comma\fi}
\makeatother
\makeatletter
\def\old@dot{.}
\catcode`\.=13
\def.{\ifmmode\old@dot\discretionary{}{}{}\else\old@dot\fi}
\makeatother
 \begin{figure}[t]
\begin{minipage}[b]{0.15\textwidth}
\centering
\begin{tikzpicture}[scale=0.8]
\node (s0) at (4,1) [varnodenoperi] {\footnotesize $\overline{\ensuremath{\v_1}\ensuremath{\v_2}}$ } ;
\node (s2) at (3,0)   [varnodenoperi] {\footnotesize $\overline{\ensuremath{\v_1}}\ensuremath{\v_2}$ } ;
\node (s4) at (5,0)   [varnodenoperi] {\footnotesize $\ensuremath{\v_1}\overline{\ensuremath{\v_2}}$ } ;
\node (s6) at (4,-1)[varnodenoperi] {\footnotesize $\ensuremath{\v_1}\ensuremath{\v_2}$ } ;
\draw [->] (s0) -- (s2) ;
\draw [->] (s2) -- (s0) ;
\draw [->] (s0) -- (s4) ;
\draw [->] (s4) -- (s0) ;
\draw [->] (s0) -- (s6) ;
\draw [->] (s6) -- (s0) ;
\draw [->] (s6) -- (s2) ;
\draw [->] (s2) -- (s6) ;
\draw [->] (s4) -- (s2) ;
\draw [->] (s2) -- (s4) ;
\draw [->] (s4) -- (s6) ;
\draw [->] (s6) -- (s4) ;
\end{tikzpicture}
\caption[fig:stateDiag]{\label{fig:stateDiag}}
\end{minipage}
\begin{minipage}[b]{0.15\textwidth}
\centering
\begin{tikzpicture}[scale=0.8]
\node (s0) at (4,1) [varnodenoperi] {\footnotesize $\overline{\ensuremath{\v_1}\ensuremath{\v_2}}$ } ;
\node (s1) at (3,0)   [varnodenoperi] {\footnotesize $\overline{\ensuremath{\v_1}}\ensuremath{\v_2}$ } ;
\node (s2) at (5,0)   [varnodenoperi] {\footnotesize $\ensuremath{\v_1}\overline{\ensuremath{\v_2}}$ } ;
\node (s3) at (4,-1)[varnodenoperi] {\footnotesize $\ensuremath{\v_1}\ensuremath{\v_2}$ } ;
\draw [->] (s0) -- (s1) ;
\draw [->] (s0) -- (s2) ;
\draw [->] (s0) -- (s3) ;
\end{tikzpicture}
\caption[fig:stateDiag2]{\label{fig:stateDiag2}}
\end{minipage}
\begin{minipage}[b]{0.16\textwidth}
\centering
\begin{tikzpicture}[scale=0.8]
\node (s0) at (4,1) [varnodenoperi] {\footnotesize $\overline{\ensuremath{\v_1}\ensuremath{\v_2}}$ } ;
\node (s1) at (3,0)   [varnodenoperi] {\footnotesize $\overline{\ensuremath{\v_1}}\ensuremath{\v_2}$ } ;
\node (s2) at (5,0)   [varnodenoperi] {\footnotesize $\ensuremath{\v_1}\overline{\ensuremath{\v_2}}$ } ;
\node (s3) at (4,-1)[varnodenoperi] {\footnotesize $\ensuremath{\v_1}\ensuremath{\v_2}$ } ;
\draw [<->] (s0) -- (s1) ;
\draw [<->] (s0) -- (s2) ;
\draw [<->] (s0) -- (s3) ;
\end{tikzpicture}
\caption[fig:stateDiag2]{\label{fig:stateDiag3}}
\end{minipage}
\caption{The state spaces of the systems from Examples~\ref{eg:factored},~\ref{eg:td},~and~\ref{eg:tdexpltrd}.
}
\end{figure}

\begin{myeg}
\label{eg:factored}
Consider the factored system $\delta = \{\ensuremath{\act_1} =(\emptyset, \{\ensuremath{\v_1}, \ensuremath{\v_2}\}),
        \ensuremath{\act_2} =(\emptyset, \{\overline{\ensuremath{\v_1}}, \ensuremath{\v_2}\}),
        \ensuremath{\act_3} =(\emptyset, \{\ensuremath{\v_1}, \overline{\ensuremath{\v_2}}\}),
        \ensuremath{\act_4} =(\emptyset, \{\overline{\ensuremath{\v_1}}, \overline{\ensuremath{\v_2}}\})\}$.
Figure~\ref{fig:stateDiag} shows $\graph(\delta)$, i.e.\ the state space of $\delta$, where different states defined on the variables $\ensuremath{\mathit{\mathcal{D}}}(\delta) = \{\ensuremath{\v_1},\ensuremath{\v_2}\}$ are shown.
Since every state can be reached via one action from every other state, the state space is a clique.
\end{myeg}
 }

For a system $\delta$, a bound on the length of action sequences is ${\mbox{\textsc{Exp}}}(\delta) = 2^\cardinality{\ensuremath{\mathit{\mathcal{D}}}(\delta)} - 1$ (i.e.\ one less than the number of valid states), where $\cardinality{\bullet}$ denotes the cardinality of a set or the length of a list.
Other bounds employed by previous approaches are topological properties of the state space.
One such topological property is the diameter, suggested by \citeauthor{BiereCCZ99}~\citeyear{BiereCCZ99}, which is the length of the longest shortest path between any two states in the state space of a system.
\begin{mydef}[Diameter]
\label{def:diam}
The diameter, written $d(\delta)$, is the length of the longest shortest action sequence, formally
\[d(\delta) = \underset{\state \in \ensuremath{\mathbb{U}}(\delta), \ensuremath{\vec{{\act}}} \in \ases{\delta}}{\max} \;\;\; \underset{\exec{\state}{\ensuremath{\vec{{\act}}}} = \exec{\state}{\ensuremath{\vec{{\act}}}'}, \ensuremath{\vec{{\act}}}' \in \ases{\delta} }{\min}\; \cardinality{\ensuremath{\vec{{\act}}}'}\]
\end{mydef}
 Note that if there is a valid action sequence between any two valid states of $\delta$, then there is a valid action sequence between them which is not longer than $d(\delta)$.
Thus it is a completeness threshold for bounded model-checking and SAT-based planning.
Another topological property that is an upper bound on plan lengths is the recurrence diameter, which is the length of the longest simple path in the state space of a transition system.
It was proposed by \citeauthor{BiereCCZ99}~\citeyear{BiereCCZ99}.
\begin{mydef}[Recurrence Diameter]
\label{def:diamrd}
Let $\textsf{\upshape distinct}(\state,\ensuremath{\vec{{\act}}})$ denote that all states traversed by executing $\ensuremath{\vec{{\act}}}$ at $\state$ are distinct states.
The recurrence diameter is the length of the longest simple path in the state space, formally
\[
\ensuremath{\mathit{rd}}(\delta) = \underset{\state \in \ensuremath{\mathbb{U}}(\delta),\ensuremath{\vec{{\act}}} \in \ases{\delta}, \textsf{\upshape distinct}(\state,\ensuremath{\vec{{\act}}})}{\max}\;\; \cardinality{\ensuremath{\vec{{\act}}}}
\]
\end{mydef}
 \begin{myeg}
\label{eg:dexpltrd}
For the system $\delta$ from Example~\ref{eg:factored}, $d(\delta) = 1$, since every state can be reached with one action from every other state.
Nonetheless, $\ensuremath{\mathit{rd}}(\delta) = 3$ as there are many paths with 3 actions in the state space that traverse distinct states, e.g. executing the action sequence $[\ensuremath{\act_1},\ensuremath{\act_2},\ensuremath{\act_3}]$ at the state $\{\overline{\v_1},\overline{\v_2}\}$ traverses the distinct states $[\{\overline{\v_1},\overline{\v_2}\}, \{\v_1,\v_2\}, \{\overline{\v_1},\v_2\}, \{\v_1,\overline{\v_2}\}]$.
\end{myeg}
Note that in general $\ensuremath{\mathit{rd}}$ is an upper bound on $d$, and that it can be exponentially larger than $d$.

\begin{mythm}[\citeauthor{BiereCCZ99}~\citeyear{BiereCCZ99}]
\label{thm:rdgediam}
For any system $\delta$, we have that $d(\delta) \leq \ensuremath{\mathit{rd}}(\delta)$.
Also, there are infinitely many systems for which the recurrence diameter is exponentially (in the number of state variables) larger than the diameter.
\end{mythm}
Like $d$, $\ensuremath{\mathit{rd}}$ is a completeness threshold for SAT-based planning and for safety bounded model-checking but, unlike $d$, $\ensuremath{\mathit{rd}}$ is also a completeness threshold for bounded model-checking of liveness properties, which was the original reason for its inception~\cite{BiereCCZ99}.

Algorithms have been developed to calculate both properties for digraphs, and those algorithms can be directly applied to state spaces of explicitly represented (e.g. tabular) transition systems.
Exact algorithms to compute $d$ have worse than quadratic runtimes in the number of states~\cite{fredman1976new,alon1997exponent,chan2010more,yuster2010computing}, and approximation algorithms have super-linear runtimes~\cite{aingworth1999fast,roditty2013fast,chechik2014better,abboud2016approximation}.
The situation is worse for $\ensuremath{\mathit{rd}}$, whose computation is NP-hard~\cite{pardalos2004note} for explicitly represented systems.
The impracticality of computing $d$ and $\ensuremath{\mathit{rd}}$ is exacerbated in settings where transition systems are described using factored representations, like in planning and model-checking~\cite{fikes1971strips,mcmillan1993symbolic}.
In particular, the worst-case running times are exponentially worse because, in the worst case, all known methods construct an explicit representation of the state space to compute $d$ or $\ensuremath{\mathit{rd}}$ of the state space of a succinctly represented system.
This follows the general pattern of complexity exponentiation of graph problems when graphs are succinctly represented, where, for succinct digraphs, the complexity of computing $d$ is $\Pi_2^P$-hard~\cite{hemaspaandra2010complexity} and the complexity of computing $\ensuremath{\mathit{rd}}$ is NEXP-hard~\cite{papadimitriou1986note}, instead of being in P and NP-hard, respectively, in the explicit case.

\subsection{Compositional Bounding of the Diameter}

The prohibitive complexity of computing $d$ or $\ensuremath{\mathit{rd}}$ suggests they can only be feasibly computed for very small factored systems, systems that are much smaller than those that arise in typical classical planning benchmarks.
However, another possibility is to utilise the computation of $d$ or $\ensuremath{\mathit{rd}}$ within compositional plan length upper bounding techniques.
Existing techniques compute an upper bound on $d$, for a given system, by computing topological properties of abstractions of the given system and then composing the abstractions' topological properties.
Those abstractions are usually much smaller than the given concrete system, where their state spaces can be exponentially smaller than the given system's state space.
Thus, computing topological properties of abstractions might be feasible.

Currently, the compositional bounding method by~\citeauthor{icaps2017}~\citeyear{icaps2017} is the most successful in decomposing a given system into the smallest abstractions.
It decomposes a given factored system using two kinds of abstraction: \emph{projection} and \emph{snapshotting}.
Projection~\cite{knoblock:94,williams:nayak:97} produces an over-approximation of the given system and it was used for bounding by many previous authors.
Snapshotting produces an under-approximation of the given system and it was introduced by~\citeauthor{icaps2017}~\citeyear{icaps2017}.
The compositional method devised by~\citeauthor{icaps2017}~\citeyear{icaps2017} recursively interleaves the application of projection and snapshotting until the system is decomposed into subsystems that can no longer be decomposed, to which we refer here as \emph{base case systems}.
\newcommand{\Balgobrace}[1]{\ensuremath{{\mbox{\textsc{Hyb}}}\langle{#1}\rangle}}
After the system is decomposed into base case systems, a topological property, which we call the \emph{base case function}, of the state space of each of the base case systems is computed.
Then the values of the base case function applied to the different base case systems are composed to bound the diameter of the concrete system.

Most authors used the base case function ${\mbox{\textsc{Exp}}}$, which is one less than the number of valid states for the given base case system~\cite{Rintanen:Gretton:2013,abdulaziz2015verified,icaps2017}.
A notable exception is \citeauthor{abdulaziz:2019}~\citeyear{abdulaziz:2019}, who used the \emph{traversal diameter}, which is a topological property of the state space, as a base case function.
The traversal diameter is one less than the largest number of states that could be traversed by any path.
\begin{mydef}[Traversal Diameter]
\label{def:td}
Let $\ensuremath{\mbox{\upshape \textsf{ss}}}(\state,\ensuremath{\vec{{\act}}})$ be the set of states traversed by executing $\ensuremath{\vec{{\act}}}$ at $\state$.
The traversal diameter is
\[\ensuremath{\mathit{td}}(\delta) = \underset{\state \in \ensuremath{\mathbb{U}}(\delta), \ensuremath{\vec{{\act}}} \in \ases{\delta}}{\max}\;\; \cardinality{\ensuremath{\mbox{\upshape \textsf{ss}}}(\state,\ensuremath{\vec{{\act}}})} - 1.\]
\end{mydef}
 \begin{myeg}
\label{eg:td}
Consider the factored system $\delta = \{\ensuremath{\act_1} =(\{\overline{\ensuremath{\v_1}}, \overline{\ensuremath{\v_2}}\}, \{\ensuremath{\v_1}, \ensuremath{\v_2}\}),
        \ensuremath{\act_2} =(\{\overline{\ensuremath{\v_1}}, \overline{\ensuremath{\v_2}}\}, \{\overline{\ensuremath{\v_1}}, \ensuremath{\v_2}\}),
        \ensuremath{\act_3} =(\{\overline{\ensuremath{\v_1}}, \overline{\ensuremath{\v_2}}\}, \{\ensuremath{\v_1}, \overline{\ensuremath{\v_2}}\})\}$.
The digraph in Figure~\ref{fig:stateDiag2} shows the state space of $\delta$.
For $\delta$, ${\mbox{\textsc{Exp}}}(\delta) = 3$, while $\ensuremath{\mathit{td}}(\delta) = 1$.
\end{myeg}
 \citeauthor{abdulaziz:2019}~\citeyear{abdulaziz:2019} showed that $\ensuremath{\mathit{td}}$ is an upper bound on $\ensuremath{\mathit{rd}}$ and a lower bound on ${\mbox{\textsc{Exp}}}$.
He also showed that $\ensuremath{\mathit{td}}$ can be exponentially smaller than ${\mbox{\textsc{Exp}}}$, as shown in the above example.
This is why, when \citeauthor{abdulaziz:2019}~\citeyear{abdulaziz:2019} used $\ensuremath{\mathit{td}}$ as a base case function, his method computed substantially tighter bounds than previous methods, which all used ${\mbox{\textsc{Exp}}}$.
 \section{The Recurrence Diameter Versus the Traversal Diameter}
We now study the relationship between the recurrence diameter and the traversal diameter.
The core insight we make here is that $\ensuremath{\mathit{rd}}$ can be exponentially smaller than $\ensuremath{\mathit{td}}$.
\begin{mythm}
\label{lem:rdexplttd}
There are infinitely many factored systems whose recurrence diameters are exponentially smaller (in the number of state variables) than their traversal diameters.
\end{mythm}
 \renewcommand{\probss}{\mathcal S}
\begin{proof}
Let, for a natural number $n$, $\ensuremath{\mathit{\mathcal{D}}}_n$ denote the indexed set of state variable $\{\v_1,\v_2,\ldots,\v_{\lceil\log n\rceil}\}$.
Let $\state^n_i$ denote the state defined by assigning all the state variables $\ensuremath{\mathit{\mathcal{D}}}_n$, s.t.\ their assignments binary encode the natural number $i$, where the index of each variable from $\ensuremath{\mathit{\mathcal{D}}}_n$ represents its endianess.
Note: $\state^n_i$ is well defined for $0\leq i\leq 2^{\lceil \log n \rceil} - 1$.

Now, for an arbitrary number $n\in\mathbb{N}$, let ${\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n$ denote the factored system (i.e. set of actions) $\{(\state^{n+1}_0, \state^{n+1}_i)\mid 1 \leq i \leq n\}\cup\{(\state^{n+1}_i, \state^{n+1}_0)\mid 1 \leq i \leq n\}$.
The recurrence diameter of the system ${\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n$ is $2$, regardless of $n$, since any action sequence that traverses more than $3$ states will traverse $\state^{n+1}_0$ more than once.
Now, let $\probss$ denote the set of states in the largest connected component in the state space of ${\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n$, which has $n+1$ states in it.
Since for any two states $\state_i^{n+1},\state_j^{n+1}\in\probss$, there is an action sequence $\ensuremath{\vec{{\act}}}\in\ases{{\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n}$ s.t. $\exec{\state_i^{n+1}}{\ensuremath{\vec{{\act}}}} = \state_j^{n+1}$, and since $\cardinality{\probss}=n+1$, then the traversal diameter of ${\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n$ is $n$.
Accordingly, and since $2^{\cardinality{\ensuremath{\mathit{\mathcal{D}}}({\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n)} - 2} = 2^{\cardinality{\ensuremath{\mathit{\mathcal{D}}}_{n+1}} - 2} = 2^{\lceil \log n \rceil - 1} \leq n$, we have that $2^{\cardinality{\ensuremath{\mathit{\mathcal{D}}}({\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n)} - 2} \leq \ensuremath{\mathit{td}}({\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n)$.
The theorem follows from this and since $\ensuremath{\mathit{rd}}({\scalebox{0.6}{\includegraphics{lotus.pdf}}}_n) = 2$.
\end{proof}

\begin{myeg}
\label{eg:tdexpltrd}
The state space of ${\scalebox{0.6}{\includegraphics{lotus.pdf}}}_3$ is depicted in Figure~\ref{fig:stateDiag3}.
$\ensuremath{\mathit{rd}}({\scalebox{0.6}{\includegraphics{lotus.pdf}}}_3) = 2$, and $\ensuremath{\mathit{td}}({\scalebox{0.6}{\includegraphics{lotus.pdf}}}_3) = 3$.
\end{myeg}
 The fact that $\ensuremath{\mathit{rd}}$ can be exponentially smaller than $\ensuremath{\mathit{td}}$ gives rise to the possibility of substantial improvements to the bounds computed if we use $\ensuremath{\mathit{rd}}$ as a base case function for compositional bounding, instead of $\ensuremath{\mathit{td}}$.

\section{Using the Recurrence Diameter for Compositional Bounding}

Here, we investigate using $\ensuremath{\mathit{rd}}$ as a base case function for the compositional algorithm by~\citeauthor{icaps2017}~\citeyear{icaps2017}.
To do that, we firstly devise a method to compute  $\ensuremath{\mathit{rd}}$.
For explicitly represented digraphs, the computational complexity of finding the length of the longest path is NP-hard~\cite{pardalos2004note}.
Thus, there is not a known method to compute it with a wort-case running time smaller than a time exponential in the size of the given digraph.
\citeauthor{BiereCCZ99}~\citeyear{BiereCCZ99} suggested the only method to compute $\ensuremath{\mathit{rd}}$ of which we are aware.
They encode the question of whether a given number $k$ is $\ensuremath{\mathit{rd}}$ of a given transition system as a SAT formula.
$\ensuremath{\mathit{rd}}$ is found by querying a SAT-solver for different values of $k$, until the SAT-solver answers positively for one $k$.
The method terminates since $\ensuremath{\mathit{rd}}$ cannot be larger than one less the number of states in the given transition system.
The size of their encoding grows linearly in $k^2$.
The encoding of Biere et al. is based on the following theorem, which we restate in our notation.
\newcommand{\ensuremath{\phi_1}}{\ensuremath{\phi_1}}

{
\renewcommand{\underset}[2]{#2#1.\; }
\begin{mythm}[\citeauthor{BiereCCZ99}~\citeyear{BiereCCZ99}]
For a factored system $\delta$ and a natural number $k$, we have that $\ensuremath{\phi_1}(\delta,k)$ is true iff $\ensuremath{\mathit{rd}}(\delta) < k$, where $\ensuremath{\phi_1}(\delta,k)$ denotes the conjunction of
\begin{enumerate}
  \item $\underset{(\state,\state')\in\graph(\delta)}{\forall}\graph(\state,\state')$,
  \item $\underset{\state,\state'\in\ensuremath{\mathbb{U}}(\delta)}{\forall}$ if $(\state,\state')\not\in\graph(\delta)$, then $\neg\graph(\state,\state')$, and
  \item if $\forall\ensuremath{x_1}\ensuremath{x_2}\dots\state_{k+1}. ({\underset{1\leq i\leq k}{\forall}} \graph(\state_i,\state_{i+1}))$ then $({\underset{1\leq i < j \leq k+1}{\exists}} \state_i=\state_j)$.
\end{enumerate}
\end{mythm}
}

\citeauthor{KroeningS03}~\citeyear{KroeningS03} use sorting networks~\cite{DBLP:books/lib/Knuth98a} to devise another encoding of the above question whose size grows linearly in $k\log^2(k)$.
However, they report that, due to hidden constants, their encoding is only significantly smaller than the encoding by \citeauthor{BiereCCZ99} when $150 < k$.
Since this is typically well beyond recurrence diameters that can be practically computed, we only implement the encoding of \citeauthor{BiereCCZ99}.\footnote{The largest $\ensuremath{\mathit{rd}}$ we computed in all our experiments was 93.}

We use an SMT solver to reason about the encoding of $\ensuremath{\mathit{rd}}$.
Thus, for decidability as well as efficiency reasons, we would like to obtain an encoding that is quantifier free, in particular, one that fits the theory of quantifier free uninterpreted functions.
Since $\ensuremath{\phi_1}$ is universally quantified, we reformulate it to its existentially quantified dual.
For predicates $Q$ and $P$ of arity $n$, let $\bigwedge Q(T). \; P(T)$ denote the conjunction of $P(T)$, for all $n$-tuples $T$ where $Q(T)$ holds.
Also, let $\bigvee$ denote the analogous disjunction.
Note: $\bigwedge Q(T). \; P(T)$ is only well defined if $Q$ is true for only a finite set of $n$-tuples.
Also, we do not explicitly bind $Q$ or the tuple $T$ when it is clear from context.

\newcommand{\ensuremath{y}}{\ensuremath{y}}
{
\newcommand{\frak{G}}{\frak{G}}
\renewcommand{\underset}[2]{#2#1.\; }
\begin{myenc}
\label{enc:rdBiere}
For  $\delta$ and $0\leq k$, let $\ensuremath{\phi_1}'(\delta,k)$ denote the conjunction of the formulae
\begin{enumerate}
  \item $\underset{(\state,\state')\in\graph(\delta)}{\bigwedge}\graph(\state,\state')$,
  \item $\underset{\{\state,\state'\}\subseteq\ensuremath{\mathbb{U}}(\delta) \wedge (\state,\state')\not\in\graph(\delta)}{\bigwedge}\neg\graph(\state,\state')$,
  \item ${\underset{1\leq i\leq k}{\bigwedge}} (\graph(\ensuremath{y}_i,\ensuremath{y}_{i+1}) \wedge \underset{i<j\leq k+1}{\bigwedge}$\\ $ \ensuremath{y}_i\neq\ensuremath{y}_j)$, and
  \item ${\underset{1\leq i\leq k+1}{\bigwedge}} (\underset{\state\in\ensuremath{\mathbb{U}}(\delta)}{\bigvee} \ensuremath{y}_i=\state)$.
\end{enumerate}
\end{myenc}
}

The SMT formula above is defined over one constant $\state$ for every state in $\ensuremath{\mathbb{U}}(\delta)$, a set of uninterpreted constants $\{\ensuremath{y}_i\mid 1\leq i \leq k+1\}$, one for every state in the simple path of length $k+1$ for which we search, and a function $\graph$ that is true for a pair of constants $(\state, \state')$ iff there is an edge from $\state$ to state $\state'$ in the state space of $\delta$.
\begin{mythm}
\label{thm:rdBiereValid}
$\ensuremath{\phi_1}'(\delta,k)$ is satisfiable iff $k \leq \ensuremath{\mathit{rd}}(\delta)$.
\end{mythm}
\newcommand{\ensuremath{\mathcal{M}}}{\ensuremath{\mathcal{M}}}
\newcommand{\ensuremath{\vDash}}{\ensuremath{\vDash}}
\begin{proof}[Proof]
\newcommand{\ensuremath{\Sigma}}{\ensuremath{\Sigma}}

An SMT formula is defined over a signature $\ensuremath{\Sigma}$, which is a finite set of symbols that are either constants, uninterpreted constants, or the standard logical connectives.
A model $\ensuremath{\mathcal{M}}$ for a signature is a function that maps uninterpreted constants to objects.
A model $\ensuremath{\mathcal{M}}$ entails a formula $\phi$, denoted $\ensuremath{\mathcal{M}} \ensuremath{\vDash} \phi$, iff $\phi$ evaluates to true, under the standard interpretation of logical connectives, after each uninterpreted constant $v$ in $\phi$ is substituted by $\ensuremath{\mathcal{M}}(v)$.
A formula $\phi$ is satisfiable iff $\exists \ensuremath{\mathcal{M}}. \ensuremath{\mathcal{M}} \ensuremath{\vDash} \phi$.

\newcommand{\enc}[2]{\ensuremath{enc(#1,#2)}}

\begin{mylem}
\label{lem:encodingasound}
If $\ensuremath{\phi_1}'(\delta,k)$ is satisfiable, then there is a list of distinct states $[\state_1,\state_2\dots\state_{k+1}]$, such that $(\state_i,\state_{i+1})\in\graph(\delta)$, for $1\leq i\leq k$.
\end{mylem}
\begin{proof}[Proof summary]

Now, since the formula $\ensuremath{\phi_1}'(\delta,k)$ is satisfiable, there is a model $\ensuremath{\mathcal{M}}$, s.t. $\ensuremath{\mathcal{M}}\ensuremath{\vDash}\ensuremath{\phi_1}'(\delta,k)$.
From the definition of entailment and the third conjunct of $\ensuremath{\phi_1}'(\delta,k)$, we have that $\graph(\ensuremath{\mathcal{M}}(\ensuremath{y}_i),\ensuremath{\mathcal{M}}(\ensuremath{y}_{i+1}))$ and $\ensuremath{\mathcal{M}}(\ensuremath{y}_i)\neq\ensuremath{\mathcal{M}}(\ensuremath{y}_j)$ hold, for all $1\leq i\leq k$ and
$i<j\leq k$.
From this, the first, the second, and fourth conjuncts of $\ensuremath{\phi_1}'(\delta,k)$
,
we have that $(\ensuremath{\mathcal{M}}(\ensuremath{y}_i),\ensuremath{\mathcal{M}}(\ensuremath{y}_{i+1}))\in\graph(\delta)$.
This finishes our proof.
\end{proof}

\begin{mylem}
\label{lem:encodingacomplete}
If there is a list of distinct states $[\state_1,\state_2\dots\state_{k+1}]$, such that $(\state_i,\state_{i+1})\in\graph(\delta)$, for $1\leq i\leq k$, then $\ensuremath{\phi_1}'(\delta,k)$ is satisfiable.
\end{mylem}
\begin{proof}[Proof summary]
Consider the model $\ensuremath{\mathcal{M}}$ defined as $\ensuremath{\mathcal{M}}(\ensuremath{y}_i) = \state_i$, if $1\leq i\leq k+1$.
Note that $\ensuremath{\mathcal{M}}$ is well-defined for the set of uninterpreted constants in $\ensuremath{\phi_1}'(\delta,k)$, i.e.\ it is well-defined for the set $\{\ensuremath{y}_i\mid 1\leq i\leq k+1\}$.
From the assumptions of this lemma and the definition of $\ensuremath{\phi_1}'(\delta,k)$, we have that $\ensuremath{\mathcal{M}}\ensuremath{\vDash}\ensuremath{\phi_1}'(\delta,k)$.
This finishes our proof.
\end{proof}

From the definition of $\ensuremath{\mathit{rd}}$, there is a list of actions $\ensuremath{\vec{{\act}}}_k\equiv[\ensuremath{\pi}_1,\ensuremath{\pi}_2\dots\ensuremath{\pi}_k]$ and a state $\state_1\in\ensuremath{\mathbb{U}}(\delta)$, s.t.\ $\exec{\state_1}{\ensuremath{\vec{{\act}}}_k}$ traverses distinct states, iff $k<\ensuremath{\mathit{rd}}(\delta)$.
Also, from the definition of $\graph(\delta)$, for any states $\state$ and $\state'$, there is an action $\ensuremath{\pi}_i\in\delta$ s.t.\ $\state' = \exec{\state}{\ensuremath{\pi}_i}$ iff $(\state,\state')\in\graph(\delta)$.
Accordingly, there is a list of distinct states $[\state_1,\state_2\dots\state_{k+1}]$, s.t.\ $(\state_i,\state_{i+1})\in\graph(\delta)$, for $1\leq i\leq k$, iff $k\leq\ensuremath{\mathit{rd}}(\delta)$.
The theorem follows from this and Lemmas~\ref{lem:encodingasound}~and~\ref{lem:encodingacomplete}.
\end{proof}

To use the above encoding to compute $\ensuremath{\mathit{rd}}$ of a given system $\delta$, we iteratively query an SMT solver to check for the satisfiability of $\ensuremath{\phi_1}'(\delta,k)$ for different values of $k$, starting at 1, until the we have an unsatisfiable formula.
The largest $k$ for which the formula is satisfiable is $\ensuremath{\mathit{rd}}(\delta)$.

Observe that, to use Encoding~\ref{enc:rdBiere}, one has to build the entire state space as a part of building the encoding, i.e. one has to build the graph $\graph(\delta)$ and include it in the encoding.
In fact, this is true for both methods, the one by \citeauthor{BiereCCZ99} and the one by \citeauthor{KroeningS03}, as they are both specified in terms of explicitly represented transition systems.
This means that the worst-case complexity of computing $\ensuremath{\mathit{rd}}$ using either one of those encodings is doubly-exponential.
Indeed, this is the best possible wort-case running time for succinct graphs generally, unless the polynomial hierarchy collapses, since computing $\ensuremath{\mathit{rd}}$ is NEXP-hard.

\paragraph{Experimental evaluation} We use Encoding~\ref{enc:rdBiere} as a base case function for the compositional algorithm by~\citeauthor{icaps2017}~\citeyear{icaps2017} instead of $\ensuremath{\mathit{td}}$, which was used as a base case by~\citeauthor{abdulaziz:2019}~\citeyear{abdulaziz:2019} and led to the tightest bounds of any existing method.
We use Yices 2.6.1~\cite{DBLP:conf/cav/Dutertre14} as the SMT solver to prove the satisfiability or unsatisfiability of the resulting SMT formulae.
We run the bounding algorithm by~\citeauthor{icaps2017}~\citeyear{icaps2017} on standard planning benchmarks (from previous planning competitions and ones we modified), once with $\ensuremath{\mathit{td}}$ as a base case and a second time with $\ensuremath{\mathit{rd}}$ as a base case.
We perform our experiments on a cluster of 2.3GHz Intel Xeon machines with a timeout of 20~minutes and a memory limit of 4GB.
Our experiments show that Encoding~\ref{enc:rdBiere} is not practical for planning problems when used as a base case function for the algorithm by~\citeauthor{icaps2017}~\citeyear{icaps2017}, where bounds are only computed within the timeout for less than 0.1\% of our set of benchmarks.
This is because computing $\ensuremath{\mathit{rd}}$ can take time that is exponential in the size of the state space, while computing $\ensuremath{\mathit{td}}$ can be computed in time that is linear in the state space~\cite{abdulaziz:2019}.

\section{A Compact Encoding of Recurrence Diameter}

We now devise a new encoding that performs better than Encoding~\ref{enc:rdBiere}.
The new encoding exploits the factored representation in a way that is reminiscent to encodings used for SAT-based planning~\cite{kautz:selman:92}.
In particular, our aim is to avoid constructing the state space in an explicit form, whenever possible.
We devise a new encoding that avoids building the state space as a part of the encoding and, effectively, we let the SMT solver build as much of it during its search as needed.
\newcommand{\ensuremath{\phi_2}}{\ensuremath{\phi_2}}
\newcommand{\ensuremath{\phi_2'}}{\ensuremath{\phi_2'}}
{
\renewcommand{\underset}[2]{#2#1.\; }
\begin{myenc}
\label{enc:rdnew}
For a state $\state$, let $\state_i$ denote the formula $(\underset{\v\in\state}{\bigwedge}\v_i)\wedge(\underset{\overline{\v}\in\state}{\bigwedge}\neg\v_i)$.
For $\delta$ and $0\leq k$, let $\ensuremath{\phi_2}(\delta,k)$ denote the conjunction of the formulae
\begin{enumerate}
  \item $\underset{1\leq i \leq k}{\bigwedge}\ensuremath{\pi}_i\rightarrow\mbox{\upshape \textsf{pre}}(\ensuremath{\pi})_i\wedge\mbox{\upshape \textsf{eff}}(\ensuremath{\pi})_{i+1}\wedge(\underset{\v\in\ensuremath{\mathit{\mathcal{D}}}(\delta)\setminus\ensuremath{\mathit{\mathcal{D}}}(\mbox{\upshape \textsf{eff}}(\ensuremath{\pi}))} {\bigwedge}\v_i\leftrightarrow\v_{i+1})$,
  \item ${\underset{1\leq i \leq k}{\bigwedge}}\underset{\ensuremath{\pi}\in\delta}{\bigvee}\ensuremath{\pi}_i$, and
  \item $\underset{1\leq i < j \leq k + 1}{\bigwedge}\underset{v\in\ensuremath{\mathit{\mathcal{D}}}(\delta)}{\bigvee}\v_i\neq\v_j$.
\end{enumerate}
\end{myenc}
}

Briefly, the encoding above states that $k$ is not $\ensuremath{\mathit{rd}}$ if there is a sequence of $k$ actions that traverses only distinct states if executed at some valid state.
In more detail, the following are the intuitive meanings of uninterpreted constants in the above formulae: (i) $\ensuremath{\pi}_i$, for all $1\leq i\leq k$ and $\ensuremath{\pi}\in\delta$, is a Boolean variable that represents whether action $\ensuremath{\pi}$ is executed at state $i$, and (ii) $\v_i$, for all $1\leq i\leq k + 1$ and $\v\in\delta$, represents the truth value of state variable $\v$ at state $i$.\footnote{We note that this encoding can easily be formulated as a propositional formula in conjunctive normal format.}

There are three main conjuncts in the encoding.
The first conjunct formalises the fact that, if an action is executed at state $i$, then all of its preconditions hold at state $i$, all of its effects hold at state $i+1$, and all the variables that are not in the effects will continue to have the same value at state $i+1$ as they did at state $i$ (i.e. the frame axiom).
The second conjunct states that at least one action must execute at state $i$.
The third conjunct states that all states are pairwise distinct by stating that for every two states, at least one variable has a different truth value in both states.

\begin{mythm}
\label{thm:rdnewValid}
$\ensuremath{\phi_2}(\delta,k)$ is satisfiable iff $k \leq \ensuremath{\mathit{rd}}(\delta)$.
\end{mythm}
\begin{proof}
Firstly, let $\ensuremath{\phi_2'}(\delta,k)$ denote \[\ensuremath{\phi_2}(\delta,k) \wedge
\bigwedge{1\leq i \leq k}.{\bigwedge \ensuremath{\pi},\ensuremath{\pi}'\in\delta\wedge \ensuremath{\pi}\neq\ensuremath{\pi}'.}\neg\ensuremath{\pi}_i \vee \neg\ensuremath{\pi}'_i.\]
\begin{mylem}
\label{lem:rdnewValid}
$\ensuremath{\phi_2}(\delta,k)$ is satisfiable iff $\ensuremath{\phi_2'}(\delta,k)$ is satisfiable.
\end{mylem}
\begin{proof}[Proof summary]
$\Rightarrow$ Since $\ensuremath{\phi_2}(\delta,k)$ is satisfiable, then there is a model $\ensuremath{\mathcal{M}}$, s.t.\ $\ensuremath{\mathcal{M}}\ensuremath{\vDash}\ensuremath{\phi_2}(\delta,k)$.
Note that $\ensuremath{\mathcal{M}}$ might not entail $\ensuremath{\phi_2'}(\delta,k)$ because $\ensuremath{\phi_2'}(\delta,k)$ has the extra conjunct that only one action is enabled in every step, i.e.\ at step $i$, if $\ensuremath{\mathcal{M}}\ensuremath{\vDash}\ensuremath{\pi}_i$ and $\ensuremath{\mathcal{M}}\ensuremath{\vDash}\ensuremath{\pi}'_i$, then $\ensuremath{\pi}=\ensuremath{\pi}'$.
Nonetheless, conjunct (i) of Encoding 2 necessitates that in order for an action to be enabled in a step, all variables that are not in its effect are left unchanged in the next step.
Accordingly, all actions enabled at a step affect the same state variables and assign all of those variables to the same value.
Thus, we can construct a model that entails $\ensuremath{\phi_2'}(\delta,k)$ by leaving only one action from the set of enabled actions at every step, and disabling the rest.
We formalise that as follows.
For every $0\leq i\leq k$, let $\Pi_i = \{\ensuremath{\pi}_i \mid \ensuremath{\pi} \in \delta \wedge \ensuremath{\mathcal{M}}\ensuremath{\vDash}\ensuremath{\pi}_i\}$, i.e.\ the set of actions enabled in step $i$.
Let $\ensuremath{\epsilon}$ be the choice function, i.e.\ the function that given a set, returns an element from that set if it is not empty, and that is otherwise undefined.
The model that entails $\ensuremath{\phi_2'}(\delta,k)$ is $\ensuremath{\mathcal{M}}'$, defined as follows.
\[
  \ensuremath{\mathcal{M}}'(c) =
  \begin{cases}
     \bot, & \text{if } p\in\Pi_i\text{ and } \ensuremath{\epsilon}(\Pi_i)\neq p\\
     \ensuremath{\mathcal{M}}(c), & \text{otherwise}.\\
  \end{cases}
\]
$\Leftarrow$ Since $\ensuremath{\phi_2'}(\delta,k)$ is the same as $\ensuremath{\phi_2}(\delta,k)$ conjoined with another formula, any model for $\ensuremath{\phi_2'}(\delta,k)$ is a model for $\ensuremath{\phi_2}(\delta,k)$.
\end{proof}
The theorem follows from Lemma~\ref{lem:rdnewValid}, Theorem~\ref{thm:rdBiereValid}, and since $\ensuremath{\phi_1}'(\delta,k) \leftrightarrow \ensuremath{\phi_2'}(\delta,k)$.
The latter fact follows by an induction on $k$, and from the definition of $\ensuremath{\mathit{\mathcal{D}}}(\delta)$ and $\graph(\delta)$.
\end{proof}

\paragraph{Experimental evaluation} We experimentally test the new encoding as a base case function for the algorithm by~\citeauthor{icaps2017}~\citeyear{icaps2017}.
Columns 2 and 3 of Table~\ref{table:boundsDoms} show some data on the bounds computed with both, Encoding~\ref{enc:rdnew} (i.e.\ $\ensuremath{\mathit{rd}}$) and $\ensuremath{\mathit{td}}$, as base case functions.
We note two observations.
Firstly, many more planning problems are successfully bounded within the timeout when Encoding~\ref{enc:rdnew} is used to compute $\ensuremath{\mathit{rd}}$ compared to using Encoding~\ref{enc:rdBiere}.
Encoding~\ref{enc:rdnew} performs much better than Encoding~\ref{enc:rdBiere} in practice since our new encoding is represented in terms of the factored representation of the system, while Encoding~\ref{enc:rdBiere} represents the system as an explicitly represented state space.
This leads to exponentially smaller formulae: Encoding~\ref{enc:rdnew} grows quadratically with the size of the given factored system, while Encoding~\ref{enc:rdBiere} grows quadratically in the size of the state space, which can be exponentially larger than the given factored system.
Indeed, Encoding~\ref{enc:rdnew} delegates the construction of the explicit state space to the SMT solver, which would effectively construct the state space during its search, but lazily.
This is clearly better than constructing the state space a priori when the formula is satisfiable (i.e. when $k\leq\ensuremath{\mathit{rd}}$) as the SMT solver only needs to find a simple path of length $k+1$.
The SMT solver does this without necessarily traversing the entire state space due to its search heuristics.
When the formula is unsatisfiable, the SMT solver has to perform an exhaustive search to produce a proof of unsatisfiability, which is equivalent to constructing the entire state space explicitly.
Since all queries to the SMT solver, except for the last one, are satisfiable, Encoding~\ref{enc:rdnew} is more practically efficient than using Encoding~\ref{enc:rdBiere}.
However, it is worth noting that Encodings~\ref{enc:rdBiere}~and~\ref{enc:rdnew} worst-case running times grow doubly-exponentially in the size of the given factored system.

Secondly, when $\ensuremath{\mathit{rd}}$ is the base case function the bounds computed are much tighter than those computed when $\ensuremath{\mathit{td}}$ as a base case function.
This agrees with the theoretical prediction of Theorem~\ref{lem:rdexplttd}.
This is shown clearly in Figure~\ref{fig:boundcompareTDvsRD} and in Table~\ref{table:boundsDoms}.
In particular, in the domains TPP, ParcPrinter, NoMystery, Logistics, OpenStacks, Woodworking, Satellites, Scanalyzer, Hyp and NewOpen (a compiled Qualitative Preference rovers domain), we have between two orders of magnitude and 50\% smaller bounds when $\ensuremath{\mathit{rd}}$ is used as a base case function compared to $\ensuremath{\mathit{td}}$.
Also, the domain Visitall has twice as many problems whose bounds are less than $10^9$ when $\ensuremath{\mathit{rd}}$ is used instead of $\ensuremath{\mathit{td}}$.
Also, specially interesting domains are Floortile and BlocksWorld, where the recurrence diameter of some of the smaller instances is successfully computed to be less than 10, but whose bounds using $\ensuremath{\mathit{td}}$ are more than $10^9$.
In contrast, equal bounds are found using $\ensuremath{\mathit{rd}}$ and $\ensuremath{\mathit{td}}$ as base case functions in Zeno.

 \section{Further Experiments}
\begin{figure*}
\centering
\begin{minipage}[b]{0.32\textwidth}
\centering
       \includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Balgo-RD-vs-Balgo-TD_ARB-bounds.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
        \includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Balgo-TD_ARB-vs-Balgo-RD-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
        \includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Balgo-RD-TDgt2-vs-Balgo-RD-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
        \includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Balgo-RD-TDgt2-vs-Balgo-RD-TDgt2-SSle50bound-bounds.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
        \includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Balgo-RD-TDgt2-SSle50bound-vs-Balgo-RD-TDgt2-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
       \includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Balgo-RD-TDgt2-SSle50bound-vs-Balgo-TD_ARB-bounds.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
\includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-vs-Mp_noshort-0-plan-withbound-Balgo-TD_ARB-planning-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
\includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-vs-Mp_noshort-0-plan-withbound-Balgo-TD_ARB-total-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
\includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-SSle50bound-vs-Mp_noshort-0-plan-withbound-Balgo-TD_ARB-planning-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
\includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-SSle50bound-vs-Mp_noshort-0-plan-withbound-Balgo-TD_ARB-total-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
\includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-SSle50bound-vs-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-planning-runtimes.png}
\end{minipage}
\begin{minipage}[b]{0.32\textwidth}
\centering
\includegraphics[width=1\textwidth,height=0.8\textwidth]{log-labelled-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-SSle50bound-vs-Mp_noshort-0-plan-withbound-Balgo-RD-TDgt2-total-runtimes.png}
\end{minipage}
     \caption{\label{fig:boundcompareTDvsRD}Different scatter-plots comparing the different bounding algorithms in terms of the quality of their bounds, the needed bound computation time, and the planning time using those bounds as a horizon for {\sc Mp}.}
\end{figure*}
{
\setlength\tabcolsep{1pt}
\def0.9{0.9}
\begin{table*}[h]
\centering
\setlength{\tabcolsep}{3.5pt}
    \begin{tabularx}{0.99\textwidth}{ c | c c c c c | c c c c c | c c c c c | c c c c c }
    \hline
          \multicolumn{1}{c}{\scriptsize }       &\multicolumn{5}{c}{\scriptsize $\ensuremath{\mathit{td}}$}       &\multicolumn{5}{c}{\scriptsize $\ensuremath{\mathit{rd}}$}       &\multicolumn{5}{c}{\scriptsize $\ensuremath{b}_1$}       &\multicolumn{5}{c}{\scriptsize $\ensuremath{b}_2$}\\
    \hline
{\scriptsize Domain}                      &{\scriptsize Min.} &{\scriptsize Max.} &{\scriptsize Avg.} &{\scriptsize \#Bnd.} &{\scriptsize \#Sol.} &{\scriptsize Min.} &{\scriptsize Max.} &{\scriptsize Avg.} &{\scriptsize \#Bnd.} &{\scriptsize \#Sol.} &{\scriptsize Min.} &{\scriptsize Max.} &{\scriptsize Avg.} &{\scriptsize \#Bnd.} &{\scriptsize \#Sol.} &{\scriptsize Min.} &{\scriptsize Max.} &{\scriptsize Avg.} &{\scriptsize \#Bnd.} &{\scriptsize \#Sol.}\\
    \hline
{\scriptsize newopen (1440) }       &{\scriptsize 3e3} &{\scriptsize 7e7  } &{\scriptsize 4e5  } &{\scriptsize 848} &{\scriptsize 157}       &{\scriptsize 2e3} &{\scriptsize 1e7  } &{\scriptsize 9e4  } &{\scriptsize 592} &{\scriptsize ----}       &{\scriptsize 2e3} &{\scriptsize 4e7  } &{\scriptsize 2e5  } &{\scriptsize 845} &{\scriptsize 218}       &{\scriptsize 2e3} &{\scriptsize 4e7  } &{\scriptsize 2e5  } &{\scriptsize 844} &{\scriptsize 219}\\
{\scriptsize logistics (407) }       &{\scriptsize 7e1} &{\scriptsize 4e6  } &{\scriptsize 4e5  } &{\scriptsize 406} &{\scriptsize 170}       &{\scriptsize 6e1} &{\scriptsize 1e4  } &{\scriptsize 3e3  } &{\scriptsize 194} &{\scriptsize ----}       &{\scriptsize 6e1} &{\scriptsize 1e4  } &{\scriptsize 2e3  } &{\scriptsize 193} &{\scriptsize 192}       &{\scriptsize 6e1} &{\scriptsize 1e5  } &{\scriptsize 4e3  } &{\scriptsize 200} &{\scriptsize 195}\\
{\scriptsize elevators (210) }       &{\scriptsize 3e6} &{\scriptsize 1e9  } &{\scriptsize 3e8  } &{\scriptsize 14} &{\scriptsize ----}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize 3e6} &{\scriptsize 1e9  } &{\scriptsize 3e8  } &{\scriptsize 14} &{\scriptsize ----}\\
{\scriptsize rover (141) }       &{\scriptsize 1e2} &{\scriptsize 1e6  } &{\scriptsize 1e5  } &{\scriptsize 51} &{\scriptsize 42}       &{\scriptsize 7e1} &{\scriptsize 9e4  } &{\scriptsize 1e4  } &{\scriptsize 38} &{\scriptsize ----}       &{\scriptsize 7e1} &{\scriptsize 8e5  } &{\scriptsize 7e4  } &{\scriptsize 52} &{\scriptsize 46}       &{\scriptsize 7e1} &{\scriptsize 8e5  } &{\scriptsize 7e4  } &{\scriptsize 52} &{\scriptsize 46}\\
{\scriptsize nomystery (124) }       &{\scriptsize 9e0} &{\scriptsize 6e4  } &{\scriptsize 1e4  } &{\scriptsize 70} &{\scriptsize 6}       &{\scriptsize 9e0} &{\scriptsize 9e3  } &{\scriptsize 2e3  } &{\scriptsize 70} &{\scriptsize ----}       &{\scriptsize 9e0} &{\scriptsize 9e3  } &{\scriptsize 2e3  } &{\scriptsize 70} &{\scriptsize 8}       &{\scriptsize 9e0} &{\scriptsize 9e3  } &{\scriptsize 2e3  } &{\scriptsize 70} &{\scriptsize 7}\\
{\scriptsize zeno (50) }       &{\scriptsize 4e1} &{\scriptsize 5e5  } &{\scriptsize 8e4  } &{\scriptsize 50} &{\scriptsize 31}       &{\scriptsize 4e1} &{\scriptsize 4e1  } &{\scriptsize 4e1  } &{\scriptsize 1} &{\scriptsize ----}       &{\scriptsize 4e1} &{\scriptsize 4e1  } &{\scriptsize 4e1  } &{\scriptsize 1} &{\scriptsize 1}       &{\scriptsize 4e1} &{\scriptsize 2e5  } &{\scriptsize 1e5  } &{\scriptsize 16} &{\scriptsize 1}\\
{\scriptsize hiking (40) }       &{\scriptsize 1e3} &{\scriptsize 1e9  } &{\scriptsize 4e8  } &{\scriptsize 22} &{\scriptsize 1}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize 1e3} &{\scriptsize 1e9  } &{\scriptsize 4e8  } &{\scriptsize 22} &{\scriptsize 1}\\
{\scriptsize TPP (89) }       &{\scriptsize 2e1} &{\scriptsize 6e8  } &{\scriptsize 4e7  } &{\scriptsize 16} &{\scriptsize 9}       &{\scriptsize 2e1} &{\scriptsize 4e4  } &{\scriptsize 8e3  } &{\scriptsize 15} &{\scriptsize ----}       &{\scriptsize 2e1} &{\scriptsize 4e4  } &{\scriptsize 8e3  } &{\scriptsize 15} &{\scriptsize 14}       &{\scriptsize 2e1} &{\scriptsize 6e8  } &{\scriptsize 4e7  } &{\scriptsize 16} &{\scriptsize 9}\\
{\scriptsize Transport (203) }       &{\scriptsize 4e5} &{\scriptsize 2e9  } &{\scriptsize 3e8  } &{\scriptsize 14} &{\scriptsize ----}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize 4e5} &{\scriptsize 1e9  } &{\scriptsize 3e8  } &{\scriptsize 14} &{\scriptsize ----}\\
{\scriptsize GED (97) }       &{\scriptsize 7e6} &{\scriptsize 7e8  } &{\scriptsize 3e8  } &{\scriptsize 5} &{\scriptsize ----}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize ----} &{\scriptsize ----  } &{\scriptsize ----  } &{\scriptsize ----} &{\scriptsize ----}       &{\scriptsize 7e6} &{\scriptsize 7e8  } &{\scriptsize 3e8  } &{\scriptsize 5} &{\scriptsize ----}\\
{\scriptsize woodworking (60) }       &{\scriptsize 2e2} &{\scriptsize 8e7  } &{\scriptsize 2e7  } &{\scriptsize 10} &{\scriptsize ----}       &{\scriptsize 6e1} &{\scriptsize 1e4  } &{\scriptsize 5e3  } &{\scriptsize 3} &{\scriptsize ----}       &{\scriptsize 6e1} &{\scriptsize 1e4  } &{\scriptsize 5e3  } &{\scriptsize 3} &{\scriptsize 1}       &{\scriptsize 2e2} &{\scriptsize 1e7  } &{\scriptsize 3e6  } &{\scriptsize 10} &{\scriptsize 1}\\
{\scriptsize visitall (70) }       &{\scriptsize 7e0} &{\scriptsize 2e3  } &{\scriptsize 6e2  } &{\scriptsize 4} &{\scriptsize 4}       &{\scriptsize 7e0} &{\scriptsize 7e4  } &{\scriptsize 1e4  } &{\scriptsize 7} &{\scriptsize ----}       &{\scriptsize 7e0} &{\scriptsize 1e3  } &{\scriptsize 4e2  } &{\scriptsize 6} &{\scriptsize 6}       &{\scriptsize 7e0} &{\scriptsize 1e3  } &{\scriptsize 4e2  } &{\scriptsize 6} &{\scriptsize 6}\\
{\scriptsize openstacks (111) }       &{\scriptsize 3e5} &{\scriptsize 3e5  } &{\scriptsize 3e5  } &{\scriptsize 6} &{\scriptsize 6}       &{\scriptsize 4e4} &{\scriptsize 4e4  } &{\scriptsize 4e4  } &{\scriptsize 6} &{\scriptsize ----}       &{\scriptsize 4e4} &{\scriptsize 4e4  } &{\scriptsize 4e4  } &{\scriptsize 6} &{\scriptsize 6}       &{\scriptsize 4e4} &{\scriptsize 4e4  } &{\scriptsize 4e4  } &{\scriptsize 6} &{\scriptsize 6}\\
{\scriptsize satellite (10) }       &{\scriptsize 6e2} &{\scriptsize 6e3  } &{\scriptsize 3e3  } &{\scriptsize 10} &{\scriptsize 9}       &{\scriptsize 4e2} &{\scriptsize 2e3  } &{\scriptsize 9e2  } &{\scriptsize 6} &{\scriptsize ----}       &{\scriptsize 4e2} &{\scriptsize 2e3  } &{\scriptsize 9e2  } &{\scriptsize 6} &{\scriptsize 5}       &{\scriptsize 4e2} &{\scriptsize 2e3  } &{\scriptsize 9e2  } &{\scriptsize 6} &{\scriptsize 5}\\
{\scriptsize scanalyzer (60) }       &{\scriptsize 4e3} &{\scriptsize 4e3  } &{\scriptsize 4e3  } &{\scriptsize 1} &{\scriptsize 1}       &{\scriptsize 6e1} &{\scriptsize 6e1  } &{\scriptsize 6e1  } &{\scriptsize 1} &{\scriptsize ----}       &{\scriptsize 6e1} &{\scriptsize 6e1  } &{\scriptsize 6e1  } &{\scriptsize 1} &{\scriptsize 1}       &{\scriptsize 4e3} &{\scriptsize 4e3  } &{\scriptsize 4e3  } &{\scriptsize 1} &{\scriptsize 1}\\
{\scriptsize storage (30) }       &{\scriptsize 1e2} &{\scriptsize 8e7  } &{\scriptsize 2e7  } &{\scriptsize 7} &{\scriptsize 4}       &{\scriptsize 6e0} &{\scriptsize 6e0  } &{\scriptsize 6e0  } &{\scriptsize 1} &{\scriptsize ----}       &{\scriptsize 6e0} &{\scriptsize 6e0  } &{\scriptsize 6e0  } &{\scriptsize 1} &{\scriptsize 1}       &{\scriptsize 1e2} &{\scriptsize 8e7  } &{\scriptsize 2e7  } &{\scriptsize 7} &{\scriptsize 4}\\
{\scriptsize trucks (33) }       &{\scriptsize 5e2} &{\scriptsize 4e8  } &{\scriptsize 8e7  } &{\scriptsize 5} &{\scriptsize 2}       &{\scriptsize 3e2} &{\scriptsize 3e2  } &{\scriptsize 3e2  } &{\scriptsize 2} &{\scriptsize ----}       &{\scriptsize 3e2} &{\scriptsize 3e2  } &{\scriptsize 3e2  } &{\scriptsize 2} &{\scriptsize 2}       &{\scriptsize 3e2} &{\scriptsize 4e8  } &{\scriptsize 8e7  } &{\scriptsize 5} &{\scriptsize 2}\\
{\scriptsize parcprinter (40) }       &{\scriptsize 8e2} &{\scriptsize 4e8  } &{\scriptsize 7e7  } &{\scriptsize 6} &{\scriptsize 1}       &{\scriptsize 8e2} &{\scriptsize 4e8  } &{\scriptsize 8e7  } &{\scriptsize 9} &{\scriptsize ----}       &{\scriptsize 8e2} &{\scriptsize 4e8  } &{\scriptsize 8e7  } &{\scriptsize 9} &{\scriptsize 3}       &{\scriptsize 8e2} &{\scriptsize 4e8  } &{\scriptsize 9e7  } &{\scriptsize 8} &{\scriptsize 2}\\
{\scriptsize maintenance (5) }       &{\scriptsize 5e1} &{\scriptsize 2e3  } &{\scriptsize 4e2  } &{\scriptsize 5} &{\scriptsize 4}       &{\scriptsize 5e1} &{\scriptsize 2e3  } &{\scriptsize 4e2  } &{\scriptsize 5} &{\scriptsize ----}       &{\scriptsize 5e1} &{\scriptsize 2e3  } &{\scriptsize 4e2  } &{\scriptsize 5} &{\scriptsize 4}       &{\scriptsize 5e1} &{\scriptsize 2e3  } &{\scriptsize 4e2  } &{\scriptsize 5} &{\scriptsize 4}\\
{\scriptsize blocksworld (10) }       &{\scriptsize 1e3} &{\scriptsize 5e8  } &{\scriptsize 1e8  } &{\scriptsize 5} &{\scriptsize 2}       &{\scriptsize 8e0} &{\scriptsize 8e0  } &{\scriptsize 8e0  } &{\scriptsize 1} &{\scriptsize ----}       &{\scriptsize 8e0} &{\scriptsize 8e0  } &{\scriptsize 8e0  } &{\scriptsize 1} &{\scriptsize 1}       &{\scriptsize 1e3} &{\scriptsize 5e8  } &{\scriptsize 1e8  } &{\scriptsize 5} &{\scriptsize 2}\\
         \hline
    \end{tabularx}
    \caption{\label{table:boundsDoms}
Column 1: the domain name and the number of instances in it.
Column 2: when using $\ensuremath{\mathit{td}}$ as a base case function: the minimum, maximum bound, the average bound computed, number of instances bounded (below $10^9$), and the number of instances solved using Madagascar with the bound as the horizon.
Column 3, 4, and 5: similar to column 2, but when $\ensuremath{\mathit{rd}}$, $\ensuremath{b}_1$, and $\ensuremath{b}_2$, respectively, are used as base case functions.
}
\end{table*}
}

Note that, although Encoding~\ref{enc:rdnew} is more efficient than Encoding~\ref{enc:rdBiere}, the number of problems that were successfully bounded is less when using $\ensuremath{\mathit{rd}}$ as a base case function compared to $\ensuremath{\mathit{td}}$, since $\ensuremath{\mathit{rd}}$ can take exponentially longer to compute than $\ensuremath{\mathit{td}}$.
Figure~\ref{fig:boundcompareTDvsRD} shows that running time difference for problems successfully bounded using both base case functions.
Also Table~\ref{table:boundsDoms} shows this in terms of the numbers of problems bounded within 20 minutes, when using $\ensuremath{\mathit{rd}}$ vs.\ $\ensuremath{\mathit{td}}$.

One thing we observe during our experiments is that many of the base case systems have traversal diameters that are 1 or 2.
We exploit that to improve the running time by devising a base case function that will only invoke the expensive computation of $\ensuremath{\mathit{rd}}$ in case $\ensuremath{\mathit{td}}$ is greater than 2.
\renewcommand{\mbox{\upshape \textsf{then}}}{\mbox{\upshape \textsf{thn}}}
\renewcommand{\mbox{\upshape \textsf{else}}}{\mbox{\upshape \textsf{els}}}
\begin{mydef}
\[   \ensuremath{b}_1(\delta)=
    \begin{cases}
      \ensuremath{\mathit{rd}}(\delta), & \text{if}\ 2 < \ensuremath{\mathit{td}}(\delta) \\
      \ensuremath{\mathit{td}}(\delta), & \text{otherwise}.
    \end{cases}
\]
\end{mydef}
Limiting the computation of $\ensuremath{\mathit{rd}}$ as in the base case function $\ensuremath{b}_1$ significantly reduces the bound computation time.
This leads to to more problems being successfully bounded as shown in column 4 of Table~\ref{table:boundsDoms}, compared to when $\ensuremath{\mathit{rd}}$ is used.
The substantially improved running time is shown in Figure~\ref{fig:boundcompareTDvsRD}.
We also observe that bounds computed using $\ensuremath{\mathit{rd}}$ as a base case function are exactly the same as those computed using $\ensuremath{b}_1$, for all problems on which they terminate.
Thus, this improvement in running time does not come at the cost of looser bounds.
Indeed, we conjecture the following.
\begin{myconj}
\label{conj:tdeqrd112}
For any factored transition system $\delta$, if $\ensuremath{\mathit{td}}(\delta)\in\{0,1,2\}$, then $\ensuremath{\mathit{td}}(\delta)=\ensuremath{\mathit{rd}}(\delta)$.
\end{myconj}

Note, however, that the number of problems successfully bounded when using $\ensuremath{b}_1$ as a base case function is still less than the number of problems bounded using $\ensuremath{\mathit{td}}$.
This is because the large computation cost of $\ensuremath{\mathit{rd}}$ on the base cases on which it is invoked is still much more than the cost of computing $\ensuremath{\mathit{td}}$.
Another technique to improve the bound computation time is to limit the computation of $\ensuremath{\mathit{rd}}$ to problems whose state spaces' sizes are bound by a constant.
This is done with the following base case function.
\begin{mydef}
\[
\ensuremath{b}_2(\delta) =
\begin{cases}
  \ensuremath{b}_1(\delta), & \text{if}\ 50<{\mbox{\textsc{Exp}}}(\delta) \\
  \ensuremath{\mathit{td}}(\delta), & \text{otherwise}.
\end{cases}
\]
\end{mydef}
We set 50 as an upper limit on the state space size as more than 95\% of abstractions whose $\ensuremath{\mathit{rd}}$ was successfully computed had values less than 50.

As shown in column 5 of Table~\ref{table:boundsDoms}, the number of problems that are successfully bounded within 20 minutes when $\ensuremath{b}_2$ is used as a base case function is substantially more than those when $\ensuremath{b}_1$ is used, especially in the domains where $\ensuremath{\mathit{rd}}$ and $\ensuremath{b}_1$ were less successful than $\ensuremath{\mathit{td}}$.
However, the bounds computed when $\ensuremath{b}_2$ is used are sometimes worse than those computed when $\ensuremath{b}_1$ is used, like in the case of TPP.
Figure~\ref{fig:boundcompareTDvsRD} shows this bound degradation and bound computation time improvement for the problems on which both methods terminate.
Nonetheless, the bounds computed using $\ensuremath{b}_2$ are still much better than $\ensuremath{\mathit{td}}$, as shown in Figure~\ref{fig:boundcompareTDvsRD}.
This is because there are abstractions whose recurrence diameter is computable within the timeout and whose state spaces have more than 50 states.
For those abstractions, $\ensuremath{\mathit{td}}$ is computed instead of $\ensuremath{\mathit{rd}}$, when $\ensuremath{b}_2$ is used.
An interesting problem is adjusting the threshold in $\ensuremath{b}_2$ to maximise the number of abstractions whose recurrence diameter can be computed within the timeout.
We do not fully explore this problem here.

\paragraph{Using the bounds for SAT-based planning}

Table~\ref{table:boundsDoms} shows that the coverage of {\sc Mp} increases if we use, as horizons, the bounds computed with base case functions involving $\ensuremath{\mathit{rd}}$, compared to when using $\ensuremath{\mathit{td}}$ as a base case function.
An exception is Zeno, where the better bound computation time using $\ensuremath{\mathit{td}}$ is decisive.
In addition to coverage, it makes sense to take a look into how the exact running times compare as many problems are solved using any of the bounds.
The plots at the bottom two rows right of Figure~\ref{fig:boundcompareTDvsRD} show the time needed for computing a plan when using different pairs of base case functions for problems on which both methods succeed.
The plots show that the planning time (excluding bound computation) using the tighter bounds is much smaller almost always, which is to be expected.
The other shows planning time including bound computation.
Interestingly, although the bound computation time is more, e.g.\ when using $\ensuremath{b}_1$ than $\ensuremath{\mathit{td}}$, tighter bounds always payoff for problems that need more than 5 seconds to solve.
Thus, time spent computing better bounds before planning is almost always well-spent.

 \section{Conclusion}

The recurrence diameter was identified by many authors as an upper bound on transition sequence lengths in the areas of verification~\cite{baumgartner2002property,KroeningS03,kroening2011linear} and AI~planning~\cite{abdulaziz2015verified,icaps2017,abdulaziz:2019}.
However, previous authors noted that computing it is not practically useful, as it can take exponentially longer than solving the underlying planning or model checking problem.
Nonetheless, we show that, indeed, computing the recurrence diameter is useful when used for compositional bounding.
We do so using a SMT encoding that exploits the factored state space representation, and by combining the recurrence diameter with the traversal diameter, which is an easier to compute topological property.

Broad directions for future work include \begin{enumerate*} \item devising methods to calculate base case functions that are tighter than the recurrence diameter and \item devising compositional methods that can compute allow better problem decompositions than those by \citeauthor{abdulaziz2015verified}~\citeyear{abdulaziz2015verified,icaps2017}.\end{enumerate*}
A third more interesting direction is devising methods that use \emph{radius} concepts for compositional bounding, which are the topological properties corresponding to the different diameter concepts (i.e.\ the diameter, the traversal diameter, and the recurrence diameter) that consider paths starting only at the initial state.
Using these radius concepts for bounding has the potential to boost the efficiency of bound computation as well as bound tightness.
A significant challenge is that the theory justifying existing compositional bounding methods fully relies on the fact that the base case function is a diameter concept (in particular, the \emph{sublist diameter})~\cite{abdulaziz2015verified}.

\section{Acknowledgements}
We would like to thank Dr.\ Charles Gretton for the very helpful discussions and comments on this paper.
We also thank the anonymous reviewers whose comments helped improve this paper.
We also thank the German Research Foundation for funding that facilitated this work through the DFG Koselleck Grant NI 491/16-1.

redpajama_set_name: RedPajamaArXiv


Over the past 6 weeks we have been creating memoirs, Haiku's and snapshots for our iBooks author. We have also put a lot of work into the iBooks so please look at them.
The room goes silent as the judges get ready to show which light it will be. The green light is shown the crowd roars, and the ones who can't believe it are the ones who are up on stage.
My name is Dylan and my group is the Hut Of Learning, the team members are me, Kris and Kelvin. We were selected from seven groups in our devision to perform in the MPR room, since the auditorium was booked. There were seven groups in the final shark tank.
When we went to Cat Tien I didn't really see how the national park was that sustainable, but I now I know that at least there are still some parts of Vietnam that are still full of wild life and is still green.
The first group was Organic Cleaning Products, after that group it was The Hut Of Learning (My group) the moment we got called my stomach did a triple backflip. When we got onto stage Kelvin was doing the introduction to our proposal, then it will be Kris who will introduce us, after that it would be me talking about the reason we should have an outdoor hut.
When I was talking for the first time in the final shark tank, I messed a bit of my sentence and as Iw as talking I got more confident which got better and better and better until the end, where the judges got to ask us questions. First question they asked us was why we were using artificial straw instead of real straw. We answered with the reason if were to use real straw then we would have to change the straw every now and then. If we use artificial straw the roof will be better because artificial straw is more durable, and if we use artificial straw we won't have to change the straw every so often.
After all the groups were finished presenting, we got to see what he results were for each group. We were the second to get our results. The room goes silent as the judges get ready to show which light it will be. The green light is shown the crowd roars, and the ones who can't believe it are the ones who are up on stage!
About 30 minutes later the presentations were over Kris, Kelvin and I still can't believe that our project got green lighted.
My final thought about the final shark tank was that I really liked how none of the teams got red lighted, and the fact that it felt like a real shark tank because it was so intense having to speak out loud in front about sixty people, and having to look at the judges as you were talking was pretty hard to. Considering that there were over sixty people.
I also really liked it because of how hard we had to work and it was really fun.
When we went to Cat Tien I was excited to find out who my roommates were, what roasted marshmallows tasted like, and to see all the wildlife.
Once we got to our cabins we got to rest for about 30 minutes and then we went to play some group activities such as the Human Not, and Alaskan Basketball. Then after that we did a Micro Eco-System activity, the objective was to observe all the living organisms in the eco system, we saw some ants but they were to fast to get a photo of them. But then we saw a giant spider and we named him Marley. This was also when I lost my camera and things went down hill. I liked Alaskan Basketball more then the Human Not because, it was less complex and it relied on throwing and running two things I like to do. I didn't really like the Human knot that much because it was so complicated and it was hard to do.
After that we went to our cabins and went to bed, but you got a choice to do the morning hike and and listen to the Gibbons sing, but we would have to wake up at about 5 O'clock which was pretty early. In the morning it was pretty cold so most of us were wearing jackets, anyway we walked to meet up with the others.
Once we got to the others we started the morning hike. We hiked a few hundred meters and then we stopped on a bridge and listened to the Gibbons sing. Once in a while the Gibbons would make these loud alarm like sounds, and then a Gibbon would make this alien like sound and all the other Gibbons would be quiet. I really liked this because we were breathing fresh air and it was nice and cool outside. Also I liked when the gibbons got loud and quiet.
When we got back we ate breakfast and group 2 (my group) went to the Primate Center where they help endangered and injured species. At the Primate Center they had Gibbons, Black Shank Dukes and Pygmy Loris's.
We walked until we got to this viewing platform where we could see birds, gibbons and other animals. In the trees we saw to young Gibbons playing with each other in the tall trees, we also saw a large bird that we thought was like a hawk or eagle. I liked this because we got to see wildlife and it was nice and windy at the top of the platform.
After that we got to go back to our cabins and rested, then we got dressed for dinner, and after that we went to do the Night Sensory Hike, it was really fun and cool because we were walking down the road at night, and we got to use our night vision which is basically when you eye switches from the normal eye sight to that sight that has night vision. We walked a few hundred meters and stopped then we were lying down on the road watching the stars and listening to the animal sounds, I liked this because it was nice and peaceful.
Then we had dinner and then we had a Bonfire which was teacher-led the teachers would tell us scary story's and let us play games around the bonfire.
That night group 2 (my group) did the Night Safari where we got to go on a bus that only had seats on the roof, so that we could see some wildlife.
When we got onto the bus, I sat next to Daniel and a few minutes into the safari our guide spotted a baby deer, which was our first animal then we spotted a female, and then we saw a giant male deer that looked at us for a few seconds. Then after that we saw a family of deers hanging around, and we saw a Porcupine and a Jackrabbit which quickly hopped into a bush. I thought that the Jackrabbit was scared because of our tour guides light.
After the Moon Bears we were told to go meet everyone at the field where we did our group activities. Once we got there we were sorted into groups this was based of which one you picked, I picked photography so I went with the photography group, but remember how I lost my camera well Mrs. Tram found a camera and it happened to be mine.
As we were walking down the road looking for things we could take a photo of, we spotted a nice tree to take a photo of, and that was where I got my winning photo.
This is the photo I won with?
Also the person who gets the best photo wins a prize. Anyway we walked on to see the Ancient Tongue tree and it was massive. It is about 300 years old now.
This was where we got to see who had the best photo, and i'm pretty sure that the highest score you could get was 15, and I got a 14.5.
Then we walked back to get dressed and ate dinner, after that we had another Bonfire but this one was student-led, and we got to practice and make up scary story's and games. But when we got to the Bonfire everyone was nervous and no one wanted to perform, so then complicated group performed some sort of game show, and after that me and Kristofer's group performed a game called Last Reaction First Reaction.
So basically one of the judges will say last reaction or first reaction if a judge says First Reaction jump then the first person to jump is out, and if a judge says last reaction jump the last person to jump is out. The last 2 contestants in the final were Halia and Ben. When Halia and Ben where competing for first place it felt intense, and it was strange to see the two M.C's battling each other.
Then the next day we went to the Moon Bear Center, where we got to hide some food and spread Peanut Butter on trees for the Moon Bears to find. I got to name two Moon Bears because they ate my food, I named one Cookie and one Fuzzy. Fuzzy was a smart bear because she spun a barrel and my food dropped out. We hid there food in there enclosure, the reason we hid the food was so that they could use there sense of smell, climbing abilities to find the food. At the Moon Bear center they also had small Sun Bears that had short fur.
That was everything that I thought was fun about Cat Tien and I hope you enjoy it to.??.
Today we got back our information report, and the way we marked it was by using NY for not Yet Meeting, A for Approaching, M for Meeting and E for Exceeding being the best score you can get, and I got an E ?.
My goal is to read more non-fiction books than fiction, I also want to read for a longer period of time while I am reading non-fiction books.
My action plan is to set up a schedule for what time i will read every night and for how long I will read every night.
So far I am only picking out which non-fiction book to read for my goal.
Yesterday night I forgot to read so I will do double this night so that i can get back on track.
Yesterday night I read 100 Facts Of Everything for about 45 minutes.
Last night I forgot to read so tonight I will read more.
Yesterday night I read 100 Facts of Everything for 45 minutes, I read about the best and the worst movies and about Dinosaurs.
This Saturday I will start to read a different non fiction book.
Last night I forgot to pick a book and read so today I will do extra.
Guinness world records of 2017, for 35 minutes.
Maybe a week ago we started our Science Reports. Kris and I chose Dry Ice and vinegar, to see if they would react to each other.
Our deadline for this experiment is on Thursday, right before our Information Report deadline on Friday.
It was really fun because at the end after we put the vinegar in the Dry Ice it gave of smoke and was more rough because the Dry Ice was breaking down, because of the vinegar.
On Wednesday kris, Billy, Daniel and I went to SISAC for A team, but B team stayed at school.SISAC was hosted at ISHCMC.Once we got there I was nervous but all my friends looked like they were at a normal basketball match.
The first team we were gonna' play was BIS who apparently is the best at basketball.But before we were about to play AIS was about to play BIS, and when the ref threw the ball up my friend Noah tapped it backwards.But a BIS player was there so he stole the ball and got an easy lay up.After that it was AIS's ball when they were dribbling up to the half court line, I felt some rain on my head.That was when the game stoped and we had to move inside.
When we came inside we saw ISHCMC and ABSIS going at it, so far ISHCMC was winning and we saw a person that used to be in SSIS Tim.He was sitting on the bench relaxing for a bit.But before we new it the game was over ISHCMC won it, then after that AIS and BIS continued there game.it was 4:0 when they left off.When we were watching BIS and AIS, ISHCMC was going head to head with ABCIS.But there was only a few minutes left and ISHCMC was winning by quite a lot.
After the IHSCMC game was over and the AIS game was over it was our turn to warm up and play a game.We were playing our game outside because it stoped raining.Once we were finished warming up our coach was picking who would start the match.
When we started the match, it was super intense because when the ref blew the whistle, and threw the ball up the court went silent. But we one the tip off then the ball went to Emre who scored the first 2 points for us.But later we fouled them and they got both of the shots in from the free throw line.
But in the end BIS won for the third time and the Dragons came home with second place.
Another week into research for our Ebooks we are making on a thing, a person or anything really. But we only have two more weeks including this one to gather all the information we need and to answer our questions.To make sure we follow our plan and we don't forget it, we are using planners.
This way we don't need to try to remember all the steps and what parts we are going to write, and at what time so we can just open the planner and then we can just follow our plans.If they don't work out than we can just change the plan for the planner.
I am making a biography about Michael Jordan and when he was at his prime, and the secret to how well he was doing in his career.But I have to get moving quick, cause I only have three weeks to gain as much information as possible.
Then thats where I have to put the information in different spots like the Introduction, Middle and the conclusion for the biography. But I have to spend more time in the middle because there are three sections I have to fill up, in three weeks and then I have to figure out a good conclusion and not just say the end after happily ever after.
Claudio on First Week Reflection!!!
www.evolvedstrategies.com on First Week Reflection!!!
1.pokerci1.biz on First Week Reflection!!!
cerveja nevada on First Week Reflection!!!
como ganhar uma renda extra no fim de semana on First Week Reflection!!!


Publish by in Category decorating ideas at March 9th, 2019. Tagged with bathroom light bars. bathroom light bars at menards. bathroom light bars bronze. bathroom light bars brushed nickel. bathroom light bars chrome. bathroom light bars home depot. bathroom light bars with receptacle. bathroom vanity light bars. cheap bathroom light bars. clearance bathroom vanity light bars. contemporary bathroom light bars. fancy bathroom light bars. light bars bathroom fixtures.
Bathroom Light Bars have 30 picture of decorating ideas, it's including Bathroom Light Bars Stupefy Vanity Bar Gallery ALL ABOUT HOUSE DESIGN Decorating Ideas 1. Bathroom Light Bars Stagger Cute How To Build Decorating Ideas 2. Bathroom Light Bars Amazing LED Vanity Wall Fixtures Bath Decorating Ideas 3. Bathroom Light Bars Sensational Bath Bar Surprising Decorating Ideas 4. Bathroom Light Bars Improbable Vanity Best Of 49 Lighting Images Decorating Ideas 5.
Tags : bathroom light bars. bathroom light bars at menards. bathroom light bars bronze. bathroom light bars brushed nickel. bathroom light bars chrome. bathroom light bars home depot. bathroom light bars with receptacle. bathroom vanity light bars. cheap bathroom light bars. clearance bathroom vanity light bars. contemporary bathroom light bars. fancy bathroom light bars. light bars bathroom fixtures.


text:
Seed-scattering drones replant fire-damaged forests in Croatia
By bne IntelliNews November 18, 2021
Seed-scattering drones from the local private company Magic Forest are attempting to replant remote forests damaged by fires in Croatia that cannot be reached by land, Reuters reported.
Summer fires in Croatia often hit areas that are hard to reach overground. Magic Forest hopes to expand the innovative scheme internationally.
The tactic applied by the Croatian company differs from other similar initiatives as the drones disperse seeds in larger containers than those seen elsewhere. They are the size of a golf ball and release ingredients to form a favourable micro-environment for a seed to take root, according to its creators.
"Besides an acorn we also put sand, grass, clay and chili inside", Reuters quoted Goran Ladisic, one of the leaders of the Magic Forest company, as saying.
"Importantly, we put chili because, in this way, the wild animals - in case of an oak it refers to wild boars - will not eat the seeds," he added.
The initiative was backed by the Promina municipality where a lot of forest fires happen during the summer.
The initiative has been developed over the past two years and the tests have shown that more than 40% of the seeds dispersed by the drones had planted.
Magic Forest has been in contact with partners in Austria, Bosnia & Herzegovina, Montenegro, Ukraine and California.
Miro, a US enterprise software publisher with Russian roots, announced yesterday a $400mn Series C round. The deal brought the company – known as RealtimeBoard when it was founded in Russia back in 2011 – to an astounding $17.5bn valuation.
No less than 2mn preliminary diagnoses using a neural network have been made to date in Moscow during medical home visits, city authorities announced last week.
Study: VCs increasingly bet on Russian-founded startups operating abroad – rather than on domestic ones
The Untitled, one of the most established VC firms investing across Russia and Eastern Europe, has analysed investment deals involving startups founded over the past 10 years in Russia or by Russian entrepreneurs.
Russian tech entrepreneurs on the rise: Forbes identifies 10 "future unicorns"
Far from their native countries, Russian-speaking entrepreneurs are thriving in the world's major tech hotspots — from Silicon Valley, to Western Europe, to South-East Asia.
A massive cyberattack took down over a dozen Ukrainian government websites, stated the Ministry of Foreign Affairs on January 14.

redpajama_set_name: RedPajamaCommonCrawl


Campaigners have called for free school meals to be offered to all children whose parents are receiving Universal Credit.
They say this is an essential first step in tackling the impact of child poverty.
At present, only Universal Credit claimants earning less than £7,400 get free school meals for their kids.
And a new study has indicated that many youngsters in low-income families are going hungry because they don't get free school meals.
Researchers at University College London (UCL) studied low-income families in London and a South East seaside town, finding that around one in four children went hungry at times, despite sacrifices made by their parents.
Half of parents in the study did not eat enough food, skipped meals or used food banks, said the report.
Some children said there were restrictions on what was available for a free school meal, which could make them feel embarrassed.
Child Poverty Action Group chief executive Alison Garnham said: "The young people in this study make the case for universal free school meals more powerfully than anyone else could.
"Their hunger, their shame, their sense of being cut off from learning and social opportunities - all because parents can't afford enough food - are appalling in a society that believes every child matters.
"Universal free school meals should be part of the solution, but wider Government action is needed to eradicate the poverty that underlies children's hunger.
"As a minimum, free school meals should be restored for all families on Universal Credit.
"It is time to re-balance family budgets after years of austerity and rising child poverty. The priority should be lifting the freeze on working and non-working benefits so that they rise again with inflation."
When Universal Credit was first introduced in 2013, all claimants were entitled to free school meals for their children.
But from April 1, 2018, the rules changed so that UC claimants had to be earning less than £7,400 to qualify for free school meals.
Campaigners want everyone on the new benefit to be eligible once again.
The report's co-author, Rebecca O'Connell, said: "Food poverty and its effects on children's and young people's physical and emotional well-being is a matter of grave concern.
"In the face of piecemeal responses and Government neglect, the outlook is set to remain bleak. Radical change is needed."
A Government spokesman said: "Tackling poverty will always be a priority for this Government.
"Employment is at a record high, wages are outstripping inflation, and absolute poverty is lower than in 2010.
"We're supporting over one million of the country's most disadvantaged children through free school meals and we continue to spend £95 billion a year on working-age benefits to ensure every child has the best start in life."
Paul Whiteman, general secretary of school leaders' union NAHT, said: "This country's record on child poverty is truly shocking.
"A record 2.9 million children from working families in the UK are living in poverty after housing costs have been paid - 70% of all poor children were in working families last year.
"Children who are hungry cannot learn as well as they might be able to. Free school meals at least guarantee that children going hungry at home get one nutritious meal a day during term time."
He added: "We have to do all that we can to extend that entitlement to every child that is going hungry, and we must fix the problems in society that cause families to fall in to the poverty trap.
"Currently one in 10 eligible children miss out on their free school meals entitlement.
"NAHT has long called for children to be automatically enrolled to receive free school meals, using the information councils already hold about their family situation.
"This would take away the barrier of stigma for parents."
The research was carried out among 45 low-income families.
Your child will also be able to get free school meals if they're in a government-funded school and in reception class, Year 1 or Year 2.


text:
Q: Find Win7 Network "Other Devices" in C#
Possible Duplicate:
IP Camera, how to detect it on the network?

I have an IP Camera connected to my network which shows up as an Other Device from the Win7 Explorer Network.
I'm trying to find the camera, and its IP from C#.
I've tried several WMI queries with no luck. I'm able to list all the PC's connected to the LAN, but not any Other Devices.
I appreciate any help. Thank you.

redpajama_set_name: RedPajamaStackExchange