∎

11institutetext:  1Department of Computer Science, KU Leuven, Celestijnenlaan
200a - box 2402, 3001 Leuven, Belgium
2ULB - Campus de la Plaine, CP212 - 1050 Bruxelles - Belgium

# Lifted Model Checking for Relational MDPs

Wen-Chi Yang1<EMAIL_ADDRESS>Jean-François Raskin2 jean-
<EMAIL_ADDRESS>Luc De Raedt1<EMAIL_ADDRESS>
(Received: date / Accepted: date)

###### Abstract

Model checking has been developed for verifying the behaviour of systems with
stochastic and non-deterministic behavior. It is used to provide guarantees
about such systems. While most model checking methods focus on propositional
models, various probabilistic planning and reinforcement frameworks deal with
relational domains, for instance, STRIPS planning and relational Markov
Decision Processes. Using propositional model checking in relational settings
requires one to ground the model, which leads to the well known state
explosion problem and intractability.

We present pCTL-REBEL, a lifted model checking approach for verifying pCTL
properties on relational MDPs. It extends REBEL, the relational Bellman update
operator, which is a lifted value iteration approach for model-based
relational reinforcement learning, toward relational model-checking. PCTL-
REBEL is lifted, which means that rather than grounding, the model exploits
symmetries and reasons at an abstract relational level.

Theoretically, we show that the pCTL model checking approach is decidable for
relational MDPs even for possibly infinite domains provided that the states
have a bounded size. Practically, we contribute algorithms and an
implementation of lifted relational model checking, and we show that the
lifted approach improves the scalability of the model checking approach.

###### Keywords:

model checking probabilistic computation tree logic (pCTL) first-order logic
lifted inference relational MDPs

##  1 Introduction

Markov Decision Processes (MDPs) are commonly used for modeling sequential
decision making scenarios where the actions have probabilistic effects. They
are useful for modeling planning and model checking tasks. In planning, it is
commonly required to make abstraction of large models. However, formal methods
most often operate on explicit-state MDPs thus do not allow for abstractions
of domain elements. This is undesirable since the number of states increases
exponentially in the domain size, making it infeasible to explicitly traverse
the state space (Slaney and Thiébaux, 2001). In such large domains, it is not
practical to apply model checking techniques as they lead to a state explosion
(Otterlo, 2004). For instance, the well known blocks world has 501 states for
5 blocks but over 58 million states for only 10 blocks (Slaney and Thiébaux,
2001).

Lifting is the key to scalablility in relational domains (Kersting, 2012; Van
den Broeck et al., 2011; de Salvo Braz et al., 2007), it is also central to
statistical relational AI (StarAI) (De Raedt et al., 2016). Lifting means
reasoning about a group of objects as a whole at the first-order level and
exploiting the shared relational structures and symmetries in the model. This
is done by making abstraction of irrelevant details of the objects. As an
illustration, an object’s full identity (e.g. a block) can be left out as long
as it satisfies the property description (e.g. blue). There has been a
significant interest in such relational representations in reinforcement
learning and planning. For instance, Džeroski et al. (2001) introduce
Relational Markov Decision Processes (RMDP), a first-order generalization of
MDPs that succinctly formulates relational models by implicitly defining
states in terms of objects and relations (Džeroski et al., 2001; Otterlo,
2004). RMDPs have been used in reinforcement learning and planning to compute
first-order policies without explicitly constructing the underlying state
space (Džeroski et al., 2001; Kersting et al., 2004; Wang et al., 2008;
Kersting and De Raedt, 2004; Driessens and Džeroski, 2004; Boutilier et al.,
2001; Sanner and Boutilier, 2009; Yoon et al., 2012). One especially
interesting example is REBEL (Kersting et al., 2004), the RElational BELlman
operator, which we will extend in this paper. REBEL is used in value iteration
to construct an optimal policy in a given RMDP. It is also a lifted inference
technique that alleviates state explosions.

Probabilistic model checking is another field in which MDPs are frequently
used. However, standard techniques are not scalable for relational domains
since they operate on explicit-state MDPs (Baier and Katoen, 2008). In this
paper, we are interested in mitigating state explosions in probabilistic model
checking by making relational abstractions. Probabilistic model checking aims
at computing whether a given model satisfies a given probabilistic property
(Baier and Katoen, 2008; Forejt et al., 2011) and it provides rigorous
guarantees. In particular, one of the standard formalisms to specify the model
and the propertes, respectively, are MDPs and Probabilistic Computational Tree
Logic (pCTL) (Forejt et al., 2011; Kwiatkowska et al., 2011; Dehnert et al.,
2017). PCTL is a temporal logic that can express model properties over time
and allows for probabilistic quantification. A property can be the machine
gives a warning before shutting down with a probability higher than 0.95 or
the probability is higher than 0.9 that the emergency power supply, after
giving a warning, stays functioning for at least 10 minutes.

Although model checking for infinite models is generally undecidable (Gabbay,
2003), a rich body of research has discussed the state-boundedness condition
that yields decidable verification of infinite systems (Bagheri Hariri et al.,
2013; Belardinelli et al., 2011, 2012; De Giacomo et al., 2012; Calvanese et
al., 2018). These studies almost exclusively focus on non-probabilistic
actions. Nevertheless, they provide great insight into relational model
checking with pCTL properties. We extend the work of Belardinelli et al.
(2012) to the probabilistic setting to show the decidability of the model
checking problem for a subclass of infinite MDPs.

Motivated by the success of temporal logics and MDPs in probabilistic model
checking and in planning, we investigate whether it is possible to lift these
approaches to RMDPs. We show that the answer is positive by introducing pCTL-
REBEL, a new framework that augments REBEL (Kersting et al., 2004) with pCTL.
More specifically, pCTL-REBEL is a relational model checking approach that
checks relational pCTL formulae in RMDPs.

The key contribution of this paper is twofold. First, we introduce a lifted
model checking algorithm, pCTL-REBEL, to mitigate the state explosion problem
in relational domains. PCTL-REBEL is fully automated and provides a complete,
lifted solution for RMDPs by extending value iteration to a relational setting
for checking a given pCTL formula. Second, while model checking is in general
undecidable for infinite MDPs, we provide decidability results for a class of
infinite MDPs satisfying the state-boundedness condition. In particular, we
prove that a finite relational abstraction exists for such infinite MDPs, and
that checking the relational abstraction is identical to checking the infinite
MDP. This means that strong guarantees for such infinite MDPs can be provided
via lifted model checking as implemented in pCTL-REBEL.

This paper is structured as follows. Section 2 provides an overview on basic
notions of relational MDPs. Section 3 reviews basic notions of model checking,
and introduces relational pCTL. In particular, Section 3.3 defines the problem
statement of this paper, i.e. probabilistic model checking in relational MDPs.
Section 4 defines a relational Bellman update operator (a generalization of
Kersting et al. (2004)) for relational value iteration, based on which,
Section 5 introduces the main algorithm, pCTL-REBEL, for relational model
checking. Section 6 provides theoretic results about obtaining decidability
for a subclass of infinite MDPs. Section 7 reports on experimental evaluation.
Section 8 discusses related work and Section 9 highlights the link between
relational model checking and safe reinforcement learning. Finally, Section 10
concludes the work.

##  2 Relational Notions and Relational MDPs

This section defines the basic relational MDPs notions that will be used in
the remainder of this paper with the running example blocks world. We closely
follow the notions of standard first-order logic (Nienhuys-Cheng and Wolf,
1997) and standard relational MDPs (Kersting et al., 2004).

###  2.1 Relational Logic

Relational logic generalizes propositional logic with variables that represent
sets of domain constants. This section provides an overview of relational
logic, following the notions of Nienhuys-Cheng and Wolf (1997).

An alphabet is a tuple $\Sigma=\langle R,D\rangle$ where $R$ is a finite set
of relation symbols and $D$ is a possibly infinite set of constants. Each
relation symbol $\mathtt{p}\in R$ is with an arity $m\geq 0$. An atom
$\mathtt{p(t_{1},...,t_{m})}$ is a relation symbol $\mathtt{p}$ followed by an
$m$-tuple of terms $\mathtt{t_{i}}$. A term is a variable $\mathtt{X}$ or a
constant $\mathtt{c}$. A variable (resp. constant) is expressed by a string
that starts with an upper (resp. lower) case letter. A conjunction is a set of
atoms, which is implicitly assumed to be existentially quantified. A definite
clause $H\leftarrow B$ consists of an atom $H$ and a conjunction $B$, stating
that $H$ is true if $B$ is true. Given an expression $\mathtt{E}$,
$vars(\mathtt{E})$ (resp. $consts(\mathtt{E})$, $terms(\mathtt{E})$) denotes
the set of all variables (resp. constants, terms) in $\mathtt{E}$. An
expression is called ground if it contains no variables. We shall make the
unique name assumption, that states all constants are unequal, that is,
$\mathtt{c_{1}\not=c_{2}}$ holds for different constants $\mathtt{c_{1}}$ and
$\mathtt{c_{2}}$. A substitution $\theta$ is a set of bindings
$\mathtt{\\{X_{1}=t_{1},...,X_{n}=t_{n}\\}}$ that assigns terms
$\mathtt{t_{i}}$ to variables $\mathtt{X_{i}}$. A grounding substitution
$\theta$ assigns constants to variables in an expression $\mathtt{E}$ such
that $\mathtt{E}\theta$ contains no variables.

In this paper, it will be convenient to use the Object Identity subsumption
framework (OI-subsumption) (Ferilli et al., 2002), which requires that any two
terms $\mathtt{t_{1},t_{2}}$ in an atom or conjunction are unequal. For
instance, under OI-subsumption the conjunction $\\{\mathtt{cl(b),on(X,Y)}\\}$
denotes the expression $\\{\mathtt{cl(b)}$, $\mathtt{on(X,Y)}$, $\mathtt{X\neq
Y}$, $\mathtt{X\neq b}$, $\mathtt{Y\neq b}\\}$. From now on, we will impose
the object identity assumption, which means that for all expressions involving
more than one term, the pairwise inequalities are added to the expression. For
ease of writing, when the context is clear, we shall not write these
inequalities explicitly. A conjunction $\mathtt{A}$ is $OI$-subsumed by
conjunction $\mathtt{B}$, denoted by $\mathtt{A}\preceq_{\theta}\mathtt{B}$,
if there exists a substitution $\theta$ such that
$\mathtt{B}\theta\subseteq\mathtt{A}$. Only substitutions that satisfy the
inequality constraints are allowed.

A unifier $\theta=\mathit{unifier}(\mathtt{A,B})$ of two conjunctions
$\mathtt{A}$ and $\mathtt{B}$ under $OI$-subsumption is a substitution such
that $\mathtt{A}\theta=\mathtt{B}\theta$. For example, the conjunctions
$\\{\mathtt{cl(X),on(y,Z)}\\}$ and $\\{\mathtt{cl(x),on(Y,Z)}\\}$ have a
unifier $\\{\mathtt{X/x,Y/y}\\}$. A maximally general specialisation (mgs) of
two conjunctions $\mathtt{A}$ and $\mathtt{B}$ under $OI$-subsumption is a
conjunction subsumed by $\mathtt{A}$ and $\mathtt{B}$ that is not properly
subsumed by any other specialisations. The mgs operation is not always unique
under $OI$-subsumption. For example, the conjunctions $\\{\mathtt{cl(X)}\\}$
and $\\{\mathtt{on(X,Y)}\\}$ have maximally general specialisations
$\\{\mathtt{cl(X),on(X,Y)}\\}$ and $\\{\mathtt{cl(X),on(Y,Z)}\\}$ that do not
OI-subsume one another.

The Herbrand base of $\Sigma=\langle R,D\rangle$, denoted as $HB^{\Sigma}$, is
the set of all ground atoms that can be constructed from $\Sigma$. A Herbrand
interpretation $s$ is a subset of $HB^{\Sigma}$ where all atoms in $s$ are
$true$ and all others are $false$. The set of all Herbrand interpretations
determined by $\Sigma$ is denoted as $S^{\Sigma}$. When the domain $D$ is
infinite, the set of all Herbrand interpretations must be infinite.

###  2.2 Relational MDP

A relational MDP (RMDP) generalizes the explicit-state MDP in a twofold
manner. First, a RMDP have structured states. More specifically, a RMDP state
is represented by a conjunction of ground atoms whereas an explicit-MDP state
is represented by a single constant. Second, a RMDP can represent a set of
states with an abstract state by allowing variables. This enables reasoning
about sets of states as a whole. In this paper, a RMDP is a variant of the
standard RMDP (Kersting et al., 2004; Boutilier et al., 2001) that varies by
allowing infinite domains. This section formally defines the RMDP, following
the notions of Kersting et al. (2004).

A RMDP is a tuple $K=\langle\Sigma,\Delta\rangle$ where $\Sigma=\langle
R,D\rangle$ containing a set of relations and a domain, and $\Delta$ is a
finite set of abstract transitions. The alphabet $\Sigma$ determines the state
space. A state $s\in S^{\Sigma}$ is a Herbrand interpretation. An abstract
state $s^{\prime}$ is then a conjunction of atoms, representing a set of
states, denoted by $s^{\prime}\Theta=\\{s\in
S^{\Sigma}|s\preceq_{\theta}s^{\prime}\\}$.

###### Example 1

Given an alphabet $\Sigma=\langle R,D\rangle$ for a blocks world with
relations $R=\\{\mathtt{cl/1,on/2}\\}$ and domain
$D=\\{\mathtt{bl_{1},bl_{2},bl_{3}}\\}$, the abstract state
$s=\\{\mathtt{cl(A),cl(C),on(A,B)}\\}$ represents six ground states

$\displaystyle s\Theta=\\{$
$\displaystyle\mathtt{\\{cl(bl_{1}){,}cl(bl_{3}){,}on(bl_{1}{,}bl_{2})\\}},\mathtt{\\{cl(bl_{1}){,}cl(bl_{2}){,}on(bl_{1}{,}bl_{3})\\}},$
$\displaystyle\mathtt{\\{cl(bl_{2}){,}cl(bl_{3}){,}on(bl_{2}{,}bl_{1})\\}},\mathtt{\\{cl(bl_{2}){,}cl(bl_{1}){,}on(bl_{2}{,}bl_{3})\\}},$
$\displaystyle\mathtt{\\{cl(bl_{3}){,}cl(bl_{2}){,}on(bl_{3}{,}bl_{1})\\}},\mathtt{\\{cl(bl_{3}){,}cl(bl_{1}){,}on(bl_{3}{,}bl_{2})\\}}\\}$

An abstract action $\alpha\not\in R$ is an atom for an action relation. An
abstract transition $\delta\in\Delta$ (based on an abstract action $\alpha$)
is a finite set of probabilistic action rules
$\\{H_{1}\xleftarrow{p_{1}:\alpha}B,...,H_{n}\xleftarrow{p_{n}:\alpha}B\\}$
where $B$ (resp. $H_{i}$) is an abstract state, representing the precondition
(resp. postcondition), and $p_{i}\in[0,1]$ is the transition probability.
These transitions denote a proper probability distribution over $H_{i}$, i.e.
$\sum^{n}_{i=1}p_{i}=1$. To ensure that abstract transitions rely only on
information in the current state, we assume that all variables in $H_{i}$ are
also in $B$, i.e. $vars(H_{i})\subseteq vars(B)$.

###### Example 2

A blocks world is defined by a RMDP $K=\langle\Sigma,\Delta\rangle$ where
$\Sigma=\langle R,D\rangle$, $R=\\{\mathtt{cl/1,on/2}\\}$ and $\Delta$
contains the following abstract transition $\mathtt{\delta_{move}}$.

$\displaystyle\mathtt{cl(A){,}cl(C){,}on(A,B)\xleftarrow{\makebox[51.21504pt]{
\scriptsize $\mathtt{0.9:move(A,B,C)}$ }}cl(A){,}cl(B){,}on(A,C)}$
$\displaystyle\mathtt{cl(A){,}cl(B){,}on(A,C)\xleftarrow{\makebox[51.21504pt]{
\scriptsize $\mathtt{0.1:move(A,B,C)}$ }}cl(A){,}cl(B){,}on(A,C)}$

A graphical illustration is in Figure 1. The abstract action
$\mathtt{move(A,B,C)}$ succeeds in moving block $\mathtt{A}$ to block
$\mathtt{B}$ from block $\mathtt{C}$ with probability $\mathtt{p_{1}}=0.9$ and
fails with probability $\mathtt{p_{2}}=0.1$. When the action fails, the state
stays the same.

Figure 1: The abstract transition $\mathtt{\delta_{move}}$ moves block
$\mathtt{A}$ to block $\mathtt{B}$ from block $\mathtt{C}$ with probability
$0.9$. It fails to move the block with probability $0.1$.

###  2.3 The underlying ground MDP

A RMDP implicitly defines an underlying ground MDP. In general, the underlying
ground MDP has an infinite state space and action space (for an infinite
domain). It also has an unbounded branching behavior, i.e. a state has an
infinite number of available actions. This section formally defines the
construction of the underlying ground MDP.

Given a RMDP $K=\langle\Sigma,\Delta\rangle$, the underlying ground MDP is a
tuple $M=\langle S,A,T\rangle$ where $S$ is a set of ground states, $A$ is a
set of ground actions and $T:S\times A\times S\rightarrow[0,1]$ is a ground
transition function. Each ground state $s\in S$ is a Herbrand interpretation
$s\subseteq HB^{\Sigma}$. Each ground state $s$ has a set of available ground
actions, denoted as $A(s)\subseteq A$. $A(s)$ is defined by grounding the
abstract actions $\alpha$ with $s$. Formally,

