# GEARS: Local Geometry-aware Hand-object Interaction Synthesis

Keyang Zhou1,2 Bharat Lal Bhatnagar1,2 Jan Eric Lenssen2 Gerard Pons-Moll1,2
1University of Tübingen, Germany
2Max Planck Institute for Informatics, Saarland Informatics Campus, Germany

###### Abstract

Generating realistic hand motion sequences in interaction with objects has
gained increasing attention with the growing interest in digital humans. Prior
work has illustrated the effectiveness of employing occupancy-based or
distance-based virtual sensors to extract hand-object interaction features.
Nonetheless, these methods show limited generalizability across object
categories, shapes and sizes. We hypothesize that this is due to two reasons:
1) the limited expressiveness of employed virtual sensors, and 2) scarcity of
available training data. To tackle this challenge, we introduce a novel joint-
centered sensor designed to reason about local object geometry near potential
interaction regions. The sensor queries for object surface points in the
neighbourhood of each hand joint. As an important step towards mitigating the
learning complexity, we transform the points from global frame to hand
template frame and use a shared module to process sensor features of each
individual joint. This is followed by a spatio-temporal transformer network
aimed at capturing correlation among the joints in different dimensions.
Moreover, we devise simple heuristic rules to augment the limited training
sequences with vast static hand grasping samples. This leads to a broader
spectrum of grasping types observed during training, in turn enhancing our
model’s generalization capability. We evaluate on two public datasets, GRAB
and InterCap, where our method shows superiority over baselines both
quantitatively and perceptually.

Figure 1: An overview of our method. The input consists of the hand
trajectory, object trajectory and object template mesh. For each time frame,
the object mesh is cropped with a cube-shaped virtual sensor positioned and
oriented based on the wrist. The cropped object points together with the hand
trajectory are fed to the Joint Initialization Network to predict coarse
joints locations. We then place more fine-grained geometry sensors at each
joint to extract joint-local object features. The features are subsequently
processed by the Joint Displacement Network to refine the initialized joints.
Finally, we fit MANO hand model [27] to the joints to get the hand mesh
sequence.

##  1 Introduction

We humans mostly rely on hands to interact with different objects in the
surrounding environment. Learning the high-dimensional space of plausible
hand-object interactions is an important and challenging task that needs to be
solved in many applications. These include modeling digital humans in
Augmented and Virtual Reality, or reasoning about potential grasps in
robotics.

Real world objects can largely differ in size, topology and geometry. Learning
a model which can adapt to object surface is a particularly demanding task,
especially when existing dynamic hand-object interaction data is very scarce.
One crucial factor determining generalization capability lies in how the
object is encoded relative to the hand. Previous work [40, 32] proposed to use
occupancy-based or distance-based virtual sensors to represent local surface
geometry. However, these features have two limitations. First, they are
inherently constrained by their expressiveness. Occupancy-based sensor
attaches an occupancy grid to the hand. Occupancy grids with a low resolution
can only detect coarse object geometry. On the other hand, increasing the grid
resolution would result in an exponential increase in feature size. Distance-
based sensor measures the distance from a fixed set of basis points rigidly
attached to the hand to the closest points on the object surface. It gives
more fine-grained features and it is also less computationally expensive.
However, a discrete collection of hand-to-object distance cannot faithfully
describe local object geometry properties such as normal directions and
curvature. Moreover, features computed by both of the aforementioned sensors
are global with respect to the hand, which means it is difficult to model the
intricate correlation between the movement of each finger. As the result,
these methods exhibit limited generalization capabilities to unseen objects of
different sizes.

The ability of humans to perform dexterous object manipulations is attributed
to the dense tactile sensory receptors in the skin. Thus, we hypothesize that
the ability to reason about local geometry is key to generalization to
arbitrary surfaces. Inspired by this, we propose a novel hand-object
interaction sensor which is local to every hand joint. Specifically, we
establish a canonical frame at each joint, and use a shared module to process
local object points within a small radius of the joint. This way, the module
learns joint-agnostic local features, which are highly generalizable from
limited training data. We further fuse together features at each joint by
self-attention operations, enabling the model to learn the compositional
relationship between different joints in forming the hand pose.

Due to the limited availability of dynamic human-object interaction data, we
present a simple yet effective method for generating dynamic hand sequences
from static grasps. Static hand grasping data is easily accessible and
exhibits a diverse range of object geometry and grasping type. With our data
augmentation procedure, we can turn them into artifical grasping sequences. We
show that adding them to our training dataset can further improve the results.

Our contributions are as follows:

  * •

We propose a learning-based method to synthesize diverse hand motion sequences
interacting with objects. Though trained only on small hand-held objects, we
show that our model naturally generalizes to objects of larger sizes (see
Figure. LABEL:fig:teaser).

  * •

We introduce a novel hand-object interaction sensor, which detects local
object surface geometry relative to hand joints. This is proven essential to
our model’s generalization capabilities.

  * •

With a simple yet effective data augmentation trick, we are able to utilizing
the vast amount of existing static hand grasp data to train our model.

  * •

Our code and pre-trained model will be released to enhance further research in
this direction.

##  2 Related Work

Static Grasp Synthesis. Synthesizing stable hand grasps given target objects
has been extensively studied in computer graphics [18] and robotics [29, 28].
Conventional analytical approaches assume a simplified contact model and solve
a constrained optimization problem to satisfy the force-closure condition [26,
1, 46, 8]. In contrast, data-driven approaches generate grasp hypotheses from
human demonstrations or annotated 3D data, and rank them according to certain
quality metrics [2, 20]. Modern robotic grasping simulators usually combine
the merits of both [23, 19]. Recently, there has been an increasing interest
in training neural network-based models for hand grasp generation [12, 30, 7,
13, 49, 3, 17, 22]. For example, [16, 15] modeled the hand-object proximity as
an implicit function.

Dynamic Grasp Synthesis. In comparison with static grasp synthesis, generating
dynamic manipulation of objects is more challenging since it additionally
requires dynamic hand and object interaction to be modeled. This task is
usually approached by optimizing hand poses to satisfy a range of contact
force constraints [21, 39, 25, 44]. With the advent of deep reinforcement
learning, a number of work explored training hand grasping control policies in
physics simulation [6, 37, 41]. Hand motions generated by these works are
physically plausible but lack natural variations. Zheng  _et al_. [45] modeled
hand poses in a canonicalized object-centric space, achieving category-level
generalization for both rigid and articulated objects. More similar to our
work are ManipNet [40] and GRIP [32], which utilized occupancy-based and
distance-based sensors to extract local object features near the hand and then
directly regressed hand poses from the features. We argue that these features
are limited by resolution and they are global with respect to the hand, hence
hindering generalization capability. In contrast, we adopt a novel joint-
centered point-based sensor which captures local object geometry in finer
details while enabling modeling the correlation among hand joints.

Full-body Human-object Interaction Synthesis. Generating realistic human
motion sequences in 3D scenes has received considerable attention in recent
years [34, 11, 43, 35, 42, 14, 24]. However, these work usually models coarse
body motion only and ignore fine-grained finger articulations. Another line of
work focused on generating full-body motion for grasping [9]. A typical
solution to this problem is first generating the final static grasping pose
and then using a motion infilling network to generate the intermediate poses
[31, 36]. [33] and [47] leveraged the existing body pose prior and hand-only
grasping prior to circumvent the limited diversity in available full-body
grasping data. Braun  _et al_. [4] adopted a physics-based approach, training
separate low-level policies for the body and fingers, and then integrating
them with a high-level policy which operates in latent space.

Grasp Refinement. As consumer-level hand tracking devices including RGB/depth
cameras, data gloves and IMUs become more accessible, it is relatively easy to
acquire hands that are approximately correct but may contain noise and
artifacts. Refining hand poses in accordance with hand-object interaction
emerges as a practical research problem [30]. [38] and [10] proposed to
identify the potential contact area on the object surface and subsequently
adjust the hand to align with the predicted contact points. Limited by their
contact representations, they can only handle static hand grasp. Zhou  _et
al_. [48] improved upon them and extended the binary contact map
representation to a spatio-temporal correspondence map, enabling the
refinement of a hand motion sequence. We deviate from these work in our
assumptions, as we only require hand and object trajectories as input.

##  3 Method

Given the trajectories of a hand and an object in interaction, we aim to
generate hand poses that align with the object motion. The object shape is
assumed to be known. We tackle this problem in three steps. First, we estimate
a coarse initial hand pose for each frame individually. We place virtual
sensors on the initialized hand joints, detecting nearby object surface points
and extracting hand-object interaction features based on these points. Local
to each joint, the features are fed to a spatio-temporal attention network,
which learns the correlation among hand joints and generates displacements to
the initialized hand joints. Lastly, we solve an optimization problem and fit
a parametric hand model to the predicted joints. See Figure. 1 for an overview
of our method.

Specifically, our input consists of the hand trajectory
$\left\\{\boldsymbol{w}^{t},\boldsymbol{R}_{H}^{t}\right\\}_{t=1}^{T}$, the
object trajectory
$\left\\{\boldsymbol{o}^{t},\boldsymbol{R}_{O}^{t}\right\\}_{t=1}^{T}$ and the
object template mesh
$\boldsymbol{M}_{O}=\left\\{\boldsymbol{V}_{O},\boldsymbol{F}_{O}\right\\}$,
with $\boldsymbol{w}^{t},\boldsymbol{o}^{t}\in\mathbb{R}^{3}$ denoting hand
and object translations and
$\boldsymbol{R}_{H}^{t},\boldsymbol{R}_{O}^{t}\in\text{SO}^{3}$ denoting hand
and object global orientations respectively. We use the MANO model [27] as our
hand representation, which is parameterized by shape $\boldsymbol{\beta}$ and
pose $\boldsymbol{\theta}$. Hence the hand trajectory is composed of the wrist
joint coordinates and the global orientation of the target MANO hand at each
frame.

###  3.1 Joint Initialization Network

Given the object position and orientation at frame $t$, we first obtain the
object mesh at that frame by
$\boldsymbol{V}_{O}^{t}=\boldsymbol{R}_{O}^{t}\boldsymbol{V}_{O}+\boldsymbol{o}^{t}$.
In order to predict an initial hand pose, only the part of the object which is
close to the wrist matters. Hence we crop the object by a cube-shaped virtual
sensor $\boldsymbol{S}^{t}$ rigidly attached to the wrist. The resulting
partial object mesh is denoted by
${\boldsymbol{M}_{O}^{t}}^{\prime}=\left\\{{\boldsymbol{V}_{O}^{t}}^{\prime},{\boldsymbol{F}_{O}^{t}}^{\prime}\right\\}$,
where
${\boldsymbol{V}_{O}^{t}}^{\prime}=\\{\boldsymbol{v}_{i}\in\boldsymbol{V}_{O}^{t}:\boldsymbol{v}_{i}\notin\boldsymbol{S}^{t}\\}$
and ${\boldsymbol{F}_{O}^{t}}^{\prime}\subseteq\boldsymbol{F}_{O}^{t}$.

Let $\boldsymbol{P}^{t}\in\mathbb{R}^{N\times 3}$ denote the point cloud
sampled on ${\boldsymbol{M}_{O}^{t}}^{\prime}$. We subsequently express the
point cloud relative to the wrist:

$\displaystyle\tilde{\boldsymbol{P}}^{t}={\boldsymbol{R}_{H}^{t}}^{T}\left(\boldsymbol{P}^{t}-\boldsymbol{w}^{t}\right).$
(1)

We additionally sample the hand trajectory centered on the current frame. We
sample $k$ frames both in the past and in the future, and express them
relative to the wrist in a similar fashion as 1. The inputs to the hand pose
initialization module are
$\left[\tilde{\boldsymbol{w}}^{t-k:t+k},\tilde{\boldsymbol{R}}_{H}^{t-k:t+k},\tilde{\boldsymbol{P}}^{t}\right]$,
where $\tilde{\boldsymbol{w}}^{t-k:t+k}$ and
$\tilde{\boldsymbol{R}}_{H}^{t-k:t+k}$ are canonicalized sampled wrist
positions and orientations respectively. In particular, we first use PointNet
to extract a global feature vector from the partial point cloud
$\boldsymbol{P}$. This feature vector is then concatenated with the trajectory
and fed to a three-layer fully-connected network. The output of the network is
denoted by $\boldsymbol{j}_{\text{init}}^{t}$, which represents the
initialized coordinates relative to the wrist. The training loss for this
module is defined by

$\displaystyle
L_{\text{init}}=\left\|\boldsymbol{j}_{\text{init}}-\boldsymbol{j}_{\text{gt}}\right\|_{2}^{2},$
(2)

where $\boldsymbol{j}_{\text{gt}}$ denotes groundtruth joint coordinates.

###  3.2 Local Geometry Sensor

