custom-line = letter = : , command = dashedline , ccommand = cdashedline ,
tikz = dashed

# Are we making much progress? Revisiting chemical reaction yield prediction
from an imbalanced regression perspective

Yihong Ma, Xiaobao Huang, Bozhao Nan,
Nuno Moniz, Xiangliang Zhang, Olaf Wiest, Nitesh V. Chawla  University of
Notre Dame, Notre Dame, Indiana, USA yma5, xhuang2, bnan, nuno.moniz,
xzhang33, owiest<EMAIL_ADDRESS>
###### Abstract.

The yield of a chemical reaction quantifies the percentage of the target
product formed in relation to the reactants consumed during the chemical
reaction. Accurate yield prediction can guide chemists toward selecting high-
yield reactions during synthesis planning, offering valuable insights before
dedicating time and resources to wet lab experiments. While recent
advancements in yield prediction have led to overall performance improvement
across the entire yield range, an open challenge remains in enhancing
predictions for high-yield reactions, which are of greater concern to
chemists. In this paper, we argue that _the performance gap in high-yield
predictions results from the imbalanced distribution of real-world data skewed
towards low-yield reactions, often due to unreacted starting materials and
inherent ambiguities in the reaction processes_. Despite this data imbalance,
existing yield prediction methods continue to treat different yield ranges
equally, assuming a balanced training distribution. Through extensive
experiments on three real-world yield prediction datasets, we emphasize the
urgent need to reframe reaction yield prediction as an imbalanced regression
problem. Finally, we demonstrate that incorporating simple cost-sensitive re-
weighting methods can significantly enhance the performance of yield
prediction models on underrepresented high-yield regions.

††copyright: none††conference: ; ;

##  1\. Introduction

Figure 1. (a) An example of reaction yield prediction. (b) A depiction of the
data-driven yield prediction workflow. (c) An illustration of the imbalanced
regression problem.

Recent advancements in machine learning have introduced a paradigm shift in
the field of computational chemistry (Guo et al., 2023). These breakthroughs
have led to a diverse array of machine learning models that now play critical
roles in assisting chemists across a broad spectrum of tasks, including but
not limited to retrosynthesis, product prediction, and drug discovery. Among
this multifaceted landscape, the prediction of reaction yields (Ahneman et
al., 2018; Schwaller et al., 2021; Saebi et al., 2023; Voinarovska et al.,
2023; Yarish et al., 2023) emerges as an issue of paramount importance in the
domain of synthesis planning, where complex molecules are synthesized through
a sequence of reaction steps. Based on the empirical categorization, yields
above 67% are classified as high yields and those below 33% are classified as
low yields (Yarish et al., 2023). In this context, the occurrence of a low-
yield reaction within this sequence can drastically impact the feasibility and
overall efficiency of the synthesis process. As a result, chemists often
prioritize the accurate prediction of high-yield reactions.

While the introduction of numerous yield prediction models has indeed
showcased improved performance across the entire yield range, the challenge of
effectively enhancing performance for high-yield reactions remains an open
problem (Maloney et al., 2023). In real-world scenarios, yield data often
exhibits a highly skewed distribution, with high yield values being much rarer
than lower ones, despite their greater importance to chemists in synthesis
planning. For example, the Buchwald-Hartwig dataset (Ahneman et al., 2018), a
widely used benchmark for yield prediction, is significantly skewed toward the
low-yield regions, with certain high-yield ranges having only few data points.
In this paper, we argue that _the increased difficulty in predicting high-
yield reactions stems from its limited availability of data samples, often due
to unreacted starting materials and inherent ambiguities in the reaction
processes_. Despite the presence of such data imbalance, existing yield
prediction methods continue to treat different yield ranges equally with the
false assumption of a balanced data distribution.

To gain a deeper insight into the field’s actual progress, we conduct
extensive experiments to benchmark six state-of-the-art yield prediction
methods on three real-world datasets. Surprisingly, the results become less
impressive than claimed when we take data imbalance into account. We discover
that _the overall good performance across the entire yield spectrum primarily
results from enhancing performance in areas with sufficient data, typically
the low-yield range, while overlooking the significant performance gap in
underrepresented high-yield regions_. This finding has motivated us to revisit
reaction yield prediction and reformulate it as an imbalanced regression
problem, a well-established topic in machine learning.

Unlike imbalanced classification, reaction yield prediction involves
regression rather than classification, and there has been limited exploration
of addressing data imbalance in the regression context (Ribeiro and Moniz,
2020). Most prior research on imbalanced regression has directly adapted the
SMOTE algorithm (Chawla et al., 2002) to regression settings (Branco et al.,
2017; Torgo et al., 2013). However, the continuous nature of target labels in
regression tasks makes these adaptations less practical. A more intuitive
solution is to apply cost-sensitive re-weighting strategies (Gong et al.,
2022) that can be seamlessly combined with various regression models. We
demonstrate that incorporating simple imbalanced regression techniques such as
Focal loss (Lin et al., 2017) or label distribution smoothing (Yang et al.,
2021) can significantly enhance the performance of yield prediction models on
underrepresented high-yield regions without sacrificing the overall
performance too much. We believe these findings have the potential to redirect
the future research direction in reaction yield prediction, benefiting both
chemistry and machine learning communities. In summary, the contributions of
this paper include:

  * •

We are the first to introduce the novel concept of reformulating reaction
yield prediction as an imbalanced regression problem.

  * •

We conduct comprehensive experiments on three real-world yield prediction
datasets to uncover and understand the limitations of existing models when
predicting high-yield reactions.

  * •

We demonstrate that incorporating cost-sensitive re-weighting methods into
existing yield prediction models can lead to significant performance
improvements on high-yield reactions.

##  2\. the examination of existing yield prediction methods

In this section, we begin by introducing the definitions of reaction yield
prediction and imbalanced regression. We then proceed to evaluate six yield
prediction methods on three real-world datasets, all viewed through the lens
of imbalanced regression.

###  2.1. Preliminaries

—c—c—cccc—cccc—cccc—cccc—

Dataset Method MAE $\downarrow$ RMSE $\downarrow$ G-Mean $\downarrow$
All Many Med. Few All Many Med. Few All Many Med. Few

B-H RF 5.5$\pm 0.2$ 4.4$\pm 0.2$ 6.0$\pm 0.2$ 6.7$\pm 0.6$ 8.1$\pm 0.3$
7.4$\pm 0.3$ 8.4$\pm 0.4$ 9.1$\pm 0.8$ 2.8$\pm 0.1$ 1.8$\pm 0.1$ 3.6$\pm 0.2$
4.1$\pm 0.4$
XGBoost 4.7$\pm 0.2$ 3.8$\pm 0.2$ 5.2$\pm 0.2$ 5.7$\pm 0.5$ 6.9$\pm 0.3$
6.1$\pm 0.4$ 7.1$\pm 0.5$ 7.8$\pm 0.7$ 2.7$\pm 0.1$ 2.0$\pm 0.1$ 3.2$\pm 0.1$
3.4$\pm 0.3$
SVM 14.6$\pm 0.3$ 12.9$\pm 0.5$ 12.9$\pm 0.7$ 26.1$\pm 1.1$ 18.5$\pm 0.4$
15.8$\pm 0.5$ 17.2$\pm 0.8$ 28.6$\pm 0.9$ 9.2$\pm 0.3$ 8.7$\pm 0.5$ 7.7$\pm
0.6$ 22.2$\pm 1.6$
MLP 4.5$\pm 0.2$ 3.4$\pm 0.3$ 5.3$\pm 0.2$ 5.3$\pm 0.4$ 7.0$\pm 0.5$ 6.0$\pm
1.0$ 7.6$\pm 0.6$ 7.3$\pm 0.6$ 2.5$\pm 0.1$ 1.8$\pm 0.1$ 3.1$\pm 0.1$ 3.3$\pm
0.3$
YieldGNN 8.7$\pm 7.9$ 8.6$\pm 9.5$ 7.6$\pm 4.6$ 12.8$\pm 14.5$ 11.1$\pm 8.7$
10.6$\pm 9.1$ 10.1$\pm 5.9$ 14.7$\pm 14.7$ 3.0$\pm 0.4$ 2.3$\pm 0.5$ 3.5$\pm
0.4$ 3.9$\pm 0.5$
Yield-BERT 5.5$\pm 0.3$ 3.8$\pm 0.3$ 6.6$\pm 0.4$ 6.6$\pm 0.5$ 8.4$\pm 0.4$
7.1 $\pm 1.4$ 9.1$\pm 0.6$ 8.9$\pm 0.8$ 3.2$\pm 0.1$ 2.2$\pm 0.1$ 4.1$\pm 0.4$
4.1$\pm 0.5$
Avg. Ranking \- 1.2 1.8 3.0 \- 1.2 2.2 2.7 \- 1.2 1.8 3.0

S-M RF 8.0$\pm 0.2$ 6.1$\pm 0.4$ 8.8$\pm 0.3$ 12.8$\pm 6.1$ 11.8$\pm 0.4$
11.2$\pm 0.9$ 12.0$\pm 0.3$ 15.9$\pm 7.6$ 4.0$\pm 0.2$ 2.3$\pm 0.1$ 5.1$\pm
0.3$ 9.8$\pm 3.8$
XGBoost 7.2$\pm 0.2$ 6.1$\pm 0.4$ 7.7$\pm 0.2$ 6.8$\pm 4.7$ 10.5$\pm 0.2$
10.1$\pm 0.8$ 10.7$\pm 0.2$ 9.7$\pm 6.3$ 4.1$\pm 0.1$ 3.1$\pm 0.2$ 4.6$\pm
0.1$ 3.9$\pm 2.7$
SVM 16.5$\pm 0.2$ 14.8$\pm 0.5$ 17.1$\pm 0.2$ 31.6$\pm 6.0$ 20.3$\pm 0.2$
18.7$\pm 0.6$ 20.8$\pm 0.3$ 33.0$\pm 6.1$ 11.1$\pm 0.2$ 9.6$\pm 0.3$ 11.7$\pm
0.3$ 30.3$\pm 6.0$
MLP 7.5$\pm 0.3$ 6.1$\pm 0.5$ 8.1$\pm 0.4$ 8.5$\pm 6.8$ 11.1$\pm 0.4$ 10.7$\pm
0.9$ 11.2$\pm 0.5$ 12.3$\pm 9.3$ 4.1$\pm 0.2$ 2.9$\pm 0.2$ 4.8$\pm 0.3$
4.5$\pm 3.5$
YieldGNN 9.1$\pm 1.2$ 7.2$\pm 0.9$ 9.9$\pm 1.9$ 10.8$\pm 7.3$ 12.6$\pm 1.5$
10.8$\pm 1.4$ 13.2$\pm 2.2$ 13.5$\pm 8.2$ 5.4$\pm 0.6$ 4.1$\pm 0.5$ 6.1$\pm
1.2$ 8.0$\pm 6.9$
Yield-BERT 9.1$\pm 0.4$ 6.3$\pm 0.4$ 10.2$\pm 0.5$ 5.1$\pm 5.4$ 13.3$\pm 0.6$
11.2$\pm 0.9$ 14.1$\pm 6.3$ 7.7$\pm 7.6$ 5.0$\pm 0.2$ 3.3$\pm 0.2$ 6.0$\pm
0.3$ 2.3$\pm 2.7$
Avg. Ranking \- 1.2 2.3 2.5 \- 1.3 2.3 2.3 \- 1.2 2.5 2.3