$\displaystyle
A(s):=\\{\alpha\theta|H_{i}\xleftarrow{p_{i}:\alpha}B\in\Delta,s\preceq_{\theta}B\\}$

Similarly, the set of ground transitions $T(s,\alpha\theta)$ of state $s$ and
action $\alpha\theta\in A(s)$ are defined by grounding the abstract
transitions.

$\displaystyle T(s,\alpha\theta):=\\{h_{i}\xleftarrow{p_{i}:\alpha\theta}s|$
$\displaystyle H_{i}\xleftarrow{p_{i}:\alpha}B\in\Delta,s\preceq_{\theta}B,$
$\displaystyle h_{i}=(s\backslash B\theta)\cup H_{i}\theta\\}$

Given $s$ and $\alpha\theta$, the probability distribution over all states
$s^{\prime}\in S$ is defined as

$\displaystyle T(s,\alpha\theta)(s^{\prime}):=p_{i},\mbox{ where
}s^{\prime}=(s\backslash B\theta)\cup H_{i}\theta$

$T$ is a proper probability distribution, i.e. $\sum_{s^{\prime}\in
S}T(s,\alpha\theta)(s^{\prime})=1$ as a consequence of the proper abstract
transitions $\Delta$.

###### Example 3

(Cont. Example 2) Consider a blocks world $K=\langle\Sigma,\Delta\rangle$
where $\Sigma=\langle R,D\rangle$, $R=\\{\mathtt{cl/1,on/2}\\}$,
$D=\\{\mathtt{a,b,c,d,e}\\}$ and $\Delta$ contains the
$\mathtt{\delta_{move}}$ transition (Fig. 1). The RMDP $K$ defines the
underlying MDP $M=\langle S,A,T\rangle$. In a ground state
$s=\\{\mathtt{cl(a)}$, $\mathtt{cl(b)}$, $\mathtt{cl(d)}$, $\mathtt{on(a,c)}$,
$\mathtt{on(d,e)}\\}\in S$, the action $\mathtt{move(a,b,c)}\in A$ leads to
the next state $s^{\prime}=\\{\mathtt{cl(a)}$, $\mathtt{cl(c)}$,
$\mathtt{cl(d)}$, $\mathtt{on(a,b)}$, $\mathtt{on(d,e)}\\}$ with probability
0.9, and stays in $s$ with probability 0.1, as illustrated in Figure 2.

Figure 2: The ground transition $\mathtt{move(a,b,c)}$ moves block
$\mathtt{a}$ to block $\mathtt{b}$ from block $\mathtt{c}$ with probability
$0.9$. It fails to move the block with probability $0.1$.

When a RMDP has an infinitely large domain, it has an infinitely large state
space. Moreover, a state may have infinitely many available actions. For
example, we can move a clear block to one of the (infinitely many) other clear
blocks. Therefore, the branching behavior of a RMDP and its underlying MDP can
be unbounded for an infinite domain, making the model checking problem
undecidable. Later, Section 6 will prove the model checking problem is
decidable for a class of infinite RMDPs that have bounded branching behavior
(see Section 6.1).

##  3 Model Checking in relational MDPs

This section defines the problem statement of this paper, namely the model
checking problem of relational MDPs. More specifically, Section 3.1 first
reviews the fundamentals of model checking, Section 3.2 then defines a
relational temporal logic used for specifying properties to be checked, and
Section 3.3 finally defines the main problem statement. Later, Section 4 and
Section 5 will provide a solution for the problem in Section 3.3.

###  3.1 Probabilistic Reachability

This section defines the probabilistic reachability property that refers to
the maximum probability of reaching a set of goal states from a given initial
state. The probabilistic reachability property is the most fundamental
property in a MDP, and is required to define the relational pCTL language in
Section 3.2. The content of this section is standard in model checking (Baier
and Katoen, 2008; Kwiatkowska et al., 2011) and is included for self-
containment.

We first define the paths in a MDP $M=\langle S,A,T\rangle$ and their
probability assignment. A path of length $n$ is denoted as
$\rho_{n}=s_{1}\xrightarrow{a_{1}}s_{2}\xrightarrow{a_{2}}...\xrightarrow{a_{n-1}}s_{n}$
where $s_{i}\in S$, $a_{i}\in A(s_{i})$ and $T(s_{i},a_{i})(s_{i+1})>0$.
Similarly, an infinite path is denoted as
$\rho=s_{1}\xrightarrow{a_{1}}s_{2}\xrightarrow{a_{2}}...$. The set of all
finite (resp. infinite) paths is denoted as
$\mathit{F\mkern-5.0muP\mkern-4.0muath}_{M}$ (resp.
$\mathit{I\mkern-5.0muP\mkern-4.0muath}_{M}$), and the set of all finite
(resp. infinite) paths starting from state $s$ is denoted as
$\mathit{F\mkern-5.0muP\mkern-4.0muath}_{M,s}$ (resp.
$\mathit{I\mkern-5.0muP\mkern-4.0muath}_{M,s}$).
$\mathit{P\mkern-4.0muath}_{M,s}{=}\mathit{F\mkern-5.0muP\mkern-4.0muath}_{M,s}\cup\mathit{I\mkern-5.0muP\mkern-4.0muath}_{M,s}$
contains all paths in $M$ that starts from $s$. The i-th state of a path
$\rho\in\mathit{P\mkern-4.0muath}_{M,s}$ is denoted as $\rho(i)$, and the last
state in $\rho$ as $last(\rho)$. To project a set of paths
$\mathit{P\mkern-4.0muath}_{M,s}$ to a probability space, it is required to
remove non-deterministic actions by a policy. A policy
$\pi:\mathit{F\mkern-5.0muP\mkern-4.0muath}_{M}\rightarrow\mathit{Dist}(A)$
takes a finite path $\rho_{n}$ and specifies a probability distribution over
the available actions $A(last(\rho_{n}))$. We write $\pi(\rho_{n})$ to denote
all possible actions selected by the policy, and $\pi(\rho_{n},a)$ to denote
the probability of action $a$ being selected.

###### Definition 1

(cf. (Kwiatkowska et al., 2011)) Given a MDP $M$ and a policy $\pi$, the
probability $P_{M}^{\pi}(\rho_{n})$ of a finite path
$\rho_{n}=s_{1}\xrightarrow{a_{1}}s_{2}\xrightarrow{a_{2}}...\xrightarrow{a_{n-1}}s_{n}\in\mathit{F\mkern-5.0muP\mkern-4.0muath}_{M,s_{1}}$
is inductively defined by

$\displaystyle P_{M}^{\pi}(\rho_{1})=1$ $\displaystyle
P_{M}^{\pi}(\rho_{n})=P_{M}^{\pi}(\rho_{n-1})\sum_{a\in\pi(\rho_{n-1})}\pi(\rho_{n-1},a)T(s_{n-1},a)(s_{n})$
(1)

where $\rho_{n}$ denotes $\rho$’s prefix of length $n$. Let
$C_{\rho_{n}}\in\mathit{I\mkern-5.0muP\mkern-4.0muath}_{M,s_{1}}$ be the basic
cylinder, i.e. the set of all infinite paths that have the prefix $\rho_{n}$,
the probability $P^{\pi}_{M}(C_{\rho_{n}})$ is then defined as the probability
of $\rho$, i.e. $P^{\pi}_{M}(C_{\rho})=P^{\pi}_{M}(\rho)$.

After defining the probability assignment for paths in a MDP, we can now
formally define the probabilistic reachability.

###### Definition 2

(cf. (Kwiatkowska et al., 2011)) Given a MDP $M=\langle S,A,T\rangle$, an
initial state $s\in S$ and a set of goal states $G\subseteq S$,
$\mathit{P\mkern-4.0muath}_{M,s}(G)\subseteq\mathit{P\mkern-4.0muath}_{M,s}$
is a set of paths that can reach $G$ from $s$. Formally,

$\displaystyle\mathit{P\mkern-4.0muath}_{M,s}(G):=\\{\rho\in\mathit{P\mkern-4.0muath}_{M,s}|\exists
i\in\mathbb{N},\rho(i)\in G\\}$

The maximum probability of reaching $G$ from $s$ in MDP $M$ is obtained by
following some optimal policy $\pi$. The optimal policy $\pi$ defines the
maximum path probability compared to any other policies in the policy space
$\Pi$ of the MDP. Formally,

$\displaystyle P^{max}_{M}(\mathit{P\mkern-4.0muath}_{M,s}(G))$
$\displaystyle:=\sup_{\pi\in\Pi}P^{\pi}_{M}(\mathit{P\mkern-4.0muath}_{M,s}(G))$
(2)

In general, $P^{max}_{M}(.)$ denotes the maximum probability of a set of paths
in $M$.

It is known that a deterministic, stationary $\epsilon$-optimal policy
suffices to achieve the maximum probabilistic reachability in a finite MDP
(Baier and Katoen, 2008). This means the policy will simplify to a function
$\pi:S\rightarrow A$ that maps a path’s last state to a single action. For an
infinite RMDP that has a finite abstraction (in Section 6), we assume there
exists an optimal deterministic, stationary policy for the maximum
probabilistic reachability.

###  3.2 Relational pCTL

This section defines Relational Probabilistic Computational Tree Logic
(relational pCTL), a temporal logic that describes the behavior of systems
over time and allows probabilistic quantification. In model checking, the pCTL
is used for specifying properties about a given RMDP that will be later
checked. The relational pCTL is a variant of the standard pCTL (cf.
(Kwiatkowska et al., 2011) and (Baier and Katoen, 2008)) that varies by
allowing relational atoms and only allowing negations in front of atoms.

The syntax of the relational pCTL is as follows. A property is always
specified by a state formula $\phi$.

$\displaystyle state\;formula\;\phi$
$\displaystyle::=\mathtt{true}\;|\;l\;|\;\neg
l\;|\;\phi\wedge\phi\;|\;P_{\bowtie p}[\psi]$ $\displaystyle
path\;formula\;\psi$
$\displaystyle::=\mathtt{X}\;\phi\;|\;\phi\;\mathtt{U^{\leq
k}}\;\phi\;|\;\phi\;\mathtt{U}\;\phi$

where $l$ is an atom (that can contain variables), $p$ is a probability and
that $0\leq p\leq 1$, $k\in\mathbb{N}$ is a step bound and
$\bowtie\;\in\\{\leq,<,\geq,>\\}$. Here, the relational pCTL generalizes the
standard pCTL by letting $l$ be a relational atom instead of a constant.

An intuition of the semantics is as follows. The semantics of the relational
pCTL resembles the standard pCTL ((Baier and Katoen, 2008)). A state either
satisfies or violates a state formula $\phi$, resulting in a boolean
evaluation for each state. A path formula $\mathtt{X}\phi$ is satisfied if
$\phi$ is satisfied in the next step; $\phi_{1}\mathtt{U^{\leq k}}\phi_{2}$ is
satisfied if $\phi_{2}$ is satisfied within $k$ steps and $\phi_{1}$ holds
before then; $\phi_{1}\mathtt{U}\phi_{2}$ is satisfied if $\phi_{2}$ is
eventually satisfied and $\phi_{1}$ holds before then.

The semantics of the relational pCTL is defined at the ground level. Given a
RMDP $K=\langle\Sigma,\Delta\rangle$ that defines a ground MDP $M=\langle
S,A,T\rangle$, we say a ground state $s\in S$ satisfies a state formula
$\phi$, denoted as $s\models\phi$, if and only if there exists a grounding
substitution $\theta$ for all free variables in $\phi$ such that $s$ satisfies
$\phi$ under $\theta$, i.e.
$s\models\phi\Leftrightarrow\exists\theta.s\models^{\theta}\phi$. All
substitutions must respect OI-subsumption, i.e. any two terms
$\mathtt{t_{1},t_{2}}$ in a conjunction must be unequal. Formally, the pCTL
satisfiability relation $\models^{\theta}$ is inductively defined as follows.

$\displaystyle s$ $\displaystyle\models^{\theta}\mathtt{true}$ $\displaystyle
s$ $\displaystyle\models^{\theta}l$ $\displaystyle\Leftrightarrow
s\preceq_{\theta}l$ $\displaystyle s$ $\displaystyle\models^{\theta}\neg l$
$\displaystyle\Leftrightarrow s\not\preceq_{\theta}l$ $\displaystyle s$
$\displaystyle\models^{\theta}\phi_{1}\land\phi_{2}$
$\displaystyle\Leftrightarrow s\models^{\theta}\phi_{1}\land
s\models^{\theta}\phi_{2}$ $\displaystyle s$
$\displaystyle\models^{\theta}\phi_{1}\lor\phi_{2}$
$\displaystyle\Leftrightarrow s\models^{\theta}\phi_{1}\lor
s\models^{\theta}\phi_{2}$ $\displaystyle s$
$\displaystyle\models^{\theta}\mathtt{P}_{\bowtie p}[\psi]$
$\displaystyle\Leftrightarrow
P_{M}^{max}(\\{\rho\in\mathit{P\mkern-4.0muath}_{M,s}|\rho\models\psi\\})\bowtie
p$

where

$\displaystyle\rho$ $\displaystyle\models\mathtt{X}\;\phi$
$\displaystyle\Leftrightarrow\rho(2)\models\phi$ $\displaystyle\rho$
$\displaystyle\models\phi_{1}\;\mathtt{U^{\leq k}}\;\phi_{2}$
$\displaystyle\Leftrightarrow\exists
i{\leq}k.\rho(i)\models\phi_{2}\land\forall j{<}i.\rho(j)\models\phi_{1}$
$\displaystyle\rho$ $\displaystyle\models\phi_{1}\;\mathtt{U}\;\phi_{2}$
$\displaystyle\Leftrightarrow\exists
i{\in}\mathbb{N}.\rho(i)\models\phi_{2}\land\forall
j{<}i.\rho(j)\models\phi_{1}$

With the aforementioned operators, additional operators can be defined as
follows where $\mathtt{F}$ stands for eventually.

  * $\mathtt{false}\equiv\neg\mathtt{true}$

  * $\mathtt{F^{\leq k}}\;\phi\equiv\mathtt{true\;U^{\leq k}}\;\phi$

  * $\mathtt{F}\;\phi\equiv\mathtt{true\;U}\;\phi$

###### Example 4

Consider a formula $\phi=\neg\mathtt{cl(A)}$ that states ”there exists an
unclear block $\mathtt{A}$ in the state”. The satisfiability relation
$s\models\phi$ can be rewritten as follows.

$\displaystyle s\models\neg\mathtt{cl(A)}$ $\displaystyle\Leftrightarrow\;$
$\displaystyle\exists\theta.s\models^{\theta}\neg\mathtt{cl(A)}$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\exists\theta.s\not\preceq_{\theta}\mathtt{cl(A)}$

For the Herbrand interpretation $s_{1}=\\{\mathtt{cl(a)}\\}$, the above
evaluates to $false$ as there does not exist any $\theta$ for the
satisfiability relation. For another Herbrand interpretation
$s_{2}=\\{\mathtt{cl(a),on(a,b)}\\}$, the above evaluates to $true$ with
$\theta=\\{\mathtt{A/b}\\}$.

###### Example 5

Consider a formula $\phi=\mathtt{P}_{\geq 0.9}[\mathtt{X\;cl(A)}]$ that states
”there exists a block $\mathtt{A}$ that can become clear in the next state
with a probability $\geq$ 0.9”. The satisfiability relation $s\models\phi$ can
be rewritten as follows.

$\displaystyle s\models\mathtt{P}_{\geq 0.9}[\mathtt{X\;cl(A)}]$
$\displaystyle\Leftrightarrow\;$
$\displaystyle\exists\theta.s\models^{\theta}\mathtt{P}_{\geq
0.9}[\mathtt{X\;cl(A)}]$ $\displaystyle\Leftrightarrow\;$
$\displaystyle\exists\theta.s\models^{\theta}P^{max}_{M}(\\{\rho\in\mathit{P\mkern-4.0muath}_{M,s}|\rho(2)\models\mathtt{cl(A)}\\})\geq
0.9$

For the Herbrand interpretation $s=\\{\mathtt{cl(a)}$, $\mathtt{on(a,b)}$,
$\mathtt{on(b,c)}\\}$, the above evaluates to $true$ with
$\theta=\\{\mathtt{A/b}\\}$ as block $\mathtt{b}$ can be clear after taking
the action $\mathtt{move(a,flr,b)}$ where $\mathtt{flr}$ stands for floor.

It is assumed that the scope of variables is within the path formula. That is,
no variable bindings exist for variables within different $\mathtt{P}_{\bowtie
p}[.]$. For example, in $\mathtt{P}_{\geq
0.7}[\mathtt{X\;cl(A)}]\land\mathtt{P}_{\geq 0.95}[\mathtt{F\;on(B,C)}]$, we
do not assume variable bindings such as $\mathtt{A=B}$ or $\mathtt{A\neq C}$.
Note $\mathtt{B\neq C}$ holds under OI-subsumption.

###  3.3 The Relational Model Checking Problem

This section defines the model checking problem for RMDPs, using the
definition of RMDP (Section 2.2) and relational pCTL (Section 3.2). Later,
Section 4 and Section 5 will illustrate techniques for solving the relational
model checking problem.