Figure 2: Visualization of our joint-local geometry sensor. (Left) Given the
joints positions and the object mesh, we sample points on the object surface
within a specified radius centered at each joint. The object points are
represented in a joint-local frame. (Right) We transform the sampled object
points from global frame to the canonical frame defined by the MANO template
hand.

Although coarse and inaccurate, the initialized joints offer an indication of
where the hand could potentially interact with the object. To refine the
initial joint positions, we need to sense local geometry properties of the
object near the interaction regions.

We introduce a novel joint-centered point-based local geometry sensor to
overcome these limitations. Specifically, given the predicted joints
$\\{\boldsymbol{j}_{i}\\}_{i=1}^{J}$, we can utilize inverse kinematics to
analytically derive the joint rotations which satisfy:

$\displaystyle\boldsymbol{j}_{k}-\boldsymbol{j}_{\text{pa}(k)}=\boldsymbol{R}_{k,\text{pa}(k)}\left(\bar{\boldsymbol{j}}_{k}-\bar{\boldsymbol{j}}_{\text{pa}(k)}\right),$
(3)

where $\boldsymbol{R}_{k,\text{pa}(k)}$ is the relative angle between the
$k$-th joint and its parent, and $\\{\bar{\boldsymbol{j}}_{k}\\}$ are joints
in the rest pose. In this manner, we can define the template frame of the
$k$-th joint by

$\displaystyle\mathcal{T}_{k}=\prod_{i\in\text{A}\left(k\right)}{\begin{array}[]{c|c}\boldsymbol{R}_{i,\text{pa}(i)}&\boldsymbol{j}_{i}\\\
\hline\cr\boldsymbol{1}&\boldsymbol{0}\end{array}},$ (6)

where $\text{A}(k)$ denotes the list of ancestors of joint $k$ and
$\mathcal{T}_{k}$ is the transformation which brings joint $k$ from the
template frame to the global frame.

By sampling object surface points within a given radius $r$ of the $k$-th
joint along with their normal vectors, we get
$\boldsymbol{F}_{k}=\\{\boldsymbol{P}_{k},\boldsymbol{N}_{k}\\}$, where
$\boldsymbol{P}_{k}=\\{\boldsymbol{v}_{i}\in\boldsymbol{V}:\left\|\boldsymbol{v}_{i}-\boldsymbol{j}_{k}\right\|_{2}^{2}<r\\}$.
We then transform the sampled points to the template frame, by

$\displaystyle\bar{\boldsymbol{F}}_{k}$
$\displaystyle=\\{\bar{\boldsymbol{P}}_{k},\bar{\boldsymbol{N}}_{k}\\}$ (7)
$\displaystyle=\\{\mathcal{T}_{k}^{-1}(\boldsymbol{P}_{k}-\boldsymbol{j}_{k}),\mathcal{T}_{k}^{-1}\boldsymbol{N}_{k}\\}.$
(8)

Since we now have the sampled object points in a joint-centered canonical
frame, we apply a learnable module $f_{\text{feat}}$ to process the
transformed points. Note that this module is shared between joints, which
greatly reduces the learning complexity. We hence arrive at a hand-object
interaction feature
$\boldsymbol{f}_{k}=f_{\text{feat}}(\bar{\boldsymbol{F}}_{k})$ for each joint
$k$. We implement $f_{\text{feat}}$ with a three-layer PointNet architecture.

###  3.3 Joint Displacement Network

With the local object features aggregated at each joint, we propose to use a
transformer architecture to predict displacement vectors to the initialized
joints. Achieving a visually plausible and smooth hand sequence requires
modeling spatio-temporal inter-joint dependencies. Hence we apply the self-
attention operation in both spatial and temporal dimensions. Concretely, we
first project the initialized joint coordinates to per-joint embedding vectors
with a fully-connected network $g_{\text{embed}}$:

$\displaystyle\boldsymbol{e}_{k}=g_{\text{embed}}(\mathcal{T}_{k}^{-1}\boldsymbol{j}_{k}),$
(9)

where $k$ is the joint index. We concatenate the joint-local sensor features
with the joint embeddings and obtain
$\boldsymbol{X}=\text{concat}(\boldsymbol{f},\boldsymbol{e})$, which is the
input feature tensor for our transformer. Note that $X$ contains features for
all the joints in all time frames. We divide $\boldsymbol{X}$ along its
spatial and temporal dimension, and apply a self-attention function to them
separately.

Spatial self-attention. The spatial self-attention module divides
$\boldsymbol{X}$ into batches of frames, and each batch contains joint
features in a single frame, denoted by $\boldsymbol{X}_{S}$. This module takes
the hands in different frames as static identities, and focuses on learning
the correlations between different fingers. Following conventional self-
attention operations, we linearly project $\boldsymbol{X}_{S}$ to queries
$\boldsymbol{Q}_{S}$, keys $\boldsymbol{K}_{S}$ and values
$\boldsymbol{V}_{S}$. The output feature is hence obtained by

$\displaystyle\tilde{\boldsymbol{X}}_{S}$
$\displaystyle=\text{sa}(\boldsymbol{Q}_{S},\boldsymbol{K}_{S},\boldsymbol{V}_{S})$
(10)
$\displaystyle=\text{softmax}\left(\frac{\boldsymbol{Q}_{S}\boldsymbol{K}_{S}^{T}}{\sqrt{l}}\right)\boldsymbol{V}_{S},$
(11)

where $l$ is the length of key, query and value vectors. See Fig. 3 (Left) for
an illustration.

Temporal self-attention. On the other hand, the temporal self-attention module
divides $\boldsymbol{X}$ into batches of joints, and each batch contains
features of a specific joint across the whole sequence, denoted by
$\boldsymbol{X}_{T}$. This module models the trajectory of each individual
joint, ensuring that all joints move in a temporally smooth and consistent
manner. We similarly project $\boldsymbol{X}_{T}$ to queries
$\boldsymbol{K}_{T}$, keys $\boldsymbol{Q}_{T}$ and values
$\boldsymbol{V}_{T}$ respectively. The module output is

$\displaystyle\tilde{\boldsymbol{X}}_{T}$
$\displaystyle=\text{sa}(\boldsymbol{Q}_{T},\boldsymbol{K}_{T},\boldsymbol{V}_{T}).$
(12)

See Fig. 3 (Right) for an illustration.

The Joint Displacement Network consists of interleaving spatial and temporal
self-attention modules. The output of the last module is fed to a linear layer
to produce the joint displacement vectors $\bar{\boldsymbol{d}}$ in template
frame. As the last step, we utilize the pose transformation derived from IK
previously to transform $\bar{\boldsymbol{d}}$ back to global frame:

$\displaystyle\boldsymbol{d}_{k}=\left(\prod_{i\in
A(k)}{\boldsymbol{R}_{i,\text{pa}(i)}}\right)\bar{\boldsymbol{d}_{k}}.$ (13)

The training loss for this module is defined by

$\displaystyle
L_{\text{disp}}=\left\|\boldsymbol{j}_{\text{disp}}+\boldsymbol{d}-\boldsymbol{j}_{\text{gt}}\right\|_{2}^{2}.$
(14)

###  3.4 Hand Fitting

With the predicted sequence of hand joints $\boldsymbol{j}$, we need to
recover the hand meshes. This is done by minimizing

$\displaystyle\mathcal{L}(\boldsymbol{\beta},\boldsymbol{\theta})=\left\|\mathcal{J}\left(H\left(\boldsymbol{\beta},\boldsymbol{\theta}\right)\right)-\boldsymbol{j}\right\|_{2}^{2}+\mathcal{L}_{\text{reg}}(\boldsymbol{\beta},\boldsymbol{\theta})\textnormal{,}$
(15)

where $\mathcal{J}$ is the function which takes hand vertices as input and
outputs joint coordinates. The second term of (15) regularizes the shape and
pose parameters of MANO,

$\mathcal{L}_{\text{reg}}(\boldsymbol{\beta},\boldsymbol{\theta})=w_{1}\left\|\boldsymbol{\beta}\right\|^{2}+w_{2}\sum_{t=1}^{T}{\left\|\boldsymbol{\theta}^{t}\right\|^{2}}\\\
+w_{3}\sum_{t=1}^{T-1}{\left\|\boldsymbol{\theta}^{t+1}-\boldsymbol{\theta}^{t}\right\|^{2}}+w_{4}\sum_{t=2}^{T-1}{\sum_{i=1}^{J}{\left\|\ddot{\boldsymbol{j}}_{i}^{t}\right\|}},$
(16)

where we enforce temporal smoothness by regularizing both the first and the
second time derivatives of the joints.

###  3.5 Data Synthesis

Accurately capturing hand motion sequences, especially in presence of
interacting objects, is a particularly challenging task. Sophisticated
solutions usually involve expensive marker-based MoCap systems. As a result,
there are only few dynamic hand-object interaction datasets available for use.
Nevertheless, capturing the hand in a static pose while grasping an object is
relatively straightforward. We can have a much larger training set if we are
able to utilizing the widely available static hand grasping datasets. In the
following, we introduce a simple yet efficient way to synthesize hand
sequences from static poses.

Given mesh of a static hand grasping an object, we first fit MANO model to the
hand to get the target joint rotations $\boldsymbol{P}^{T}$, global
orientation $\mathbf{R}^{T}$ and translation $\boldsymbol{d}^{T}$, where $T$
is the desired sequence length. We then generate a source hand as the first
frame of the sequence, where the pose is generated by adding a small random
Gaussian noise to the mean MANO pose. Similarly, we perturb $\mathbf{R}^{T}$
with Gaussian noise to get the global orientation of the initial hand. Next,
we compute the average distance moved by the hand per frame from GRAB. The
initial translation is determined by moving along the negative normal
direction of the target hand palm by this distance.

To obtain hand meshes in intermediate time steps, we apply linear
interpolation to hand translation and spherical linear interpolation to joint
rotations:

$\displaystyle\boldsymbol{d}^{t}$
$\displaystyle=(1-t)\boldsymbol{d}^{0}+t\boldsymbol{d}^{T}$ (17)
$\displaystyle\boldsymbol{P}^{t}$
$\displaystyle=\text{SLERP}(\boldsymbol{P}^{0},\boldsymbol{P}^{T},t)$ (18)
$\displaystyle\boldsymbol{R}^{t}$
$\displaystyle=\text{SLERP}(\boldsymbol{R}^{0},\boldsymbol{R}^{T},t).$ (19)

Generating sequences in this way could result in hand-object intersections.
Rather than relying on path planning algorithms to prevent collisions, we
simply compute the highest intersection volume of a sequence and eliminate
sequences with intersection volume surpassing a predefined threshold. See
Figure. 4 for a sample sequence.

###  3.6 Implementation Details

For Joint Initialization Network, the side length of the cube sensor is 18cm.
We sample 2000 points on the partial object mesh as input to PointNet. We
uniformly sample 10 frames in the past and in the future within a 1 second
time window to compute the trajectory feature. When querying for joint-local
object points, we use the sphere sensor with a radius of 2.5cm. A maximum of
300 points are sampled in the neighbourhood of each joint.

Figure 3: An illustration of spatial and temporal attention networks. We first
process the features of each joint by PointNet. For spatial attention, every
joint attends to every other joint of the same hand. While for temporal
attention, a joint in one frame attends to the same joint in every other
frame. Figure 4: A sample training sequence synthesized by our heuristic rule.
At the rightmost side of the time axis is a static grasping pose from ObMan
[12]. We synthesize intermediate poses by interpolating joint angles from the
mean MANO pose.

##  4 Experiments

| MPJPE (mm) $\downarrow$ | PD (mm) $\downarrow$ | IV ($\text{cm}^{3}$) $\downarrow$ | C-IoU (%) $\uparrow$
---|---|---|---|---
TOCH | 8.18 | 5.37 | 2.72 | 20.1
ManipNet | 9.32 | 5.66 | 3.21 | 18.3
GRIP | 7.71 | 4.80 | 2.51 | 19.9
GEARS (ours) | 7.24 | 4.36 | 2.24 | 22.7
Table 1: We quantitatively compare GEARS to other baselines on the GRAB dataset. Each model is trained with the same amount data, including the synthetic sequences generated from ObMan. | PD (mm) $\downarrow$ | IV ($\text{cm}^{3}$) $\downarrow$
---|---|---
ManipNet | 8.22 | 6.15
GRIP | 7.92 | 5.68
GEARS (ours) | 7.44 | 5.21
Table 2: Quantitative comparison on InterCap. We evaluate on a selected subset of objects where hand interaction is involved. | MPJPE (mm) $\downarrow$ | C-IoU (%) $\uparrow$
---|---|---
$r=0$ | 9.34 | 14.8
$r=0.02$ | 7.28 | 22.1
$r=0.03$ | 7.24 | 21.9
w/o displacement | 9.63 | 13.2
w/o attention | 7.85 | 18.4
w/o synthetic | 7.31 | 20.6
Ours (iterative) | 7.37 | 19.2
Ours (full) | 7.24 | 22.7
Table 3: Ablaion studies evaluated on GRAB. The variable $r$ refers to the
radius of joint-local sensor in millimeters.