AZ RF 20.3$\pm 0.8$ 19.1$\pm 0.7$ 23.6$\pm 2.5$ 32.0$\pm 4.3$ 25.2$\pm 0.9$
23.6$\pm 0.8$ 29.8$\pm 3.0$ 36.4$\pm 3.9$ 13.8$\pm 0.8$ 13.1$\pm 0.6$ 16.0$\pm
3.0$ 26.0$\pm 6.4$
XGBoost 20.6$\pm 1.0$ 19.5$\pm 1.0$ 23.9$\pm 3.4$ 30.4$\pm 6.1$ 27.2$\pm 1.3$
25.6$\pm 1.3$ 31.9$\pm 3.6$ 37.9$\pm 6.0$ 11.8$\pm 1.0$ 11.3$\pm 1.1$ 14.0$\pm
3.6$ 19.7$\pm 6.5$
SVM 25.0$\pm 0.8$ 23.5$\pm 0.7$ 28.0$\pm 2.4$ 41.7$\pm 3.9$ 28.9$\pm 0.9$
27.1$\pm 0.7$ 32.5$\pm 2.4$ 43.9$\pm 3.8$ 18.6$\pm 0.9$ 17.5$\pm 0.7$ 20.8$\pm
2.9$ 37.6$\pm 5.8$
MLP 22.1$\pm 1.7$ 21.5$\pm 1.3$ 25.0$\pm 5.0$ 26.0$\pm 6.9$ 29.7$\pm 2.1$
28.9$\pm 1.9$ 33.4$\pm 4.9$ 32.8$\pm 7.4$ 12.0$\pm 1.2$ 11.6$\pm 0.9$ 14.6$\pm
5.0$ 15.6$\pm 6.7$
YieldGNN 22.5$\pm 0.8$ 21.5$\pm 0.6$ 25.5$\pm 3.3$ 33.4$\pm 6.7$ 28.0$\pm 1.0$
26.5$\pm 1.0$ 32.0$\pm 3.7$ 38.6$\pm 6.0$ 15.2$\pm 1.1$ 14.6$\pm 0.9$ 17.0$\pm
3.1$ 25.7$\pm 9.2$
Yield-BERT 25.6$\pm 2.5$ 24.3$\pm 2.6$ 28.7$\pm 3.8$ 38.4$\pm 10.1$ 32.5$\pm
3.0$ 30.7$\pm 3.0$ 37.5$\pm 3.6$ 45.2$\pm 9.9$ 15.7$\pm 1.5$ 15.1$\pm 1.7$
18.0$\pm 4.7$ 26.2$\pm 10.8$
Avg. Ranking \- 1.0 2.0 3.0 \- 1.0 2.2 2.8 \- 1.0 2.0 3.0

Table 1. Reaction yield prediction results on three real-world datasets. We
report the average performance across 10 repetitions in all experiments and
present the average rankings for the _many-shot_ , _medium-shot_ , and _few-
shot_ regions, respectively.

###### Definition 0: Reaction yield prediction.

Reaction yield prediction is a regression problem that predicts the yield
value $y\in[0,100]$ of a chemical reaction $rxn=({\mathcal{R}},P)$ composed of
multiple reactant molecules ${\mathcal{R}}$ and a single product molecule $P$.
A yield prediction model comprises an encoder
$g:rxn\rightarrow{\bm{h}}\in{\mathbb{R}}^{d}$ and a decoder
$f:{\bm{h}}\rightarrow\hat{y}\in[0,100]$. The encoder $g(\cdot)$ takes the
form of a graph neural network (GNN) or a sequential model, depending on the
actual representations of molecules. The decoder $f(\cdot)$ outputs the yield
prediction $\hat{y}$ based on the encoded reaction embedding ${\bm{h}}$.

###### Definition 0: Imbalanced regression.

Let $\mathcal{D}=\\{({\bm{x}}_{i},y_{i})\\}_{i=1}^{N}$ denote the training
dataset of a regression problem, where ${\bm{x}}_{i}\in{\mathbb{R}}^{d}$ is
the input feature vector and $y_{i}\in{\mathbb{R}}$ is the label. We divide
the label space ${\mathcal{Y}}$ into $K$ disjoint bins with equal intervals
that cover the entire range of target values, i.e.,
$[b_{0},b_{1}),[b_{1},b_{2}),\dots,[b_{B-1},b_{B})$. Let ${\mathcal{C}}_{k}$
be the set of data samples in the $k$-th bin with $k\in\\{1,2,\dots,B\\}$. The
data imbalance occurs when the label distribution is highly skewed, i.e.,
$\frac{\max_{k}|{\mathcal{C}}_{k}|}{\min_{k}|{\mathcal{C}}_{k}|}\gg 1$. To
facilitate fair evaluation considering data imbalance, the bins are classified
into _many-shot_ , _medium-shot_ , and _few-shot_ regions based on the number
of training samples.

The left section of Figure 2 visualizes the division of these regions on three
real-world benchmark yield prediction datasets.

Figure 2. A comparison between yield distributions (left) and test error
distributions (right) on three benchmark datasets.

###  2.2. Evaluation Settings for Yield Prediction

####  2.2.1. Datasets