Just like standard model checking (Baier and Katoen, 2008), for a given model
$M$ and a given pCTL formula $\phi$, relational model checking computes
$Sat_{M}(\phi)$, i.e. all states in $M$ that satisfy $\phi$. The significance
of relational model checking is that it computes $Sat_{M}(\phi)$ at a lifted
level by using relational states to represent a group of underlying ground
states. Hence, relational model checking finds a set of abstract states that
represents $Sat_{M}(\phi)$.

###### Definition 3

Given a RMDP $K=\langle\Sigma,\Delta\rangle$ that defines the underlying MDP
$M=\langle S,A,T\rangle$ and a relational pCTL formula $\phi$, the relational
model checking problem is to determine a set of abstract states
$Sat_{K}(\phi)$ that represents all Herbrand interpretations
$Sat_{M}(\phi)\subseteq S$ that satisfy $\phi$. Formally,
$Sat_{M}(\phi)=\\{s\in S|s\models\phi\\}$. The task is to find a set of
abstract states $Sat_{K}(\phi)$ in $K$ such that

$s\in Sat_{M}(\phi)\Leftrightarrow\exists s_{a}\in
Sat_{K}(\phi).s\preceq_{\theta}s_{a}$

In this work, we will solve the relational model checking problem of two types
of RMDPs. The first type is the RMDPs that have a finite domain (i.e. finite
RMDPs). The second type is a special class of RMDPs that have an infinite
domain (i.e. infinite RMDPs).

We discuss decidability of the two types of RMDPs. The model checking problem
for a finite RMDP is decidable. This is because when the domain is finite, the
state space is also finite, i.e. the underlying ground MDP is finite. One can
thus enumerate all states and collect the states that satisfy the given
property. In contrast, an infinite RMDP can contain infinitely many states,
which makes enumerating all states infeasible. In this case, we focus on a
class of infinite RMDPs where there exists a finite abstraction for the
underlying infinite ground MDP. More details are given in Section 6.

##  4 Relational Value Iteration

This section defines relational value iteration, the essential building block
for the pCTL-REBEL algorithm (cf. Section 5). For a pCTL formula
$\mathtt{P_{\bowtie p}[\psi]}$ and a RMDP, relational value iteration computes
the probabilities of the states satisfying $\psi$. These probabilities are
computed by iteratively applying the relational Bellman operator (cf. Section
4.1). The relational Bellman operator is complex as it involves reasoning
about objects and relations at the relational level. Section 4.2, 4.3 and 4.4
describe in detail the three components of the relational Bellman operator,
respectively. Section 4.5 then illustrates the relational Bellman operator
with an example.

###  4.1 Relational Bellman Operator

The relational Bellman operator extends REBEL (Kersting et al., 2004), that
computes the probabilistic reachability operator $\mathtt{P_{\bowtie
p}[F^{\leq k}}\mathtt{S}]$111REBEL is used for computing the optimal policy
for reaching a set of goal states in model-based relational reinforcement
learning, thus it computes a reachability property. In particular, it
calculates the probabilities of all states satisfying a reachability goal
$\mathtt{S}$ where $\mathtt{S}$ is an abstract state. To support the other
operators i.e. $\mathtt{P_{\bowtie p}[U^{\leq k}\cdot]}$, $\mathtt{P_{\bowtie
p}[U\;\cdot]}$ and $\mathtt{P_{\bowtie p}[X\;\cdot]}$, REBEL needs to be
generalized in multiple ways, as will be discussed in Sections 4.2, 4.3 and
4.4.

The probability of a state satisfying a given path formula $\psi$ is encoded
in the state value function $V:S\rightarrow[0,1]$. Just like the standard
Bellman operator, the relational Bellman operator takes an initial state value
function $V_{0}$ and iteratively computes $V_{1},V_{2},...,V_{k}$ for $k$
steps. $k$ is given for a step-bounded formula222Step-boundedness is commonly
called a finite horizon in AI. . For an unbounded formula, the probability
converges to a good enough approximation with a large enough $k$. We now
formally define the state value function and the relational Bellman operator,
following the notations of Kersting et al. (2004).

###### Definition 4

(cf. Kersting et al. (2004)) A state value function $V$ is an ordered set of
V-rules of the form $c\leftarrow B$ where $B$ is an abstract state and
$c\in[0,1]$, representing the probability of reaching a goal state from $B$.
The value $V(s)$ of a Herbrand interpretation $s$ is assigned by the first
rule such that $s\preceq_{\theta}B$.

Given a set of (abstract) goal states $G$, the initial state value function
$V_{0}$ is defined as

$\displaystyle 1.0$ $\displaystyle\leftarrow s,\forall s\in G$ $\displaystyle
0$ $\displaystyle\leftarrow\emptyset$

This means that any Herbrand interpretation subsumed by a goal state $s\in G$
is assigned a state value 1.0 by the first rule, while all other states are
assigned the state value 0 by the second rule. The role of
$0\leftarrow\emptyset$ is to ensures that all states are assigned a value.
Hence it is often the last V-rule to capture the states that are not captured
by any previous rules.

###### Definition 5

(cf. Kersting et al. (2004)) A state-action value function $Q$ is an ordered
set of Q-rules of the form $c:A\leftarrow B$ where $A$ is an abstract action
and $B$ is an abstract state, representing the probability of reaching a goal
state when $A$ is taken in $B$. The value $Q(s,a)$ of a Herbrand
interpretation $s$ and an action $a$ is assigned by the first rule such that
$s\preceq_{\theta}B$ and $a\preceq_{\theta}A$.

The state value functions $V_{1},V_{2},...$ are computed by iteratively
applying the relational Bellman operator333This paper uses a special case of
the general relational Bellman operator that has no reward component and the
discount factor is 1. Hence our work addresses a special case of relational
model-based reinforcement learning. More details will be given in Section 9.
in equation 3.