###  4.1 Datasets

GRAB. We train GEARS on GRAB [30], a large-scale MoCap dataset for whole-body
grasping. GRAB contains interaction sequences with $51$ objects. Following the
official protocol, we select $10$ objects for validation and testing, and
train with the rest. Due to symmetry of the two hands, we flip left hands to
increase the amount of training data. We further augment the training set by
transferring grasps to objects of varying sizes, following [48].

InterCap. InterCap is a dataset of whole-body human-scene interaction captured
by multiview RGB-D cameras. It features frame-wise pseudo-groundtruth
annotations for body, hand and 6D object poses, which are reconstructed by
jointly reasoning about human and object contact areas. As we solely focus on
hand-object interaction, we consider a subset of objects where the hand is in
interaction.

ObMan. ObMan [12] is a static hand grasping dataset. It consists of object
models taken from Shapenet [5] and synthetic hand grasps generated by the
robotic grasping software GraspIt [23]. Since it only has static hand poses,
we cannot directly train on it. Instead, we apply the data synthesis technique
and generate 200 sequences for training and testing. Each sequence has a fixed
length of 60 frames.

###  4.2 Metrics

Mean Per-Joint Position Error (MPJPE). We report the average Euclidean
distance between predicted and groundtruth 3D hand joints.

Penetration Depth (PD). Penetration depth is the minimum distance required for
moving a mesh to make it no longer in intersection with another mesh. We
approximate it by finding the maximum vertex-to-object distance for all the
penetrating hand vertices.

Intersection Volume (IV). We measure hand-object inter-penetration by
voxelizing hand and object meshes and reporting the volume of voxels occupied
by both. However, interpreting this metric in isolation could be misleading,
since it does not account for non-effective grasping artifacts.

Contact IoU (C-IoU). This metric evaluates the Intersection-over-Union between
the groundtruth binary hand-object contact map and the contact map of
predicted hands. The contact map is defined on the object surface. It takes a
value of 1 if a hand vertex is within $\pm 2\mathrm{mm}$ of an object vertex
and 0 otherwise.

###  4.3 Baselines

TOCH [48] is an object-centric model designed for refining noisy hand-object
interaction sequences. We tailor it to our task by feeding it with the
groundtruth hand trajectory and replacing the noisy hands in the training set
with flat hands.

ManipNet [40] relies on both occupancy-based and distance-based sensors to
generate dexterous hand motions. Since the original work assumed a different
hand model, we adapt it to MANO to compare on a fair ground.

GRIP [32] takes body arm trajectory as input to generate hand poses. It
employs a standalone module to denoise the arm trajectory and obtain hand
trajectory. For fair comparison, we directly provide GRIP with input hand
trajectories.

###  4.4 Quantitative and Qualitative Evaluation

To verify that our GEARS generates realistic interaction sequences, we first
evaluate our method on GRAB and compare with the aforementioned baselines. The
results are reported in Table. 1. GEARS outperforms other baselines on all
four metrics, which clearly demonstrates the advantage of our method. We can
observe that although both ManipNet and GRIP rely on distance-based sensors,
GRIP achieves better performance both in terms of joint accuracy and inter-
penetration score. We hypothesize that it could attribute to the two-stage
approach followed by GRIP. Similar to us, GRIP generates a coarse hand first
and subsequently refined it. Moreover, TOCH incurs a higher MPJPE but also
achieves higher contact IoU than GRIP. This observation shows that a higher
joint error doesn’t necessarily indicate worse grasping quality. TOCH
leverages an object-centric interaction representation, which naturally
encourages hand-object contact. See Figure. 5 (top row) for qualitative
results on GRAB.

GRAB contains mostly small-to-medium sized household objects. To assess our
model’s generalization capability to larger objects, we evaluate on the
InterCap dataset. We exclude TOCH from this comparison because the object-
centric contact map used by TOCH is highly sensitive to object size. Since the
groundtruth hand pose annotations of InterCap are not accurate enough, we only
report penetration depth and intersection volume, see Table. 2. Compared to
GRIP and ManipNet, GEARS incurs less penetration with the objects. Note that
all three methods report higher numbers than on GRAB. It can be partially
explained by the fact that the input hand trajectory provided by InterCap may
exhibit a certain degree of noise. See Figure. 5 (bottom rows) for a
qualitative comparison on InterCap.

Figure 5: Qualitative results on GRAB (top row) and InterCap (bottom two
rows). GEARS makes effective contact with the objects while avoiding hand-
object inter-penetration.

###  4.5 Ablation Studies

We ablate different components of GEARS and report the change in performance
on GRAB to further justify our proposed method, see Table 3. We first evaluate
how sensitive is the model to different sensor radius. Zero radius means that
sensor features are neglected by the network. We can observe that as long as
the radius is set within a reasonable range, it doesn’t have a significant
impact on performance.

Moreover, we train three baseline models, for which i) the Joint Displacement
Network is removed; ii) spatio-temporal attention is replaced by fully-
connected layers; iii) additional synthetic training sequences are not used.
It’s clear that the Joint Displacement Network plays the most important role
in our architecture. This agrees with our intuition that local object geometry
features are essential to fine-grained placement of joints.

Lastly, we design an iterative baseline, where at inference time the output of
the Joint Displacement Network is fed back to itself as input. We expect that
one more round of pose refining would further improve the generation quality.
Surprisingly, the iterative refining approach doesn’t bring any benefit. We
hypothesize that the underlying reason could be distributional shift of test
data, since the Joint Displacement Network has only seen the output of Joint
Initialization Network during training.

##  5 Conclusion

We present GEARS, a learning-based method for generating hand interaction
sequences given hand and object trajectories. The main insight which makes
GEARS effective is the novel joint-centered point-based sensor which captures
local geometry properties of the target object. Furthermore, we design a
spatio-temporal self-attention architecture to process joint-local features
and learn the correlation among hand joints during interaction. GEARS is
capable of generalizing across objects of varying sizes and categories. We
show that GEARS outperforms previous methods in terms of generation quality
and generalizability.

Acknowledgements This work is supported by the German Federal Ministry of
Education and Research (BMBF): Tübingen AI Center, FKZ: 01IS18039A. This work
is funded by the Deutsche Forschungsgemeinschaft (DFG, German Research
Foundation) - 409792180 (Emmy Noether Programme, project: Real Virtual
Humans). Gerard Pons-Moll is a member of the Machine Learning Cluster of
Excellence, EXC number 2064/1 – Project number 390727645. The project was made
possible by funding from the Carl Zeiss Foundation.