We use three real-world benchmark datasets for predicting reaction yields,
sourced from either high-throughput experimentation (HTE) or electronic
laboratory notebooks (ELN). Following prior research on imbalanced regression
(Yang et al., 2021; Gong et al., 2022; Liu et al., 2023), we categorize the
bins within the target yield space into three disjoint subsets: _many-shot_
(bins with over $\\#_{\text{upper}}$ reactions), _medium-shot_ (bins with
$\\#_{\text{lower}}$ to $\\#_{\text{upper}}$ reactions), and _few-shot_ (bins
with fewer than $\\#_{\text{lower}}$ reactions) regions, based on their
respective counts of reactions. For all three datasets, we set the bin size to
1.

  * •

B-H (Ahneman et al., 2018): It comprises 3,955 Buchward-Hartwig reactions from
HTE, with the number of reactions per bin varying between 1 and 412. Here,
$\\#_{\text{lower}}$ is set to 25, and $\\#_{\text{upper}}$ is set to 50.

  * •

S-M (Perera et al., 2018): It consists of 5,760 Suzuki-Miyaura reactions from
HTE, with the number of reactions per bin ranging from 1 to 209. Here,
$\\#_{\text{lower}}$ is set to 20, and $\\#_{\text{upper}}$ is set to 65.

  * •

AZ (Saebi et al., 2023): It includes 750 Buchward-Hartwig reactions from ELN
at AstraZeneca, with the number of reactions per bin ranging from 0 to 145.
Here, $\\#_{\text{lower}}$ is set to 3, and $\\#_{\text{upper}}$ is set to 5.

####  2.2.2. Yield prediction methods

  * •

Machine learning methods: Random Forest (RF), XGBoost, Support Vector Machines
(SVM)

  * •

Deep learning methods: Multi-layer Perceptron (MLP), YieldGNN (Saebi et al.,
2023), Yield-BERT (Schwaller et al., 2021)

####  2.2.3. Evaluation pipeline

We report yield prediction results on _many-shot_ , _medium-shot_ , and _few-
shot_ regions as well as on the entire yield space (i.e., the _all_ region).
In all three datasets, 70% of the data is used for training and the remaining
30% is reserved for testing. Our evaluation employs common yield prediction
metrics: mean absolute error (MAE) and root mean square error (RMSE).
Additionally, we also utilize the geometric mean of $L_{1}$ errors (G-Mean) as
a supplementary metric. Lower values ($\downarrow$) of MAE, RMSE, and G-Mean
indicate better yield prediction performance.

####  2.2.4. Implementation details

For RF, XGBoost, SVM, and MLP, the input features include structural
fingerprints (e.g., ECFP), chemical properties (e.g., NMR shifts, HOMO/LUMO
energies, vibrations, dipole moments), and reaction-specific parameters (e.g.,
scale, volume, temperature). For Yield-BERT, the SMILES representation of the
reaction is used as input; an encoder based on a pre-trained BERT (Kenton and
Toutanova, 2019) for SMILES is employed, with a k-Nearest Neighbors (kNN)
regressor serving as the decoder. For YieldGNN, we construct graph structures
to represent the molecules involved in the reaction; a GNN is used to encode
the reaction, while an MLP is used to decode the reaction embedding into yield
predictions. We employ the $L_{1}$ distance as the training loss
${\mathcal{L}}$ in all experiments.

###  2.3. Uncovering and Understanding the Performance Gap in High-Yield
Predictions

Figure 2 provides an insightful comparison between yield distributions and
test error distributions, both as functions of yield values. Regarding the
yield distribution, we note that the _few-shot_ region predominantly comprises
high-yield reactions, while the _many-shot_ region primarily consists of low-
yield reactions. Specifically in the B-H and S-M datasets, 81% and 100% of the
_few-shot_ reactions fall into the high-yield category, while 89% and 100% of
the _many-shot_ reactions belong to the low-yield category. This finding
establishes a clear connection between yields and their distributions.

To quantify the impact of data imbalance on prediction errors, we compute the
Pearson correlation coefficients between the testing error distribution and
the training yield distribution. Across all three reaction yield prediction
datasets, we consistently observe negative correlation coefficients, with
values of -0.42, -0.28, and -0.07, respectively. Moreover, in the right part
of Figure 2, it is evident that the _few-shot_ region (in orange) exhibits the
largest test error, while the _many-shot_ region (in blue) demonstrates the
smallest error. To complement this observation, we further evaluate the yield
prediction performance of six state-of-the-art models using three metrics and
report the average performance rankings for the three regions in Table 2.1. As
a result, the average ranking indicates a decline in model performance as we
transition from the _many-shot_ region to the _medium-shot_ and _few-shot_
regions.

Therefore, both observations from Figure 2 and Table 2.1 converge to the same
conclusion: During the training process, low-yield values with a larger number
of data samples tend to be learned better in comparison to those high yields
with fewer samples. This highlights the demand for specialized machine
learning techniques that can effectively address the challenge of data
imbalance.

##  3\. mitigating data imbalance for better high-yield predictions

In this section, we present two cost-sensitive re-weighting methods for
imbalanced regression, which can be seamlessly integrated into the learning
process of existing yield prediction models. We also provide evidence of their
effectiveness in high-yield predictions.

###  3.1. Cost-sensitive Re-weighting Methods

The key idea is to assign a weight $w_{i}\in{\mathcal{W}}$ to each training
sample $({\bm{x}}_{i},y_{i})$, resulting in the following modified loss
function ${\mathcal{L}}^{\prime}$:

(1)
${\mathcal{L}}^{\prime}=\frac{1}{N}\sum_{i=1}^{N}w_{i}{\mathcal{L}}(y_{i},\hat{y}_{i}),$

where ${\mathcal{L}}$ is a loss function for regression tasks, such as $L_{1}$
loss, MSE loss, and Huber loss. The distinctiveness of each re-weighting
method arises from the various designs of training weights ${\mathcal{W}}$.

####  3.1.1. Focal Loss

The Focal loss (Lin et al., 2017) is a specialized loss function designed to
address imbalanced learning problems. It assigns varying weights to individual
training samples based on their prediction difficulties. The goal is to reduce
the impact of easily predictable samples while amplifying the importance of
challenging samples during the training process. The weight $w_{i}$ is defined
as:

(2) $w_{i}=\textsc{sigmoid}(\alpha{\mathcal{L}}(y_{i},\hat{y}_{i}))^{\gamma}$

where $\textsc{sigmoid}(\cdot)$ is the sigmoid function, and $\alpha$,
$\gamma$ are hyper-parameters. This results in the scaling factor of each
training sample ranging from 0 to 1, depending on the prediction error.
Notably, when $\gamma=0$, the Focal loss is equivalent to the original loss
${\mathcal{L}}$. In all experiments, we set $\alpha$ to 0.2 and $\gamma$ to 1.

####  3.1.2. Label Distribution Smoothing

Label distribution smoothing (LDS) (Yang et al., 2021) assigns varying weights
to training samples based on their label density. The objective is to mitigate
the impact of redundant samples while accentuating the significance of
sparsely represented samples during training. To account for the continuity of
labels, a Gaussian kernel is employed to smooth the empirical label density
distribution of the label space ${\mathcal{Y}}$. The weight $w_{i}$ for each
training sample is defined as:

(3) $w_{i}=\frac{1}{\int_{\mathcal{Y}}K(y_{i},y)|{\mathcal{C}}_{k}|dy},$

where $K(y,y^{\prime})=\exp\left(-\frac{\left\lVert
y-y^{\prime}\right\rVert^{2}}{2\sigma^{2}}\right)$ represents a Gaussian
kernel with kernel size $\ell$ and standard deviation $\sigma$, and
${\mathcal{C}}_{k}$ denotes the set of training samples in the $k$-th bin
where $y_{i}\in[b_{k-1},b_{k})$. In all experiments, we set $\ell$ to 5 and
$\sigma$ to 2.

—c—c—cc—cc—cc—

Dataset Method MAE $\downarrow$ RMSE $\downarrow$ G-Mean $\downarrow$
All Few All Few All Few

B-H Vanilla 4.5$\pm 0.2$ 5.3$\pm 0.4$ 7.0$\pm 0.5$ 7.3$\pm 0.6$ 2.5$\pm 0.1$
3.3$\pm 0.3$
+Focal 4.6$\pm 0.2$ 5.0$\pm 0.3$ 6.5$\pm 0.3$ 6.8$\pm 0.5$ 2.8$\pm 0.1$
3.0$\pm 0.4$
+LDS 4.8$\pm 0.3$ 4.6$\pm 0.5$ 7.1$\pm 0.7$ 6.3$\pm 0.5$ 2.8$\pm 0.2$ 2.8$\pm
0.4$
+Focal+LDS 4.7$\pm 0.2$ 5.4$\pm 0.4$ 6.7$\pm 0.2$ 7.3$\pm 0.5$ 2.8$\pm 0.1$
3.4$\pm 0.4$

S-M Vanilla 7.5$\pm 0.3$ 8.5$\pm 6.8$ 11.1$\pm 0.4$ 12.3$\pm 9.3$ 4.1$\pm 0.2$
4.5$\pm 3.5$
+Focal 8.5$\pm 0.1$ 7.0$\pm 2.3$ 12.0$\pm 0.3$ 10.0$\pm 3.6$ 5.0$\pm 0.1$
3.5$\pm 1.1$
+LDS 8.0$\pm 0.3$ 6.1$\pm 2.8$ 11.3$\pm 0.4$ 8.1$\pm 3.8$ 4.7$\pm 0.2$ 3.8$\pm
1.7$
+Focal+LDS 8.6$\pm 0.3$ 5.7$\pm 2.2$ 12.0$\pm 0.4$ 7.8$\pm 3.2$ 5.1$\pm 0.1$
3.0$\pm 1.3$

AZ Vanilla 22.1$\pm 1.7$ 26.0$\pm 6.9$ 29.7$\pm 2.1$ 32.8$\pm 7.4$ 12.0$\pm
1.2$ 15.6$\pm 6.7$
+Focal 22.0$\pm 1.0$ 26.2$\pm 4.4$ 29.5$\pm 1.3$ 33.2$\pm 5.0$ 13.0$\pm 0.7$
16.1$\pm 5.9$
+LDS 22.2$\pm 1.3$ 24.4$\pm 6.5$ 29.1$\pm 1.6$ 30.6$\pm 6.8$ 12.9$\pm 0.8$
14.8$\pm 7.3$
+Focal+LDS 22.0$\pm 1.0$ 25.7$\pm 5.9$ 29.3$\pm 1.2$ 33.2$\pm 7.6$ 12.5$\pm
0.8$ 14.2$\pm 4.9$

Table 2. Comparison of reaction yield prediction performance with and without
cost-sensitive re-weighting methods on _all_ and _few-shot_ regions. The best
results are highlighted in bold, and the second-best results are underlined.

###  3.2. Effectiveness in High-Yield Predictions

Table 3.1.2 presents the experiment results on the same three yield prediction
datasets, demonstrating the effectiveness of cost-sensitive re-weighting
methods (i.e., Focal loss, LDS, and the combination of both) when integrated
with existing yield prediction models. Across all three datasets, imbalanced
regression methods consistently achieve the best results in all 9 combinations
of evaluation metrics (MAE, RMSE, and G-Mean) in the _few-shot_ region.
Meanwhile, the base model (“Vanilla”) without any imbalanced regression
designs maintains its superiority in 6 out of 9 combinations in the _all_
region. This observation is understandable and aligns with the trade-off
between prediction performance in underrepresented data regions and
performance across the entire dataset.

However, it’s important to note that while there is a performance drop in the
_all_ region, this drop is not significant compared to the substantial
performance improvement observed in the _few-shot_ region. Specifically, the
average performance drops are 6.7%, 15.7%, and 0.7%, while the average
performance improvements are 14.0%, 34.3%, and 7.3% on each dataset,
respectively. This observation underscores the effectiveness of incorporating
simple imbalanced regression methods into existing yield prediction models as
a plug-in module. Furthermore, it is important to highlight that by tailoring
more sophisticated imbalanced regression techniques to yield prediction, we
could anticipate a further performance improvement.

##  4\. Conclusion

In this paper, we have highlighted a critical issue in reaction yield
prediction – the prevalent focus on achieving superior performance across the
entire yield spectrum, often at the expense of overlooking yield regions with
limited training samples, particularly the high-yield areas, which are of
greater concern to chemists. Through extensive experiments on three real-world
datasets, we have emphasized the urgent need to reframe reaction yield
prediction as an imbalanced regression problem. Moreover, we have demonstrated
that by incorporating simple cost-sensitive re-weighting techniques, we can
significantly enhance the performance of yield prediction models in
underrepresented high-yield regions.

## References

  * (1)
  * Ahneman et al. (2018) Derek T Ahneman, Jesús G Estrada, Shishi Lin, Spencer D Dreher, and Abigail G Doyle. 2018.  Predicting reaction performance in C–N cross-coupling using machine learning.  _Science_ (2018).
  * Branco et al. (2017) Paula Branco, Luís Torgo, and Rita P Ribeiro. 2017.  SMOGN: a pre-processing approach for imbalanced regression. In _First international workshop on learning with imbalanced domains: Theory and applications_.
  * Chawla et al. (2002) Nitesh V Chawla, Kevin W Bowyer, Lawrence O Hall, and W Philip Kegelmeyer. 2002.  SMOTE: synthetic minority over-sampling technique.  _Journal of artificial intelligence research_ (2002).
  * Gong et al. (2022) Yu Gong, Greg Mori, and Frederick Tung. 2022.  RankSim: Ranking Similarity Regularization for Deep Imbalanced Regression. In _ICML_.
  * Guo et al. (2023) Zhichun Guo, Kehan Guo, Bozhao Nan, Yijun Tian, Roshni G Iyer, Yihong Ma, Olaf Wiest, Xiangliang Zhang, Wei Wang, Chuxu Zhang, et al. 2023\.  Graph-based molecular representation learning. In _IJCAI_.
  * Kenton and Toutanova (2019) Jacob Devlin Ming-Wei Chang Kenton and Lee Kristina Toutanova. 2019.  Bert: Pre-training of deep bidirectional transformers for language understanding. In _NAACL_.
  * Lin et al. (2017) Tsung-Yi Lin, Priya Goyal, Ross Girshick, Kaiming He, and Piotr Dollár. 2017.  Focal loss for dense object detection. In _ICCV_.
  * Liu et al. (2023) Gang Liu, Tong Zhao, Eric Inae, Tengfei Luo, and Meng Jiang. 2023.  Semi-Supervised Graph Imbalanced Regression. In _KDD_.
  * Maloney et al. (2023) Michael P Maloney, Connor W Coley, Samuel Genheden, Nessa Carson, Paul Helquist, Per-Ola Norrby, and Olaf Wiest. 2023.  Negative Data in Data Sets for Machine Learning Training.
  * Perera et al. (2018) Damith Perera, Joseph W Tucker, Shalini Brahmbhatt, Christopher J Helal, Ashley Chong, William Farrell, Paul Richardson, and Neal W Sach. 2018.  A platform for automated nanomole-scale reaction screening and micromole-scale synthesis in flow.  _Science_ (2018).
  * Ribeiro and Moniz (2020) Rita P Ribeiro and Nuno Moniz. 2020.  Imbalanced regression and extreme value prediction.  _Machine Learning_ (2020).
  * Saebi et al. (2023) Mandana Saebi, Bozhao Nan, John E Herr, Jessica Wahlers, Zhichun Guo, Andrzej M Zurański, Thierry Kogej, Per-Ola Norrby, Abigail G Doyle, Nitesh V Chawla, et al. 2023\.  On the use of real-world datasets for reaction yield prediction.  _Chemical Science_ (2023).
  * Schwaller et al. (2021) Philippe Schwaller, Alain C Vaucher, Teodoro Laino, and Jean-Louis Reymond. 2021.  Prediction of chemical reaction yields using deep learning.  _Machine learning: science and technology_ (2021).
  * Torgo et al. (2013) Luís Torgo, Rita P Ribeiro, Bernhard Pfahringer, and Paula Branco. 2013.  Smote for regression. In _Portuguese conference on artificial intelligence_.
  * Voinarovska et al. (2023) Varvara Voinarovska, Mikhail Kabeshov, Dmytro Dudenko, Samuel Genheden, and Igor V Tetko. 2023.  When yield prediction does not yield prediction: an overview of the current challenges.  _Journal of Chemical Information and Modeling_ (2023).
  * Yang et al. (2021) Yuzhe Yang, Kaiwen Zha, Yingcong Chen, Hao Wang, and Dina Katabi. 2021.  Delving into deep imbalanced regression. In _ICLR_.
  * Yarish et al. (2023) Dzvenymyra Yarish, Sofiya Garkot, Oleksandr O Grygorenko, Dmytro S Radchenko, Yurii S Moroz, and Oleksandr Gurbych. 2023.  Advancing molecular graphs with descriptors for the prediction of chemical reaction yields.  _Journal of Computational Chemistry_ (2023).


#  ltlf Best-Effort Synthesis in Nondeterministic
Planning Domains

Giuseppe De Giacomo  Gianmarco Parretti Corresponding Author. Email:
<EMAIL_ADDRESS>Shufang Zhu Corresponding Author. Email:
<EMAIL_ADDRESS>University of Oxford, UK  University of Rome “La
Sapienza”, Italy

###### Abstract

We study best-effort strategies (aka plans) in fully observable
nondeterministic domains (FOND) for goals expressed in Linear Temporal Logic
on Finite Traces (ltlf). The notion of best-effort strategy has been
introduced to also deal with the scenario when no agent strategy exists that
fulfills the goal against every possible nondeterministic environment
reaction. Such strategies fulfill the goal if possible, and do their best to
do so otherwise. We present a game-theoretic technique for synthesizing best-
effort strategies that exploit the specificity of nondeterministic planning
domains. We formally show its correctness and demonstrate its effectiveness
experimentally, exhibiting a much greater scalability with respect to a direct
best-effort synthesis approach based on re-expressing the planning domain as
generic environment specifications.

##  1 Introduction

Recently there has been quite some interest in synthesis [27, 21] for
realizing goals (or tasks) $\varphi$ against environment specifications
$\mathcal{E}$ [3, 4], especially when both $\varphi$ and $\mathcal{E}$ are
expressed in Linear Temporal Logic on finite traces (ltlf) [19, 20], the
finite trace variant of ltl [28], a logic specification language that is
commonly adopted in Formal Methods [6]. In this setting, synthesis amounts to
finding an agent strategy that wins, i.e., generates a trace satisfying
$\varphi$, whatever is the (counter-)strategy chosen by the environment, which
in turn has to satisfy its specification $\mathcal{E}$. This form of synthesis
can be seen as an extension of FOND planning [23, 24], as shown in, e.g., [18,
10].

Obviously, a winning strategy for the agent may not exist. To handle this
possibility, the notion of strong cyclic plans was introduced [12, 11]: if a
(strong) plan does not exist, there may still exist a plan that could win
assuming the environment is not strictly adversarial. Building on this
intuition, Aminof et al. [1] proposed the notion of best-effort strategies (or
plans), which formally capture the idea that the agent could do its best by
adopting a strategy that wins against a maximal set (though not all) of
possible environment strategies. It was then shown in [5] that best-effort
strategies capture the game-theoretic rationality principle that a player (the
agent) would not use a strategy that is “dominated” by another one (i.e., if
another strategy fulfills the goal against more environment behaviors, then
the player should adopt that strategy). Best-effort strategies have some
notable properties: (_i_) they always exist, (_ii_) if a winning strategy
exists, then best-effort strategies are exactly the winning strategies,
(_iii_) best-effort strategies can be computed in 2EXPTIME as winning
strategies (best-effort synthesis is indeed 2EXPTIME-complete).

In [5] an algorithm for ltlf best-effort synthesis has been presented. This
algorithm is based on creating, solving, and combining the solutions of three
distinct games (with three different objectives) played in the same game
arena. The arena is obtained from the deterministic finite-state automata
(DFAs) corresponding to the ltlf specification of the agent goal $\varphi$ and
the ltlf specification of the environment $\mathcal{E}$. As a result, the size
of the arena is, in the worst-case, double-exponential both in $\varphi$ and
in $\mathcal{E}$. Using this framework, we can also capture best-effort
synthesis in nondeterministic planning domains. In particular, one can simply
re-express nondeterministic planing domains (FOND) in ltlf [19, 3, 26] and
then use the ltlf best-effort synthesis approach directly. However, observe
that in planning, while the (temporally extended) goal $\varphi$ is typically
small, the environment specification $\mathcal{E}$ is large, being the entire
planning domain (i.e., a representation of how the world the agent is immersed
in works). This observation motivates our paper.

We study ltlf best-effort synthesis directly in the context of
nondeterministic (adversarial) planning domains. Specifically, our
contributions are:

  * •

A framework for best-effort synthesis in nondeterministic (adversarial)
planning domains;

  * •

A synthesis technique for best-effort synthesis, inspired by the one in [5],
that takes full advantage of the specificity of planning domains as
environment specifications;

  * •

A symbolic best-effort synthesis algorithm that performs and scales well;

  * •

An empirical evaluation of the practical effectiveness of the approach.

Our results show that computing best-effort strategies for ltlf goals in
nondeterministic domains is much more effective than using ltlf best-effort
synthesis directly. In fact, our technique can be implemented quite
efficiently, with only a small overhead wrt to computing winning strategies
(i.e., strong plans) in FOND. Hence, it is completely feasible in practice to
return a best-effort strategy instead of giving up when a winning strategy
does not exist.

Figure 1: An arch. We denote location names in the blocks.

Running Example.  We now present a relatively simple example to illustrate the
key structure of ltlf best-effort synthesis in nondeterministic planning
domains. This example, adapted from [26], represents a human-robot co-assembly
task in a shared workplace. Specifically, the human and robot involved in the
task are considered as the environment and the agent, respectively. In the
shared workplace, the robot can perform grasp/place actions to pick/drop
blocks and transfer/transit actions to move its robotic arm with/without a
block in its gripper. After every robot action, the human can react by also
moving blocks among locations to interfere with the robot, hence introducing
nondeterminism to robot actions. Consider a robot _goal_ (aka _task_) of
assembling an arch of blocks, as depicted in Figure 1. It is easy to see that
the agent has _no_ _winning strategy_ (aka _strong solution_) to assemble the
arch, since the human can always disassemble it. Therefore, standard synthesis
[20, 18] would conclude the task as _unrealizable_ , hence “giving up".
However, the robot still has the chance to fulfill the goal, should the human
cooperate or even perform flawed reactions due to e.g. lack of adequate
training. Therefore, instead of simply giving up, the agent should try its
best to pursue the goal by exploiting human reactions. _Best-effort
strategies_ (aka _best-effort solutions_) precisely capture this intuition.

##  2 Preliminaries

Traces. Let $\Sigma$ be a set of propositions. A trace
$\pi=\pi_{0}\pi_{1}\ldots$ is a sequence of propositional interpretations
(sets), where for every $i\geq 0$, $\pi_{i}\in 2^{\Sigma}$ is the $i$-th
interpretation of $\pi$. Intuitively, $\pi_{i}$ is interpreted as the set of
propositions that are $true$ at instant $i$. The length of a trace is $|\pi|$.
A trace $\pi$ is an infinite trace if $|\pi|=\infty$, which is formally
denoted as $\pi\in(2^{\Sigma})^{\omega}$; otherwise $\pi$ is a finite trace,
denoted as $\pi\in(2^{\Sigma})^{*}$. If a trace $\pi$ is finite, we denote by
$\mathtt{lst}(\pi)$ its last instant (i.e., index). Moreover, by
$\pi^{k}=\pi_{0}\cdots\pi_{k}$ we denote the _prefix_ of $\pi$ up to the
$k$-th iteration.

LTLf Basics. Linear Temporal Logic on finite traces (ltlf) is a specification
language to express temporal properties on finite and non-empty traces [19].
In particular, ltlf has the same syntax as ltl, which is instead interpreted
over infinite traces [28]. Given a set of propositions $\Sigma$, ltlf formulas
are generated as follows:

$\varphi::=p\mid\varphi\wedge\varphi\mid\neg\varphi\mid\raisebox{-1.1625pt}{\LARGE$\circ$}\varphi\mid\varphi\mathop{\mathcal{U}}\varphi.$

$p\in\Sigma$ is an atom, $\circ$ (_Next_), and $\mathop{\mathcal{U}}$
(_Until_) are temporal operators. We use standard Boolean abbreviations such
as $\vee$ (or) and $\supset$ (implies), $\mathit{true}$ and $\mathit{false}$.
Moreover, we define the following abbreviations _Weak Next_
$\raisebox{-1.1625pt}{\LARGE$\bullet$}\varphi\equiv\neg\raisebox{-1.1625pt}{\LARGE$\circ$}\neg\varphi$,
_Eventually_ $\Diamond\varphi\equiv\mathit{true}\mathop{\mathcal{U}}\varphi$
and _Always_ $\Box\varphi\equiv\neg\Diamond\neg\varphi$. The size of
$\varphi$, written $|\varphi|$, is the number of all subformulas of $\varphi$.

Given an ltlf formula $\varphi$ over $\Sigma$ and a finite, non-empty trace
$\pi\in(2^{\Sigma})^{+}$, we define when $\varphi$ _holds_ at instant
$i~{}(0\leq i\leq\mathtt{lst}(\pi))$, written as $\pi,i\models\varphi$,
inductively on the structure of $\varphi$, as:

  * •

$\pi,i\models p\text{ iff }p\in\pi_{i}$;

  * •

$\pi,i\models\lnot\varphi\text{ iff }\pi,i\not\models\varphi$;

  * •

$\pi,i\models\varphi_{1}\wedge\varphi_{2}\text{ iff
}\pi,i\models\varphi_{1}\text{ and }\pi,i\models\varphi_{2}$;

  * •

$\pi,i\models\raisebox{-1.1625pt}{\LARGE$\circ$}\varphi\text{ iff
}i<\mathtt{lst}(\pi)$ and $\pi,i+1\models\varphi$;

  * •

$\pi,i\models\varphi_{1}\mathop{\mathcal{U}}\varphi_{2}$ iff $\exists j$ such
that $i\leq j\leq\mathtt{lst}(\pi)$ and $\pi,j\models\varphi_{2}$, and
$\forall k,i\leq k<j$ we have that $\pi,k\models\varphi_{1}$.

We say $\pi$ _satisfies_ $\varphi$, written as $\pi\models\varphi$, if
$\pi,0\models\varphi$.

FOND Planning for ltlf Goals. Planning in Fully Observable Nondeterministic
(FOND) domains for ltlf goals concerns computing a strategy to fulfill a
temporally extended goal expressed as an ltlf formula in a planning domain,
where the agent has full observability, regardless of how the environment non-
deterministically reacts to agent actions. In this paper, we extend existing
works on synthesis-based approaches to planning in FOND domains [18, 9, 10] to
compute best-effort strategies [5].

##  3 Framework

We begin by presenting our framework. First, we introduce the notion of
nondeterministic planning domain and then formalize the problem of ltlf best-
effort synthesis in nondeterministic planning domains.

###  3.1 Nondeterministic Planning Domains

In our framework, a nondeterministic planning domain is intuitively considered
as the arena of a two-player game, in which the agent and the environment can
perform actions and reactions, respectively. Starting from the initial state
of the domain, the agent and the environment move in turns, such that at each
turn, the agent makes an action and the environment responds with some
reaction. State transitions are determined only if both players complete their
moves following the preconditions of their respective moves. In such a domain,
the nondeterminism for the agent comes from not knowing how the environment
will react.

Formally, we define a nondeterministic planning domain as a tuple
$\mathcal{D}=(2^{\mathcal{F}},s_{0},Act,React,\alpha,\beta,\delta)$, where:
$\mathcal{F}$ is a finite set of fluents such that $2^{\mathcal{F}}$ is the
state space and $|\mathcal{F}|$ is the size of the domain; $s_{0}\in
2^{\mathcal{F}}$ is the initial state; $Act$ and $React$ are finite sets of
agent actions and environment reactions, respectively;
$\alpha:2^{\mathcal{F}}\rightarrow 2^{Act}$ and $\beta:2^{\mathcal{F}}\times
Act\rightarrow 2^{React}$ denote preconditions of agent actions and
environment reactions, respectively; and $\delta:2^{\mathcal{F}}\times
Act\times React\mapsto 2^{\mathcal{F}}$ is the transition function such that
$\delta(s,a,r)=s^{\prime}\in 2^{\mathcal{F}}$ if $a\in\alpha(s)$ and
$r\in\beta(s,a)$, and $\delta(s,a,r)$ is undefined otherwise.

In particular, we require planning domains to satisfy the following three
rules:

  * •

_Existence of agent action_. For every state $s\in 2^{\mathcal{F}}$, there
exists at least one agent action $a$ such that $a\in\alpha(s)$. Formally:

$\forall s\in 2^{\mathcal{F}}.\alpha(s)\neq\emptyset.$

This rule guarantees that the agent can perform at least one action in every
state of the domain111If this is not the case, it is sufficient to add a new
agent action $\mathit{nop}$ with a corresponding environment reaction
$\mathit{nopr}$ such that $\delta(s,\mathit{nop},\mathit{nopr})=s$..

  * •

_Existence of environment reaction_. For every state $s\in 2^{\mathcal{F}}$
and agent action $a\in\alpha(s)$, there exists at least one environment
reaction $r\in\beta(s,a)$ such that $\delta(s,a,r)$ is defined. Formally:

$\forall s\in 2^{\mathcal{F}},\forall a\in\alpha(s).\beta(s,a)\neq\emptyset.$

This rule guarantees that the environment is able to respond to any agent
action that follows the action precondition.

  * •

_Uniqueness of environment reaction_. For every state $s\in 2^{\mathcal{F}}$,
agent action $a\in\alpha(s)$, and successor state $s^{\prime}=\delta(s,a,r)$
for some $r\in\beta(s,a)$, the reaction $r$ is unique. Formally:

$\forall s\in 2^{\mathcal{F}},\forall a\in\alpha(s),\forall
r_{1},r_{2}\in\beta(s,a).$

$\delta(s,a,r_{1})=\delta(s,a,r_{2})\supset r_{1}=r_{2}.$

This rule guarantees that, given a state $s$ and an agent action
$a\in\alpha(s)$, all the environment responses in $\beta(s,a)$ are
distinguishable by just looking at the resulting successor state222Observe
that if this rule does not hold in our domain, we can easily modify the domain
by introducing fluents to represent possible environment reactions and record
the reaction in the resulting state, hence complying to the rule..

Observe that the nondeterministic planning domains adopted in FOND [12, 23],
say expressed in PDDL [25], can be immediately captured by our notion along
the line discussed in [17].

A state trace of $\mathcal{D}$ is a (finite or infinite) sequence
$\tau=s_{0}s_{1}\ldots$ of states in $2^{\mathcal{F}}$ such that $s_{0}$ is
the initial state of $\mathcal{D}$. A trace $\tau$ is legal, if for every $i$
there exists an agent action $a_{i}$ and an environment reaction $r_{i}$ such
that $s_{i+1}=\delta(s_{i},a_{i},r_{i})$ with $a_{i}\in\alpha(s_{i})$ and
$r_{i}\in\beta(s_{i},a_{i})$.

We denote by $\vec{a}=a_{0}a_{1}\ldots$ (resp. $\vec{r}=r_{0}r_{1}\ldots$) a
sequence of agent actions (resp. environment reactions) and by $\vec{a}^{\ k}$
(resp. $\vec{r}^{\ k}$) the prefix of $\vec{a}$ (resp. $\vec{r}$ ) up to
action $a_{k}$ (resp. reaction $r_{k}$). We use $\vec{a}_{\epsilon}$ and
$\vec{r}_{\epsilon}$ to denote the empty sequence of agent actions and
environment reactions (when $k<0$), respectively. Consider $\vec{a}$ and
$\vec{r}$ with the same length, we denote the trace induced by $\vec{a}$ and
$\vec{r}$ on $\mathcal{D}$ as $\mathtt{Trace}(\vec{a},\vec{r})$ defined as
follows:

  * •

$\mathtt{Trace}(\vec{a}_{\epsilon},\vec{r}_{\epsilon})=s_{0}$

  * •

$\mathtt{Trace}(\vec{a}^{k},\vec{r}^{k})=\\\
~{}~{}~{}~{}\mathtt{Trace}(\vec{a}^{k-1},\vec{r}^{k-1})\cdot\delta(\mathtt{lst}(\mathtt{Trace}(\vec{a}^{k-1},\vec{r}^{k-1}),a_{k},r_{k}))$

If
$\delta(\mathtt{lst}(\mathtt{Trace}(\vec{a}^{k-1},\vec{r}^{k-1}),a_{k},r_{k}))$
is undefined or $\vec{a}$ and $\vec{r}$ are in different length,
$\mathtt{Trace}(\vec{a},\vec{r})$ returns undefined.

An agent strategy is a function $\sigma:(2^{\mathcal{F}})^{+}\rightarrow Act$
mapping traces of states on $\mathcal{D}$ to agent actions. Note that in the
synthesis literature, agent strategies are typically defined as functions
$\sigma^{\prime}:React^{*}\rightarrow Act$ mapping histories of environment
reactions to agent actions. However, we define agent strategies equivalently
as functions $\sigma:(2^{\mathcal{F}})^{+}\rightarrow Act$ to be more in line
with existing works on planning and reasoning about actions [18]. The
equivalence follows by noting that: (_i_) every strategy
$\sigma:(2^{\mathcal{F}})^{+}\rightarrow Act$ directly corresponds to a
strategy $\sigma^{\prime}:React^{*}\rightarrow Act$ by the requirement of
uniqueness of environment reaction; (_ii_) every strategy
$\sigma^{\prime}:React^{*}\rightarrow Act$ directly corresponds to a strategy
$\sigma:(2^{\mathcal{F}})^{+}\rightarrow Act$ since the transition function
$\delta$ is deterministic. An agent strategy $\sigma$ is legal if, for every
legal trace $\tau$, it holds that for all its prefixes $\tau^{k}$, if
$a_{k}=\sigma(\tau^{k})$, then $a_{k}\in\alpha(\mathtt{lst}(\tau^{k}))$.

An environment strategy is a function $\gamma:Act^{+}\rightarrow React$. Given
a sequence of agent actions $\vec{a}$ and an environment strategy $\gamma$, we
denote by $\vec{\gamma}(\vec{a})$ the sequence of environment reactions
obtained by applying $\gamma$ recursively on every finite prefix $\vec{a}^{\
k}~{}(k\geq 0)$ of $\vec{a}$, i.e.,
$\vec{\gamma}(\vec{a})_{k}=\gamma(\vec{a}^{\ k})$. An environment strategy is
legal, if for every sequence of agent actions $\vec{a}$, it holds that for all
its prefixes $\vec{a}^{\ k}$, if
$\tau=\mathtt{Trace}(\vec{a}^{k-1},\vec{\gamma}(\vec{a}^{k-1}))$ is defined,
hence legal, and ${a}_{k}\in\alpha(\mathtt{lst}(\tau))$, then
$r_{k}=\gamma(\vec{a}^{\ k-1}\cdot a_{k})\in\beta(\mathtt{lst}(\tau),a_{k}))$.