$\displaystyle V_{t+1}\underbrace{(s)}_{\text{ \leavevmode\hbox
to11.75pt{\vbox to11.75pt{\pgfpicture\makeatletter\hbox{\hskip
5.87407pt\lower-5.87407pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.67407pt}{0.0pt}\pgfsys@curveto{5.67407pt}{3.13374pt}{3.13374pt}{5.67407pt}{0.0pt}{5.67407pt}\pgfsys@curveto{-3.13374pt}{5.67407pt}{-5.67407pt}{3.13374pt}{-5.67407pt}{0.0pt}\pgfsys@curveto{-5.67407pt}{-3.13374pt}{-3.13374pt}{-5.67407pt}{0.0pt}{-5.67407pt}\pgfsys@curveto{3.13374pt}{-5.67407pt}{5.67407pt}{-3.13374pt}{5.67407pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.75pt}{-2.25555pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{1}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}$
$\displaystyle=\overbrace{\max_{a\in
A(s)}\underbrace{\sum_{s^{\prime}}T(s,a,s^{\prime})V_{t}(s^{\prime})}_{\text{
\leavevmode\hbox to11.75pt{\vbox
to11.75pt{\pgfpicture\makeatletter\hbox{\hskip 5.87407pt\lower-5.87407pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.67407pt}{0.0pt}\pgfsys@curveto{5.67407pt}{3.13374pt}{3.13374pt}{5.67407pt}{0.0pt}{5.67407pt}\pgfsys@curveto{-3.13374pt}{5.67407pt}{-5.67407pt}{3.13374pt}{-5.67407pt}{0.0pt}\pgfsys@curveto{-5.67407pt}{-3.13374pt}{-3.13374pt}{-5.67407pt}{0.0pt}{-5.67407pt}\pgfsys@curveto{3.13374pt}{-5.67407pt}{5.67407pt}{-3.13374pt}{5.67407pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.75pt}{-2.25555pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{2}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}}^{\text{
\leavevmode\hbox to11.75pt{\vbox
to11.75pt{\pgfpicture\makeatletter\hbox{\hskip 5.87407pt\lower-5.87407pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.67407pt}{0.0pt}\pgfsys@curveto{5.67407pt}{3.13374pt}{3.13374pt}{5.67407pt}{0.0pt}{5.67407pt}\pgfsys@curveto{-3.13374pt}{5.67407pt}{-5.67407pt}{3.13374pt}{-5.67407pt}{0.0pt}\pgfsys@curveto{-5.67407pt}{-3.13374pt}{-3.13374pt}{-5.67407pt}{0.0pt}{-5.67407pt}\pgfsys@curveto{3.13374pt}{-5.67407pt}{5.67407pt}{-3.13374pt}{5.67407pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.75pt}{-2.25555pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{3}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} }
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}=\max_{a\in
A(s)}Q_{t+1}(s,a)$ (3)

To reason about the objects and the relations at the relational level, the
relational Bellman operator consists of three components and each component is
solved by an algorithm: \small{1}⃝ Regression: Deriving the abstract states
$s$ in $V_{t+1}$ \small{2}⃝ Qrules: Computing $Q(s,a)$ for all actions $a\in
A(s)$ \small{3}⃝ VRules: Updating $V_{t+1}$ by maximizing over $Q(s,a)$. These
three components will be described in detail in Section 4.2, 4.3 and 4.4,
respectively.

OneIteration (Algorithm 1) implements the relational Bellman operator
(Equation 3) using Regression (Algorithm 2), QRules (Algorithm 3) and VRules
(Algorithm 4). OneIteration directly calls QRules and VRules, and QRules
directly calls Regression. In order to provide support to the until operator
$\mathtt{U^{\leq k}}$ and the next operator $\mathtt{X}$, Algorithms 1-4
extends algorithms by Kersting et al. (2004) that compute the eventually pCTL
operator $\mathtt{F^{\leq k}}$. We mark the modified part in the algorithms
blue. Specifically, Algorithm 1 has two extra parameters $\mathtt{S}$ and
$\psi$. The details will be given in the following sub-sections.

$Q_{t+1}:=$
QRules$(V_{t},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{S_{1}}})$

$V_{t+1}:=$
VRules$(Q_{t+1},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\psi})$

return $V_{t+1}$

Algorithm 1 OneIteration$(V_{t},\psi)$ returns $V_{t+1}$, given $V_{t}$ and a
formula $\psi$ of the form of $\mathtt{S_{1}\;U^{\leq k}S_{2}}$ or
$\mathtt{X\;S_{2}}$. OneIteration implements Equation 3. OneIteration is
composed of QRules (Algorithm 3) and VRules (Algorithm 4).

###  4.2 Logical Regression

Logical regression is a standard technique that reasons about abstract
transitions at the relational level (Boutilier et al., 2001; Kersting et al.,
2004; Sanner and Boutilier, 2009). It is essential to scalability as it
mitigates state explosions by exploiting the relational state structures
instead of operating on the underlying ground states. It does so by searching
backwards the possible pre-states that can reach a given state $G$ after
following a given abstract transition rule $H\xleftarrow{p:\alpha}B$.

This section extends the standard logical regression to handle relational pCTL
operators. Logical regression is used in Equation 3 \small{1}⃝ to identify the
states $s$ that can reach $s^{\prime}$ by taking one action. We first
illustrate logical regression with the blocks world example, then discuss its
implementation Regression (Algorithm 2).

###### Example 6

To illustrate logical regression, consider an abstract state
$G=\\{\mathtt{on(a,b)}\\}$ and the transition rule
$\delta_{\mathtt{move_{1}}}$ (in Figure 1).

$\delta_{\mathtt{move_{1}}}:\mathtt{cl(A){,}cl(C){,}on(A,B)\xleftarrow{\makebox[51.21504pt]{
\scriptsize $\mathtt{0.9:move(A,B,C)}$ }}cl(A){,}cl(B){,}on(A,C)}$

By applying the substitution $\theta=\\{\mathtt{A/a,B/b}\\}$ to
$\delta_{\mathtt{move_{1}}}$, the pre-state can be obtained, as shown as
follows. This means that any concrete state that is subsumed by
$\mathtt{\\{cl(a),cl(b),on(a,C)\\}}$ can reach some state in $G$ by taking one
action $\mathtt{move(a,b,C)}$.

$\mathtt{cl(a),cl(b),on(a,C)\xrightarrow{0.9:move(a,b,C)}on(a,b)}$

A reachability path formula $\mathtt{\psi=[F^{\leq k}\;\cdot]}$ can be
computed by recursively applying logical regression for $\mathtt{k}$ steps. In
particular, relational regression identifies all states $S$ that qualitatively
satisfy $\mathtt{[F^{\leq k}\;\cdot]}$. Figure 4 shows an example with
$\mathtt{k}=2$.

Figure 3:  The figure shows the derived paths by applying two logical
regressions on $\\{\mathtt{on(a,b)}\\}$ with $\delta_{move_{1}}$. The abstract
states from left to right reach $\\{\mathtt{on(a,b)}\\}$ with probabilities
$0.81$, $0.9$ and $1.0$, respectively444The probabilities are calculated by
Equation 1. More details in Section 4.3 and 4.4. . This means that all these
abstract states satisfy $\mathtt{P_{\geq 0.7}[F^{\leq 2}\;on(a,b)]}$.

Equation 3 \small{1}⃝ is implemented in Regression (Algorithm 2) by using
logical regression. Regression considers one step and identifies all states
that satisfy a path formula with $\mathtt{F^{\leq 1}}$, $\mathtt{U^{\leq 1}}$
or $\mathtt{X}$. The path operators $\mathtt{U^{\leq 1}}$ and $\mathtt{X}$ are
actually a $\mathtt{F^{\leq 1}}$ operator with additional constraints. That
is, the $\mathtt{S_{1}}\;\mathtt{U^{\leq 1}}\mathtt{S_{2}}$ formula, so called
the constrained reachability, imposes the constraint of going through only the
states where $\mathtt{S_{1}}$ holds. The $\mathtt{X}\;\mathtt{S_{2}}$ formula
imposes the constraint that $\mathtt{S_{2}}$ must be reached after taking
exactly one transition. Regression generalizes the WEAKESTPRE algorithm from
REBEL (Kersting et al., 2004) in two ways. The generalized part is marked
blue. First, for the case that the given formula is of the form
$\mathtt{S_{1}\;U^{\leq k}S_{2}}$, Regression ensures that all pre-states must
satisfy $\mathtt{S_{1}}$. Second, to support infinite RMDPs, Regression must
filter the pre-states by a given state bound $b$. More details will be given
in Section 6.3.

$Pre_{i}:=\emptyset$

foreach  _$\mathtt{S_{2}^{\prime}}\subseteq\mathtt{S_{2}}$ and
$\mathtt{H_{i}^{\prime}}\subseteq H_{i}$ s.t.
$\theta=\mathit{unifier}(\mathtt{S_{2}^{\prime}},\mathtt{H_{i}^{\prime}})$
exists_ do

$\mathtt{S}:=(\mathtt{S_{2}}\theta\backslash\mathtt{H_{i}^{\prime}}\theta)\cup
B\theta$

// identify a pre-state $\mathtt{S}$

foreach  _$l\in(\mathtt{S_{2}}\theta\backslash\mathtt{H_{i}^{\prime}}\theta)$
and $l^{\prime}\in H_{i}\theta\cup B\theta$ s.t. $unifier(l,l^{\prime})$
exists _ do

add $l\neq l^{\prime}$ to $\mathtt{S}$

// add object inequalities to $\mathtt{S}$

$\mathtt{S_{pre}}:=mgs(\mathtt{S},\mathtt{S_{1}})$

// apply the $\mathtt{S_{1}}$ constraint

foreach  _ $\mathtt{s_{pre}}\in\mathtt{S_{pre}}$_ do

if  _$|terms(\mathtt{s_{pre}})|\leq$ b_ then add $\mathtt{s_{pre}}$ to
$Pre_{i}$

// apply the state bound555The state bound $b\in\mathbb{N}$ is for infinite
RMDPs. More details in Section 6.

return $Pre_{i}$

Algorithm 2 Regression$(\delta,\mathtt{S_{1}},\mathtt{S_{2}})$ returns all
states that reach $\mathtt{S_{2}}$ by only going through states subsumed by
$\mathtt{S_{1}}$ by following an action rule
$\delta=H_{i}\xleftarrow{p_{i}:\alpha}B$. $\mathtt{S_{1}}$ and
$\mathtt{S_{2}}$ are abstract states. All returned states must be legal and
respect the OI assumption. Regression implements Equation 3 ①.

###  4.3 Q-Rules Generation

This section explains the calculation of the Q values for all state-action
pairs (cf. Equation 3 ②). In this step, for a state $s$, we must consider each
possible action $a\in A(s)$ and calculate its expected probability $Q(s,a)$.
Later, the resulting Q function will be maximized over the actions (cf.
Section 4.4). Equation 3 ② is implemented in QRules (Algorithm 3).

This algorithm is relatively complex since it operates at the relational level
and is required to combine abstract Q-rules. First, it creates the partial
Q-rules of a given V-rule and an abstract transition. Each of these partial
Q-rules considers only one single post-condition $H_{i}$ thus is not complete.
Then, to integrate all post-conditions $H_{1},...,H_{n}$, the partial Q-rules
must be combined by unifying their actions. This results in the final
$Q(s,a)$. Furthermore, it calculates the Q-rules for all possible actions at
once. QRules modifies the QRULES algorithm in REBEL (Kersting et al., 2004) in
two ways. The modified part is marked blue. First, for the case that the given
formula is of the form $\mathtt{S_{1}\;U^{\leq k}S_{2}}$, QRules must pass an
extra parameter $\mathtt{S_{1}}$ to Algorithm 2. Second, it computes the
special case of the general Bellman operator that has no reward component and
the discount factor is 1.

$Q_{t+1}:=\emptyset$

/* fix an action $\alpha$ */

foreach  _$H_{i}\xleftarrow{p_{i}:\alpha}B$ for $\alpha$_ do

foreach  _$v\leftarrow V\in V_{t}$_ do

$Pre_{i}$ :=
Regression$(H_{i}\xleftarrow{p_{i}:\alpha}B,{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathtt{S_{1}}},V)$

/* derive a subset of Q-rules */

$partialQ:=\\{q:A\leftarrow S|S\in Pre_{i}\mbox{ and
}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}q=p_{i}\times
V_{t}(V)}\mbox{ and }A=\alpha\theta\\}$

if  _$Q_{t+1}=\emptyset$_ then $Q_{t+1}:=partialQ$

else

$newQ:=\emptyset$

_ _ for  _all pairs $q_{1}:A_{1}\leftarrow S_{1}\in Q_{t+1}$ and _

 __ $q_{2}:A_{2}\leftarrow S_{2}\in partialQ$ do

/* combine the Q-rules by unifying the state-action pairs */

if  _$A\leftarrow S:=mgs(A_{1}\leftarrow S_{1},A_{2}\leftarrow S_{2})$ exists_
then

$q:=q_{1}+q_{2}$

add $q:A\leftarrow S$ to $newQ$

$Q_{t+1}:=newQ$

return $Q_{t+1}$

Algorithm 3 QRules$(V_{t},\mathtt{S_{1}})$ returns the Q-rules of all state-
action pairs, i.e. $Q_{t+1}(s,a)$, given the previous state value function
$V_{t}$ and the abstract state $\mathtt{S_{1}}$. All $s$ in $Q_{t+1}(s,a)$
must be subsumed by $\mathtt{S_{1}}$. All returned Q-rules must be legal and
respect the OI assumption. QRules implements Equation 3 ②.

###  4.4 V-Rules Generation

This section calculates the new state value function $V_{t+1}$ by maximizing
the state action value function $Q_{t+1}$ (cf. Equation 3 ③). Equation 3 ③ is
implemented in VRules (Algorithm 4). VRules orders the Q-rules in
$Q_{t+1}(s,a)$ decreasingly, and removes redundant Q-rules. It orders the
Q-rules decreasingly so that a state is always assigned a maximum probability
(as defined in Equation 2). A Q-rule $q$ is redundant if it is subsumed by
some other $q^{\prime}$ that has a higher Q-value. This means that redundant
Q-rules are never used to assign probabilities to any state action pairs.

VRules generalizes the VRULES algorithm in REBEL (Kersting et al., 2004) to
handle non-absorbing goal states for the next operator $\mathtt{X\;S_{2}}$.
The generalized part is marked blue. VRules treats the until formula
$\mathtt{S_{1}\;U^{\leq k}\;S_{2}}$ and the next formula $\mathtt{X\;S_{2}}$
differently. On one hand, since the formula $\mathtt{S_{1}\;U^{\leq
k}\;S_{2}}$ contains the absorbing goal state $\mathtt{S_{2}}$,
$\mathtt{S_{2}}$ must be used to eliminate redundant rules. On the other hand,
since $\mathtt{S_{2}}$ in $\mathtt{X\;S_{2}}$ is not absorbing666Due to the
constraint of reaching $\mathtt{S_{2}}$ after exactly one step,
$\mathtt{S_{2}}$ is not used for eliminating rules, resulting in an empty
$Q_{abs}$.

$V_{t+1}:=\emptyset$

sort $Q_{t+1}$ in decreasing order of Q-values

/* Add absorbing Q-rules */

if  _$\psi=\mathtt{S_{1}\;U^{\leq k}S_{2}}$_ then
$Q_{abs}:=\\{1.0:\mathtt{\emptyset\leftarrow S|S\in S_{2}}\\}$

else $Q_{abs}:=\emptyset$

$Q_{t+1}:=Q_{abs}+Q_{t+1}$

// attach absorbing Q-rules to the top of $Q_{t+1}$

while  _$Q_{t+1}\neq\emptyset$_ do

remove the top Q-rule $d:A\leftarrow B$ from their $Q_{t+1}$

if  _no other rule $d:A^{\prime}\leftarrow B^{\prime}$ in $Q_{t+1}$ exists
s.t. $B^{\prime}$ subsumes $B$_ then

add $d\leftarrow B$ to $V_{t+1}$

/* remove redundant Q-rules */

remove all rules $d^{\prime\prime}\leftarrow B^{\prime\prime}$ from $Q_{t+1}$
s.t. $B$ subsumes $B^{\prime\prime}$

return $V_{t+1}$

Algorithm 4 VRules$(Q_{t+1},\psi)$ returns $V_{t+1}$ by maximizing over the
given Q-rule $Q_{t+1}$ for a pCTL formula $\psi$. For the formula
$\psi=\mathtt{S_{1}\;U^{\leq k}S_{2}}$, $\mathtt{S_{2}}$ is used to eliminate
redundant Q-rules. All returned V-rules must be legal and respect the OI
assumption. VRules implements Equation 3 ③.

###  4.5 An Illustration of the Relational Bellman Operator

This section illustrates applying relational Bellman operator (Equation 3) in
relational value iteration with examples. Relational value iteration can
handle pCTL path formulas with abstract states, namely, $\mathtt{X\;S_{2}}$,
$\mathtt{S_{1}\;U^{\leq k}S_{2}}$ and $\mathtt{S_{1}\;U\;S_{2}}$ where
$\mathtt{S_{1}}$ and $\mathtt{S_{2}}$ are abstract states. Recall that in each
iteration, the relational Bellman operator takes a state value function
$V_{t}$ and computes $V_{t+1}$. One iteration is required for
$\mathtt{X\;S_{2}}$, $\mathtt{k}$ iterations are required for
$\mathtt{S_{1}\;U^{\leq k}S_{2}}$, and arbitrarily many iterations are
required to get an accurate enough approximation for
$\mathtt{S_{1}\;U\;S_{2}}$. We consider the blocks world domain and two
formulas.

$\delta_{\mathtt{move_{1}}}:\mathtt{cl(A){,}cl(C){,}on(A,B)\xleftarrow{\makebox[51.21504pt]{
\scriptsize $\mathtt{0.9:move(A,B,C)}$ }}cl(A){,}cl(B){,}on(A,C)}$
$\delta_{\mathtt{move_{2}}}:\mathtt{cl(A){,}cl(B){,}on(A,C)\xleftarrow{\makebox[51.21504pt]{
\scriptsize $\mathtt{0.1:move(A,B,C)}$ }}cl(A){,}cl(B){,}on(A,C)}$

Formula 1 $\psi_{2}=\mathtt{X\;on(a,b)}$:

Find all states that reach $\mathtt{on(a,b)}$ in the next state.

Formula 2 $\psi_{1}=\mathtt{on(c,d)\;U^{\leq 1}on(a,b)}$:

Find all states that reach $\mathtt{on(a,b)}$ within 1 step by going through
only the states where $\mathtt{on(c,d)}$ holds.

#### Relational Bellman Operator on Formula 1: $\mathtt{X\;on(a,b)}$

For the formula $\psi_{1}=\mathtt{X\;on(a,b)}$, the initial function $V_{0}$
is

  * $1.0\leftarrow\mathtt{on(a,b)}$

  * $0.0\leftarrow\emptyset$

① After applying Regression on $\psi_{1}$ using the transition
$\delta_{\mathtt{move_{1}}}$, namely Regression$(\delta_{\mathtt{move_{1}}}$,
$\emptyset$, $\mathtt{on(a,b)})$777The second argument is $\emptyset$ as the
$\mathtt{X}$ operator does not impose constraints on pre-states (unlike
$\psi_{2}$ that will come later)., the following set $Pre_{1}$ of pre-states
is obtained. These pre-states respect the OI assumption that we omit the
object inequalities here. A similar set $Pre_{2}$ of pre-states after
following $\delta_{\mathtt{move_{2}}}$ can be obtained, which is not listed
here.

  * $\mathtt{S_{1}}=\mathtt{cl(a),cl(b),on(a,Z)}$

  * $\mathtt{S_{2}}=\mathtt{cl(X),cl(a),on(X,Z),on(a,b)}$

  * $\mathtt{S_{3}}=\mathtt{cl(X),cl(Y),on(X,a),on(a,b)}$

  * $\mathtt{S_{4}}=\mathtt{cl(X),cl(Y),on(X,Z),on(a,b)}$

② QRule$(V_{0},\emptyset)$888The second argument is $\emptyset$ as the
$\mathtt{X}$ operator does not have absorbing goals (unlike $\psi_{2}$ that
will come later). assigns values to the pre-states $Pre_{1}$ and $Pre_{2}$,
and combines the rules to obtain $Q_{1}(s,a)$ for all state-action pair. The
obtained Q-rules are listed as follows. All rules respect the OI assumption.

$\displaystyle\langle 1\rangle$
$\displaystyle\;1.0:\mathtt{move(X,a,Z)\leftarrow
cl(X),cl(a),on(X,Z),on(a,b)}$ $\displaystyle\langle 2\rangle$
$\displaystyle\;1.0:\mathtt{move(X,Y,a)\leftarrow
cl(X),cl(Y),on(X,a),on(a,b)}$ $\displaystyle\langle 3\rangle$
$\displaystyle\;1.0:\mathtt{move(X,Y,Z)\leftarrow
cl(X),cl(Y),on(X,Z),on(a,b)}$ $\displaystyle\langle 4\rangle$
$\displaystyle\;0.9:\mathtt{move(a,b,Z)\leftarrow cl(a),cl(b),on(a,Z)}$
$\displaystyle\langle 5\rangle$
$\displaystyle\;0.9:\mathtt{move(X,a,Z)\leftarrow
cl(X),cl(a),on(X,Z),on(a,b)}$ $\displaystyle\langle 6\rangle$
$\displaystyle\;0.9:\mathtt{move(X,Y,a)\leftarrow
cl(X),cl(Y),on(X,a),on(a,b)}$ $\displaystyle\langle 7\rangle$
$\displaystyle\;0.9:\mathtt{move(X,Y,Z)\leftarrow
cl(X),cl(Y),on(X,Z),on(a,b)}$ $\displaystyle\langle 8\rangle$
$\displaystyle\;0.1:\mathtt{move(a,Y,b)\leftarrow cl(a),cl(Y),on(a,b)}$
$\displaystyle\langle 9\rangle$
$\displaystyle\;0.1:\mathtt{move(X,a,Z)\leftarrow
cl(X),cl(a),on(X,Z),on(a,b)}$ $\displaystyle\langle 10\rangle$
$\displaystyle\;0.1:\mathtt{move(X,Y,a)\leftarrow
cl(X),cl(Y),on(X,a),on(a,b)}$ $\displaystyle\langle 11\rangle$
$\displaystyle\;0.1:\mathtt{move(X,Y,Z)\leftarrow
cl(X),cl(Y),on(X,Z),on(a,b)}$ $\displaystyle\langle 12\rangle$
$\displaystyle\;0.0:\mathtt{move(X,Y,Z)\leftarrow cl(X),cl(Y),on(X,Z)}$

③ VRule$(Q_{1},\psi_{1})$ removes redundant Q-rules, drops the action
component in the non-redundant Q-rules to obtain $V_{1}$. The V-rules in
$V_{1}$ are shown as follows. The numbering of the V-rules inherits the one
for the Q-rules.

$\displaystyle\langle 1\rangle$
$\displaystyle\;1.0\leftarrow\mathtt{cl(X),cl(a),on(X,Z),on(a,b)}$
$\displaystyle\langle 2\rangle$
$\displaystyle\;1.0\leftarrow\mathtt{cl(X),cl(Y),on(X,a),on(a,b)}$
$\displaystyle\langle 3\rangle$
$\displaystyle\;1.0\leftarrow\mathtt{cl(X),cl(Y),on(X,Z),on(a,b)}$
$\displaystyle\langle 4\rangle$
$\displaystyle\;0.9\leftarrow\mathtt{cl(a),cl(b),on(a,Z)}$
$\displaystyle\langle 8\rangle$
$\displaystyle\;0.1\leftarrow\mathtt{cl(a),cl(Y),on(a,b)}$
$\displaystyle\langle 12\rangle$
$\displaystyle\;0.0\leftarrow\mathtt{cl(X),cl(Y),on(X,Z)}$

We have applied the relational Bellman operator to the formula
$\mathtt{X\;on(a,b)}$ to obtain $V_{1}$. $V_{1}$ assigns to all states the
maximum probability of reaching $\mathtt{on(a,b)}$ after one step.

#### Relational Bellman Operator on Formula 2: $\mathtt{on(c,d)\;U^{\leq
1}on(a,b)}$

For the formula $\psi_{2}=\mathtt{on(c,d)\;U^{\leq 1}on(a,b)}$, the initial
value function $V_{0}$ is

  * $1.0\leftarrow\mathtt{on(a,b)}$

  * $0.0\leftarrow\emptyset$

① After applying Regression on $\psi_{2}$ using the transition
$\delta_{\mathtt{move_{1}}}$, namely Regression$(\delta_{\mathtt{move_{1}}}$,
$\mathtt{on(c,d)}$, $\mathtt{on(a,b)})$, the following set $Pre_{1}$ of pre-
states is obtained. These pre-states respect the OI assumption that we omit
the object inequalities here. All pre-states satisfy the constraint
$\mathtt{on(c,d)}$. A similar set $Pre_{2}$ of pre-states after following
$\delta_{\mathtt{move_{2}}}$ can be obtained, which is not listed here.

  * $\mathtt{S_{1}}{=}\mathtt{cl(a),cl(b),on(a{,}Z),on(c{,}d)}$

  * $\mathtt{S_{2}}{=}\mathtt{cl(a),cl(b),on(a{,}c),on(c{,}d)}$

  * $\mathtt{S_{3}}{=}\mathtt{cl(X),cl(a),on(X{,}Z),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{4}}{=}\mathtt{cl(a),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{5}}{=}\mathtt{cl(c),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{6}}{=}\mathtt{cl(X),cl(a),on(X{,}c),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{7}}{=}\mathtt{cl(X),cl(Y),on(X{,}a),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{8}}{=}\mathtt{cl(X),cl(c),on(X{,}a),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{9}}{=}\mathtt{cl(X),cl(Y),on(X{,}Z),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{10}}{=}\mathtt{cl(a),cl(Y),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{11}}{=}\mathtt{cl(a),cl(c),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{12}}{=}\mathtt{cl(c),cl(Y),on(a{,}b),on(c{,}d)}$

  * $\mathtt{S_{13}}{=}\mathtt{cl(X),cl(Y),on(X{,}c),on(a{,}b),on(c{,}d)}$

② QRule$(V_{0},\mathtt{on(c,d)})$ assigns values to the pre-states $Pre_{1}$
and $Pre_{2}$, and combines the rules to obtain $Q_{1}(s,a)$ for all state-
action pair. The resulting $Q_{1}$ is the same as the one in the previous
example $\psi_{1}$ with the additional $\mathtt{on(c,d)}$. To avoid
redundancy, we do not list $Q_{1}$ here.
③ VRule$(Q_{1},\psi_{1})$ inserts the absorbing rule
$\mathtt{1.0:\emptyset\leftarrow on(a,b)}$ for the absorbing state
$\mathtt{on(a,b)}$, removes redundant Q-rules and then returns the compact
$V_{1}$. The V-rules in $V_{1}$ are as shown as follows.

$\displaystyle\;1.0\leftarrow\mathtt{on(a,b)}$
$\displaystyle\;0.9\leftarrow\mathtt{cl(a),cl(b),on(a{,}Z),on(c{,}d)}$
$\displaystyle\;0.9\leftarrow\mathtt{cl(a),cl(b),on(a{,}c),on(c{,}d)}$
$\displaystyle\;0.0\leftarrow\mathtt{cl(X),cl(Y),on(X{,}Z),on(c{,}d)}$

##  5 Main Contribution – the pCTL-REBEL Algorithm

This section introduces the main algorithm in this paper, pCTL-REBEL, that
solves the relational model checking problem (Section 3.3). Formally, given a
pCTL-REBEL $\phi$ and a RMDP $K$, pCTL-REBEL identifies the set
$Sat_{K}(\phi)$ of abstract states that represent all Herbrand interpretations
that satisfy $\phi$. PCTL-REBEL is based on relational value iteration
(Section 4) and operates at the relational level.

Different from relational value iteration (Section 4) that computes one single
operator $\mathtt{U^{\leq k}}$ or $\mathtt{X}$ at a time, pCTL-REBEL allows
for full relational pCTL formulas. In other words, pCTL-REBEL allows nested
formulas. It is standard practice to represented a (nested) pCTL or CTL
formula as a parse tree (Baier and Katoen, 2008). In a parse tree, each leaf
node is an abstract state and each inner node contains exactly one operator.
We give an example of a nested relational pCTL formula.

###### Example 7

A nested relational pCTL formula example is as follows.

$\displaystyle\phi_{\mathtt{nested}}=$ $\displaystyle\mathtt{P_{\geq
0.5}[cl(a)\;U^{\leq 4}(on(a,b)}\mathtt{\wedge P_{\geq 0.8}[P_{\geq
0.9}[X\;cl(e)]\;U^{\leq 2}on(c,d)])]}$

A state $s$ satisfies $\phi_{\mathtt{nested}}$ if and only if $s$ satisfies
the following three conditions: (1) $s$ reaches $\mathtt{on(a,b)}$ within 4
steps with a probability greater than 0.5 by going through only the states
where $\mathtt{cl(a)}$ holds. (2) Then, $s$ reaches $\mathtt{on(c,d)}$ within
2 steps with a probability greater than 0.8 by going through only a set of
states that satisfy $\phi_{1}=\mathtt{P_{\geq 0.9}[X\;cl(e)]}$. (3) The states
that satisfy $\mathtt{P_{\geq 0.9}[X\;cl(e)]}$ can enter $\mathtt{cl(e)}$ with
a probability greater than 0.9 after exactly one step. The nested formula
$\phi_{\mathtt{nested}}$ is complex at first sight, however, it can be
represented as a parse tree in Figure 4.

Figure 4: This is the parse tree of $\phi_{\mathtt{nested}}$. Each inner node
of the parse tree is annotated with a sub-formula $\phi_{i}$ and handles one
operator. $\phi_{1}$ handles $\mathtt{X}$, $\phi_{2}$ handles $\mathtt{U^{\leq
2}}$, $\phi_{3}$ handles $\land$ and $\phi_{4}$ handles $\mathtt{U^{\leq 4}}$.

pCTL-REBEL utilizes the parse tree of a given formula. A parse tree is
recursively evaluated upwards. Given the child states, every inner node
evaluates a sub-formula $\phi_{i}$ to produce $Sat(\phi_{i})$, and then folds
the sub-tree with $Sat(\phi_{i})$ so that the upper inner node can be
activated. The final set $Sat(\phi)$ is produced by the root. For example, in
Figure 4, the intermediate state set $Sat(\phi_{i})$ is used to evaluate
$Sat(\phi_{i+1})$. The state set $Sat(\phi_{4})$ is returned as the solution.

Section 5.1 defines the pCTL-REBEL algorithm, which is composed of three
mutually-recursive algorithms. Then, Section 5.2 gives an overview of the
features of pCTL-REBEL.

###  5.1 The pCTL-REBEL algorithm

The pCTL-REBEL algorithm reforms the satisfiability relation
$\models^{\theta}$ (Section 3.2). It decomposes a given formula $\phi$ into
its parse tree, and recursively evaluates the parse tree to compute
$Sat_{K}(\phi)$, i.e. all states in $K$ that satisfy $\phi$. To do so, pCTL-
REBEL consists of three mutually-recursive algorithms Check, CheckUntil and
CheckNext that call each other recursively. In particular, CheckUntil handles
the until formulas $\mathtt{P_{\bowtie p}[\phi_{1}\;U^{\leq k}\phi_{2}]}$,
CheckNext handles the next formulas $\mathtt{P_{\bowtie p}[X\;\phi_{2}]}$, and
Check handles any other operators.

Check (Algorithm 5) is always the first algorithm activated. It implements the
satisfiability relation $\models^{\theta}$ (Section 3.2). Given a RMDP $K$ and
a pCTL formula $\phi$, Check returns the set $Sat_{K}(\phi)$, i.e. all
abstract states that satisfy $\phi$ in $K$. Check decomposes $\phi$ based on
the outermost operator. When the given formula is a relation atom $l$, it
returns a set of a single abstract state $\\{l\\}$. When the given formula is
of the form $\phi_{1}\land\phi_{2}$, it first performs model checking to
$\phi_{1}$ and $\phi_{2}$, respectively, to get two sets of abstract states
$Sat1$ and $Sat2$. Then, for each possible pair of abstract states $s_{1}\in
Sat1$ and $s_{2}\in Sat2$, it collects all maximally general specialisations
$mgs(s_{1},s_{2})$ and returns them as output. Since each $mgs(s_{1},s_{2})$
is OI-subsumed by $s_{1}$ and $s_{2}$ by definition, it automatically
satisfies $\phi_{1}\land\phi_{2}$. When the outermost operator is a
$\mathtt{U}$ or $\mathtt{U^{\leq k}}$, it calls CheckUntil (Algorithm 6). When
the outermost operator is a $\mathtt{X}$, it calls CheckNext (Algorithm 7).

if  _$\phi$ = l_ then return {l}

if  _$\phi$ = $\neg l$_ then return {$\neg l$}

else if  _$\phi$ = $\phi_{1}\land\phi_{2}$_ then

return
$\\{mgs(s1,s2)\;|\;s1\in\mathtt{Check(\phi_{1})},s2\in\mathtt{Check(\phi_{2})}\\}$

else if  _$\phi$ = $\phi_{1}\lor\phi_{2}$_ then

return $\mathtt{Check(\phi_{1})}\cup\mathtt{Check(\phi_{2})}$

else if  _$\phi$ = $\mathtt{P}_{\bowtie p}[\phi_{1}\mathtt{U^{\leq
k}}\phi_{2}]$_ then

return CheckUntil($\phi$)

else if  _$\phi$ = $\mathtt{P}_{\bowtie p}[\mathtt{X}\;\phi_{2}]$_ then

return CheckNext($\phi$)

Algorithm 5 Check$(\phi)$ returns the set $Sat_{K}(\phi)$ of states in $K$
that satisfy $\phi$ by recursively evaluating the parse tree of $\phi$. This
is a realization of the satisfiability relation (Section 3.2). Check is
mutually recursive with CheckUntil and CheckNext.

CheckUntil (Algorithm 6) is mutually recursive with Check (Algorithm 5). It is
called when the given formula has an until operator. Based on the until
operator, CheckUntil decomposes the formula into two sub-formulas, and calls
Check to obtain two corresponding sets of abstracts states. It uses the
relational Bellman operator (Algorithm 1) to compute the unbounded
$\mathtt{U}$ and the bounded $\mathtt{U^{\leq k}}$ operators. Specifically,
given a RMDP $K$ and a pCTL until formula of the form $\phi=\mathtt{P_{\bowtie
p}[\phi_{1}U^{\leq k}\phi_{2}]}$ or $\phi=\mathtt{P_{\bowtie
p}[\phi_{1}U\phi_{2}]}$, CheckUntil returns $Sat_{K}(\phi)$, i.e. all abstract
states that satisfy $\phi$ in $K$. CheckUntil implements a value iteration
algorithm. When the given formula has a bounded $\mathtt{U^{\leq k}}$
operator, $\mathtt{k}$ iterations are performed. When the given formula has a
unbounded $\mathtt{U}$ operator, $\mathtt{k}$ is set to infinity, and
relational value iteration is performed until convergence. The convergence
condition of CheckUntil is twofold. First, the abstract states in the value
function do not change, i.e. states in $V_{t}$ and $V_{t-1}$ are the same.
Second, the state values do not change more than a given threshold $\epsilon$,
i.e. $\max_{s\in V_{t}}V_{t}(s)-V_{t-1}(s)<\epsilon$. After value iteration is
done and the final value function $V_{t}$ is obtained, CheckUntil collects and
returns the abstract states in $V_{t}$ that satisfy the given probability
threshold $\mathtt{\bowtie p}$.

$\mathtt{S_{1}}:=$ Check$(\phi_{1})$

$\mathtt{S_{2}}:=$ Check$(\phi_{2})$

if  _$\mathtt{k}$ is not given_ then $\mathtt{k}:=\infty$

// set k as infinity for unbounded U

$V_{0}:=\\{1.0\leftarrow
s|s\in\mathtt{S_{2}}\\}\cup\\{0\leftarrow\emptyset\\}$

// Initialize $V_{0}$

$t:=0$

// t is the number of iterations so far

$\epsilon^{\prime}:=\infty$

// $\epsilon^{\prime}$ is the distance between $V_{t}$ and $V_{t+1}$

while  _$t <\mathtt{k}$ or $\epsilon^{\prime}\geq\epsilon$_ do

$V_{t+1}$ := OneIteration$(V_{t},\mathtt{S_{1}\;U^{\leq k}S_{2}})$

$\epsilon^{\prime}:=V_{t+1}$ \- $V_{t}$

$t:=t+1$

$Sat_{K}(\phi):=\emptyset$

foreach  _$p_{i}\leftarrow s_{i}\in V_{t}$_ do

if  _$p_{i}\bowtie\mathtt{p}$_ then add $s_{i}$ to $Sat_{K}(\phi)$

return $Sat_{K}(\phi)$

Algorithm 6 CheckUntil$(\phi)$ returns the set $Sat_{K}(\phi)$ of states in
$K$ that satisfy $\phi$, where $\phi$ is of the form of $\mathtt{P_{\bowtie
p}[\phi_{1}U^{\leq k}\phi_{2}]}$ or $\mathtt{P_{\bowtie
p}[\phi_{1}U\phi_{2}]}$. CheckUntil uses relational value iteration
(OneIteration, Algorithm 1). CheckUntil is mutually recursive with Check.

CheckNext (Algorithm 7) is mutually recursive with Check (Algorithm 5). It is
called by Check when the given formula is of the form $\phi=\mathtt{P_{\bowtie
p}[X\;\phi_{2}]}$, and it calls Check to obtain the set of abstracts states
that satisfy the sub-formula $\phi_{2}$. CheckNext computes the $\mathtt{X}$
operator. Specifically, given a RMDP $K$ and a pCTL next formula of the form
$\phi=\mathtt{P_{\bowtie p}[X\;\phi_{2}]}$, CheckNext returns $Sat_{K}(\phi)$,
i.e. all abstract states that satisfy $\phi$ in $K$. CheckNext calls the
relational Bellman operator (Algorithm 1) once to obtain the final value
function $V_{1}$. Then it collects and returns the abstract states in $V_{1}$
that satisfy the given probability threshold $\mathtt{\bowtie p}$. CheckNext
needs only one iteration as it is only required to look ahead for one time
step for the next operator.

$\mathtt{S_{2}}$ = Check$(\phi_{2})$

$V_{0}:=\\{1.0\leftarrow
s|s\in\mathtt{S_{2}}\\}\cup\\{0\leftarrow\emptyset\\}$

$V_{1}$ := OneIteration$(V_{0},\mathtt{X\;S_{2}})$

$Sat_{K}(\phi):=\emptyset$

foreach  _$p_{i}\leftarrow s_{i}\in V_{1}$_ do

if  _$p_{i}\bowtie\mathtt{p}$_ then add $s_{i}$ to $Sat_{K}(\phi)$

return $Sat_{K}(\phi)$

Algorithm 7 CheckNext$(\phi)$ returns the set $Sat_{K}(\phi)$ of states in $K$
that satisfy $\phi$, where $\phi$ is of the form of $\mathtt{P_{\bowtie
p}[\mathtt{X}\;\phi_{2}]}$. CheckNext uses relational value iteration
(OneIteration, Algorithm 1). CheckNext is mutually recursive with Check.

###  5.2 Properties of pCTL-REBEL

PCTL-REBEL is a relational model checking algorithm that finds a set
$Sat_{K}(\phi)$ of states in a RMDP $K$ that represents all states that
satisfy $\phi$. We discuss the properties of pCTL-REBEL.

Lifted

Rather than working at the ground level, pCTL-REBEL performs lifted inference
as both the formula and the states are specified at an abstract level using
relational representations. This allows pCTL-REBEL to exploit relational
symmetries in the model and make abstraction of the domain size, thus mitigate
the state explosion problem. The lifted inference was discussed in detail in
Section 4.

Sound for step-bounded pCTL formulas

PCTL-REBEL is sound for finite RMDPs (that have a finite domain) and any
bounded pCTL formulas. That is, it finds pCTL-REBEL is not sound for the step-
unbounded operator $\mathtt{U}$, just like many other value iteration
algorithms. This is because pCTL-REBEL uses a naive termination criterion with
some arbitrary convergence threshold $\epsilon$ (see CheckUntil, Algorithm 6).
Although this naive stopping criterion is not sound, it achieves precise
approximation in practice. We refer the details to Haddad and Monmege (2014).

Complete

PCTL-REBEL is complete for finite RMDPs. That is, it assigns state values to
all states in the given model. PCTL-REBEL captures the entire state space by
using abstract states in the value function. Specifically, the value function
assigns state values using an order set of V-rules (containing abstract
states). Those states that are not captured by the previous V-rules are
guaranteed to be assigned a value 0 by the last V-rule $0\leftarrow\emptyset$
(Section 4.1).

##  6 Relational Model Checking for Infinite MDPs

As discussed in Section 3.3, it is clear that when the domain is finite, the
model checking problem is decidable as one can enumerates all states in the
model. However, when the domain is infinite, the state space can be infinite,
making enumerating all states infeasible. This section considers decidability
of a special class of infinite RMDPs. Under the state-boundedness condition
(Belardinelli et al., 2011), a finite abstraction of an infinite RMDP can be
constructed. Checking the finite abstraction instead of the underlying
infinite model makes the model checking problem decidable. This section adopts
the approach of Belardinelli et al. (2011) to construct a finite abstraction
of such infinite RMDPs.

This section also shows that pCTL-REBEL naturally handles the finite
abstraction of some infinite RMDP. pCTL-REBEL does so since it reasons at the
relational level, where an abstract state represents an infinite number of
Herbrand interpretations. When reasoning about an abstract state, pCTL-REBEL
actually reasons about an infinite number of Herbrand interpretations at once.

Section 6.1 defines a finite abstraction of a given infinite RMDP under the
state-boundedness condition. Section 6.2 proves that checking a relational
pCTL formula $\phi$ against the finite abstraction is equivalent to checking
$\phi$ against the infinite RMDP. Section 6.3 shows that pCTL-REBEL can handle
an infinite, state-bounded RMDP.

###  6.1 Abstract MDP: a Finite Abstraction of an Infinite RMDP

In general, the relational model checking problem is undecidable due to the
possibly infinite domain. To obtain decidability, this section constructs a
finite abstraction of a given infinite RMDP, called the abstract RMDP, under
the state-boundedness condition. Later the abstract RMDP can be used to obtain
decidable model checking.

The state-boundedness condition states that any state concerns only a finite
number of objects. Since this imposes no restrictions on the domain size, a
state-bounded RMDP can contain an infinite number of states. For example,
consider a blocks world where there are infinitely many blocks and a table
with a capacity $b$. An agent can take a block away or put a new block to the
table, but no more than $b$ blocks can be on the table at any moment. Hence,
the state bound is $b$. Since any two states can describe totally different
blocks, the model still contains infinitely many states. We say the blocks on
the table are in the active domain. Now we formally define active domain and
state-boundedness.

###### Definition 6

An interpretation $s^{\prime}$ is a finite subset of a Herbrand interpretation
$s$ in some RMDP, i.e. $s^{\prime}\subseteq s$. The active domain of
$s^{\prime}$, denoted $\mathit{adom}(s^{\prime})$, is the set of all domain
objects in $s^{\prime}$.

Since an interpretation $s^{\prime}$ is finite, its active domain
$\mathit{adom}(s^{\prime})$ is finite as well. An interpretation $s^{\prime}$
is like an Herbrand interpretation but concerns only a finite number of
objects. That is, atoms in $s^{\prime}$ are $true$ and atoms not in
$s^{\prime}$ are $false$.

###### Definition 7

Given a RMDP $K=\langle\Sigma,\Delta\rangle$, its underlying MDP $M=\langle
S,A,T\rangle$, a state bound $b$, and a starting interpretation $s_{0}$ such
that $|\mathit{adom}(s_{0})|\leq b$, a MDP $M_{b}=\langle
S_{b},A_{b},T_{b}\rangle$ can be defined by including all interpretations that
are reachable from $s_{0}$ and contain at most $b$ constants. Formally,
$M_{b}=\langle S_{b},A_{b},T_{b}\rangle$ is defined as

$\displaystyle S_{b}$ $\displaystyle:=\\{s\;|\;s\in S,|\mathit{adom}(s)|\leq
b\\}$ $\displaystyle T_{b}$ $\displaystyle:=\\{h\xleftarrow{p:a}b\in T|h\in
S_{b},b\in S_{b}\\}$ $\displaystyle A_{b}$
$\displaystyle:=\\{a|h\xleftarrow{p:a}b\in T_{b}\\}$

If $b\in\mathbb{N}$, then $M_{b}$ is called state-bounded or $b$-bounded.

The b-bounded MDP $M_{b}$ is uniquely defined for an RMDP and a state bound.
Roughly speaking, $M_{b}$ a sub-MDP of $M$ that concerns at most $b$ object in
any state.

###### Example 8

Consider a blocks world $K=\langle\Sigma,\Delta\rangle$ with $\Sigma=\langle
R,D\rangle$ where $R=\mathtt{\\{cl/1,on/2\\}}$,
$D=\\{\mathtt{bl_{i}}|i\in\mathbb{N}\\}$ is infinite, and $\Delta$ contains
the following rules (as in Figure 1).

$\delta_{\mathtt{move_{1}}}:\mathtt{cl(A){,}cl(C){,}on(A,B)\xleftarrow{\makebox[51.21504pt]{
\scriptsize $\mathtt{0.9:move(A,B,C)}$ }}cl(A){,}cl(B){,}on(A,C)}$
$\delta_{\mathtt{move_{2}}}:\mathtt{cl(A){,}cl(B){,}on(A,C)\xleftarrow{\makebox[51.21504pt]{
\scriptsize $\mathtt{0.1:move(A,B,C)}$ }}cl(A){,}cl(B){,}on(A,C)}$

Given a state-bound $b$, $K$ defines a $b$-bounded MDP $M_{b}=\langle
S_{b},A_{b},T_{b}\rangle$ such that each interpretation $s_{b}\in S_{b}$
contains at most $b$ blocks. Any block that is not in $s_{b}$ does not exist.
We will use this blocks world example throughout this section.

Not all domain objects in a state-bounded MDP are relevant for checking a
relational pCTL formula. By abstracting away the irrelevant objects, an
abstraction $M_{\phi}$ of a state-bounded MDP $M_{b}$ can be constructed,
based on a given relational pCTL formula $\phi$. Checking $\phi$ against
$M_{\phi}$ is equivalent to checking $\phi$ against $M$. This is done by
preserving all $\phi$-relevant domain objects, and abstracting all other
objects with variables. The $\phi$-relevant domain objects are defined as
$consts(\phi)\cup consts(\Delta)$, namely, the domain objects that $\phi$
explicitly concerns. Furthermore, if the formula $\phi$ concerns a finite
number of objects, the abstraction $M_{\phi}$ is finite. We assume all
formulas contain at most $b$ objects where $b$ is the state bound of $M$.

The abstraction $M_{\phi}$ of a given a state-bounded MDP $M_{b}$ and a pCTL
formula $\phi$ is an abstract RMDP (ARMDP). An ARMDP is just like a finite
RMDP but allows for variables.

###### Definition 8

For a $b$-bounded MDP $M_{b}=\langle S_{b},A_{b},T_{b}\rangle$ of a RMDP
$K=\langle\Sigma,\Delta\rangle$ and a relational pCTL formula $\phi$ that
contains at most $b$ constants, a $b$-bounded abstract RMDP (ARMDP)
$M_{\phi}=\langle S_{\phi},\Sigma,\Delta,V\rangle$ is defined where

$\displaystyle S_{\phi}=\\{s_{\phi}|$ $\displaystyle\exists s\in
S_{b}.\;s\preceq_{\theta}s_{\phi},$ $\displaystyle consts(s_{\phi})\subseteq
consts(\phi)\cup consts(\Delta),$ $\displaystyle vars(s_{\phi})\subseteq V\\}$

and $V$ is a set of $b-|consts(\phi)\cup consts(\Delta)|$ distinct variables.
All terms in $s_{\phi}\in S_{\phi}$ are from a finite set of terms

$terms(S_{\phi}):=V\cup consts(\phi)\cup consts(\Delta)$

It is assumed that $vars(\phi)\in V$. It is assumed that states in $S_{\phi}$
are not syntactic variants, that is, they are not a variable renaming of one
another.

Structurally, an ARMDP resembles a finite RMDP but allows for variables. A
$b$-bounded ARMDP $M_{\phi}=\langle S_{\phi},\Sigma,\Delta,V\rangle$ is finite
since only a finite number of terms are allowed in the state space $S_{\phi}$.
Furthermore, each state $s_{\phi}\in S_{\phi}$ contains at most $b$ terms,
i.e. $\max\limits_{s_{\phi}\in S_{\phi}}|terms(s_{\phi})|=b$, and represents
an infinite set of Herbrand interpretations in the underlying MDP $M_{b}$.
Hence, a $b$-bounded ARMDP has bounded branching behavior, i.e. the number of
available actions in any state is finite. The bounded branching behavior
directly results from the state-boundedness condition.

###### Example 9

Consider the $b$-bounded MDP $M_{b}=\langle S_{b},A_{b},T_{b}\rangle$ in
example 8, $M_{b}$ and a given formula $\phi=\mathtt{cl(a)}$ defines an ARMDP
$M_{\phi}=\langle S_{\phi},\Sigma,\Delta,V\rangle$ where
$terms(S_{\phi})=\\{\mathtt{Bl_{1},Bl_{2},...,Bl_{b-1},a}\\}$.
$terms(S_{\phi})$ contains all allowed terms in $S_{\phi}$. The abstract
states $s_{1}=\\{\mathtt{cl(a)}\\}\in S_{\phi}$ and
$s_{2}=\\{\mathtt{cl(Bl_{1})}\\}\in S_{\phi}$ represent the set
$s\Theta\subseteq S$ of all Herbrand interpretations that have at least one
clear block. The set $s\Theta$ is infinite and can be enumerated by assigning
elements in $D$ to $\mathtt{Bl_{1}}$.

This section has identified a class of infinite RMDPs, namely the state-
bounded MDP, that has a finite abstraction. A finite abstraction ARMDP
$M_{\phi}$ can be constructed, given a state-bounded MDP $M_{b}$ and a pCTL
formula $\phi$. ARMDPs can be naturally handled by pCTL-REBEL for their
similarities to a finite RMDP. The next section will show that checking $\phi$
against $M_{\phi}$ is equivalent to checking $\phi$ against $M_{b}$.

###  6.2 Decidable Model Checking for ARMDPs

This section proves decidability of the model checking problem for a special
class of infinite RMDPs, namely, the ARMDP, which is defined in Section 6.1.
The decidability is obtained by proving that model checking the ARMDP yields
equivalent results as model checking the underlying infinite, state-bounded
MDP.

The aim of this section is to prove theorem 6.1. That is, the abstraction
$M_{\phi}$ constructed by a state-bounded MDP $M_{b}$ and a pCTL sentence
$\phi$ has sufficient information for model checking $\phi$.

###### Theorem 6.1

For a $b$-bounded MDP $M_{b}$ and its corresponding ARMDP $M_{\phi}$ based on
a pCTL sentence $\phi$, checking $\phi$ against $M_{\phi}$ is equivalent to
checking $\phi$ against $M_{b}$, formally,

$\displaystyle M_{b}\models\phi\Leftrightarrow M_{\phi}\models\phi$

Theorem 6.1 is proven by using probabilistic bisimulation. Probabilistic
bisimulation is a standard model checking technique to compare two
probabilistic transition systems (Baier and Katoen, 2008). If two states from
two transition systems are probabilistic bisimilar with respect to a pCTL
formula $\phi$, then their behaviors are indistinguishable with respect to
$\phi$. Hence, checking $\phi$ in either system yields identical results.
Theorem 6.1 extends the theorem by Belardinelli et al. (2011)[Theorem 2] for
the probabilistic setting999More specifically, as compared to their work, this
paper uses RMDPs instead of artifact systems, MDPs instead of Kripke
structures, Herbrand interpretations instead of databases, and probabilistic
bisimulation instead of bisimulation. .

We prove Theorem 6.1 in two steps. First, we define indistinguishable states
(Definition 9) and probabilistic bisimulation (Definition 10). Second, we show
that an ARMDP and its underlying state-bounded MDP actually define a
probabilistic bisimulation (Proposition 1 and 2).

###### Definition 9

Given a $b$-bounded MDP $M_{b}=\langle S_{b},A_{b},T_{b}\rangle$ and a pCTL
sentence $\phi$, consider two Herbrand interpretations $s_{1}$ and $s_{2}$ in
$S_{b}$ such that $C_{1}=consts(s_{1})\subset D$ and
$C_{2}=consts(s_{2})\subset D$. Let $C$ be a finite set all $\phi$-relevant
domain objects

$C:=consts(\phi)\cup consts(\Delta)\subseteq C_{1}\cap C_{2}$

$s_{1}$ and $s_{2}$ are called indistinguishable101010Indistinguishable states
are also commonly called isomorphic states. under $C$, if and only if $s_{1}$
and $s_{2}$ are renamings of one another for a bijection $f:C_{1}\setminus
C\mapsto C_{2}\setminus C$ for irrelevant domain objects. Formally,

$\displaystyle s_{1}\sim_{C}s_{2}\iff\;f(s_{1})=s_{2}$

We abuse the notation and let $f(s_{1})$ be the state of renaming constants in
$s_{1}$.

Definition 9 has defined the distinguishable states in a state-bounded MDP,
concerning different objects $C_{1}$, $C_{2}$, under a pCTL formula $\phi$.
Those indistinguishable states are essentially renamings of one another, hence
can be represented by the same abstract state in the corresponding ARMDP
$M_{\phi}$. As a consequence of Definition 8 and Definition 9, $M_{\phi}$ is
analogous to $M_{b}$, except for that $M_{\phi}$ allows for variables. We can
define a finite ARMDP $M_{\phi}$ that captures all (infinitely many)
indistinguishable states in $M_{b}$. Therefore, checking $M_{\phi}$ against
$\phi$ is decidable. The only thing left is to show checking $M_{\phi}$ yields
the same results as checking $M_{b}$. Specifically, we will prove $M_{\phi}$
is a probabilistic bisimulation of $M_{b}$.

###### Example 10

(Cont. Example 9) Consider a state-bounded blocks world $M_{b}=\langle
S_{b},A_{b},T_{b}\rangle$ of a pCTL formula $\phi=\mathtt{cl(a)}$ where the
state bound $b$ is 2. Two Herbrand interpretations
$s_{3}=\\{\mathtt{cl(b),on(b,a)})\\}\in S_{b}$ and
$s_{4}=\\{\mathtt{cl(c),on(c,a)})\\}\in S_{b}$ are indistinguishable under
$C=\\{\mathtt{a}\\}$ and a bijection $\mathtt{(b,c)}\in f$. That is, $s_{3}$
and $s_{4}$ are variable renamings of each other thus can be represented by
the abstract state $s_{5}=\\{\mathtt{cl(Bl_{1}),on(Bl_{1},a)}\\}$ in the
corresponding ARMDP $M_{\phi}$.

###### Definition 10

(cf. (Baier and Katoen, 2008)) Consider a $b$-bounded MDP $M_{b}=\langle
S_{b},A_{b},T_{b}\rangle$, a pCTL formula $\phi$ and the finite set $C$ of
$\phi$-relevant constants, $\mathcal{R}\subseteq S_{b}\times S_{b}$ is a
probabilistic bisimulation if for any pair of states $\langle
s_{1},s_{2}\rangle\in\mathcal{R}$:

  1. 1.

$s_{1}$ and $s_{2}$ are indistinguishable under $C$, i.e. $s_{1}\sim_{C}s_{2}$

  2. 2.

$s_{1}$ and $s_{2}$ have the identical probabilities of going to any other
distinguishable states, i.e. $\forall a\in A:P(s_{1},a,s)=P(s_{2},a,s)$ for
each $s\in S/\mathcal{R}$

$s_{1}$ and $s_{2}$ are probabilistic bisimilar.

Given the formal definition of probabilistic bisimulation, Propositions 1 and
2 will prove that an ARMDP and its underlying state-bounded MDP defines a
probabilistic bisimulation. That is, Theorem 6.1 is proven by Propositions 1
and 2.

###### Proposition 1

For an ARMDP $M_{\phi}=\langle S_{\phi},\Sigma,\Delta,V\rangle$ based on a
$b$-bounded MDP $M_{b}=\langle S_{b},A,_{b}T_{b}\rangle$ and a pCTL sentence
$\phi$, if two states are indistinguishable, then they either both can fire a
transition rule or both cannot fire a transition rule. Formally, for any
transition rule of the form

$H_{i}\xleftarrow{p_{i}:\alpha}B$

if $s_{1}\sim_{C}s_{2}$, then

$\displaystyle s_{1}\preceq_{\theta_{1}}B\iff s_{2}\preceq_{\theta_{2}}B$

for two indistinguishable substitutions $\theta_{1}$ and $\theta_{2}$.

###### Proposition 2

For an ARMDP $M_{\phi}=\langle S_{\phi},\Sigma,\Delta,V\rangle$ based on a
$b$-bounded MDP $M_{b}=\langle S_{b},A_{b},T_{b}\rangle$ and a pCTL sentence
$\phi$, if two states are indistinguishable, then they have the identical
probabilities of going to any other distinguishable states. Formally, for any
transition rule $\delta\in\Delta$ of the form

$\\{H_{1}\xleftarrow{p_{1}:\alpha}B,...,H_{n}\xleftarrow{p_{n}:\alpha}B\\}$

if $s_{1}\sim_{C}s_{2}$, then they define two sets of ground transition rules
$t(s_{1},a\theta_{1})$ and $t(s_{2},a\theta_{2})$ that share the same
transition probabilities.

$\displaystyle
t(s_{1},\alpha\theta_{1}):=\\{h_{1,i}\xleftarrow{p_{i}:\alpha\theta_{1}}s_{1}|$
$\displaystyle
H_{i}\xleftarrow{p:\alpha}B\in\delta,s_{1}\preceq_{\theta_{1}}B,$
$\displaystyle h_{1,i}=(s_{1}\backslash B\theta_{1})\cup H_{i}\theta_{1}\\}$
$\displaystyle
t(s_{2},\alpha\theta_{2}):=\\{h_{2,i}\xleftarrow{p_{i}:\alpha\theta_{2}}s_{2}|$
$\displaystyle
H_{i}\xleftarrow{p:\alpha}B\in\delta,s_{2}\preceq_{\theta_{2}}B,$
$\displaystyle h_{2,i}=(s_{2}\backslash B\theta_{2})\cup H_{i}\theta_{2}\\}$

Propositions 1 and 2 have shown that the indistinguishable relation $\sim_{C}$
between an ARMDP and its underlying state-bounded MDP is a probabilistic
bisimulation. $\sim_{C}$ is an equivalence relation that two probabilistic
bisimilar states exhibit identical behavior. In other words, the ARMDP and the
underlying MDP denote a mutual, step-wise simulation of indistinguishable
states. With a similar reasoning in (Belardinelli et al., 2011), we conclude
that the model checking problem for infinite, state-bounded MDPs is decidable
as it can be done on its corresponding finite ARMDP.

###  6.3 pCTL-REBEL for Infinite MDPs

PCTL-REBEL can handle an infinite, state-bounded RMDP by reasoning about its
finite abstraction. Specifically, given an infinite, state-bounded MDP $M$ and
a pCTL formula $\phi$, a finite ARMDP $M_{\phi}$ can be constructed and
naturally checked by pCTL-REBEL.

Since an ARMDP is just like a RMDP but concerns at most $b$ objects in a state
(Section 6.1), pCTL-REBEL requires only one adaption that restricts the state
size. That is, all states that have more than $b$ objects must be eliminated.
The number of objects in a state bound is simply obtained by counting all
variables and constants as OI assumption is imposed. The adaption of
maintaining the state bound is implemented in Regression (Algorithm 2) in
pCTL-REBEL. As pCTL-REBEL for an ARMDP is almost equivalent to pCTL-REBEL for
a RMDP, the only extra parameter required for an ARMDP is the state bound.

PCTL-REBEL for an infinite, state-bounded MDP is lifted and complete, just as
like pCTL-REBEL for a finite RMDP (Section 5.2). We discuss properties of
pCTL-REBEL for state-bounded MDPs in detail.

Lifted

PCTL-REBEL checks a state-bounded, infinite RMDP that has a finite abstraction
(namely, an ARMDP) at the lifted level. Specifically, pCTL-REBEL operates on
the ARMDP that is bisimilar to the underlying ground MDP. The lifted inference
for an ARMDP is just like for a finite RMDP with a state bound constraint.

Sound for step-bounded pCTL formulas

Just like in the finite RMDP case, pCTL-REBEL is sound for ARMDPs and any
bounded pCTL formulas. This is a consequence of Theorem 6.1 that shows
checking an ARMDP yields exactly the same results as its underlying MDP. More
specifically, for an ARMDP, pCTL-REBEL returns a set of abstract states that
are probabilistic bisimilar to all ground states in the underlying infinite
MDP that satisfy the formula.

Complete

PCTL-REBEL is complete for ARMDPs as it assigns a state value to all states.
PCTL-REBEL captures the entire state space using the abstract states in the
value function, just like in the case of finite RMDPs (see Section 5.2).

##  7 Experiments

We aim to answer the following questions in the is section. Q1 and Q2 focus on
the benefits of pCTL-REBEL. Q3-Q5 focus on the limitations of pCTL-REBEL.

  * Q1

What formulas can pCTL-REBEL check in practice?

  * Q2

How does pCTL-REBEL compare with state-of-the-art model checkers?

  * Q3

How well does pCTL-REBEL handle indefinite-horizon formulae?

  * Q4

How well does pCTL-REBEL handle a complex relational transition function?

  * Q5

How are the relative costs of the different pCTL operators?

We implemented and validated a (non-optimized) pCTL-REBEL research prototype
using SWI-Prolog 8.0.2, with the constraint handling rules library.
Experiments were run on a 2.4 GHz Intel i5 processor. The execution time was
estimated by SWI-Prolog’s built-in predicate
$\mathtt{statistics(run\\_time,\cdot)}$. We use the blocks world
dataset111111https://qcomp.org/benchmarks/#blocksworld and the boxworld
dataset121212https://qcomp.org/benchmarks/#boxworld. We compare pCTL-REBEL
with the state-of-the-art model checkers PRISM (Kwiatkowska et al., 2011) and
STORM (Dehnert et al., 2017)131313The experiments will be made public once the
paper is accepted. We set a time-out of 1800 seconds for all model checkers.
PCTL-REBEL’s state bound is sometimes referred as number of blocks/cities so
as to provide a direct comparison with PRISM and STORM.

The blocks world and the box world datasets originate from
IPPC-2008141414http://ippc-2008.loria.fr/wiki/index.php/Results.html#Fully_Observable_Non-
Deterministic_.28FOND.29_track_2 and are originally specified in the ppddl
language. STORM and PRISM operate on the converted prism-format files151515The
ppddl models are first converted to the jani format by the ppddl2jani tool
(attached in the datasets), then converted to the prism format by ePMC (Hahn
et al., 2014). , and pCTL-REBEL operates on the converted prolog-format
files161616The ppddl models are translated to prolog models as PCTL-REBEL is
implemented in prolog. . We discard the reward structure in the model. The
blocks world dataset is simplified to have the relations
$\mathtt{on/2,clear/1}$ and the action $\mathtt{move/3}$ with a success
probability of 0.9. The box world dataset has the relations
$\mathtt{bin/2,on/2,tin/2,can\mathchar 45\relax drive/2}$ and the actions
$\mathtt{drive/3,load/2,unload/2}$. In the box world, a box in a city is
expressed as $\mathtt{bin(B,C)}$, a box on a truck is expressed as
$\mathtt{on(B,T)}$, and a truck in a city is expressed as $\mathtt{tin(T,C)}$.
Roads connecting cities are expressed as $\mathtt{can\mathchar 45\relax
drive(C1,C2)}$. A box can be loaded onto ($\mathtt{load(B,T)}$) or unloaded
from a truck ($\mathtt{unload(B,T)}$). Trucks can travel from a city to
another ($\mathtt{drive(T,C1,C2)}$). The $\mathtt{load/2}$ and
$\mathtt{unload/2}$ actions succeed with probability 0.9. The
$\mathtt{drive/2}$ action succeeds with probability 0.8.

### Q1: What formulas can pCTL-REBEL check in practice?

Although pCTL-REBEL can check any formulae of the pCTL language in Section
3.2, in practice, some formulae are more costly than others. This experiment
aims at evaluating the performance of different pCTL formulae in Table 1.
Table 1 includes formulae ranging from classic planning properties, i.e.
reachability properties (Kersting et al., 2004; Boutilier et al., 2001; Sanner
and Boutilier, 2009) to more complex, nested pCTL properties, e.g. the
following $\phi_{\mathtt{nested}}(i,j)$ formula. Recall that
$\phi_{\mathtt{nested}}(4,2)$ was discussed in Example 7, and its parse tree
is in Figure 4. Table 1 also includes a formula that has an indefinite
horizon.

$\displaystyle\phi_{\mathtt{nested}}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}i},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}j})=\mathtt{P_{\geq
0.5}[cl(a)U^{\leq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}i}}(on(a,b)}\mathtt{\wedge
P_{\geq 0.8}[P_{\geq
0.9}[X\;cl(e)]U^{\leq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}j}}on(c,d)])]}$