## References

  * Bicchi [1995] Antonio Bicchi.  On the closure properties of robotic grasping.  _The International Journal of Robotics Research_ , 14(4):319–334, 1995.
  * Bohg et al. [2013] Jeannette Bohg, Antonio Morales, Tamim Asfour, and Danica Kragic.  Data-driven grasp synthesis—a survey.  _IEEE Transactions on Robotics_ , 30(2):289–309, 2013.
  * Brahmbhatt et al. [2020] Samarth Brahmbhatt, Chengcheng Tang, Christopher D Twigg, Charles C Kemp, and James Hays.  Contactpose: A dataset of grasps with object contact and hand pose.  In _Computer Vision–ECCV 2020: 16th European Conference, Glasgow, UK, August 23–28, 2020, Proceedings, Part XIII 16_ , pages 361–378. Springer, 2020.
  * Braun et al. [2024] Jona Braun, Sammy Christen, Muhammed Kocabas, Emre Aksan, and Otmar Hilliges.  Physically plausible full-body hand-object interaction synthesis.  In _International Conference on 3D Vision (3DV)_ , 2024.
  * Chang et al. [2015] Angel X Chang, Thomas Funkhouser, Leonidas Guibas, Pat Hanrahan, Qixing Huang, Zimo Li, Silvio Savarese, Manolis Savva, Shuran Song, Hao Su, et al.  Shapenet: An information-rich 3d model repository.  _arXiv preprint arXiv:1512.03012_ , 2015.
  * Christen et al. [2022] Sammy Christen, Muhammed Kocabas, Emre Aksan, Jemin Hwangbo, Jie Song, and Otmar Hilliges.  D-grasp: Physically plausible dynamic grasp synthesis for hand-object interactions.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR)_ , 2022.
  * Corona et al. [2020] Enric Corona, Albert Pumarola, Guillem Alenya, Francesc Moreno-Noguer, and Grégory Rogez.  Ganhand: Predicting human grasp affordances in multi-object scenes.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 5031–5041, 2020.
  * El-Khoury et al. [2011] S El-Khoury, A Sahbani, and P Bidaud.  3d objects grasps synthesis: A survey.  In _13th World Congress in Mechanism and Machine Science_ , pages 573–583, 2011.
  * Ghosh et al. [2023] Anindita Ghosh, Rishabh Dabral, Vladislav Golyanik, Christian Theobalt, and Philipp Slusallek.  Imos: Intent-driven full-body motion synthesis for human-object interactions.  In _Computer Graphics Forum_ , pages 1–12. Wiley Online Library, 2023.
  * Grady et al. [2021] Patrick Grady, Chengcheng Tang, Christopher D Twigg, Minh Vo, Samarth Brahmbhatt, and Charles C Kemp.  Contactopt: Optimizing contact to improve grasps.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 1471–1481, 2021.
  * Hassan et al. [2021] Mohamed Hassan, Duygu Ceylan, Ruben Villegas, Jun Saito, Jimei Yang, Yi Zhou, and Michael J Black.  Stochastic scene-aware motion prediction.  In _Proceedings of the IEEE/CVF International Conference on Computer Vision_ , pages 11374–11384, 2021.
  * Hasson et al. [2019] Yana Hasson, Gül Varol, Dimitrios Tzionas, Igor Kalevatykh, Michael J. Black, Ivan Laptev, and Cordelia Schmid.  Learning joint reconstruction of hands and manipulated objects.  In _CVPR_ , 2019.
  * Jiang et al. [2021a] Hanwen Jiang, Shaowei Liu, Jiashun Wang, and Xiaolong Wang.  Hand-object contact consistency reasoning for human grasps generation.  _arXiv preprint arXiv:2104.03304_ , 2021a.
  * Jiang et al. [2023] Nan Jiang, Tengyu Liu, Zhexuan Cao, Jieming Cui, Zhiyuan Zhang, Yixin Chen, He Wang, Yixin Zhu, and Siyuan Huang.  Full-body articulated human-object interaction.  In _Proceedings of the IEEE/CVF International Conference on Computer Vision_ , pages 9365–9376, 2023.
  * Jiang et al. [2021b] Zhenyu Jiang, Yifeng Zhu, Maxwell Svetlik, Kuan Fang, and Yuke Zhu.  Synergies between affordance and geometry: 6-dof grasp detection via implicit representations.  _Robotics: science and systems_ , 2021b.
  * Karunratanakul et al. [2020] Korrawe Karunratanakul, Jinlong Yang, Yan Zhang, Michael J Black, Krikamol Muandet, and Siyu Tang.  Grasping field: Learning implicit representations for human grasps.  In _2020 International Conference on 3D Vision (3DV)_ , pages 333–344. IEEE, 2020.
  * Karunratanakul et al. [2021] Korrawe Karunratanakul, Adrian Spurr, Zicong Fan, Otmar Hilliges, and Siyu Tang.  A skeleton-driven neural occupancy representation for articulated hands.  In _2021 International Conference on 3D Vision (3DV)_ , pages 11–21. IEEE, 2021.
  * Kry and Pai [2006] Paul G Kry and Dinesh K Pai.  Interaction capture and synthesis.  _ACM Transactions on Graphics (TOG)_ , 25(3):872–880, 2006.
  * León et al. [2010] Beatriz León, Stefan Ulbrich, Rosen Diankov, Gustavo Puche, Markus Przybylski, Antonio Morales, Tamim Asfour, Sami Moisio, Jeannette Bohg, James Kuffner, et al.  Opengrasp: a toolkit for robot grasping simulation.  In _International Conference on Simulation, Modeling, and Programming for Autonomous Robots_ , pages 109–120. Springer, 2010.
  * Li et al. [2007] Ying Li, Jiaxin L Fu, and Nancy S Pollard.  Data-driven grasp synthesis using shape matching and task-based pruning.  _IEEE Transactions on visualization and computer graphics_ , 13(4):732–747, 2007.
  * Liu [2009] C Karen Liu.  Dextrous manipulation from a grasping pose.  In _ACM SIGGRAPH 2009 papers_ , pages 1–6. 2009.
  * Liu et al. [2023] Shaowei Liu, Yang Zhou, Jimei Yang, Saurabh Gupta, and Shenlong Wang.  Contactgen: Generative contact modeling for grasp generation.  In _Proceedings of the IEEE/CVF International Conference on Computer Vision_ , 2023.
  * Miller and Allen [2004] Andrew T Miller and Peter K Allen.  Graspit! a versatile simulator for robotic grasping.  _IEEE Robotics & Automation Magazine_, 11(4):110–122, 2004.
  * Mir et al. [2024] Aymen Mir, Xavier Puig, Angjoo Kanazawa, and Gerard Pons-Moll.  Generating continual human motion in diverse 3d scenes.  In _International Conference on 3D Vision (3DV)_ , 2024.
  * Mordatch et al. [2012] Igor Mordatch, Zoran Popović, and Emanuel Todorov.  Contact-invariant optimization for hand manipulation.  In _Proceedings of the ACM SIGGRAPH/Eurographics symposium on computer animation_ , pages 137–144, 2012.
  * Nguyen [1988] Van-Duc Nguyen.  Constructing force-closure grasps.  _The International Journal of Robotics Research_ , 7(3):3–16, 1988.
  * Romero et al. [2017] Javier Romero, Dimitrios Tzionas, and Michael J. Black.  Embodied hands: Modeling and capturing hands and bodies together.  _ACM Transactions on Graphics, (Proc. SIGGRAPH Asia)_ , 36(6), 2017.
  * Sahbani et al. [2012] Anis Sahbani, Sahar El-Khoury, and Philippe Bidaud.  An overview of 3d object grasp synthesis algorithms.  _Robotics and Autonomous Systems_ , 60(3):326–336, 2012.
  * Shimoga [1996] Karun B Shimoga.  Robot grasp synthesis algorithms: A survey.  _The International Journal of Robotics Research_ , 15(3):230–266, 1996.
  * Taheri et al. [2020] Omid Taheri, Nima Ghorbani, Michael J Black, and Dimitrios Tzionas.  Grab: A dataset of whole-body human grasping of objects.  In _European Conference on Computer Vision_ , pages 581–600. Springer, 2020.
  * Taheri et al. [2022] Omid Taheri, Vasileios Choutas, Michael J. Black, and Dimitrios Tzionas.  GOAL: Generating 4D whole-body motion for hand-object grasping.  In _Conference on Computer Vision and Pattern Recognition (CVPR)_ , 2022.
  * Taheri et al. [2024] Omid Taheri, Yi Zhou, Dimitrios Tzionas, Yang Zhou, Duygu Ceylan, Soren Pirk, and Michael J Black.  Grip: Generating interaction poses using latent consistency and spatial cues.  2024\.
  * Tendulkar et al. [2023] Purva Tendulkar, Dídac Surís, and Carl Vondrick.  Flex: Full-body grasping without full-body grasps.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 21179–21189, 2023.
  * Wang et al. [2021] Jiashun Wang, Huazhe Xu, Jingwei Xu, Sifei Liu, and Xiaolong Wang.  Synthesizing long-term 3d human motion and interaction in 3d scenes.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 9401–9411, 2021.
  * Wang et al. [2022] Jingbo Wang, Yu Rong, Jingyuan Liu, Sijie Yan, Dahua Lin, and Bo Dai.  Towards diverse and natural scene-aware 3d human motion synthesis.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 20460–20469, 2022.
  * Wu et al. [2022] Yan Wu, Jiahao Wang, Yan Zhang, Siwei Zhang, Otmar Hilliges, Fisher Yu, and Siyu Tang.  Saga: Stochastic whole-body grasping with contact.  In _Proceedings of the European Conference on Computer Vision (ECCV)_ , 2022.
  * Xu et al. [2023] Yinzhen Xu, Weikang Wan, Jialiang Zhang, Haoran Liu, Zikang Shan, Hao Shen, Ruicheng Wang, Haoran Geng, Yijia Weng, Jiayi Chen, et al.  Unidexgrasp: Universal robotic dexterous grasping via learning diverse proposal generation and goal-conditioned policy.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition_ , pages 4737–4746, 2023.
  * Yang et al. [2021] Lixin Yang, Xinyu Zhan, Kailin Li, Wenqiang Xu, Jiefeng Li, and Cewu Lu.  Cpf: Learning a contact potential field to model the hand-object interaction.  In _Proceedings of the IEEE/CVF International Conference on Computer Vision_ , pages 11097–11106, 2021.
  * Ye and Liu [2012] Yuting Ye and C Karen Liu.  Synthesis of detailed hand manipulations using contact sampling.  _ACM Transactions on Graphics (TOG)_ , 31(4):1–10, 2012.
  * Zhang et al. [2021] He Zhang, Yuting Ye, Takaaki Shiratori, and Taku Komura.  Manipnet: neural manipulation synthesis with a hand-object spatial representation.  _ACM Transactions on Graphics (TOG)_ , 40(4):1–14, 2021.
  * Zhang et al. [2024] Hui Zhang, Sammy Christen, Zicong Fan, Luocheng Zheng, Jemin Hwangbo, Jie Song, and Otmar Hilliges.  ArtiGrasp: Physically plausible synthesis of bi-manual dexterous grasping and articulation.  In _International Conference on 3D Vision (3DV)_ , 2024.
  * Zhang et al. [2022] Xiaohan Zhang, Bharat Lal Bhatnagar, Sebastian Starke, Vladimir Guzov, and Gerard Pons-Moll.  Couch: Towards controllable human-chair interactions.  In _European Conference on Computer Vision_ , pages 518–535. Springer, 2022.
  * Zhao et al. [2022] Kaifeng Zhao, Shaofei Wang, Yan Zhang, Thabo Beeler, and Siyu Tang.  Compositional human-scene interaction synthesis with semantic control.  In _European Conference on Computer Vision_ , pages 311–327. Springer, 2022.
  * Zhao et al. [2013] Wenping Zhao, Jianjie Zhang, Jianyuan Min, and Jinxiang Chai.  Robust realtime physics-based motion control for human grasping.  _ACM Transactions on Graphics (TOG)_ , 32(6):1–12, 2013.
  * Zheng et al. [2023a] Juntian Zheng, Qingyuan Zheng, Lixing Fang, Yun Liu, and Li Yi.  Cams: Canonicalized manipulation spaces for category-level functional hand-object manipulation synthesis.  In _Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR)_ , pages 585–594, 2023a.
  * Zheng and Qian [2005] Yu Zheng and Wen-Han Qian.  Coping with the grasping uncertainties in force-closure analysis.  _The international journal of robotics research_ , 24(4):311–327, 2005.
  * Zheng et al. [2023b] Yanzhao Zheng, Yunzhou Shi, Yuhao Cui, Zhongzhou Zhao, Zhiling Luo, and Wei Zhou.  Coop: Decoupling and coupling of whole-body grasping pose generation.  In _Proceedings of the IEEE/CVF International Conference on Computer Vision (ICCV)_ , pages 2163–2173, 2023b.
  * Zhou et al. [2022] Keyang Zhou, Bharat Lal Bhatnagar, Jan Eric Lenssen, and Gerard Pons-Moll.  Toch: Spatio-temporal object-to-hand correspondence for motion refinement.  In _European Conference on Computer Vision (ECCV)_. Springer, 2022.
  * Zhu et al. [2021] Tianqiang Zhu, Rina Wu, Xiangbo Lin, and Yi Sun.  Toward human-like grasp: Dexterous grasping via semantic representation of object-hand.  In _Proceedings of the IEEE/CVF International Conference on Computer Vision_ , pages 15741–15751, 2021.


Now, we prove a bound for the difference between $X$ and $v'$ using the above characterizations.
Observe that the above equation systems only differ structurally by the error term $\kappa(s)$.
Let thus $f(s) = \ExpectedSumStrat{\strategy}{X}(s) - v'(s)$.
This $f$ is a fixed point of the following equation system:

\begin{align*}
f(\targetstate) & = f(\sinkstate) = 0 \\
f(s) & = \kappa(s) + {\sum}_{a \in \mathcal{K}(s)} \strategy(s, a) \cdot \ExpectedSumMDP{\mdptransitions}{s}{a}{f}
\end{align*}

Clearly, $f$ again is unique by <ref>.

Given a state $s$, the probability to reach the terminal states $\targetstate$ and $\sinkstate$ in $\cardinality{S}$ steps following strategy $\strategy$ is bounded from below by $\delta_{\min}(\strategy)^{\cardinality{\States}}$ due to <ref>.
Consequently, the probability of not reaching these states in $\cardinality{\States}$ steps is bounded from above by $1 - \delta_{\min}(\strategy)^{\cardinality{S}} < 1$.
Hence, we can bound the difference between $\ExpectedSumStrat{\strategy}{X}$ and $v'$ by

\begin{equation*}
\kappa(s) \cdot {\sum}_{n=0}^\infty \cardinality{S} \left( 1 - \delta_{\min}(\strategy)^{\cardinality{S}} \right)^n = \kappa(s) \cdot \cardinality{S} \delta_{\min}(\strategy)^{-\cardinality{S}}. \qed
\end{equation*}

§.§.§ Bounding Reachability on Similar MDP

In this lemma, we show that MDP which are sufficiently similar also have similar reachability values.

Let $\MDP = (\States, \Actions, \stateactions, \mdptransitions)$ be an MDP, $\targetset \subseteq \States$ a set of target states, $\mathcal{K} \subseteq \States \times \stateactions$ a set of state-action pairs, and $\MDP' = (\States', \Actions', \stateactions', \mdptransitions')$ an arbitrary MDP with $\mathcal{K} \subseteq \States' \times \stateactions'$ that coincides with $\MDP$ on $\mathcal{K}$ and $\targetset$, i.e. (i) $\stateactions(s) = \stateactions'(s)$ for all $s \in \mathcal{K}$, (ii) $\mdptransitions(s, a) = \mdptransitions'(s, a)$ for all $(s, a) \in \mathcal{K}$, and (iii) $\targetset \subseteq \States'$.
Moreover, let $\strategy$ be a strategy in $\MDP$, $s \in \States \intersection \States'$ an arbitrary state in both MDP, and $N \in \Naturals$ a natural number.

\begin{equation*}
\ProbabilityMDP<\MDP, s><\strategy>[\boundedreach<N> \targetset] \geq \ProbabilityMDP<\MDP', s><\strategy'>[\boundedreach<N> \targetset] - \ProbabilityMDP<\MDP, s><\strategy>[\boundedreach<N> \overline{\mathcal{K}}],
\end{equation*}

where $\strategy'$ is an arbitrary strategy equal to $\strategy$ on all finite paths over $\mathcal{K}$, i.e. $\strategy(\finitepath) = \strategy'(\finitepath)$ for all $\finitepath \in \mathcal{K}^\star \times \States \intersection \Finitepaths<\MDP>$.

For a finite path $\finitepath = s_1 a_1 \ldots a_{n-1} s_n \in \Finitepaths<\MDP>$, let $\ProbabilityMDP<\MDP, s><\strategy>[\finitepath]$ denote the probability of path $\finitepath$ occurring when following strategy $\strategy$ from state $s$.
Let $\mathcal{K}_N$ denote the (finite) set of all finite paths $\finitepath$ of length $N$ starting in $s$ such that all state-action pairs $(s_i, a_i)$ in $\finitepath$ are in $\mathcal{K}$.
Similarly, let $\lnot \mathcal{K}_N$ denote the set of all such paths containing at least one state-action pair not in $\mathcal{K}$.
Let $\mathcal{R}(\finitepath)$ be a function which returns $1$ if some target state of $\targetset$ is in path $\finitepath$ and $0$ otherwise.
Then, we have the following:

\begin{align}
& \ProbabilityMDP<\MDP', s><\strategy'>[\boundedreach<N> \targetset] - \ProbabilityMDP<\MDP, s><\strategy>[\boundedreach<N> \targetset] \label{eq:stm:dql_no_ec:similar_mdp_bound:first} \\
& \qquad = \begin{aligned}
\sum_{\mathclap{\finitepath \in \mathcal{K}_N}} \left( \ProbabilityMDP<\MDP', s><\strategy'>[\finitepath] \cdot \mathcal{R}(\finitepath) - \ProbabilityMDP<\MDP, s><\strategy>[\finitepath] \cdot \mathcal{R}(\finitepath) \right) + & \\
\qquad \sum_{\mathclap{\finitepath \in \lnot \mathcal{K}_N}} \left( \ProbabilityMDP<\MDP', s><\strategy'>[\finitepath] \cdot \mathcal{R}(\finitepath) - \ProbabilityMDP<\MDP, s><\strategy>[\finitepath] \cdot \mathcal{R}(\finitepath) \right) &
\end{aligned} \label{eq:stm:dql_no_ec:similar_mdp_bound:second} \\
& \qquad = \sum_{\finitepath \in \lnot \mathcal{K}_N} \left( \ProbabilityMDP<\MDP', s><\strategy'>[\finitepath] \cdot \mathcal{R}(\finitepath) - \ProbabilityMDP<\MDP, s><\strategy>[\finitepath] \cdot \mathcal{R}(\finitepath) \right) \label{eq:stm:dql_no_ec:similar_mdp_bound:third} \\
& \qquad \leq \sum_{\finitepath \in \lnot \mathcal{K}_N} \ProbabilityMDP<\MDP', s><\strategy'>[\finitepath] \cdot \mathcal{R}(\finitepath) \label{eq:stm:dql_no_ec:similar_mdp_bound:fourth} \\
& \qquad \leq \sum_{\finitepath \in \lnot \mathcal{K}_N} \ProbabilityMDP<\MDP', s><\strategy'>[\finitepath] \label{eq:stm:dql_no_ec:similar_mdp_bound:fifth} \\
& \qquad = \ProbabilityMDP<\MDP, s><\strategy>[\boundedreach<N> \overline{\mathcal{K}}] \label{eq:stm:dql_no_ec:similar_mdp_bound:sixth}
\end{align}