Given a legal agent strategy $\sigma$ and a legal environment strategy
$\gamma$, there exists a unique trace of $\mathcal{D}$ that is induced by both
$\sigma$ and $\gamma$, which we denote as $\mathtt{Play}(\sigma,\gamma)$.
Formally, $\mathtt{Play}(\sigma,\gamma)=s_{0}s_{1}\ldots$ is such that $s_{0}$
is the initial state of $\mathcal{D}$ and for every $i\geq 0$,
$s_{i+1}=\delta(s_{i},a_{i},r_{i})$ with $a_{i}=\sigma(s_{0}\ldots s_{i})$ and
$r_{i}=\gamma(a_{0}\ldots a_{i})$. We can prove by induction that
$\mathtt{Play}(\sigma,\gamma)$ is indeed defined and legal.

######  Theorem 3.1.

Let $\mathcal{D}$ be a planning domain, $\sigma$ a legal agent strategy, and
$\gamma$ a legal environment strategy. Then, $\mathtt{Play}(\sigma,\gamma)$ is
defined and legal.

Strong and Cooperative Solutions. Given a planning domain $\mathcal{D}$, an
agent _goal_ is an ltlf formula $\varphi$ defined over the fluents
$\mathcal{F}$ of the domain $\mathcal{D}$. A legal trace $\tau$ of
$\mathcal{D}$ satisfies $\varphi$ in $\mathcal{D}$, written
$\tau\models_{\mathcal{D}}\varphi$, if there exists a prefix of $\tau$ that
satisfies $\varphi$. An agent strategy $\sigma$ is a _strong solution_ for
$\varphi$ in $\mathcal{D}$ if, $\sigma$ is legal and for every legal
environment strategy $\gamma$, it holds that
$\mathtt{Play}(\sigma,\gamma)\models_{\mathcal{D}}\varphi$. If such a strategy
$\sigma$ exists, we say that there exists a strong solution for $\varphi$ in
$\mathcal{D}$, which is $\sigma$. Furthermore, an agent strategy $\sigma$ is a
_cooperative solution_ for $\varphi$ in $\mathcal{D}$, if $\sigma$ is legal
and there exists a legal environment strategy $\gamma$ such that
$\mathtt{Play}(\sigma,\gamma)\models_{\mathcal{D}}\varphi$. If such a strategy
$\sigma$ exists, there exists a cooperative solution for $\varphi$ in
$\mathcal{D}$, which is $\sigma$.