We now discuss in detail Table 1. First, all formulae in Table 1 are checked
against models that have infinitely many objects. This is possible due to its
relational computation. Second, pCTL-REBEL can handle classic planning tasks
by formulating them as reachability formulae (property 1,2,5, Table 1) or
constrained reachability formulae (property 3,6, Table 1). For example, Figure
5 visualizes the states that satisfies property 2 in Table 1. Third, pCTL-
REBEL can check, in an infinite model, formulae that have an infinite horizon
(property 5, Table 1). This is not possible for explicit-state model checkers
as the number of state is infinite. Finally, pCTL-REBEL can handle nested
formulae such as $\phi_{\mathtt{nested}}(i,j)$ (property 4, Table 1). Under
the time-out of 1800 seconds, pCTL-REBEL can compute
$\phi_{\mathtt{nested}}(3,1)$, which is cheaper to compute than
$\phi_{\mathtt{nested}}(4,2)$. Nonetheless, Figure 6 visualizes the results of
$\phi_{\mathtt{nested}}(4,2)$ by relaxing the time limit. More discussion
about nested formulae is in Experiment 7.

domain | property | formula | runtime(sec)
---|---|---|---
blocks |  | bounded reachability
---
with det. actions
$\mathtt{P_{\geq 0.5}[F^{\leq 10}on(a,b)]}$ | 11171717Kersting et al. (2004) reported a runtime of roughly 10 minutes for this task
blocks | bounded reachability | $\mathtt{P_{\geq 0.5}[F^{\leq 10}on(a,b)]}$ | 226
blocks |  | bounded
---
constrained reachability
$\mathtt{P_{\geq 0.5}[on(c,d)U^{\leq 5}on(a,b)]}$ | 7.1
blocks | a nested property | $\phi_{\mathtt{nested}}(3,1)$ | 1554
box | unbounded reachability | $\mathtt{P_{\geq 0.5}[F\;bin(b1,paris)]}$ | 0.7
box |  | bounded
---
constrained reachability
$\mathtt{P_{\geq 0.5}[tin(t1,paris)U^{\leq 5}bin(b1,paris)]}$ | 0.365
Table 1: PCTL-REBEL can perform a range of pCTL properties in the infinite
blocks and box worlds under a time-out of 1800 seconds.