In Equation (<ref>), we simply split the set of all paths of length $N$ into $\mathcal{K}_N$ and $\lnot \mathcal{K}_N$.
For Equations (<ref>) and (<ref>), note that $\ProbabilityMDP<\MDP', s><\strategy'>$ and $\ProbabilityMDP<\MDP, s><\strategy>$ agree on $\mathcal{K}_N$ by choice of $\MDP'$ and $\strategy'$.

§.§.§ Repeating Events in Markov Processes

Finally, we prove a general statement of Markov processes.
The statement itself seems to be quite obvious, yet surprisingly tricky to prove.
In essence, we want to show the following.
Suppose that we are given a Markov process $X_t$ on some probability space $\Omega$ together with a sequence of events $A_t$.
Moreover, assume that for a significant set of atoms $\omega \in \Omega$ there is an infinite set of times $T$ such that the conditional probability of $A_t$ occurring is at least $\varepsilon > 0$, i.e. $\Probability[X_t \in A_t \mid X_{t-1}(\omega)] > \varepsilon$.
Then, the set of atoms for which infinitely many $A_t$ actually occur is also significant.
The subtle difficulty of this statement arises from the fact that (i) conditional probabilities are considered, and (ii) the set $T$ depends on the particular atom $\omega$.

Fix some probability space $(\Omega, \mathcal{F}, \Probability)$ and a measure space $(S, \mathcal{S})$.
Let $X_t : \Omega \to S$ be a Markov process on $\Omega$ and $A_t \in \mathcal{S}$ measurable events in $S$.
Assume that the set $\Omega' = \{\omega \in \Omega \mid \exists T.~\cardinality{T} = \infty \land \forall t \in T.~\Probability[X_t \in A_t \mid X_{t-1}](\omega) > \varepsilon\}$ has positive measure, i.e. $\Probability[\Omega'] > 0$, and that $\Omega'_t = \{\omega \in \Omega \mid \Probability[X_t \in A_t \mid X_{t-1}](\omega) > \varepsilon\}$ is measurable for all $t \in \Naturals$.
Then, $\Probability[\{\omega \in \Omega \mid \exists T.~\cardinality{T} = \infty \land \forall t \in T.~X_\algostep(\omega) \in A_t\}] = \Probability[\Omega']$.

r<> d()𝖳𝗋𝗒_#1#2(#2)
r<> d()𝖲𝗎𝖼𝖼_#1#2(#2)
r<> d()𝖳𝗋𝗂𝖾𝗌𝖩_#1#2(#2)
r<> r<> d()𝖳𝗋𝗒𝖩_#1,#2#3(#3)
r<> r<> r<>𝖳𝗋𝗒𝖠𝗍𝖳𝖩^#2_#1,#3
r<> r<>𝖳𝗋𝗂𝖾𝗌𝖩_#1,#2
r<> r<>𝖳𝗋𝗒𝖳𝗂𝗆𝖾𝗌𝖩_#1,#2

Let $\omega \in \Omega'$.
By assumption, for each such $\omega$, there exists an infinite set of time-points $\tries(\omega) = \{t_1, t_2, \cdots\}$ with $1 \leq t_1 < t_2 < \cdots$ where $\Probability[X_t \in A_t \mid X_{t-1}](\omega) > \varepsilon$.
We call such an event a try of $\omega$.
Denote $\ithtry<i>(\omega) = t_i$ or $\infty$ if no such $t_i$ exists, e.g. for $\omega \notin \Omega'$.
Informally, $\ithtry<i>$ is the time of the $i$-th try of some outcome $\omega$.
$\ithtry<i>$ is measurable by assumption, since its pre-images can be constructed using $\Omega'_t$.
Moreover, let $\successes(\omega) = \{s_1, s_2, \cdots\} \subseteq \tries(\omega)$ be the times where $X_{s_j}(\omega) \in A_{s_j}$, called $j$-th success(ful try).
Note that $\successes(\omega)$ possibly is finite or even empty for some outcomes $\omega$, even for $\omega \in \Omega'$, since infinitely many tries may fail.
Now, let $\jthsuccess<j>(\omega) = s_j \in \successes(\omega)$ the time of the $j$-th success or $\infty$ if no such $s_j$ exists, i.e. $j > \cardinality{\successes(\omega)}$.
$\jthsuccess<j>$ is measurable since $\ithtry<i>$, $X_t$ and $A_t$ are measurable.
To succinctly capture corner-cases, we further define $\jthsuccess<0> = 0$.
The successes $\successes(\omega)$ naturally partition the set $\tries(\omega)$ into $\triesafter<j>(\omega) = \{t \in \tries(\omega) \mid \jthsuccess<j>(\omega) < t \leq \jthsuccess<j+1>(\omega)\}$.

We use $\ithtryafter<i><j>(\omega)$ to refer to the $i$-th element of $\triesafter<j>(\omega)$, or $\infty$ if no such element exists.
$\ithtryafter<i><j>$ is measurable due to $\jthsuccess<j>$ being measurable.
Informally, $\ithtryafter<i><j>(\omega)$ denotes the time of the $i$-th try since the $j$-th success.

We show that after a sufficient number of tries, there is a success with high probability.
Repeating this argument inductively, we then show that there are infinitely many successes for almost all outcomes $\omega$ in $\Omega'$.

Let thus $\ithtryattafter<i><t><j>$ denote the set of runs which at time $t$ have succeeded $j$ times and since the $j$-th success experienced $i$-th tries, where this $i$-th try happens exactly at time $t$.

\begin{equation*}
\ithtryattafter<i><t><j> \coloneqq \{\omega \in \Omega' \mid \ithtryafter<i><j>(\omega) = t\}.
\end{equation*}

Note that this definition implicitly includes the condition $\jthsuccess<j>(\omega) \leq t < \jthsuccess<j+1>(\omega)$ by definition of $\ithtryafter<i><j>$.
Thus, $\ithtryattafter<i><t><j>$ are disjoint for fixed $i$ and $j$.

We furthermore define $\atleastitriesafter<i><j> = \Union_{t=1}^\infty \ithtryattafter<i><t><j> = \{\omega \in \Omega' \mid \ithtryafter<i><j>(\omega) < \infty\}$ as the set of outcomes which after their $j$-th success experienced at least $i - 1$[$\ithtryafter<i><j>(\omega) = t$ does not exclude that the try at time t is successful.] unsuccessful tries.
We have $\atleastitriesafter<i><j> = \atleastitriesafter<i+1><j> \union \atleastitriesafter<1><j+1>$, since the $i$-th try either fails and the $i+1$-th try is experienced later (since $\atleastitriesafter<i><j> \subseteq \Omega'$, implying infinitely many tries) or the try succeeds.
Observe that $\atleastitriesafter<i+1><j>$ and $\atleastitriesafter<1><j+1>$ are not disjoint, since, for example, the runs succeeding at the $i+1$-th try also are an element of $\atleastitriesafter<1><j+1>$.
On the contrary, we show that $\Probability[\atleastitriesafter<i><j> \setminus \atleastitriesafter<1><j+1>] = 0$, i.e. almost all runs in $\atleastitriesafter<i><j>$ will eventually succeed again.

To this end, we argue that for any fixed $j$ we have that $\lim_{i \to \infty} \Probability[\atleastitriesafter<i><j>] = 0$.
Fix some $j$ and $i$ with $\Probability[\atleastitriesafter<i><j>] > 0$ (otherwise there is nothing to prove, since $\atleastitriesafter<i><j>$ is monotonically decreasing in $i$).
Let $\ithtrytimesafter<i><j> = \{t \mid \Probability[\ithtryattafter<i><t><j>] > 0\}$ which is non-empty by the previous condition.
Clearly, $\Probability[\atleastitriesafter<i><j>] = \sum_{t=1}^\infty \Probability[\ithtryattafter<i><t><j>] = \sum_{t \in \ithtrytimesafter<i><j>} \Probability[\ithtryattafter<i><t><j>]$, as $\ithtryattafter<i><t><j>$ are disjoint.
Observe that $\ithtryattafter<i><t><j>$ is the intersection of several conditions on $X_{t'}$ for $t' < t$ and requiring that $\Probability[X_t \in A_t \mid X_{t-1}] > \varepsilon$.
Hence, by the Markov property

\begin{equation*}
\Probability[X_t \notin A_t \mid \ithtryattafter<i><t><j>] = 1 - \Probability[X_t \in A_t \mid \ithtryattafter<i><t><j>] = 1 - \Probability[X_t \in A_t \mid X_{t-1}] < 1 - \varepsilon.
\end{equation*}

Intuitively, this means that the probability of a try at time $t$ succeeding does not depend on the number of previous tries and successes.
Thus, for all $t \in \ithtrytimesafter<i><j>$, we have $\Probability[X_t \notin A_t \intersection \ithtryattafter<i><t><j>] < (1 - \varepsilon) \cdot \Probability[\ithtryattafter<i><t><j>]$.
Observe that $\Union_{t=1}^\infty (X_t \notin A_t \intersection \ithtryattafter<i><t><j>) = \atleastitriesafter<i+1><j>$ since the intersection implies that the $i$-th try at time $t$ was unsuccessful.

\begin{align*}
\Probability[\atleastitriesafter<i+1><j>] & = \Probability[{\Union}_{t=1}^\infty X_t \notin A_t \intersection \ithtryattafter<i><t><j>] = {\sum}_{t=1}^\infty \Probability[X_t \notin A_t \intersection \ithtryattafter<i><t><j>] \\
& = {\sum}_{t \in \ithtrytimesafter<i><j>} \Probability[X_t \notin A_t \intersection \ithtryattafter<i><t><j>] \\
& < {\sum}_{t=1}^\infty (1 - \varepsilon) \cdot \Probability[\ithtryattafter<i><t><j>] = (1 - \varepsilon) \cdot \Probability[{\Union}_{t=1}^\infty \ithtryattafter<i><t><j>] \\
& = (1 - \varepsilon) \cdot \Probability[\atleastitriesafter<i><j>].
\end{align*}

Consequently, $\lim_{i \to \infty} \Probability[\atleastitriesafter<i><j>] = 0$ for any fixed $j$.

As argued before, we have $\atleastitriesafter<i><j> = \atleastitriesafter<i+1><j> \union \atleastitriesafter<1><j+1>$.
Iterating this equation yields $\atleastitriesafter<i><j> = \atleastitriesafter<i+k><j> \union \atleastitriesafter<1><j+1>$ for any $k \geq 1$ and consequently $\atleastitriesafter<1><j> = \Intersection_{i=1}^\infty \atleastitriesafter<i><j> \union \atleastitriesafter<1><j+1>$.
Informally, this equation can be read as all outcomes which succeed at least $j$ times either try infinitely often or succeed at least $j+1$ times.
Let $\atleastitriesafter<\infty><j> = \Intersection_{i=1}^\infty \atleastitriesafter<i><j> = \{\omega \in \Omega' \mid \jthsuccess<j>(\omega) < \infty = \jthsuccess<j+1>(\omega)\}$.
Clearly, $\atleastitriesafter<\infty><j> \intersection \atleastitriesafter<1><j+1> = \emptyset$, thus we have $\Probability[\atleastitriesafter<1><j+1> \setminus \atleastitriesafter<1><j>] = \Probability[\atleastitriesafter<\infty><j>]$.
Additionally, we have $\Probability[\atleastitriesafter<\infty><j>] = \inf_{i \in \Naturals} \Probability[\atleastitriesafter<i><j>] = 0$ by the above reasoning.
Hence $\Probability[\atleastitriesafter<1><j+1> \setminus \atleastitriesafter<1><j>] = 0$.
This implies that almost all runs in $\Omega'$ succeed infinitely often, concluding the proof.

[1]
Agarwal, C., Guha, S., Kretínský, J., Muruganandham, P.: PAC
statistical model checking of mean payoff in discrete- and continuous-time
In: S. Shoham, Y. Vizel (eds.) Computer Aided Verification - 34th
International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022,
Proceedings, Part II, Lecture Notes in Computer Science, vol. 13372,
pp. 3–25. Springer (2022).

[2]
Aljazzar, H., Leue, S.: Generation of counterexamples for model checking of
markov decision processes.
In: QEST 2009, Sixth International Conference on the Quantitative
Evaluation of Systems, Budapest, Hungary, 13-16 September 2009, pp. 197–206.
IEEE Computer Society (2009).

[3]
Andriushchenko, R., Bork, A., Budde, C.E., Češka, M., Hahn, E.M.,
Hartmanns, A., Israelsen, B., Jansen, N., Jeppson, J., Junges, S., Köhl,
M.A., Könighofer, B., Křetínský, J., Meggendorfer, T., Parker, D.,
Pranger, S., Quatmann, T., Ruijters, E., Taylor, L., Volk, M., Weininger, M.,
Zhang, Z.: Tools at the frontiers of quantitative verification: QComp 2023
competition report.
TOOLympics  (to appear)

[4]
Angluin, D.: Learning with hints.
In: D. Haussler, L. Pitt (eds.) Proceedings of the First Annual
Workshop on Computational Learning Theory, COLT '88, Cambridge, MA, USA,
August 3-5, 1988., pp. 167–181. ACM/MIT (1988).

[5]
Ashok, P., Butkova, Y., Hermanns, H., Kretínský, J.:
Continuous-time markov decisions based on partial exploration.
In: S.K. Lahiri, C. Wang (eds.) Automated Technology for Verification
and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA,
USA, October 7-10, 2018, Proceedings, Lecture Notes in Computer
Science, vol. 11138, pp. 317–334. Springer (2018).

[6]
Ashok, P., Chatterjee, K., Daca, P., Kretínský, J., Meggendorfer,
T.: Value iteration for long-run average reward in markov decision processes.
In: R. Majumdar, V. Kuncak (eds.) Computer Aided Verification - 29th
International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017,
Proceedings, Part I, Lecture Notes in Computer Science, vol. 10426,
pp. 201–221. Springer (2017).

[7]
Ashok, P., Chatterjee, K., Kretínský, J., Weininger, M., Winkler,
T.: Approximating values of generalized-reachability stochastic games.
In: H. Hermanns, L. Zhang, N. Kobayashi, D. Miller (eds.) LICS '20:
35th Annual ACM/IEEE Symposium on Logic in Computer Science,
Saarbrücken, Germany, July 8-11, 2020, pp. 102–115. ACM (2020).

[8]
Ashok, P., Daca, P., Kretínský, J., Weininger, M.: Statistical
model checking: Black or white?
In: T. Margaria, B. Steffen (eds.) Leveraging Applications of Formal
Methods, Verification and Validation: Verification Principles - 9th
International Symposium on Leveraging Applications of Formal Methods, ISoLA
2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I,
Lecture Notes in Computer Science, vol. 12476, pp. 331–349. Springer

[9]
Ashok, P., Kretínský, J., Weininger, M.: PAC statistical model
checking for markov decision processes and stochastic games.
In: I. Dillig, S. Tasiran (eds.) Computer Aided Verification - 31st
International Conference, CAV 2019, New York City, NY, USA, July 15-18,
2019, Proceedings, Part I, Lecture Notes in Computer Science, vol.
11561, pp. 497–519. Springer (2019).

[10]
Azeem, M., Evangelidis, A., Kretínský, J., Slivinskiy, A.,
Weininger, M.: Optimistic and topological value iteration for simple
stochastic games.
In: A. Bouajjani, L. Holík, Z. Wu (eds.) Automated Technology
for Verification and Analysis - 20th International Symposium, ATVA 2022,
Virtual Event, October 25-28, 2022, Proceedings, Lecture Notes in
Computer Science, vol. 13505, pp. 285–302. Springer (2022).

[11]
Badings, T.S., Romao, L., Abate, A., Parker, D., Poonawala, H.A., Stoelinga,
M., Jansen, N.: Robust control for dynamical systems with non-gaussian noise
via formal abstractions.
J. Artif. Intell. Res. 76, 341–391 (2023)

[12]
Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A.,
Somenzi, F.: Algebraic decision diagrams and their applications.
Formal Methods in System Design 10(2/3), 171–206 (1997).

[13]
Baier, C., D'Argenio, P.R., Größer, M.: Partial order reduction for
probabilistic branching time.
Electron. Notes Theor. Comput. Sci. 153(2), 97–116 (2006).

[14]
Baier, C., Größer, M., Ciesinski, F.: Partial order reduction for
probabilistic systems.
In: 1st International Conference on Quantitative Evaluation of
Systems (QEST 2004), 27-30 September 2004, Enschede, The Netherlands, pp.
230–239. IEEE Computer Society (2004).

[15]
Baier, C., Katoen, J.: Principles of model checking.
MIT Press (2008)

[16]
Baier, C., Katoen, J., Hermanns, H.: Approximate symbolic model checking of
continuous-time markov chains.
In: J.C.M. Baeten, S. Mauw (eds.) CONCUR '99: Concurrency Theory,
10th International Conference, Eindhoven, The Netherlands, August 24-27,
1999, Proceedings, Lecture Notes in Computer Science, vol. 1664, pp.
146–161. Springer (1999).

[17]
Baier, C., Klein, J., Leuschner, L., Parker, D., Wunderlich, S.: Ensuring the
reliability of your model checker: Interval iteration for markov decision
In: R. Majumdar, V. Kuncak (eds.) Computer Aided Verification - 29th
International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017,
Proceedings, Part I, Lecture Notes in Computer Science, vol. 10426,
pp. 160–180. Springer (2017).

[18]
Barnat, J., Brim, L., Černá, I., Ceska, M., Tumova, J.:
Probdivine-mc: Multi-core LTL model checker for probabilistic systems.
In: Fifth International Conference on the Quantitative Evaluaiton of
Systems (QEST 2008), 14-17 September 2008, Saint-Malo, France, pp. 77–78.
IEEE Computer Society (2008).

[19]
Barto, A.G., Bradtke, S.J., Singh, S.P.: Learning to act using real-time
dynamic programming.
Artif. Intell. 72(1-2), 81–138 (1995).

[20]
Basset, N., Kwiatkowska, M.Z., Wiltsche, C.: Compositional controller synthesis
for stochastic games.
In: P. Baldan, D. Gorla (eds.) CONCUR 2014 - Concurrency Theory -
25th International Conference, CONCUR 2014, Rome, Italy, September 2-5,
2014. Proceedings, Lecture Notes in Computer Science, vol. 8704, pp.
173–187. Springer (2014).

[21]
Basset, N., Kwiatkowska, M.Z., Wiltsche, C.: Compositional strategy synthesis
for stochastic games with multiple objectives.
Inf. Comput. 261(Part), 536–587 (2018).

[22]
Bellman, R.: Dynamic programming.
Science 153(3731), 34–37 (1966)

[23]
Bertsekas, D.P.: Value and policy iterations in optimal control and adaptive
dynamic programming.
IEEE Trans. Neural Netw. Learning Syst. 28(3), 500–509

[24]
Billingsley, P.: Probability and measure.
John Wiley & Sons (2008)

[25]
Bogdoll, J., Fioriti, L.M.F., Hartmanns, A., Hermanns, H.: Partial order
methods for statistical model checking and simulation.
In: R. Bruni, J. Dingel (eds.) Formal Techniques for Distributed
Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011,
and 31st IFIP WG 6.1 International Conference, FORTE 2011, Reykjavik,
Iceland, June 6-9, 2011. Proceedings, Lecture Notes in Computer
Science, vol. 6722, pp. 59–74. Springer (2011).

[26]
Bogdoll, J., Hartmanns, A., Hermanns, H.: Simulation and statistical model
checking for modestly nondeterministic models.
In: J.B. Schmitt (ed.) Measurement, Modelling, and Evaluation of
Computing Systems and Dependability and Fault Tolerance - 16th International
GI/ITG Conference, MMB & DFT 2012, Kaiserslautern, Germany, March
19-21, 2012. Proceedings, Lecture Notes in Computer Science, vol.
7201, pp. 249–252. Springer (2012).

[27]
Bohlender, D., Bruintjes, H., Junges, S., Katelaan, J., Nguyen, V.Y., Noll, T.:
A review of statistical model checking pitfalls on real-time stochastic
In: T. Margaria, B. Steffen (eds.) Leveraging Applications of Formal
Methods, Verification and Validation. Specialized Techniques and Applications
- 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October
8-11, 2014, Proceedings, Part II, Lecture Notes in Computer Science,
vol. 8803, pp. 177–192. Springer (2014).

[28]
Bohy, A., Bruyère, V., Raskin, J.: Symblicit algorithms for optimal
strategy synthesis in monotonic markov decision processes.
In: K. Chatterjee, R. Ehlers, S. Jha (eds.) Proceedings 3rd Workshop
on Synthesis, SYNT 2014, Vienna, Austria, July 23-24, 2014, EPTCS,
vol. 157, pp. 51–67 (2014).

[29]
Bønneland, F.M., Jensen, P.G., Larsen, K.G., Muñiz, M., Srba, J.:
Partial order reduction for reachability games.
In: W. Fokkink, R. van Glabbeek (eds.) 30th International Conference
on Concurrency Theory, CONCUR 2019, August 27-30, 2019, Amsterdam, the
Netherlands, LIPIcs, vol. 140, pp. 23:1–23:15. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik (2019).

[30]
Boyer, B., Corre, K., Legay, A., Sedwards, S.: Plasma-lab: A flexible,
distributable statistical model checking library.
In: K.R. Joshi, M. Siegle, M. Stoelinga, P.R. D'Argenio (eds.)
Quantitative Evaluation of Systems - 10th International Conference, QEST
2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, Lecture
Notes in Computer Science, vol. 8054, pp. 160–164. Springer (2013).

[31]
Bozkurt, A.K., Wang, Y., Zavlanos, M.M., Pajic, M.: Control synthesis from
linear temporal logic specifications using model-free reinforcement learning.
CoRR abs/1909.07299 (2019).

[32]
Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V.,
Kretínský, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.:
Verification of markov decision processes using learning algorithms.
In: F. Cassez, J. Raskin (eds.) Automated Technology for Verification
and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW,
Australia, November 3-7, 2014, Proceedings, Lecture Notes in Computer
Science, vol. 8837, pp. 98–114. Springer (2014).

[33]
Brázdil, T., Kiefer, S., Kucera, A.: Efficient analysis of probabilistic
programs with an unbounded counter.
J. ACM 61(6), 41:1–41:35 (2014).

[34]
Bryant, R.E.: Graph-based algorithms for boolean function manipulation.
IEEE Trans. Computers 35(8), 677–691 (1986).

[35]
Budde, C.E., D'Argenio, P.R., Hartmanns, A.: Better automated importance
splitting for transient rare events.
In: K.G. Larsen, O. Sokolsky, J. Wang (eds.) Dependable Software
Engineering. Theories, Tools, and Applications - Third International
Symposium, SETTA 2017, Changsha, China, October 23-25, 2017, Proceedings,
Lecture Notes in Computer Science, vol. 10606, pp. 42–58. Springer

[36]
Budde, C.E., D'Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model
checker for nondeterminism and rare events.
In: D. Beyer, M. Huisman (eds.) Tools and Algorithms for the
Construction and Analysis of Systems - 24th International Conference, TACAS
2018, Held as Part of the European Joint Conferences on Theory and Practice
of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018,
Proceedings, Part II, Lecture Notes in Computer Science, vol. 10806,
pp. 340–358. Springer (2018).

[37]
Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.:
JANI: quantitative model and tool interaction.
In: A. Legay, T. Margaria (eds.) Tools and Algorithms for the
Construction and Analysis of Systems - 23rd International Conference, TACAS
2017, Held as Part of the European Joint Conferences on Theory and Practice
of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings,
Part II, Lecture Notes in Computer Science, vol. 10206, pp. 151–168

[38]
Budde, C.E., Hartmanns, A., Klauck, M., Kretínský, J., Parker, D.,
Quatmann, T., Turrini, A., Zhang, Z.: On correctness, precision, and
performance in quantitative verification - qcomp 2020 competition report.
In: T. Margaria, B. Steffen (eds.) Leveraging Applications of Formal
Methods, Verification and Validation: Tools and Trends - 9th International
Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes,
Greece, October 20-30, 2020, Proceedings, Part IV, Lecture Notes in
Computer Science, vol. 12479, pp. 216–241. Springer (2020).

[39]
Bulychev, P.E., David, A., Larsen, K.G., Mikucionis, M., Poulsen, D.B., Legay,
A., Wang, Z.: UPPAAL-SMC: statistical model checking for priced timed
In: H. Wiklicky, M. Massink (eds.) Proceedings 10th Workshop on
Quantitative Aspects of Programming Languages and Systems, QAPL 2012,
Tallinn, Estonia, 31 March and 1 April 2012., EPTCS, vol. 85, pp.
1–16 (2012).

[40]
Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski,
A.: Compositional design methodology with constraint markov chains.
In: QEST 2010, Seventh International Conference on the Quantitative
Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pp.
123–132. IEEE Computer Society (2010).

[41]
Chang, H.S., Hu, J., Fu, M.C., Marcus, S.I.: Simulation-based algorithms for
Markov decision processes.
Springer Science & Business Media (2013)

[42]
Chatterjee, K., Chmelik, M., Daca, P.: CEGAR for compositional analysis of
qualitative properties in markov decision processes.
Formal Methods Syst. Des. 47(2), 230–264 (2015).

[43]
Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal
end-component decomposition and related graph problems in probabilistic
In: D. Randall (ed.) Proceedings of the Twenty-Second Annual
ACM-SIAM Symposium on Discrete Algorithms, SODA 2011, San Francisco,
California, USA, January 23-25, 2011, pp. 1318–1336. SIAM (2011).

[44]
Chatterjee, K., Henzinger, M.: An O(n\({}^{\mbox{2}}\)) time
algorithm for alternating büchi games.
In: Y. Rabani (ed.) Proceedings of the Twenty-Third Annual ACM-SIAM
Symposium on Discrete Algorithms, SODA 2012, Kyoto, Japan, January 17-19,
2012, pp. 1386–1399. SIAM (2012).

[45]
Chatterjee, K., Henzinger, M.: Efficient and dynamic algorithms for alternating
büchi games and maximal end-component decomposition.
J. ACM 61(3), 15:1–15:40 (2014).

[46]
Chatterjee, K., Henzinger, T.A.: Value iteration.
In: O. Grumberg, H. Veith (eds.) 25 Years of Model Checking -
History, Achievements, Perspectives, Lecture Notes in Computer
Science, vol. 5000, pp. 107–138. Springer (2008).

[47]
Chatterjee, K., Meggendorfer, T., Saona, R., Svoboda, J.: Faster algorithm for
turn-based stochastic games with bounded treewidth.
In: N. Bansal, V. Nagarajan (eds.) Proceedings of the 2023 ACM-SIAM
Symposium on Discrete Algorithms, SODA 2023, Florence, Italy, January
22-25, 2023, pp. 4590–4605. SIAM (2023).

[48]
Ciesinski, F., Baier, C., Größer, M., Klein, J.: Reduction techniques
for model checking markov decision processes.
In: Fifth International Conference on the Quantitative Evaluaiton of
Systems (QEST 2008), 14-17 September 2008, Saint-Malo, France, pp. 45–54.
IEEE Computer Society (2008).

[49]
Courcoubetis, C., Yannakakis, M.: Markov decision processes and regular events.
In: M.S. Paterson (ed.) Automata, Languages and Programming, pp.
336–349. Springer Berlin Heidelberg, Berlin, Heidelberg (1990)

[50]
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification.
J. ACM 42(4), 857–907 (1995).

[51]
D'Argenio, P., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for
lightweight verification of markov decision processes.
Int. J. Softw. Tools Technol. Transf. 17(4), 469–484

[52]
D'Argenio, P.R., Hartmanns, A., Sedwards, S.: Lightweight statistical model
checking in nondeterministic continuous time.
In: T. Margaria, B. Steffen (eds.) Leveraging Applications of Formal
Methods, Verification and Validation. Verification - 8th International
Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings,
Part II, Lecture Notes in Computer Science, vol. 11245, pp.
336–353. Springer (2018).

[53]
D'Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and
refinement strategies for probabilistic analysis.
In: H. Hermanns, R. Segala (eds.) Process Algebra and Probabilistic
Methods, Performance Modeling and Verification, Second Joint International
Workshop PAPM-PROBMIV 2002, Copenhagen, Denmark, July 25-26, 2002,
Proceedings, Lecture Notes in Computer Science, vol. 2399, pp. 57–76.
Springer (2002).

[54]
David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal
In: C. Baier, C. Tinelli (eds.) Tools and Algorithms for the
Construction and Analysis of Systems - 21st International Conference, TACAS
2015, Held as Part of the European Joint Conferences on Theory and Practice
of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings,
Lecture Notes in Computer Science, vol. 9035, pp. 206–211. Springer

[55]
David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., van Vliet,
J., Wang, Z.: Statistical model checking for networks of priced timed
In: U. Fahrenberg, S. Tripakis (eds.) Formal Modeling and Analysis of
Timed Systems - 9th International Conference, FORMATS 2011, Aalborg,
Denmark, September 21-23, 2011. Proceedings, Lecture Notes in Computer
Science, vol. 6919, pp. 80–96. Springer (2011).

[56]
David, A., Larsen, K.G., Legay, A., Mikucionis, M., Wang, Z.: Time for
statistical model checking of real-time systems.
In: G. Gopalakrishnan, S. Qadeer (eds.) Computer Aided Verification -
23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20,
2011. Proceedings, Lecture Notes in Computer Science, vol. 6806, pp.
349–355. Springer (2011).

[57]
De Alfaro, L.: Formal verification of probabilistic systems.
1601. Citeseer (1997)

[58]
Dehnert, C., Junges, S., Katoen, J., Volk, M.: A storm is coming: A modern
probabilistic model checker.
In: R. Majumdar, V. Kuncak (eds.) Computer Aided Verification - 29th
International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017,
Proceedings, Part II, Lecture Notes in Computer Science, vol. 10427,
pp. 592–600. Springer (2017).

[59]
Deng, Y., Hennessy, M.: Compositional reasoning for weighted markov decision
Sci. Comput. Program. 78(12), 2537–2579 (2013).

[60]
Díaz, Á.F., Baier, C., Earle, C.B., Fredlund, L.: Static partial
order reduction for probabilistic concurrent systems.
In: Ninth International Conference on Quantitative Evaluation of
Systems, QEST 2012, London, United Kingdom, September 17-20, 2012, pp.
104–113. IEEE Computer Society (2012).

[61]
Eisentraut, J., Kelmendi, E., Kretínský, J., Weininger, M.: Value
iteration for simple stochastic games: Stopping criterion and learning
Inf. Comput. 285(Part), 104886 (2022).

[62]
Fan, C., Huang, Z., Mitra, S.: Approximate partial order reduction.
In: K. Havelund, J. Peleska, B. Roscoe, E.P. de Vink (eds.) Formal
Methods - 22nd International Symposium, FM 2018, Held as Part of the
Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018,
Proceedings, Lecture Notes in Computer Science, vol. 10951, pp.
588–607. Springer (2018).

[63]
Filar, J., Vrieze, K.: Competitive markov decision processes  (1996)

[64]
Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D.: Automated verification
techniques for probabilistic systems.
In: M. Bernardo, V. Issarny (eds.) Formal Methods for Eternal
Networked Software Systems - 11th International School on Formal Methods for
the Design of Computer, Communication and Software Systems, SFM 2011,
Bertinoro, Italy, June 13-18, 2011. Advanced Lectures, Lecture Notes in
Computer Science, vol. 6659, pp. 53–113. Springer (2011).

[65]
Fu, J., Topcu, U.: Probably approximately correct MDP learning and control
with temporal logic constraints.
In: D. Fox, L.E. Kavraki, H. Kurniawati (eds.) Robotics: Science and
Systems X, University of California, Berkeley, USA, July 12-16, 2014 (2014).

[66]
Fujita, M., McGeer, P.C., Yang, J.C.: Multi-terminal binary decision diagrams:
An efficient data structure for matrix representation.
Formal Methods in System Design 10(2/3), 149–169 (1997).

[67]
Grover, K., Kretínský, J., Meggendorfer, T., Weininger, M.:
Anytime guarantees for reachability in uncountable markov decision processes.
In: B. Klin, S. Lasota, A. Muscholl (eds.) 33rd International
Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022,
Warsaw, Poland, LIPIcs, vol. 243, pp. 11:1–11:20. Schloss Dagstuhl -
Leibniz-Zentrum für Informatik (2022).

[68]
Haddad, S., Monmege, B.: Reachability in mdps: Refining convergence of value
In: J. Ouaknine, I. Potapov, J. Worrell (eds.) Reachability Problems
- 8th International Workshop, RP 2014, Oxford, UK, September 22-24, 2014.
Proceedings, Lecture Notes in Computer Science, vol. 8762, pp.
125–137. Springer (2014).

[69]
Haddad, S., Monmege, B.: Interval iteration algorithm for mdps and imdps.
Theor. Comput. Sci. 735, 111–131 (2018).

[70]
Hahn, E.M., Hartmanns, A., Hensel, C., Klauck, M., Klein, J.,
Kretínský, J., Parker, D., Quatmann, T., Ruijters, E.,
Steinmetz, M.: The 2019 comparison of tools for the analysis of quantitative
formal models - (qcomp 2019 competition report).
In: D. Beyer, M. Huisman, F. Kordon, B. Steffen (eds.) Tools and
Algorithms for the Construction and Analysis of Systems - 25 Years of
TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic,
April 6-11, 2019, Proceedings, Part III, Lecture Notes in Computer
Science, vol. 11429, pp. 69–92. Springer (2019).

[71]
Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: abstraction
refinement for infinite probabilistic models.
In: J. Esparza, R. Majumdar (eds.) Tools and Algorithms for the
Construction and Analysis of Systems, 16th International Conference, TACAS
2010, Held as Part of the Joint European Conferences on Theory and Practice
of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings,
Lecture Notes in Computer Science, vol. 6015, pp. 353–357. Springer

[72]
Hartmanns, A., Hermanns, H.: The modest toolset: An integrated environment for
quantitative modelling and verification.
In: E. Ábrahám, K. Havelund (eds.) Tools and Algorithms
for the Construction and Analysis of Systems - 20th International Conference,
TACAS 2014, Held as Part of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014.
Proceedings, Lecture Notes in Computer Science, vol. 8413, pp.
593–598. Springer (2014).

[73]
Hartmanns, A., Junges, S., Quatmann, T., Weininger, M.: A practitioner's guide
to MDP model checking algorithms.
In: S. Sankaranarayanan, N. Sharygina (eds.) Tools and Algorithms for
the Construction and Analysis of Systems - 29th International Conference,
TACAS 2023, Held as Part of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023,
Proceedings, Part I, Lecture Notes in Computer Science, vol. 13993,
pp. 469–488. Springer (2023).

[74]
Hartmanns, A., Kaminski, B.L.: Optimistic value iteration.
In: S.K. Lahiri, C. Wang (eds.) Computer Aided Verification - 32nd
International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020,
Proceedings, Part II, Lecture Notes in Computer Science, vol. 12225,
pp. 488–511. Springer (2020).

[75]
He, R., Jennings, P., Basu, S., Ghosh, A.P., Wu, H.: A bounded statistical
approach for model checking of unbounded until properties.
In: C. Pecheur, J. Andrews, E.D. Nitto (eds.) ASE 2010, 25th
IEEE/ACM International Conference on Automated Software Engineering,
Antwerp, Belgium, September 20-24, 2010, pp. 225–234. ACM (2010).

[76]
Henriques, D., Martins, J.G., Zuliani, P., Platzer, A., Clarke, E.M.:
Statistical model checking for markov decision processes.
In: Ninth International Conference on Quantitative Evaluation of
Systems, QEST 2012, London, United Kingdom, September 17-20, 2012, pp.
84–93. IEEE Computer Society (2012).

[77]
Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate
probabilistic model checking.
In: B. Steffen, G. Levi (eds.) Verification, Model Checking, and
Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice,
Italy, January 11-13, 2004, Proceedings, Lecture Notes in Computer
Science, vol. 2937, pp. 73–84. Springer (2004).

[78]
Hermanns, H., Krcál, J., Kretínský, J.: Compositional
verification and optimization of interactive markov chains.
In: P.R. D'Argenio, H.C. Melgratti (eds.) CONCUR 2013 - Concurrency
Theory - 24th International Conference, CONCUR 2013, Buenos Aires,
Argentina, August 27-30, 2013. Proceedings, Lecture Notes in Computer
Science, vol. 8052, pp. 364–379. Springer (2013).

[79]
Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR.
In: A. Gupta, S. Malik (eds.) Computer Aided Verification, 20th
International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008,
Proceedings, Lecture Notes in Computer Science, vol. 5123, pp.
162–175. Springer (2008).

[80]
Hoeffding, W.: Probability inequalities for sums of bounded random variables.
In: The Collected Works of Wassily Hoeffding, pp. 409–426. Springer

[81]
Howard, R.A.: Dynamic programming and markov processes.  (1960)

[82]
Jégourel, C., Legay, A., Sedwards, S.: A platform for high performance
statistical model checking - PLASMA.
In: C. Flanagan, B. König (eds.) Tools and Algorithms for the
Construction and Analysis of Systems - 18th International Conference, TACAS
2012, Held as Part of the European Joint Conferences on Theory and Practice
of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012.
Proceedings, Lecture Notes in Computer Science, vol. 7214, pp.
498–503. Springer (2012).

[83]
Jégourel, C., Legay, A., Sedwards, S.: Importance splitting for
statistical model checking rare properties.
In: N. Sharygina, H. Veith (eds.) Computer Aided Verification - 25th
International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19,
2013. Proceedings, Lecture Notes in Computer Science, vol. 8044, pp.
576–591. Springer (2013).

[84]
Jones, A., Aksaray, D., Kong, Z., Schwager, M., Belta, C.: Robust satisfaction
of temporal logic specifications via reinforcement learning.
CoRR abs/1510.06460 (2015).

[85]
Karmarkar, N.: A new polynomial-time algorithm for linear programming.
Combinatorica 4(4), 373–396 (1984).

[86]
Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based
abstraction-refinement framework for markov decision processes.
Formal Methods Syst. Des. 36(3), 246–280 (2010).

[87]
Kearns, M.J., Mansour, Y., Ng, A.Y.: A sparse sampling algorithm for
near-optimal planning in large markov decision processes.
Machine Learning 49(2-3), 193–208 (2002).

[88]
Kearns, M.J., Singh, S.P.: Near-optimal reinforcement learning in polynomial
Machine Learning 49(2-3), 209–232 (2002).

[89]
Khachiyan, L.G.: A polynomial algorithm in linear programming.
In: Doklady Academii Nauk SSSR, vol. 244, pp. 1093–1096 (1979)

[90]
Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Klüppelholz,
S., Märcker, S., Müller, D.: Advances in symbolic probabilistic
model checking with PRISM.
In: M. Chechik, J. Raskin (eds.) Tools and Algorithms for the
Construction and Analysis of Systems - 22nd International Conference, TACAS
2016, Held as Part of the European Joint Conferences on Theory and Practice
of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016,
Proceedings, Lecture Notes in Computer Science, vol. 9636, pp.
349–366. Springer (2016).

[91]
Kolobov, A., Mausam, Weld, D.S., Geffner, H.: Heuristic search for generalized
stochastic shortest path mdps.
In: F. Bacchus, C. Domshlak, S. Edelkamp, M. Helmert (eds.)
Proceedings of the 21st International Conference on Automated Planning and
Scheduling, ICAPS 2011, Freiburg, Germany June 11-16, 2011. AAAI (2011).

[92]
Kretínský, J., Meggendorfer, T.: Efficient strategy iteration for
mean payoff in markov decision processes.
In: D. D'Souza, K.N. Kumar (eds.) Automated Technology for
Verification and Analysis - 15th International Symposium, ATVA 2017, Pune,
India, October 3-6, 2017, Proceedings, Lecture Notes in Computer
Science, vol. 10482, pp. 380–399. Springer (2017).

[93]
Kretínský, J., Meggendorfer, T.: Of cores: A partial-exploration
framework for markov decision processes.
Log. Methods Comput. Sci. 16(4) (2020).

[94]
Kretínský, J., Meggendorfer, T., Weininger, M.: Stopping criteria
for value iteration on stochastic games with quantitative objectives.
In: LICS, pp. 1–14 (2023).

[95]
Kretínský, J., Ramneantu, E., Slivinskiy, A., Weininger, M.:
Comparison of algorithms for simple stochastic games.
Inf. Comput. 289(Part), 104885 (2022).

[96]
Kurkowski, S., Camp, T., Colagrosso, M.: MANET simulation studies: the
Mobile Computing and Communications Review 9(4), 50–61

[97]
Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model
checking with PRISM: a hybrid approach.
STTT 6(2), 128–142 (2004).

[98]
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of
probabilistic real-time systems.
In: G. Gopalakrishnan, S. Qadeer (eds.) Computer Aided Verification -
23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20,
2011. Proceedings, Lecture Notes in Computer Science, vol. 6806, pp.
585–591. Springer (2011).

[99]
Lai, T.L., Robbins, H.: Asymptotically efficient adaptive allocation rules.
Advances in applied mathematics 6(1), 4–22 (1985)

[100]
Larsen, K.G.: Priced timed automata and statistical model checking.
In: E.B. Johnsen, L. Petre (eds.) Integrated Formal Methods, 10th
International Conference, IFM 2013, Turku, Finland, June 10-14, 2013.
Proceedings, Lecture Notes in Computer Science, vol. 7940, pp.
154–161. Springer (2013).

[101]
Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large
markov decision processes.
STTT 17(4), 457–467 (2015).

[102]
Legay, A., Sedwards, S., Traonouez, L.: Scalable verification of markov
decision processes.
In: C. Canal, A. Idani (eds.) Software Engineering and Formal Methods
- SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS,
Grenoble, France, September 1-2, 2014, Revised Selected Papers, Lecture
Notes in Computer Science, vol. 8938, pp. 350–362. Springer (2014).

[103]
McMahan, H.B., Likhachev, M., Gordon, G.J.: Bounded real-time dynamic
programming: RTDP with monotone upper bounds and performance guarantees.
In: L.D. Raedt, S. Wrobel (eds.) Machine Learning, Proceedings of the
Twenty-Second International Conference (ICML 2005), Bonn, Germany, August
7-11, 2005, ACM International Conference Proceeding Series, vol.
119, pp. 569–576. ACM (2005).

[104]
Meggendorfer, T.: Verification of discrete-time markov decision processes.
Ph.D. thesis, Technical University of Munich, Germany (2021).

[105]
Meggendorfer, T.: PET - A partial exploration tool for probabilistic
In: A. Bouajjani, L. Holík, Z. Wu (eds.) Automated Technology
for Verification and Analysis - 20th International Symposium, ATVA 2022,
Virtual Event, October 25-28, 2022, Proceedings, Lecture Notes in
Computer Science, vol. 13505, pp. 320–326. Springer (2022).

[106]
Pineau, J., Gordon, G.J., Thrun, S.: Point-based value iteration: An anytime
algorithm for pomdps.
In: G. Gottlob, T. Walsh (eds.) IJCAI-03, Proceedings of the
Eighteenth International Joint Conference on Artificial Intelligence,
Acapulco, Mexico, August 9-15, 2003, pp. 1025–1032. Morgan Kaufmann (2003).

[107]
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic
Wiley Series in Probability and Statistics. Wiley (1994).

[108]
Quatmann, T., Katoen, J.: Sound value iteration.
In: H. Chockler, G. Weissenbacher (eds.) Computer Aided Verification
- 30th International Conference, CAV 2018, Held as Part of the Federated
Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part
I, Lecture Notes in Computer Science, vol. 10981, pp. 643–661.
Springer (2018).

[109]
Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation.
In: Z. Liu, A.P. Ravn (eds.) Automated Technology for Verification
and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October
14-16, 2009. Proceedings, Lecture Notes in Computer Science, vol.
5799, pp. 120–134. Springer (2009).

[110]
Roohi, N., Wang, Y., West, M., Dullerud, G.E., Viswanathan, M.: Statistical
verification of the toyota powertrain control verification benchmark.
In: G. Frehse, S. Mitra (eds.) Proceedings of the 20th International
Conference on Hybrid Systems: Computation and Control, HSCC 2017,
Pittsburgh, PA, USA, April 18-20, 2017, pp. 65–70. ACM (2017).

[111]
Schrijver, A.: Theory of linear and integer programming.
Wiley-Interscience series in discrete mathematics and optimization.
Wiley (1999)

[112]
Segala, R.: Modeling and verification of randomized distributed real-time
systems  (1996)

[113]
Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box
probabilistic systems.
In: R. Alur, D.A. Peled (eds.) Computer Aided Verification, 16th
International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004,
Proceedings, Lecture Notes in Computer Science, vol. 3114, pp.
202–215. Springer (2004).

[114]
Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic
In: K. Etessami, S.K. Rajamani (eds.) Computer Aided Verification,
17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July
6-10, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3576,
pp. 266–280. Springer (2005).

[115]
Sen, K., Viswanathan, M., Agha, G.A.: VESTA: A statistical model-checker
and analyzer for probabilistic systems.
In: Second International Conference on the Quantitative Evaluaiton of
Systems (QEST 2005), 19-22 September 2005, Torino, Italy, pp. 251–252.
IEEE Computer Society (2005).

[116]
Strehl, A.L.: Probably approximately correct (PAC) exploration in
reinforcement learning.
In: International Symposium on Artificial Intelligence and
Mathematics, ISAIM 2008, Fort Lauderdale, Florida, USA, January 2-4, 2008

[117]
Strehl, A.L., Li, L., Littman, M.L.: Reinforcement learning in finite mdps:
PAC analysis.
J. Mach. Learn. Res. 10, 2413–2444 (2009).

[118]
Strehl, A.L., Li, L., Wiewiora, E., Langford, J., Littman, M.L.: PAC
model-free reinforcement learning.
In: W.W. Cohen, A. Moore (eds.) Machine Learning, Proceedings of the
Twenty-Third International Conference (ICML 2006), Pittsburgh,
Pennsylvania, USA, June 25-29, 2006, ACM International Conference
Proceeding Series, vol. 148, pp. 881–888. ACM (2006).

[119]
Suilen, M., Simão, T.D., Parker, D., Jansen, N.: Robust anytime learning
of markov decision processes.
In: S. Koyejo, S. Mohamed, A. Agarwal, D. Belgrave, K. Cho, A. Oh
(eds.) Advances in Neural Information Processing Systems 35: Annual
Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New
Orleans, LA, USA, November 28 - December 9, 2022 (2022).

[120]
Sutton, R.S., Barto, A.G.: Reinforcement learning - an introduction.
Adaptive computation and machine learning. MIT Press (1998).

[121]
Szepesvári, C.: Algorithms for Reinforcement Learning.
Synthesis Lectures on Artificial Intelligence and Machine Learning.
Morgan & Claypool Publishers (2010).

[122]
Tarjan, R.E.: Depth-first search and linear graph algorithms.
SIAM J. Comput. 1(2), 146–160 (1972).

[123]
Valiant, L.G.: A theory of the learnable.
Commun. ACM 27(11), 1134–1142 (1984).

[124]
Watkins, C.J., Dayan, P.: Q-learning.
Machine learning 8(3-4), 279–292 (1992)

[125]
Weininger, M.: Solving stochastic games reliably.
Ph.D. thesis, Technical University of Munich, Germany (2022).

[126]
Weininger, M., Grover, K., Misra, S., Kretínský, J.: Guaranteed
trade-offs in dynamic information flow tracking games.
In: 2021 60th IEEE Conference on Decision and Control (CDC),
Austin, TX, USA, December 14-17, 2021, pp. 3786–3793. IEEE (2021).

[127]
White, D.J.: Real applications of markov decision processes.
Interfaces 15(6), 73–83 (1985)

[128]
White, D.J.: Further real applications of markov decision processes.
Interfaces 18(5), 55–61 (1988)

[129]
White, D.J.: A survey of applications of markov decision processes.
Journal of the operational research society 44(11),
1073–1096 (1993)

[130]
Wimmer, R., Braitling, B., Becker, B., Hahn, E.M., Crouzen, P., Hermanns, H.,
Dhama, A., Theel, O.E.: Symblicit calculation of long-run averages for
concurrent probabilistic systems.
In: QEST 2010, Seventh International Conference on the Quantitative
Evaluation of Systems, Williamsburg, Virginia, USA, 15-18 September 2010, pp.
27–36. IEEE Computer Society (2010).

[131]
Younes, H.L.S.: Ymer: A statistical model checker.
In: K. Etessami, S.K. Rajamani (eds.) Computer Aided Verification,
17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July
6-10, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3576,
pp. 429–433. Springer (2005).

[132]
Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of
probabilistic properties with unbounded until.
In: J. Davies, L. Silva, A. da Silva Simão (eds.) Formal
Methods: Foundations and Applications - 13th Brazilian Symposium on Formal
Methods, SBMF 2010, Natal, Brazil, November 8-11, 2010, Revised Selected
Papers, Lecture Notes in Computer Science, vol. 6527, pp. 144–160.
Springer (2010).

[133]
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event
systems using acceptance sampling.
In: E. Brinksma, K.G. Larsen (eds.) Computer Aided Verification, 14th
International Conference, CAV 2002,Copenhagen, Denmark, July 27-31, 2002,
Proceedings, Lecture Notes in Computer Science, vol. 2404, pp.
223–235. Springer (2002).

[134]
Zamani, Z., Sanner, S., Fang, C.: Symbolic dynamic programming for continuous
state and action mdps.
In: J. Hoffmann, B. Selman (eds.) Proceedings of the Twenty-Sixth
AAAI Conference on Artificial Intelligence, July 22-26, 2012, Toronto,
Ontario, Canada. AAAI Press (2012).