###  3.2 Best-Effort Synthesis in Planning Domains

We now introduce the problem of ltlf best-effort synthesis in nondeterministic
planning domains. In doing so, we need to define what it means for an agent to
make its best-effort to achieve its goal in a planning domain. To formalize
such strategies, we adapt the definitions in [5] and consider first the notion
of dominance.

######  Definition 3.2.

Let $\mathcal{D}$ be a planning domain, $\varphi$ an ltlf formula, and
$\sigma_{1},\sigma_{2}$ two legal agent strategies. $\sigma_{1}$ dominates
$\sigma_{2}$ for $\varphi$ in $\mathcal{D}$, written
$\sigma_{1}\geq_{\varphi|\mathcal{D}}\sigma_{2}$, if for every legal
environment strategy $\gamma$,
$\mathtt{Play}(\sigma_{2},\gamma)\models_{\mathcal{D}}\varphi$ implies
$\mathtt{Play}(\sigma_{1},\gamma)\models_{\mathcal{D}}\varphi$.

Furthermore, a legal agent strategy $\sigma_{1}$ strictly dominates legal
agent strategy $\sigma_{2}$ for goal $\varphi$ in $\mathcal{D}$, written
$\sigma_{1}>_{\varphi|\mathcal{D}}\sigma_{2}$, if
$\sigma_{1}\geq_{\varphi|\mathcal{D}}\sigma_{2}$ and
$\sigma_{2}\not\geq_{\varphi|\mathcal{D}}\sigma_{1}$. Intuitively,
$\sigma_{1}>_{\varphi|\mathcal{D}}\sigma_{2}$ shows that $\sigma_{1}$ does at
least as well as $\sigma_{2}$ against every legal environment strategy in
$\mathcal{D}$ and strictly better against at least one such strategy. If
$\sigma_{1}$ strictly dominates $\sigma_{2}$, then an agent using $\sigma_{2}$
is not doing its “best” to achieve the goal. Within this framework, a best-
effort solution is a legal agent strategy that is not strictly dominated by
any other legal strategies.

######  Definition 3.3.

A legal agent strategy $\sigma$ is a best-effort solution for $\varphi$ in
$\mathcal{D}$ iff there is no legal agent strategy $\sigma^{\prime}$ such that
$\sigma^{\prime}>_{\varphi|\mathcal{D}}\sigma$.

It is worth noting that, although we adapt the definitions of best-effort
solutions from [5], the key difference is that, in our framework, best-effort
solutions are required to be legal agent strategies, i.e., to always satisfy
agent action preconditions. However, in the best-effort synthesis setting
defined in [5], since the environment is specified as an ltl/ltlf formula,
there are no such preconditions for the agent to follow.

######  Definition 3.4.

The problem of ltlf best-effort synthesis in nondeterministic planning domains
is defined as a pair $\mathcal{P}=(\mathcal{D},\varphi)$, where $\mathcal{D}$
is a nondeterministic planning domain and $\varphi$ is an ltlf formula. Best-
effort synthesis of $\mathcal{P}$ computes a best-effort solution for
$\varphi$ in $\mathcal{D}$.

In particular, if the synthesis problem $\mathcal{P}=(\mathcal{D},\varphi)$
admits a strong solution for $\varphi$ in $\mathcal{D}$, then computing a
best-effort solution coincides with computing a strong solution. This
observation is analogous to the one for ltlf best-effort synthesis in [5],
where the environment is specified in ltl/ltlf.

######  Proposition 3.5.

Let $\mathcal{P}=(\mathcal{D},\varphi)$ be the defined synthesis problem that
admits a strong solution for $\varphi$ in $\mathcal{D}$ and $\sigma$ an agent
strategy. We have that $\sigma$ is a best-effort solution for $\varphi$ in
$\mathcal{D}$ iff $\sigma$ is a strong solution for $\varphi$ in
$\mathcal{D}$.

In order to compute best-effort solutions, we first observe that a best-effort
solution can be considered as a strategy $\sigma$ such that for every history
$h\in(2^{\mathcal{F}})^{+}$, i.e., a finite and legal sequence of states of a
planning domain $\mathcal{D}$, that is consistent with $\sigma$, $\sigma$
extends $h$ to fulfill the goal whenever possible. Hence, one of the following
possibilities holds: (_i_) if the agent can extend $h$ to fulfill the goal
regardless of how the environment reacts, then any extension of $h$ following
$\sigma$ should ensure goal completion; (_ii_) if no extension of $h$ allows
the agent to fulfill the goal, then $\sigma$ just behaves legally; (_iii_) if
there are only some extensions of $h$, but not all, that allow the agent to
fulfill the goal, then there should exist an extension of $h$ following
$\sigma$ that fulfills the goal. Observe that (_iii_) guarantees that the
agent does its best, assuming the environment might cooperate to help the
agent fulfill its goal.

Consider an agent strategy $\sigma$. We now formalize these three
possibilities by assigning a value to each history $h$ consistent with
$\sigma$, as in [5]. For a legal agent strategy $\sigma$ and a history $h$
that is consistent with $\sigma$, we use $\Gamma(h,\sigma)$ to denote the set
of legal environment strategies $\gamma$ in $\mathcal{D}$ such that $h$ is a
prefix of $\mathtt{Play}(\sigma,\gamma)$. Furthermore, we denote by
$\mathcal{H}_{\mathcal{D}}(\sigma)$ the set of legal histories $h$ such that
$\Gamma(h,\sigma)$ is nonempty, i.e., the set of legal histories of
$\mathcal{D}$ that are consistent with $\sigma$ with some legal environment
strategy $\gamma$. We define the value of $h$ that is consistent with a legal
agent strategy $\sigma$ as follows:

  * •

$val(\sigma,h)=+1$ (winning), if
$\mathtt{Play}(\sigma,\gamma)\models_{\mathcal{D}}\varphi$ for every
$\gamma\in\Gamma(h,\sigma)$;

  * •

$val(\sigma,h)=-1$ (losing), if
$\mathtt{Play}(\sigma,\gamma)\not\models_{\mathcal{D}}\varphi$ for every
$\gamma\in\Gamma(h,\sigma)$;

  * •

$val(\sigma,h)=0$ (pending), otherwise.

Let $val(h)$ be the maximal value of $val(\sigma,h)$, considering all the
strategies $\sigma$ such that $h\in\mathcal{H}_{\mathcal{D}}(\sigma)$333We
consider $val(h)$ only if there exists at least one agent strategy $\sigma$
such that $h\in\mathcal{H}_{\mathcal{D}}(\sigma)$.. The following theorem
states that a best-effort solution $\sigma$ guarantees to maximize the value
of every history $h$ that is consistent with $\sigma$.

######  Theorem 3.6 (Maximality Condition).

An agent strategy $\sigma$ is a best-effort solution for $\varphi$ in
$\mathcal{D}$ iff for every $h\in\mathcal{H}_{\mathcal{D}}(\sigma)$ it holds
that $val(\sigma,h)=val(h)$.

While classical synthesis and planning settings (see e.g. [27, 20, 18]) first
require checking the realizability of the problem, i.e., the existence of a
solution, in the case of best-effort synthesis realizability is trivial, as
there always exists a best-effort solution.

######  Theorem 3.7.

Let $\mathcal{P}=(\mathcal{D},\varphi)$ be a problem of ltlf best-effort
synthesis in nondeterministic planning domains. There always exists a best-
effort solution $\sigma$ for $\varphi$ in $\mathcal{D}$.

In order to prove Theorem 3.7, we show that we can always construct a strategy
$\hat{\sigma}$ that satisfies the Maximality Condition. To do so, we construct
a chain of legal agent strategies $\sigma_{0},\sigma_{1},\ldots$ by selecting
for each $i\geq 0$, a history $h\in\mathcal{H}_{\mathcal{D}}(\sigma_{i})$ that
has not yet been marked as stabilized, i.e., such that
$val(\sigma_{i},h)<val(h)$, and maximizing the value $val(\sigma_{i+1},h)$.
$\sigma_{i+1}$ is constructed by selecting a strategy $\sigma$ such that
$val(\sigma,h)=val(h)$ and setting
$\sigma_{i+1}=\sigma_{i}[h\leftarrow\sigma]$, where
$\sigma_{i}[h\leftarrow\sigma]$ denotes the strategy that agrees with
$\sigma_{i}$ everywhere, except in $h$ and all its extensions where it agrees
with $\sigma$. $\hat{\sigma}$ is the point-wise limit of the chain of
strategies, i.e., $\hat{\sigma}=lim_{i}\ \sigma_{i}$.

##  4 Synthesizing Best-Effort Solutions