[capbesideposition=right,top,capbesidewidth=0.4]figure[]

Figure 5: The abstracts states that satisfy $\mathtt{P_{\geq 0.5}[F^{\leq
10}on(a,b)]}$. Any state subsumed by $\mathtt{on(a,b)}$ is a goal state thus
has a value 1. The states that are further away from the upper-left corner
require more successful actions to reach $\mathtt{on(a,b)}$ thus have a
smaller probability.

[capbesideposition=right,top,capbesidewidth=0.3]figure[]

Figure 6: Similar to Figure 5, this illustrates the abstract states that
satisfy $\phi_{\mathtt{nested}}(4,2)$ in the blocks world.

### Q2: How does pCTL-REBEL compare with state-of-the-art model checkers?

State-of-the-art model checkers STORM and PRISM do not operate on a RMDP. They
require the RMDP to be grounded to an explicit-state MDP, which leads to a
state explosion. This experiment evaluates how well STORM and PRISM handles
such state explosions in practice. In particular, we show that pCTL-REBEL, by
lifting, performs better in mitigating state explosions in relational domains.

The state explosion problem is illustrated in Figure 7, showing the number of
ground states (Slaney and Thiébaux, 2001) and the corresponding
transitions181818The number of ground transitions is obtained from the STORM
model checker.  grow much faster than the number of abstract states191919The
number of abstract states is the number of integer partitions that capture all
relational structures. For example, for three blocks, there are three abstract
states $\mathtt{\\{cl(A),cl(B),cl(C)\\}}$,
$\mathtt{\\{cl(A),cl(B),on(B,C)\\}}$ and
$\mathtt{\\{cl(A),on(A,B),on(B,C)\\}}$. . Although all numbers grow
exponentially, the number of abstract states is more resistant to the domain
size than the others.

[capbesideposition=right,top,capbesidewidth=0.4]figure[]

Figure 7: The blocks world stats. When the number of blocks grows, the number
of ground states and the number of non-deterministic transitions explode more
than the minimum number of abstract states.

We compare the scalability of the three model checkers (including 4 PRISM
engines and 3 STORM engines) using a simple reachability property
$\mathtt{P_{\geq 0.5}[F^{\leq 10}on(a,b)]}$ in the blocks world. We measure
how the runtime grows with respect to the domain size, shown in Figure 8. The
results shows that pCTL-REBEL is more scalable than any PRISM or STORM engine
in relational domains. Under the time constraint, pCTL-REBEL can handle 15
blocks (6.6e13 ground states) whereas PRISM can handle at most 8 blocks (4.0e5
ground states) and STORM can handle at most 9 blocks (4.6e6 ground states).

We analyze Figure 8 to compare lifting with other optimization techniques.
Observe that Figure 8 categorizes all engines in three groups: (1) relational
model checking: pCTL-REBEL, (2) symbolic model checking: PRISM’s mtbdd,
sparse, hybrid engines and STORM’s dd, hybrid engines, and (3) explicit-state
model checking: PRISM’s explicit engine and STORM’s sparse engine. Compared to
pCTL-REBEL, not only the explicit-state approaches, but also the symbolic
approaches are much less resilient to the growth of the domain size. This
illustrates that although symbolic model checking methods are known to handle
large domains, their ability of handling state explosions in relational
domains is limited. Furthermore, unlike other engines, the runtime of pCTL-
REBEL saturates when the domain grows to a certain extent. This is a
consequence of lifted inference, reflecting that the number of relational
structures saturates for a fixed formulae.

[capbesideposition=right,top,capbesidewidth=0.4]figure[]

Figure 8: The property $\mathtt{P_{\geq 0.5}[F^{\leq 10}on(a,b)]}$ of is
checked by three model checkers. With a time-out of 1800 seconds, PRISM can
handle at most 8 blocks with the explicit engine, STORM can handle at most 9
blocks with the sparse engine, and pCTL-REBEL can handle 15 blocks.

### Q3: How well does pCTL-REBEL handle indefinite-horizon formulae?

PCTL-REBEL suffers a runtime explosion when cheking a formula that has an
indefinite horizon. Specifically, the runtime grows exponentially with respect
to the horizon. This experiment aims at analyzing pCTL-REBEL’s performance of
handling indefinite-horizon formulae. We use the reachability property
$\mathtt{P_{\geq 0.5}[F\;on(a,b)]}$ that has an indefinite horizon in the
blocks world.

To analyze the cause of runtime explosion, we split the checking process of an
indefinite-horizon formula into two stages: (1) the state recognition stage
and (2) the value convergence stage. In the state recognition stage, pCTL-
REBEL identifies new satisfying states in each iteration. This stage ends when
no more new satisfying states are found. In the value convergence stage, all
states found by pCTL-REBEL have already been identified in the previous stage.
As a consequence, the second stage, in practice, only updates the values of
the identified states until convergence. Notice that these two stages are just
for analyzing purposes as pCTL-REBEL conducts exactly the same computation in
both stages.

PCTL-REBEL suffers from a runtime explosion when checking an indefinite-
horizon formula. Specifically, runtime increases exponentially when the number
of required iterations grows, as shown Figure 9(a). It also shows that most of
the runtime is taken by the value convergence stage. Moreover, Figure 9(b)
shows in detail that the later iterations are more expensive than the earlier
iterations. This means that although the job of the value convergence state is
seemingly easier than the state recognition stage, it takes way more time due
to the redundant computation attempting to identify new states.

In summary, pCTL-REBEL suffers from a runtime explosion when handling
indefinite formulae. The main cause is the redundant computation conducted in
the value convergence stage. That is, pCTL-REBEL performs the same computation
without being aware of the two-stage nature of the indefinite-horizon
formulae. This problem can be mitigated by optimizing the algorithm so as to
reduce the time taken by the second stage. The optimization should benefit
finite-horizon formulae that has a large step

Figure 9: The results obtained from checking the reachability property
$\mathtt{P_{\geq 0.5}[F\;on(a,b)]}$ in the blocks world. (a) The runtime
increases exponentially to the number of required iterations. Most of the
runtime is taken by the value convergence stage (b) The later iterations are
more expensive than the earlier iterations.

### Q4: How well does pCTL-REBEL handle a complex relational transition
function?

The blocks world domain has a simple relational transition function that
consists of only one $\mathtt{move}$ rule (see Fig 1). However, it is common
to have constraints on the action, resulting in a more relationally complex
transition function that consists of more rules. One example is the box world
domain where the action $\mathtt{drive(T,C1,C2)}$ is constrained by the
underlying road map below202020The road networks are automatically generated
by the box world dataset. A truck $\mathtt{T}$ can drive from $\mathtt{C1}$ to
$\mathtt{C2}$ only if $\mathtt{can\mathchar 45\relax drive(C1,C2)}$ exists.

    can-drive(city0,city2).
    can-drive(city0,city1).
    can-drive(city0,city6).
    can-drive(city1,city0).
    can-drive(city1,city6).
    can-drive(city1,city3).
    can-drive(city1,city4).
    can-drive(city1,city2).
    can-drive(city1,city5).
    can-drive(city2,city0).
    can-drive(city2,city1).
    can-drive(city2,city6).
    can-drive(city3,city1).
    can-drive(city3,city6).
    can-drive(city3,city4).
    can-drive(city3,city5).
    can-drive(city4,city1).
    can-drive(city4,city3).
    can-drive(city4,city6).
    can-drive(city4,city5).
    can-drive(city5,city4).
    can-drive(city5,city1).
    can-drive(city5,city3).
    can-drive(city6,city0).
    can-drive(city6,city1).
    can-drive(city6,city2).
    can-drive(city6,city3).
    can-drive(city6,city4).

This experiment examines how well pCTL-REBEL handles complex relational
transition functions. We use the reachability property $\phi=$
$\mathtt{P_{\geq 0.5}[F\;bin(b1,city0)]}$ and automatically generated road
maps. The results are shown in Figure 10 where pCTL-REBEL can handle a road
map containing at most 8 cities under a time-out of 1800 seconds. The runtime
increases exponentially with respect to the size of the road network. Recall
that without a road network, it takes only 0.7 seconds to check $\phi$ (see
property 5, Table 1). Since the road network makes the model dynamics more
complex, more transition rules are required, resulting in runtime explosions.
In short, pCTL-REBEL works the best when the dynamics of the objects is
simple, e.g. in the blocks world or in the box world without a road map.

[capbesideposition=right,top,capbesidewidth=0.4]figure[]

Figure 10: The results obtained from checking the reachability property
$\mathtt{P_{\geq 0.5}[F\;bin(b1,city0)]}$ in the box world. The runtime
increases exponentially when the transition structure becomes more complex.

### Q5: How are the relative costs of the different pCTL operators?

It is crucial to know what kind of formulae pCTL-REBEL can handle efficiently
when designing properties for a model. This experiment aims at giving insight
into how different factors affect pCTL-REBEL’s performance.

Some path operators are more costly than others. e.g. the $\mathtt{X}$
operator is the cheapest since it requires only one iteration. The
reachability operator $\mathtt{F}$ is generally more expensive than the
constrained reachability operator $\mathtt{U}$ since $\mathtt{U}$ is a
stricter operator that prunes out more states. For example, checking
$\mathtt{P_{\leq 0.9}[F^{\leq 7}\;on(a,b)]}$ (18.494 seconds) is more costly
than checking $\mathtt{P_{\leq 0.9}[on(c,d)\;U^{\leq 7}\;on(a,b)]}$ (0.733
seconds). A nested formula is more costly than a flat formula since it
requires several recursive checking processes.

The formula structure also influences runtime. Specifically, increasing an
inner step bound is more expensive increasing an outer step bound. Taking the
formula $\phi_{\mathtt{nested}}(i,j)$ (see Experiment 1) for example, the
parameters $\mathtt{i}$ and $\mathtt{j}$ are both step bounds for $\mathtt{U}$
formulae, but $\mathtt{i}$ is attached to an outer sub-formula and
$\mathtt{j}$ is attached to the inner sub-formula. Hence, increasing
$\mathtt{j}$ increases the total runtime a lot more, compared to increasing
$\mathtt{i}$, as shown in Figure 11. The cause is that by increasing the inner
step bound, we increase the number of satisfying states for the inner sub-
formula, resulting in an overhead to outer sub-formulae.

[capbesideposition=right,top,capbesidewidth=0.4]figure[]

Figure 11: The runtime of $\phi_{\mathtt{nested}}(i,j)$ for different values
of i and j. The argument i is the step bound of the outer $\mathtt{U}$
operator, and j is the step bound of the inner $\mathtt{U}$ operator. The
runtime grows exponentially when either step bound increases. However, the
runtime is more sensitive to the inner step bound j.

##  8 Related work

This paper introduces pCTL-REBEL, a relational model checking technique for
relational MDPs that reasons at the relational level and mitigates the state
explosion problem. PCTL-REBEL extends existing frameworks. First, pCTL-REBEL
extends pCTL model checking with relational representations. As far as the
authors know, pCTL-REBEL is the first relational technique for pCTL model
checking. Second, pCTL-REBEL extends the decidability results of infinite,
state-bounded MDPs to the probabilistic setting.

To mitigate the state explosion problem in model checking, several grouping
techniques have been proposed. Different from our work, the following methods
exploit other types of symmetries instead of relational structures. Symbolic
model checking (McMillan, 1993) is a form of model checking that symbolically
represents the state space and the set of states in which a formula holds.
Symbolic model checking is often implemented using BDDs that are Boolean
formulas in canonical form, in which isomorphic subformulas are shared, to
allow efficient operations on the sets of states that they represent. Symbolic
model checking have been first used for model-checking of plain non
probabilistic finite state systems (McMillan, 1993). It has been adapted to
the probabilistic case in (Kwiatkowska et al., 2011). But contrary to our
algorithm, this symbolic methods only apply to finite state MDPs. Another
method to mitigate the state explosion problem is abstraction-refinement. This
method performs successively abstractions by partitioning the state space into
regions, and the model checking algorithms handle regions instead of
individual states (de Alfaro and Roy, 2007; Roy et al., 2008). These
techniques focus on grouping states into regions that have similar local
properties but they are usually abstractions that are not exact as the states
in a region can have different dynamics (future evaluations). Similarly,
Marthi (2007) uses abstract MDP to aggregate not only states but also actions
by exploiting the temporal dependency of actions. In addition, game-based
abstraction techniques construct abstractions of MDPs, by merging concrete
transitions into abstract transitions (Kattenbelt et al., 2008). Different
from our work, the abstractions approximate upper and lower bounds instead of
exact values.