We now provide an algorithm for ltlf best-effort synthesis in nondeterministic
planning domains based on game-theoretic techniques. In particular, we use DFA
games for adversarial/cooperative reachability and safety [20, 5, 31] to
capture the environment being adversarial/cooperative and agent always
following its action preconditions, respectively.

###  4.1 DFA Games

A _DFA game_ is a pair $\mathcal{A}=(\mathcal{T},Acc)$, where $\mathcal{T}$ is
a deterministic transition system acting as the _game arena_ and $Acc\subseteq
Q^{\omega}$ is the acceptance condition. Specifically, $\mathcal{T}=(Act\times
React,Q,q_{0},\varrho)$ is a deterministic transition system, where $Act\times
React$ is the alphabet, in which $Act$ and $React$ are two disjoint sets of
variables under the control of the agent and the environment, respectively;
$Q$ is a finite set of states; $q_{0}\in Q$ is the initial state;
$\varrho\colon Q\times Act\times React\rightarrow Q$ is the transition
function. Given an infinite word $\pi=\pi_{0}\pi_{1}\ldots\in(Act\times
React)^{\omega}$, the run $\rho={\sf{Run}{(}}\pi,\mathcal{T})$ of $\pi$ on
$\mathcal{T}$ is an infinite sequence $\rho=q_{0}q_{1}\ldots\in Q^{\omega}$
such that $q_{0}$ is the initial state of $\mathcal{T}$ and
$q_{i+1}=\varrho(q_{i},\pi_{i})$ for every $i\geq 0$. Analogously, we denote
by $\rho^{k+1}={\sf{Run}{(}}\pi^{k},\mathcal{T})$ the finite sequence
$\rho^{k+1}=q_{0}q_{1}\ldots q_{k+1}$ obtained from running $\pi^{k}$ on
$\mathcal{T}$. A run $\rho$ is _accepting_ if $\rho\in Acc$. We denote by
$\mathcal{L}(\mathcal{A})$ the set of words $\pi$ accepted by $\mathcal{A}$,
i.e., such that $\rho={\sf{Run}{(}}\pi,\mathcal{T})$ is accepting. In this
work, we specifically consider the following acceptance conditions:

  * •

Reachability. Given a set $R\subseteq
Q,\mathtt{Reach}(R)=\\{q_{0}q_{1}\ldots\in Q^{\omega}\mid\exists k\geq
0.q_{k}\in R\\}$, i.e., a state in $R$ is visited at least once.

  * •

Safety. Given a set $S\subseteq Q,\mathtt{Safe}(S)=\\{q_{0}q_{1}\ldots\in
Q^{\omega}\mid\forall k\geq 0.q_{k}\in S\\}$, i.e., only states in $S$ are
visited.

  * •

Safety-Reachability. Given two sets $S,R\subseteq Q,\mathtt{SafeReach}(S,R)$
$=\\{q_{0}q_{1}\ldots\in Q^{\omega}\mid\exists\ell\geq 0.q_{\ell}\in R\text{
and }\forall 0\leq k\leq\ell.q_{k}\in S\\}$, i.e., a state in $R$ is visited
at least once and until then only states in $S$ are visited.

Notably, a deterministic transition system with reachability acceptance
condition defines a deterministic finite state automaton (DFA).

An agent strategy on a DFA game is a function $\kappa:Q\rightarrow Act$.444For
the DFA games considered in this paper, it is sufficient to define strategies
in this form, which are called _positional strategies_. More general forms of
strategies, mapping histories of the game to agent actions/environment
reactions, are only needed for more sophisticated games [33]. Given an agent
strategy $\kappa$, a sequence of environment reactions
$\vec{r}=r_{0}r_{1}\ldots\in React^{\omega}$, and a transition system
$\mathcal{T}$, we denote by ${\sf{Run}{(}}\kappa,\vec{r},\mathcal{T})$, the
unique sequence $q_{0}q_{1}\ldots\in Q^{\omega}$ on $\mathcal{T}$ _induced_ by
(or _consistent with_) $\kappa$ and $\vec{r}$ as follows: $q_{0}$ is the
initial state of $\mathcal{T}$, and for every $i\geq 0$,
$q_{i+1}=\varrho(q_{i},a_{i},r_{i})$, where $a_{i}=\kappa(q_{i})$.

An agent strategy $\kappa$ is _winning_ in the game
$\mathcal{A}=(\mathcal{T},Acc)$, if for every sequence of environment
reactions $\vec{r}\in React^{\omega}$, it holds that
${\sf{Run}{(}}\kappa,\vec{r},\mathcal{T})\in Acc$. In _DFA games_ , $q\in Q$
is a _winning_ state, if the agent has a winning strategy in the game
$\mathcal{A}^{\prime}=(\mathcal{T}^{\prime},Acc)$, where
$\mathcal{T}^{\prime}=(Act\times React,Q,q,\delta)$, i.e., on the same
structure but with a new initial state $q$. We denote by
$W_{adv}(\mathcal{T},Acc)$ (sometimes $W_{adv}$ when $\mathcal{T}$ and $Acc$
are clear from the context) the set of all agent winning states. Intuitively,
$W_{adv}$ represents the “agent winning region", from which the agent can win
the game, no matter how the environment behaves. A positional strategy that is
winning from every state in the winning region is called _uniform winning_.

Similarly, an agent strategy $\kappa$ is _cooperatively winning_ in a game
$\mathcal{A}=(\mathcal{T},Acc)$ if there exists a sequence of environment
reactions $\vec{r}\in React^{\omega}$ such that
${\sf{Run}{(}}\kappa,\vec{r},\mathcal{T})\in Acc$. Hence, $q\in Q$ is a
_cooperatively winning state_ , if the agent has a cooperatively winning
strategy in the game $\mathcal{A}^{\prime}=(\mathcal{T}^{\prime},Acc)$, where
$\mathcal{T}^{\prime}=(Act\times React,Q,q,\delta)$. By
$W_{coop}(\mathcal{T},Acc)$ (sometimes $W_{coop}$), we denote the set of all
the agent cooperatively winning states. A positional strategy that is winning
from every state in the cooperatively winning region is called _uniform
cooperatively winning_.

###  4.2 Synthesis Technique

The key idea of our game-theoretic synthesis approach is reducing the
synthesis problem to DFA games, where the game arena is obtained by suitably
composing the nondeterministic planning domain and the DFA of the ltlf
formula. We first show how to transform the nondeterministic planning domain
$\mathcal{D}$ into a deterministic transition system, which is then composed
with the DFA of the ltlf formula to obtain the game arena.

In order to transform the domain $\mathcal{D}$ to a deterministic transition
system, we need to drop the preconditions of both agent actions and
environment reactions and transform the partial transition function into a
total transition function. To that end, we introduce two new states,
$s^{ag}_{err}$ and $s^{env}_{err}$, indicating that the agent and the
environment violate their respective preconditions. Formally, given a
nondeterministic planning domain
$\mathcal{D}=(2^{\mathcal{F}},s_{0},Act,React,\alpha,\beta,\delta)$, the
corresponding deterministic transition system $\mathcal{D}_{+}=(Act\times
React,2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\},s_{0},\delta^{\prime}$)
is constructed as follows:

  * •

$Act\times React$ is the alphabet;

  * •

$2^{\mathcal{F}}\cup\\{s^{ag}_{err}\cup s^{env}_{err}\\}$ is the state space,
where $s^{ag}_{err}$ is the agent error state, and $s^{env}_{err}$ is the
environment error state;

  * •

$s_{0}\in 2^{\mathcal{F}}$ is the initial state;

  * •

$\delta^{\prime}:(2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\})\times
Act\times React\rightarrow
2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\}$ is such that if
$s\in\\{s^{ag}_{err},s^{env}_{err}\\}$ then $\delta^{\prime}(s,a,r)=s$,
otherwise

$\delta^{\prime}(s,a,r)=\begin{cases}\delta(s,a,r)&\text{ if
}a\in\alpha(s)\text{ and }r\in\beta(s,a)\\\ s^{ag}_{err}&\text{ if
}a\not\in\alpha(s)\\\ s^{env}_{err}&\text{ if }a\in\alpha(s)\text{ and
}r\notin\beta(s,a).\end{cases}$

Intuitively, the transitions of $\mathcal{D}_{+}$ are the same as in
$\mathcal{D}$, except that the transitions move to $s^{ag}_{err}$ and
$s^{env}_{err}$ when agent action or environment reaction preconditions are
violated, respectively. Once an error state is reached, $\mathcal{D}_{+}$ just
keeps looping there.

We now construct the game arena, on which the agent and the environment
control actions and reactions, respectively, through an ad-hoc composition of
$\mathcal{D}_{+}$ and (the transition system of) the DFA of the agent goal
$\varphi$. Given an ltlf formula $\varphi$ over $\mathcal{F}$, we first obtain
its corresponding DFA
$\mathcal{A}_{\varphi}=(\mathcal{T}_{\varphi},\mathtt{Reach}(R_{\varphi}))$,
where $\mathcal{T}_{\varphi}=(2^{\mathcal{F}},Q,q_{0},\varrho)$ is the
transition system and $R_{\varphi}\subseteq Q$ is the set of final states.
Note that the transitions of $\mathcal{A}_{\varphi}$ are defined wrt fluents
$\mathcal{F}$, i.e., the transition function of $\mathcal{T}_{\varphi}$ is in
the form of $\varrho:Q\times 2^{\mathcal{F}}\rightarrow Q$. But the
transitions of $\mathcal{D}_{+}$ are defined wrt agent actions and environment
reactions. Hence, the composition of $\mathcal{D}_{+}$ and
$\mathcal{T}_{\varphi}$ needs to suitably synchronize the transitions of both.
To that end, we map the fluent evaluations in the states of $\mathcal{D}_{+}$
to the transition conditions that follow the transition function $\varrho$.

Formally, the composition
$\mathcal{T}=\mathcal{D}_{+}\circ\mathcal{T}_{\varphi}$ is such that
$\mathcal{T}=(Act\times
React,(2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\})\times
Q,(s_{0},\varrho(q_{0},s_{0})),\partial)$, where:

  * •

$Act\times React$ is the alphabet;

  * •

$(2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\})\times Q$ is the set of
states;

  * •

$(s_{0},\varrho(q_{0},s_{0}))$ is the initial state;

  * •

$\partial:((2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\})\times
Q)\times Act\times
React\rightarrow((2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\})\times
Q)$ is the transition function such that:

$\partial((s,q),a,r)=\begin{cases}(s^{\prime},\varrho(q,s^{\prime}))&\text{if
}s^{\prime}\not\in\\{s^{ag}_{err},s^{env}_{err}\\}\\\
(s^{ag}_{err},q)&\text{if }s^{\prime}=s^{ag}_{err}\\\
(s^{env}_{err},q)&\text{if }s^{\prime}=s^{env}_{err}\end{cases}$

where $s^{\prime}=\delta^{\prime}(s,a,r)$.

Intuitively, $\mathcal{T}$ is a deterministic transition system that
simultaneously retains the state of the domain $\mathcal{D}$ and the progress
in the DFA $\mathcal{A}_{\varphi}$ in satisfying the ltlf goal $\varphi$. In
particular, note that the function $\partial$ is defined such that if the
$\mathcal{T}$ reaches an environment/agent error state, $\mathcal{T}$ cannot
reach any other state afterwards. In fact, a positional strategy $\kappa$ on
$\mathcal{T}=\mathcal{D}_{+}\circ\mathcal{T}_{\varphi}$ also induces a
strategy $\sigma^{\prime}:React^{*}\rightarrow Act$ in the planning domain
$\mathcal{D}$.

######  Definition 4.1.

Let $\kappa:Q\rightarrow Act$ be a positional strategy on
$\mathcal{T}=\mathcal{D}_{+}\circ\mathcal{T}_{\varphi}$. $\kappa$ induces an
agent strategy $\sigma^{\prime}:React^{*}\rightarrow Act$:
$\sigma^{\prime}(\vec{r}_{\epsilon})=\kappa(t_{0})$, where $t_{0}$ is the
initial state of $\mathcal{T}$; for every $i\geq 0$,
$\sigma^{\prime}(\vec{r}^{\ i})=\kappa(t)$, where $\vec{r}^{\ i}=r_{0}\ldots
r_{i}$ and $t$ is the last state in the finite sequence
$\rho^{i+1}={\sf{Run}{(}}\pi^{i},\mathcal{T})$ with
$\pi^{i}=(\sigma^{\prime}(\vec{r}_{\epsilon})\cup
r_{0})(\sigma^{\prime}(\vec{r}^{\ 0})\cup
r_{1})\ldots(\sigma^{\prime}(\vec{r}^{\ i-1})\cup r_{i})$.