Many studies integrate model checking techniques into other AI fields. In
planning, authors compute the optimal policy at the first-order level using
value iteration (Boutilier et al., 2001; Sanner and Boutilier, 2009; Kersting
et al., 2004), which can be seen as a probabilistic reachability task, namely
a special case of the general probabilistic model checking problem. This paper
generalizes this special case with a temporal logic thus fits in the Planning
as Model Checking paradigm (Giunchiglia and Traverso, 2000). In robotics,
model checking techniques are used for online motion planning (Lahijanian et
al., 2012; Maly et al., 2013; He et al., 2015) where the states are labeled
with propositions. This results in a multi-dimensional state space that grows
explonentially with the domain size (He et al., 2015), which is the problem
this paper directly tackles. Generally, our work can be applied a wide range
of frameworks that have a large model, particularly in relational domains.

There is a fruitful literature on theoretical results for infinite systems.
Decidable conditions for the infinite systems verification problem has been
defined in first-order mu-calculus (Bagheri Hariri et al., 2013; Calvanese et
al., 2018; De Giacomo et al., 2012; De Giacomo et al., 2015) and first-order
CTL (Belardinelli et al., 2011, 2012). However, these studies focus on the
non-probabilistic setting. Our work contributes to extending the theoretic
results to stochastic models by introducing the abstract relational MDP. A
limitation of the relational pCTL language is that does not support
quantification across, which could be investigated as described in the work of
Belardinelli et al. (2013).

##  9 Towards Safe Reinforcement Learning

Recently, a converging interest has emerged about the pursuit of general
dynamic systems that can autonomously reason and learn from interaction with
the environment (Giacomo, 2019). As such systems require the ability of
reasoning about first-order state representations and safety (Amodei et al.,
2016), pCTL-REBEL fits in as a first-order model checking technique that is
also particularly relevant in safe reinforcement learning.

Safe reinforcement learning is the process of learning a policy that maximizes
the expected reward in domains where some safety constraints should be
respected. In particular, safe exploration, i.e. guaranteeing an agent’s
safety in the exploration phase, is a non-trivial problem. Commonly used
exploration strategies such as $\epsilon$-greedy and softmax sometimes select
a random action, which can result in catastrophic situations (Amodei et al.,
2016). Existing research recognizes the importance of providing safety
guarantees in reinforcement learning (Garcia and Fernández, 2015; Pecka and
Svoboda, 2014; Lahijanian et al., 2012; Teichteil-Königsbuch, 2012; Sprauel et
al., 2014; Giunchiglia and Traverso, 2000; Mason et al., 2018; Hasanbeig et
al., 2019; Alshiekh et al., 2018; Jansen et al., 2020). However, most studies
are based on techniques that require explicit state exploration whereas only
few studies touch on safe exploration in relational domains (Driessens and
Džeroski, 2004; Martínez et al., 2017) In particular, several studies have
investigated augmenting reinforcement learning with model checking techniques.
This includes preventing the agent from taking risky actions (Alshiekh et al.,
2018; Jansen et al., 2020; Fulton and Platzer, 2018), synthesizing an initial
safe partial policy for learning (Leonetti et al., 2012), learning a policy
that maximizes the probability of satisfying a temporal formula (Hasanbeig et
al., 2019), and shaping the reward function based on a temporal formula (De
Giacomo et al., 2019). These work can be augmented with our work for
scalability in large relational domains.

pCTL-REBEL can be used as a safe model-based reinforcement learning algorithm
as it performs value iteration in a setting where safety constraints are
formulated as pCTL formulae. More formally, it derives the states in an RMDP
that satisfy a given (relational) pCTL formula that encodes goal states. This
means that pCTL-REBEL tackles a special safe reinforcement learning task where
the reward is one for goal states, zero for all other states, and the discount
factor is one (Kersting et al., 2004; Yoon et al., 2012; Otterlo, 2004).
Formally, the Bellman update in this paper

$\displaystyle V_{0}(s)$ $\displaystyle=\begin{cases}0&,\forall s\not\in G\\\
1&,\forall s\in G\end{cases}$ $\displaystyle V_{t+1}(s)$
$\displaystyle=\max_{a}\sum_{s^{\prime}}T(s,a,s^{\prime})V_{t}(s^{\prime})$

is a special case of the general Bellman operator

$\displaystyle V_{0}(s)$ $\displaystyle=\begin{cases}0&,\forall s\not\in G\\\
r&,\forall s\in G\end{cases}$ $\displaystyle V_{t+1}(s)$
$\displaystyle=\max_{a}\sum_{s^{\prime}}T(s,a,s^{\prime})[R(s,a,s^{\prime})+\gamma
V_{t}(s^{\prime})]$

where $r$ is a reward value $\in\mathbb{R}$.

It is an interesting avenue for further research to investigate representing
general reward functions within this framework. Furthermore, pCTL-REBEL can
naturally combine with relational reinforcement learning (Džeroski et al.,
2001) to achieve safe relational reinforcement learning as both use relational
representations and work at an abstract level rather than at the ground level.

##  10 Conclusions

We have introduced a framework for lifted model checking in relational
domains. To this aim, relational Markov Decision Processes have been
integrated with model checking principles for pCTL. The result is a very
expressive framework for model checking in probabilistic planning domains that
are relational, that is, involve objects as well as the relations among them.
The framework is lifted in that it does not require to first ground the
relational MDP and then exhaustively check all possible paths, but rather
works at a more abstract relational level where variables are only
instantiated whenever needed. The resulting algorithm is based on the
relational Bellman operator REBEL. It is quite complex but manages to rather
compactly compress enormous spaces of ground states in a couple of 10s of
rules. The algorithm has not yet been optimised, and one route for further
work is to combine pCTL-REBEL with expressive first order decision diagrams
(Wang et al., 2008) to gain efficiency and to further compress the abstract
states. Another route for further work is to explore the use of pCTL-REBEL for
reasoning and reinforcement learning in safety-critical contexts.

###### Acknowledgements.

This work was supported by the FNRS-FWO joint programme under EOS No.
30992574. It has also received funding from the Flemish Government under the
“Onderzoeksprogramma Artificiële Intelligentie (AI) Vlaanderen” programme, the
EU H2020 ICT48 project “TAILOR”, under contract #952215; and the Wallenberg
AI, Autonomous Systems and Software Program (WASP) funded by the Knut and
Alice Wallenberg Foundation.

## References

  * de Alfaro and Roy (2007) de Alfaro L, Roy P (2007) Magnifying-lens abstraction for markov decision processes. In: Damm W, Hermanns H (eds) Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 325–338
  * Alshiekh et al. (2018) Alshiekh M, Bloem R, Ehlers R, Könighofer B, Niekum S, Topcu U (2018) Safe reinforcement learning via shielding. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pp 2669–2678
  * Amodei et al. (2016) Amodei D, Olah C, Steinhardt J, Christiano P, Schulman J, Mané D (2016) Concrete problems in ai safety. 1606.06565
  * Bagheri Hariri et al. (2013) Bagheri Hariri B, Calvanese D, De Giacomo G, Deutsch A, Montali M (2013) Verification of relational data-centric dynamic systems with external services. In: Proceedings of the 32Nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, ACM, New York, NY, USA, PODS ’13, pp 163–174, doi: 10.1145/2463664.2465221, URL http://doi.acm.org/10.1145/2463664.2465221
  * Baier and Katoen (2008) Baier C, Katoen JP (2008) Principles of Model Checking (Representation and Mind Series). The MIT Press
  * Belardinelli et al. (2011) Belardinelli F, Lomuscio A, Patrizi F (2011) Verification of deployed artifact systems via data abstraction. In: Kappel G, Maamar Z, Motahari-Nezhad HR (eds) Service-Oriented Computing, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 142–156
  * Belardinelli et al. (2012) Belardinelli F, Lomuscio A, Patrizi F (2012) An abstraction technique for the verification of artifact-centric systems. 13th International Conference on the Principles of Knowledge Representation and Reasoning, KR 2012
  * Belardinelli et al. (2013) Belardinelli F, Lomuscio A, Patrizi F (2013) Verification of agent-based artifact systems. CoRR abs/1301.2678, URL http://arxiv.org/abs/1301.2678, 1301.2678
  * Boutilier et al. (2001) Boutilier C, Reiter R, Price B (2001) Symbolic dynamic programming for first-order mdps. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence - Volume 1, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, IJCAI’01, pp 690–697, URL http://dl.acm.org/citation.cfm?id=1642090.1642184
  * Van den Broeck et al. (2011) Van den Broeck G, Taghipour N, Meert W, Davis J, De Raedt L (2011) Lifted probabilistic inference by first-order knowledge compilation. In: Proceedings of the Twenty-Second international joint conference on Artificial Intelligence, AAAI Press/International Joint Conferences on Artificial Intelligence; Menlo …, pp 2178–2185
  * Calvanese et al. (2018) Calvanese D, Giacomo GD, Montali M, Patrizi F (2018) First-order µ-calculus over generic transition systems and applications to the situation calculus. Information and Computation 259:328 – 347, doi: https://doi.org/10.1016/j.ic.2017.08.007, URL http://www.sciencedirect.com/science/article/pii/S0890540117301487, 22nd International Symposium on Temporal Representation and Reasoning
  * De Giacomo et al. (2012) De Giacomo G, Lespérance Y, Patrizi F (2012) Bounded situation calculus action theories and decidable verification. Proc of KR 12
  * De Giacomo et al. (2015) De Giacomo G, Lespérance Y, Patrizi F (2015) Bounded situation calculus action theories. CoRR abs/1509.02012, URL http://arxiv.org/abs/1509.02012, 1509.02012
  * De Giacomo et al. (2019) De Giacomo G, Iocchi L, Favorito M, Patrizi F (2019) Foundations for restraining bolts: Reinforcement learning with ltlf/ldlf restraining specifications. Proceedings of the International Conference on Automated Planning and Scheduling 29(1):128–136, URL https://ojs.aaai.org/index.php/ICAPS/article/view/3549
  * De Raedt et al. (2016) De Raedt L, Kersting K, Natarajan S, Poole D (2016) Statistical relational artificial intelligence: Logic, probability, and computation. Synthesis Lectures on Artificial Intelligence and Machine Learning 10(2):1–189, doi: 10.2200/S00692ED1V01Y201601AIM032, URL https://doi.org/10.2200/S00692ED1V01Y201601AIM032, https://doi.org/10.2200/S00692ED1V01Y201601AIM032
  * Dehnert et al. (2017) Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: A modern probabilistic model checker. In: Majumdar R, Kunčak V (eds) Computer Aided Verification, Springer International Publishing, Cham, pp 592–600
  * Driessens and Džeroski (2004) Driessens K, Džeroski S (2004) Integrating guidance into relational reinforcement learning. Machine Learning 57:271–304, doi: 10.1023/B:MACH.0000039779.47329.3a
  * Džeroski et al. (2001) Džeroski S, De Raedt L, Driessens K (2001) Relational reinforcement learning. Machine learning 43(1-2):7–52
  * Ferilli et al. (2002) Ferilli S, Fanizzi N, Mauro ND, Basile TMA (2002) Efficient theta-subsumption under object identity. In: In Atti del Workshop AI*IA su Apprendimento Automatico
  * Forejt et al. (2011) Forejt V, Kwiatkowska M, Norman G, Parker D (2011) Automated Verification Techniques for Probabilistic Systems, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 53–113. doi: 10.1007/978-3-642-21455-4_3, URL https://doi.org/10.1007/978-3-642-21455-4_3
  * Fulton and Platzer (2018) Fulton N, Platzer A (2018) Safe reinforcement learning via formal methods: Toward safe control through proof and learning. In: AAAI, pp 6485–6492, URL https://www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/17376
  * Gabbay (2003) Gabbay DM (2003) Many-Dimensional Modal Logics: Theory and Applications. Elsevier North Holland
  * Garcia and Fernández (2015) Garcia J, Fernández F (2015) A comprehensive survey on safe reinforcement learning. J Mach Learn Res 16:1437–1480
  * Giacomo (2019) Giacomo GD (2019) Queryable self-deliberating dynamic systems, URL https://www.cse.ust.hk/pg/seminars/S19/giacomo.html, iJCAI
  * Giunchiglia and Traverso (2000) Giunchiglia F, Traverso P (2000) Planning as model checking. In: Biundo S, Fox M (eds) Recent Advances in AI Planning, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 1–20
  * Haddad and Monmege (2014) Haddad S, Monmege B (2014) Reachability in MDPs: Refining Convergence of Value Iteration. In: 8th International Workshop on Reachability Problems (RP’14), Springer-Verlag, Oxford, United Kingdom, Proceedings of the 8th International Workshop on Reachability Problems (RP’14), vol 8762, pp 125–137, doi: 10.1007/978-3-319-11439-2_10, URL https://hal.archives-ouvertes.fr/hal-01091122
  * Hahn et al. (2014) Hahn EM, Li Y, Schewe S, Turrini A, Zhang L (2014) IscasMC: A web-based probabilistic model checker. In: Nineteenth international symposium of the Formal Methods Europe association (FM), Springer, Lecture Notes in Computer Science, vol 8442, pp 312–317
  * Hasanbeig et al. (2019) Hasanbeig M, Kantaros Y, Abate A, Kroening D, Pappas GJ, Lee I (2019) Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp 5338–5343
  * He et al. (2015) He K, Lahijanian M, Kavraki LE, Vardi MY (2015) Towards manipulation planning with temporal logic specifications. In: 2015 IEEE International Conference on Robotics and Automation (ICRA), pp 346–352, doi: 10.1109/ICRA.2015.7139022
  * Jansen et al. (2020) Jansen N, Könighofer B, Junges S, Serban A, Bloem R (2020) Safe reinforcement learning using probabilistic shields. In: Konnov I, Kovacs L (eds) 31st International Conference on Concurrency Theory, CONCUR 2020, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp 31–316, doi: 10.4230/LIPIcs.CONCUR.2020.3
  * Kattenbelt et al. (2008) Kattenbelt M, Kwiatkowska M, Norman G, Parker D (2008) Game-based probabilistic predicate abstraction in prism. Electronic Notes in Theoretical Computer Science 220(3):5–21, doi: https://doi.org/10.1016/j.entcs.2008.11.016, URL https://www.sciencedirect.com/science/article/pii/S1571066108004532, proceedings of the Sixth Workshop on Quantitative Aspects of Programming Languages (QAPL 2008)
  * Kersting (2012) Kersting K (2012) Lifted probabilistic inference. In: ECAI, pp 33–38
  * Kersting and De Raedt (2004) Kersting K, De Raedt L (2004) Logical markov decision programs and the convergence of logical td($\lambda$). In: Camacho R, King R, Srinivasan A (eds) Inductive Logic Programming, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 180–197
  * Kersting et al. (2004) Kersting K, Otterlo MV, De Raedt L (2004) Bellman goes relational. In: Proceedings of the Twenty-first International Conference on Machine Learning, ACM, New York, NY, USA, ICML ’04, pp 59–, doi: 10.1145/1015330.1015401, URL http://doi.acm.org/10.1145/1015330.1015401
  * Kwiatkowska et al. (2011) Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Proc. 23rd International Conference on Computer Aided Verification (CAV’11), Springer, LNCS, vol 6806, pp 585–591
  * Lahijanian et al. (2012) Lahijanian M, Andersson SB, Belta C (2012) Temporal logic motion planning and control with probabilistic satisfaction guarantees. IEEE Transactions on Robotics 28(2):396–409, doi: 10.1109/TRO.2011.2172150
  * Leonetti et al. (2012) Leonetti M, Iocchi L, Patrizi F (2012) Automatic generation and learning of finite-state controllers. In: Ramsay A, Agre G (eds) Artificial Intelligence: Methodology, Systems, and Applications, Springer Berlin Heidelberg, Berlin, Heidelberg, pp 135–144
  * Maly et al. (2013) Maly MR, Lahijanian M, Kavraki LE, Kress-Gazit H, Vardi MY (2013) Iterative temporal motion planning for hybrid systems in partially unknown environments. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Association for Computing Machinery, New York, NY, USA, HSCC ’13, p 353–362, doi: 10.1145/2461328.2461380, URL https://doi.org/10.1145/2461328.2461380
  * Marthi (2007) Marthi B (2007) Automatic shaping and decomposition of reward functions. In: Proceedings of the 24th International Conference on Machine Learning, Association for Computing Machinery, New York, NY, USA, ICML ’07, p 601–608, doi: 10.1145/1273496.1273572, URL https://doi.org/10.1145/1273496.1273572
  * Martínez et al. (2017) Martínez D, Alenyà G, Torras C (2017) Relational reinforcement learning with guided demonstrations. Artificial Intelligence 247:295 – 312, doi: https://doi.org/10.1016/j.artint.2015.02.006, URL http://www.sciencedirect.com/science/article/pii/S0004370215000284, special Issue on AI and Robotics
  * Mason et al. (2018) Mason G, Calinescu R, Kudenko D, Banks A (2018) Assurance in Reinforcement Learning Using Quantitative Verification, Springer International Publishing, Cham, pp 71–96. doi: 10.1007/978-3-319-66790-4_5, URL https://doi.org/10.1007/978-3-319-66790-4_5
  * McMillan (1993) McMillan KL (1993) Symbolic Model Checking, Springer US, Boston, MA, pp 25–60. doi: 10.1007/978-1-4615-3190-6_3, URL https://doi.org/10.1007/978-1-4615-3190-6_3
  * Nienhuys-Cheng and Wolf (1997) Nienhuys-Cheng SH, Wolf Rd (1997) Foundations of Inductive Logic Programming. Springer-Verlag, Berlin, Heidelberg