Indeed, with $\sigma^{\prime}$ we can also obtain the equivalent strategy
$\sigma:(2^{\mathcal{F}})^{+}\rightarrow Act$ (c.f. Section 3.1) in
$\mathcal{D}$. Sometimes, for simplicity, we directly say that positional
strategy $\kappa$ induces strategy $\sigma:(2^{\mathcal{F}})^{+}\rightarrow
Act$ (rather than saying that $\kappa$ induces strategy
$\sigma^{\prime}:React^{*}\rightarrow Act$ which is equivalent to a strategy
$\sigma:(2^{\mathcal{F}})^{+}\rightarrow Act$).

Given a synthesis problem $\mathcal{P}=(\mathcal{D},\varphi)$, we now detail
how to compute a best-effort solution for $\varphi$ in $\mathcal{D}$ by
reducing to suitable DFA games on the game arena $\mathcal{T}=(Act\times
React,(2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\})\times
Q,(s_{0},\varrho(q_{0},s_{0})),\partial)$ constructed as above. In the
following, we denote by $R^{\prime}_{\varphi}$ the set of states in
$\mathcal{T}$ by lifting the final states $R_{\varphi}$ in
$\mathcal{T}_{\varphi}$ to $\mathcal{T}$. Hence,
$R^{\prime}_{\varphi}=\\{(s,q)\mid q\in R_{\varphi}\\}$. Moreover, we denote
by $S^{ag}_{err}$ and $S^{env}_{err}$ the sets of states by lifting the agent
error state and the environment error state in $\mathcal{D}_{+}$ to
$\mathcal{T}$, respectively. Therefore, $S^{ag}_{err}$ and $S^{env}_{err}$
indicate the agent and the environment violate their respective preconditions.
Hence $S^{ag}_{err}=\\{(s,q)\mid s=s^{ag}_{err}\\}$ and
$S^{env}_{err}=\\{(s,q)\mid s=s^{env}_{err}\\}$). Sometimes, we write $\neg
S^{ag}_{err}$ as an abbreviation for
$((2^{\mathcal{F}}\cup\\{s^{ag}_{err},s^{env}_{err}\\})\times Q)\setminus
S^{ag}_{err}$ to indicate that the agent has not yet violated its
precondition. Similarly for $\neg S^{env}_{err}$.

Algorithm 1. Given problem $\mathcal{P}=(\mathcal{D},\varphi)$ of ltlf best-
effort synthesis in nondeterministic planning domains, proceed as follows:

  1. 1.

Construct the DFA
$\mathcal{A}_{\varphi}=(\mathcal{T}_{\varphi},\mathtt{Reach}(R_{\varphi}))$ of
agent goal $\varphi$ and the transition system $\mathcal{D}_{+}$ of domain
$\mathcal{D}$.

  2. 2.

Construct arena $\mathcal{T}=(\mathcal{D}_{+}\circ\mathcal{T}_{\varphi})$ by
composition.

  3. 3.

In the DFA game $(\mathcal{T},\mathtt{Reach}(\lnot
S^{ag}_{err}\cap(S^{env}_{err}\cup R^{\prime}_{\varphi})))$, compute a
positional uniform winning strategy $\kappa_{adv}$. Let $W_{adv}$ be the
winning region.

  4. 4.

In the DFA game $(\mathcal{T},\mathtt{Reach}(\lnot S^{ag}_{err}\cap\lnot
S^{env}_{err}\cap R^{\prime}_{\varphi}))$, compute a positional uniform
cooperatively winning strategy $\kappa_{coop}$. Let $W_{coop}$ be the
cooperatively winning region.

  5. 5.

Construct positional strategy $\kappa$ from $\kappa_{adv}$ and $\kappa_{coop}$
as follows:

$\kappa(s,q)=\begin{cases}\kappa_{adv}(s,q)&\text{ if }(s,q)\in W_{adv}\\\
\kappa_{coop}(s,q)&\text{ if }(s,q)\in W_{coop}\backslash W_{adv}\\\ \text{any
}a\in\alpha(s)&\text{ otherwise}\end{cases}$

where $\alpha(s)=Act$, if $s\in\\{s^{ag}_{err},s^{env}_{err}\\}$, such that
the agent can perform any action at an error state.

  6. 6.

Return the (best-effort) solution $\sigma$ for $\varphi$ in $\mathcal{D}$
induced by $\kappa$.

Due to the requirement of _existence of agent action_ , at every state $s\in
2^{\mathcal{F}}$, there always exists an agent action $a\in\alpha(s)$
(possibly $nop$).

It is worth noting that Algorithm 1 also allows us to check whether the
computed best-effort solution is a strong solution as well. This is indicated
by the value of $val(\sigma,s_{0})$. More specifically, we have that the
computed solution $\sigma$ is a strong solution if $t_{0}\in W_{adv}$, where
$t_{0}$ is the initial state of
$\mathcal{T}=\mathcal{D}_{+}\circ\mathcal{T}_{\varphi}$.

######  Theorem 4.2 (Correctness).

Let $\mathcal{D}$ be a nondeterministic planning domain, $\varphi$ an ltlf
goal, and $\sigma$ the agent strategy returned by Algorithm 1. Then, $\sigma$
is a best-effort solution for $\varphi$ in $\mathcal{D}$.

To prove this theorem, we make use of several intermediate results, which are
given in the next section.

Figure 2: An execution example of a best-effort solution for the arch-building
task described in Section 1. Robot actions and human reactions are shown in
blue and red, respectively.

###  4.3 Correctness

In order to prove Theorem 4.2, we first show the connection between strong and
cooperative solutions for the agent goal in a planning domain to winning and
cooperatively winning strategies in the corresponding DFA games, respectively.

######  Theorem 4.3.

Let $\mathcal{D}$ be a planning domain, $\varphi$ an ltlf goal, and
$\mathcal{T}=\mathcal{D}_{+}\circ\mathcal{T}_{\varphi}$ the constructed game
arena. The following two hold:

  1. (_a_)

there is a strong solution for $\varphi$ in $\mathcal{D}$ iff the agent has a
winning strategy in $(\mathcal{T},\mathtt{SafeReach}(\lnot
S^{ag}_{err},\,S^{env}_{err}\cup R^{\prime}_{\varphi}))$.

  2. (_b_)

there is a cooperative solution for $\varphi$ in $\mathcal{D}$ iff the agent
has a cooperatively winning strategy in $(\mathcal{T},\mathtt{SafeReach}(\lnot
S^{ag}_{err}\cap\lnot S^{env}_{err},R^{\prime}_{\varphi}))$.

To prove Theorem 4.3, we first observe that a strong solution for $\varphi$ in
$\mathcal{D}$ guarantees that the agent always follows its action precondition
(i.e., never visits $S^{ag}_{err}$) and either forces the environment to
violate its reaction precondition or eventually satisfies $\varphi$ (i.e.,
eventually reaches $S^{env}_{err}\cup R^{\prime}_{\varphi}$ ). Hence, the
agent’s goal is to satisfy

$\Box(\lnot S^{ag}_{err})\land\Diamond(S^{env}_{err}\lor
R^{\prime}_{\varphi})$

(For simplicity, we abuse notations and consider sets of states as atomic
propositions). Therefore, the reduced game for computing a strong solution is
$(\mathcal{T},\mathtt{SafeReach}(\lnot S^{ag}_{err},\,S^{env}_{err}\cup
R^{\prime}_{\varphi}))$. Similarly for proving (_b_).

Next, we show that the safety-reachability games can be solved by reducing to
pure reachability games, the correctness of which can be shown by
construction.

######  Lemma 4.4.

Let $\mathcal{T}$, $S^{ag}_{err}$, $S^{env}_{err}$ and $R^{\prime}_{\varphi}$
be as defined above. Then, for every run $\rho$ on $\mathcal{T}$:

  * •

$\rho$ is an accepting run of $\mathtt{SafeReach}(\lnot
S^{ag}_{err},\,S^{env}_{err}\cup R^{\prime}_{\varphi})$ iff $\rho$ is an
accepting run of $\mathtt{Reach}(\lnot S^{ag}_{err}\cap(S^{env}_{err}\cup
R^{\prime}_{\varphi}))$.

  * •

$\rho$ is an accepting run of $\mathtt{SafeReach}(\lnot S^{ag}_{err}\cap\neg
S^{env}_{err},R^{\prime}_{\varphi})$ iff $\rho$ is an accepting run of
$\mathtt{Reach}(\lnot S^{ag}_{err}\cap S^{env}_{err}\cap
R^{\prime}_{\varphi})$.

By Theorem 4.3 and Lemma 4.4, the computed winning strategy $\kappa_{adv}$ for
$\mathtt{Reach}(\lnot S^{ag}_{err}\cap(S^{env}_{err}\cup
R^{\prime}_{\varphi}))$ and the cooperative winning strategy $\kappa_{coop}$
for $\mathtt{Reach}(\lnot S^{ag}_{err}\cap S^{env}_{err}\cap
R^{\prime}_{\varphi})$ indeed correspond to a strong solution and a
cooperative solution for $\varphi$ in $\mathcal{D}$, respectively.

We now show that the computed final strategy $\sigma$ by combing
$\kappa_{adv}$ and $\kappa_{coop}$ is a best-effort solution for $\varphi$ in
$\mathcal{D}$. We prove this through Theorem 3.6 by showing that $\sigma$
satisfies the Maximality Condition.

######  Theorem 4.5.

Let $\sigma$ be the strategy returned by Algorithm 1. For every
$h\in\mathcal{H}_{\mathcal{D}}(\sigma)$ it holds $val(\sigma,h)=val(h)$.

To prove Theorem 4.5, first observe that every sequence of states $\rho$ on
$\mathcal{T}$ that does not end at an environment/agent error state
corresponds to a legal history $h$ on $\mathcal{D}$. The strategy $\sigma$
returned by Algorithm 1 satisfies that, for every
$h\in\mathcal{H}_{\mathcal{D}}(\sigma)$, one of the following holds: (_i_) the
corresponding run $\rho$ on $\mathcal{T}$ ends at a state $s\in W_{adv}$ hence
$h$ can surely be extended to satisfy $\varphi$ in $\mathcal{D}$ using
$\sigma$ (i.e., from $h$ the agent has a strong solution); (_ii_) the
corresponding run $\rho$ on $\mathcal{T}$ ends at a state $s\in
W_{coop}\backslash W_{adv}$ hence $h$ can possibly be extended to satisfy
$\varphi$ in $\mathcal{D}$ using $\sigma$, should the environment cooperate
(i.e., from $h$ the agent has a cooperative solution); (_iii_) the
corresponding run $\rho$ on $\mathcal{T}$ ends at a state $s\notin
W_{coop}\cup W_{adv}$ hence $h$ cannot be extended to satisfy $\varphi$ in
$\mathcal{D}$ (i.e., from $h$ the agent has neither a strong nor a cooperative
solution). Moreover, $\sigma$ is guaranteed to be a legal strategy since the
agent can only perform legal actions.

Finally, we can prove Theorem 4.2 (the correctness of Algorithm 1 in Section
4.2) as an immediate result of Theorems 4.5 and 3.6.

###  4.4 Computational Complexity

The computational complexity of ltlf best-effort synthesis in nondeterministic
planning domains is the following:

######  Theorem 4.6.

ltlf best-effort synthesis in nondeterministic planning domains is:

  * •

2EXPTIME-complete in the size of the ltlf goal;

  * •

EXPTIME-complete in the size of the domain.

Regarding the complexity in the size of the ltlf goal, the hardness comes from
ltlf synthesis, and the membership comes from the ltlf-to-DFA construction
(double-exponential in the size of the ltlf formula). Hence, if we consider
simple reachability goals in the form of $\varphi=\Diamond(R)$, where $R$ is a
propositional formula over the fluents $\mathcal{F}$ of the planning domain,
the problem is just polynomial in the size of $\varphi=\Diamond(R)$ since the
DFA can be constructed in polynomial time. Regarding the complexity in the
size of the domain, the hardness comes from planning itself [18], and the
membership comes from the construction of the deterministic transition system
from the planning domain (single-exponential in the number of fluents).

An interesting observation from Theorem 4.6 is that best-effort synthesis
provides an efficient alternative approach to planning in nondeterministic
domains for both ltlf and reachability goals. In fact, instead of looking for
a strong solution, which may not exist, one can look for a best-effort
solution, which, on the one hand, always exists and on the other hand is
directly a strong solution if the problem admits one.

Running Example (cont.).  We present the computed best-effort solution
produced by our synthesis algorithm for the running example in Section 1. We
represent the arch-building task as a suitable ltlf formula and the dynamics
of the interactions between the robot and the human (seen as the agent and the
environment, respectively) as a nondeterministic planning domain. Figure 2
presents a (simplified) execution example of a best-effort solution to
building the arch. Note that at the initial state, all blocks are placed in
storage (state $0$). Then the robot successfully placed the block $o_{4}$ at
the location $l_{2}$ without any interference from the human (state $1$).
Next, the robot placed the block $o_{3}$ at $l_{1}$, and the human helped
build the arch by placing $o_{2}$ at $l_{4}$ (state $2$). Seeing the human
being cooperative, the robot decides to be lazy, hence not doing anything.
However, the human now punishes the robot for being lazy by undoing what the
robot has done, thus removing $o_{3}$ back to storage (state $3$). The robot
now realizes that the human is not always cooperative, so it proceeds by
placing $o_{3}$ back at $l_{1}$, and the human cooperates by placing $o_{1}$
at $l_{3}$ (state $4$). Finally, the robot can build the arch by placing
$o_{0}$ at the top, with no interference from the human (state $5$). This
example well illustrates the basic characteristic of best-effort solutions:
handling both adversarial and cooperative environment behaviors, even if the
environment switches back and forth between behaving adversarially and
cooperatively instead of always being adversarial or cooperative.

##  5 Implementation and Empirical Evaluation

We implemented our algorithm for ltlf best-effort synthesis in planning
domains in a tool called BeSyftP, leveraging the symbolic ltlf synthesis
framework [32] that is integrated in all state-of-the-art ltlf synthesis tools
[7, 15]. The explicit-state DFAs of ltlf formulas are constructed by lydia
[16], the overall best-performing tool for ltlf-to-DFA construction. BeSyftP
uses the _symbolic_ DFA encoding proposed in [32] to represent the DFAs
symbolically and integrates the symbolic encoding of a planning domain
(specified in a variant of PDDL) proposed in [26] for symbolic domain
representation. Both symbolic DFAs and planning domains are represented in
Binary Decision Diagrams (BDDs) [8], with the BDD library CUDD-3.0.0 [29].
Following [32], BeSyftP constructs and solves symbolic DFA games using Boolean
operations provided by CUDD, such as quantification, negation and conjunction.
In particular, positional strategies are obtained with Boolean synthesis [22].
Finally, best-effort strategies are computed by applying suitable Boolean
operations to the obtained positional winning strategy and cooperatively
winning strategy.

Experimental Comparison. To show the efficiency of our technique for ltlf
best-effort synthesis in nondeterministic planning domains, we want to compare
it with the approach of reducing to ltlf best-effort synthesis, by re-
expressing the domain as an ltlf formula. More specifically, we adapted the
domain-to-ltlf translation in [26] to obtain the ltlf formula $\mathcal{E}$ of
the nondeterministic planning domain. Next, we can utilize the ltlf best-
effort synthesis technique from [5] to solve the problem of $\varphi$ (agent
goal) under $\mathcal{E}$.

We also evaluated the performance of BeSyftP considering the overhead of
computing best-effort solutions wrt computing strong and cooperative
solutions. Therefore, we also implemented the adversarial and cooperative
synthesis approaches for computing strong and cooperative solutions in
_AdvSyftP_ and _CoopSyftP_ , respectively.

Benchmarks. For benchmarks, we consider nondeterministic planning domains as
the same one in the running example of building-an-arch described in Section
1. In order to have scalable benchmarks, we consider agent goals as putting
$O$ objects at $L$ locations in line, hence the difficulty of the benchmarks
increases as either $O$ or $L$ increases. Note that for all these benchmarks,
the agent does not have a strong solution to fulfill the goal, i.e., it needs
a best-effort solution. Our benchmarks consider at most 8 objects
($1\leq|O|\leq 8$) and 1000 locations ($1\leq|L|\leq 1000$).

Experiment Setup. All experiments were run on a laptop with an operating
system 64-bit Ubuntu 20.04, 3.6 GHz CPU, and 12 GB of memory. Time out was set
to 1200 seconds.

Figure 3: Comparison of BeSyftP and the algorithm from Aminof et al. [5] on
benchmarks with $|O|=1$ and $1\leq|L|\leq 10$ (in log scale). Figure 4:
Comparison of _BeSyftP_ , _AdvSyftP_ and _CoopSyftP_ on benchmarks with
$|L|=10$ and $1\leq|O|\leq 6$ (in log scale).

Experimental Results. As shown in Figure 3 (for better vision, we only plot
the results on instances with up to $10$ locations), utilizing the ltlf best-
effort synthesis approach from [5] can solve the instances with one object
($|O|=1$) up to $6$ locations ($|L|\leq 6$).555Notice that if we increase the
number of objects to $2$, the synthesis approach from [5] can still solve the
corresponding instances. But if we increase the number of objects to $3$, it
times out immediately. Instead, BeSyftP can solve all the instances with
$|O|=1$ up to $10$ locations and more (up to $1000$), showing much greater
scalability.666If we increase $|O|$ to $6$, our approach can only handle
instances with $|L|$ up to $10$. This is because $|L|$ only affects the size
of the planning domain, on which the synthesis complexity is EXPTIME. Instead,
$|O|$ also affects the ltlf goal, on which the complexity is 2EXPTIME.

Figure 4 shows the results of comparing the performance of computing best-
effort solutions (BeSyftP) with that of computing strong (_AdvSyftP_) and
cooperative (_CoopSyftP_) ones. Note that, since all benchmarks are
unrealizable, _AdvSyftP_ terminates earlier than both _CoopSyftP_ and BeSyftP
(with $20\%\sim 25\%$ less time cost). Interestingly, BeSyftP takes roughly
the same time as _CoopSyftP_ (with $10\%\sim 15\%$ more time cost). This shows
that, although computing a best-effort solution requires solving two games and
combining the computed adversarial and cooperative solutions, BeSyftP requires
only a small overhead with respect to both _AdvSyftP_ and _CoopSyftP_.

##  6 Conclusion

In this paper, we have developed a framework for ltlf best-effort synthesis in
nondeterministic (adversarial) planning domains, and a solution technique that
admits a scalable symbolic implementation. The approach presented here can be
extended to different forms of goal specification. In particular, we can
expect a further complexity reduction if we express goals in pure-past
temporal logics [14]. Also, the game-based techniques adopted here could
possibly be extended to handle best-effort synthesis under multiple
environment specifications [13, 1, 2]. Another promising extension is
considering maximally permissive strategies [30], which allows the agent to
choose a best-effort solution during execution instead of committing to a
single solution beforehand We leave this for future work.

## Acknowledgments

This work has been partially supported by the ERC-ADG White- Mech (No.
834228), the EU ICT-48 2020 project TAILOR (No. 952215), the PRIN project
RIPER (No. 20203FFYLK), and the PNRR MUR project FAIR (No. PE0000013). This
work has been carried out while Gianmarco Parretti was enrolled in the Italian
National Doctorate on Artificial Intelligence run by Sapienza University of
Rome.

## References

  * [1] Benjamin Aminof, Giuseppe De Giacomo, Alessio Lomuscio, Aniello Murano, and Sasha Rubin, ‘Synthesizing strategies under expected and exceptional environment behaviors’, in IJCAI, pp. 1674–1680, (2020).
  * [2] Benjamin Aminof, Giuseppe De Giacomo, Alessio Lomuscio, Aniello Murano, and Sasha Rubin, ‘Synthesizing best-effort strategies under multiple environment specifications’, in KR, pp. 42–51, (2021).
  * [3] Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, and Sasha Rubin, ‘Planning and synthesis under assumptions’, arXiv, (2018).
  * [4] Benjamin Aminof, Giuseppe De Giacomo, Aniello Murano, and Sasha Rubin, ‘Planning under LTL environment specifications’, in ICAPS, pp. 31–39, (2019).
  * [5] Benjamin Aminof, Giuseppe De Giacomo, and Sasha Rubin, ‘Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up’, in IJCAI, pp. 1766–1772, (2021).
  * [6] Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen, Principles of Model Checking, MIT Press, 2008.
  * [7] Suguman Bansal, Yong Li, Lucas M. Tabajara, and Moshe Y. Vardi, ‘Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications’, in AAAI, pp. 9766–9774, (2020).
  * [8] Randal E. Bryant, ‘Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams’, ACM Comput. Surv., 24(3), 293–318, (1992).
  * [9] Alberto Camacho, Meghyn Bienvenu, and Sheila A McIlraith, ‘Towards a unified view of ai planning and reactive synthesis’, in ICAPS, pp. 58–67, (2019).
  * [10] Alberto Camacho and Sheila A. McIlraith, ‘Strong fully observable non-deterministic planning with LTL and LTLf goals’, in IJCAI, pp. 5523–5531, (2019).
  * [11] Alessandro Cimatti, Marco Pistore, Marco Roveri, and Paolo Traverso, ‘Weak, strong, and strong cyclic planning via symbolic model checking.’, AIJ, 1–2(147), 35–84, (2003).
  * [12] Alessandro Cimatti, Marco Roveri, and Paolo Traverso, ‘Strong planning in non-deterministic domains via model checking’, in AIPS, pp. 36–43, (1998).
  * [13] Daniel Alfredo Ciolek, Nicolás D’Ippolito, Alberto Pozanco, and Sebastian Sardiña, ‘Multi-tier automated planning for adaptive behavior’, in ICAPS, pp. 66–74, (2020).
  * [14] Giuseppe De Giacomo, Antonio Di Stasio, Francesco Fuggitti, and Sasha Rubin, ‘Pure-past linear temporal and dynamic logic on finite traces’, in IJCAI, pp. 4959–4965, (2020).
  * [15] Giuseppe De Giacomo and Marco Favorito, ‘Compositional approach to translate LTLf/LDLf into deterministic finite automata’, in ICAPS, pp. 122–130, (2021).
  * [16] Giuseppe De Giacomo and Marco Favorito, ‘Lydia: A tool for compositional LTLf /LDLf synthesis’, in ICAPS, pp. 122–130, (2021).
  * [17] Giuseppe De Giacomo and Yves Lespérance, ‘The nondeterministic situation calculus’, in KR, pp. 216–226, (2021).
  * [18] Giuseppe De Giacomo and Sasha Rubin, ‘Automata-Theoretic Foundations of FOND Planning for LTLf and LDLf Goals.’, in IJCAI, pp. 4729–4735, (2018).
  * [19] Giuseppe De Giacomo and Moshe Y. Vardi, ‘Linear Temporal Logic and Linear Dynamic Logic on Finite Traces’, in IJCAI, pp. 854–860, (2013).
  * [20] Giuseppe De Giacomo and Moshe Y. Vardi, ‘Synthesis for LTL and LDL on Finite Traces’, in IJCAI, pp. 1558–1564, (2015).
  * [21] Bernd Finkbeiner, ‘Synthesis of Reactive Systems.’, Dependable Software Systems Eng., 45, 72–98, (2016).
  * [22] Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi, ‘BDD-based Boolean functional synthesis’, in CAV, pp. 402–421, (2016).
  * [23] H. Geffner and B. Bonet, A Concise Introduction to Models and Methods for Automated Planning, 2013.
  * [24] Malik Ghallab, Dana S. Nau, and Paolo Traverso, Automated planning - theory and practice, 2004.
  * [25] Patrik Haslum, Nir Lipovetzky, Daniele Magazzeni, and Christian Muise, An Introduction to the Planning Domain Definition Language, 2019.
  * [26] Keliang He, Andrew M Wells, Lydia E Kavraki, and Moshe Y Vardi, ‘Efficient Symbolic Reactive Synthesis for Finite-Horizon Tasks’, in ICRA, pp. 8993–8999, (2019).
  * [27] A. Pnueli and R. Rosner, ‘On the synthesis of a reactive module’, in POPL, p. 179–190, (1989).
  * [28] Amir Pnueli, ‘The temporal logic of programs’, in FOCS, pp. 46–57, (1977).
  * [29] Fabio Somenzi, ‘CUDD: CU Decision Diagram Package 3.0.0. Universiy of Colorado at Boulder’, (2016).
  * [30] Shufang Zhu and Giuseppe De Giacomo, ‘Synthesis of maximally permissive strategies for ltlf specifications’, in IJCAI, pp. 2783–2789. ijcai.org, (2022).
  * [31] Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi, ‘A symbolic approach to safety LTL synthesis’, in HVC, pp. 147–162, (2017).
  * [32] Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi, ‘Symbolic LTLf Synthesis’, in IJCAI, pp. 1362–1369, (2017).
  * [33] Martin Zimmermann, Felix Klein, and Alexander Weinert, ‘Infinite games’, in Lecture Notes (Chapters 1 and 2), (2016).