1

Counterexample-Guided Abstraction Refinement for
POMDPs

arXiv:1701.06209v4 [cs.LO] 10 Mar 2017

Xiaobin Zhang, Bo Wu, and Hai Lin,

Abstract—Partially Observable Markov Decision Process
(POMDP) is widely used to model probabilistic behavior for
complex systems. Compared with MDPs, POMDP models a
system more accurate but solving a POMDP generally takes
exponential time in the size of its state space. This makes the
formal verification and synthesis problems much more challenging for POMDPs, especially when multiple system components
are involved. As a promising technique to reduce the verification
complexity, the abstraction method tries to find an abstract system with a smaller state space but preserves enough properties for
the verification purpose. While abstraction based verification has
been explored extensively for MDPs, in this paper, we present the
first result of POMDP abstraction and its refinement techniques.
The main idea follows the counterexample-guided abstraction
refinement (CEGAR) framework. Starting with a coarse guess for
the POMDP abstraction, we iteratively use counterexamples from
formal verification to refine the abstraction until the abstract
system can be used to infer the verification result for the original
POMDP. Our main contributions have two folds: 1) we propose
a novel abstract system model for POMDP and a new simulation
relation to capture the partial observability then prove the
preservation on a fragment of Probabilistic Computation Tree
Logic (PCTL); 2) to find a proper abstract system that can prove
or disprove the satisfaction relation on the concrete POMDP, we
develop a novel refinement algorithm. Our work leads to a sound
and complete CEGAR framework for POMDP.
Index Terms—Partially observable Markov decision process,
verification, abstraction methods, counterexample-guided refinement

I. I NTRODUCTION
Probabilistic behavior widely exists in practice for complex
systems. To model such systems, Markov decision processes
(MDPs) can be used to capture both nondeterminisms in
system decision making and probabilistic behaviors in state
transitions. As an extension of MDP, partially observable
MDP (POMDP) considers another layer of uncertainties by
assuming that the system states are not directly observable.
This partial observability allows POMDPs to model systems
more accurately but introduces more computational expenses
when solving a POMDP[1]. This is especially the case when
the formal verification and synthesis problems are considered
regarding system properties.
Consider system properties that can be specified by temporal
logics such as Probabilistic Computation Tree Logic (PCTL)
[2]. The model checking problem answers whether or not a
system satisfies a given PCTL specification, for example, the
probability to reach a set of bad states is less than 0.1%.
The authors
University of

were with Department of Electrical Engineering,
Notre Dame, Notre Dame, IN 46556, USA.
(xzhang11@nd.edu; bwu3@nd.edu; hlin1@nd.edu).

For MDPs, the model checking of PCTL formula can be
solved in polynomial time in the size of state space [3],
while for POMDPs it generally requires exponential time
[4], [5], [6]. When the system contains multiple sub-systems,
the compositional verification can dramatically increase the
computational cost for MDPs and can be even worse for
POMDPs. This is known as the state space explosion problem.
As an important technique to conquer the state space explosion, abstraction is a method for abstracting the state space of
the original (concrete) system and creating an abstract system
that contains smaller state space but can still conservatively
approximate the behavior of the concrete system [7], [8].
With a valid abstract system, the model checking problem
can be reasoned on a smaller state space and its solution for
the concrete system can be inferred correspondingly. While
the abstraction methods have been proposed and applied to
probabilistic systems such as MDPs in recent years [7], [8],
[9], [10], [11], [12], to the best of the authors’ knowledge
the abstraction methods have not been extensively explored
for POMDPs where the partial observability brings new challenges.
Motivated by the power of abstraction method in reducing
model checking complexity, we consider here the abstraction
method for POMDPs. To have the abstraction method well
established for POMDPs, two key questions must be answered:
1) how to define the form of the abstract system; 2) how to find
a proper abstract system. For non-probabilistic systems and
MDPs, counterexample-guided abstraction refinement (CEGAR) framework is widely considered to answer the second
question with different abstraction forms being defined [13],
[7], [8], [14]. Generally, CEGAR starts with a very coarse
abstraction and uses the counterexamples diagnosed from the
abstract systems to iteratively refine the abstraction.
In this article, we propose a sound and complete CEGAR framework for POMDPs, which allows the automatic
reasoning on finding a proper abstraction for POMDPs. A
safety fragment of PCTL (safe-PCTL)[8] with finite horizon
is considered as the system specification. As the abstraction
for POMDPs, z-labeled 0/1-weighted automata (0/1-WAz ) are
extended from 0/1-weighted automata (0/1-WA) [3], [12]
by defining the observation labeling function for discrete
states. Given a POMDP, its corresponding 0/1-WAz can be
defined with the observation labeling function representing
the observation information. We then propose a simulation
relation, safe simulation, for 0/1-WAz and prove that the safe
simulation preserves the properties considered. This gives the
foundation of the soundness of our CEGAR framework.
With 0/1-WAz and safe simulation relation, we further

2

address a novel CEGAR framework to find a proper 0/1WAz as the abstraction of POMDP. Initially, we start with the
coarsest abstract system generated from a quotient construction and iteratively check the satisfaction relation of the given
specification on the abstract system. Counterexamples from
model checking on 0/1-WAz are derived following algorithms
in [15] in the forms of a finite set of finite paths that violate
the specification with large enough accumulative probability.
Given these counterexamples, we verify whether or not these
counterexamples are real witnesses for violation of the given
specification on the concrete system. If not, we use these
spurious counterexamples to refine the quotient construction
and update the abstract system until satisfaction relation is
proved to be true or real counterexample has been found for
the concrete system.
A. Our contributions
The technical contributions are summarized in the order in
which they appear in the article as follows:
z
• We propose 0/1-WA as the form of abstract systems
for POMDPs and give the conversion rules between 0/1WAz and POMDP. On 0/1-WAz , we design a new notion
of simulation relation, safe simulation, which is extended
from strong simulation relation for MDPs [16]. With safe
simulation relation capturing the property of the partial
observability from POMDP, we prove the preservation
of finite horizon safe-PCTL between the abstract system
(0/1-WAz ) and the concrete system (0/1-WAz induced
from the original POMDP).
• We present a CEGAR framework to automatically find
a proper abstract system to prove or disprove the satisfaction relation of the concrete system. We first define
the quotient construction rules to generate candidate
abstract systems based on a given state space partition.
Starting with the coarsest partition, we iteratively refine
the abstract systems using counterexamples returned from
model checking on the abstract systems. Following our
refinement algorithm, we prove the soundness and completeness of our CEGAR framework for POMDP. An
example is given to show the effectiveness of our CEGAR
framework to reduce the state space size of POMDP.

Still using strong simulation relation to restrict abstraction,
[8] considers CEGAR on a special class of MDPs. Instead
of an action set, the transition options for each state are
determined by a set of distributions and the adversary will
select a distribution to transit. From this point of view, each
distribution is defined under a unique action. With system
specification given by PCTL, different counterexample forms
for MDPs are discussed. For safety PCTL, an MDP and
simulation relation pair is used as the counterexample, then
the spuriousness of the counterexample can be checked by
standard simulation checking algorithm [19]. Based on that a
refinement will try to split the invalidating state.
While quotient construction based on state space partition
can reduce the size of state space, recent work in [12]
uses 0/1-WA as the assumptions for MDPs and reduces the
transition links and terminal nodes in multi-terminal binary
decision diagrams (MTBDDs) representation of MDPs. The
L∗ algorithm is then applied to learn an MTBDD as a proper
assumption. But their method limits the choice of transition
probabilities for 0/1-WA to be either the transition probabilities from MDP or 1/0, which limits the form of abstractions.
Beside abstraction based assumption for the compositional
verification of MDPs, there are also results on classical assumptions [10], [9], [20]. Compared with the abstraction based
assumptions mentioned earlier, classical assumptions usually
preserve only linear-time properties instead of branching-time
properties between the assumption and the original system.
This kind of assumptions can lead to a smaller state space but
may not preserve rich enough properties and hard to guarantee
the completeness.
For CEGAR framework of POMDP, our work is mainly
inspired from [7], [8] where the safe-PCTL specification is
considered and simulation based abstraction is discussed.
C. Outline of the article
The rest of this article is organized as follows. In Section 2,
we give necessary definition and notations. The 0/1-WAz as
the abstract system for POMDP and safe simulation relation
are introduced in Section 3. Then the CEGAR framework is
presented in Section 4 and an illustration example is given in
Section 5. Finally, we conclude this article with future work
in Section 6.

B. Related work
Abstraction methods and the refinement algorithms based
on counterexamples have been extensively explored for probabilistic systems. In [7], probabilistic automata (PA) is considered. Compared with MDPs the transition distribution under
an action in PA is not deterministic, i.e., there can be multi
distributions defined for single state and action pair. With
quotient construction to build abstract system, strong simulation relation [16] is used to describe the properties shared
between abstract and concrete system since strong simulation
preserves the safety fragment of PCTL specification. Strong
simulation relation also inspires us to derive safe simulation
relation for POMDPs. To refine the abstract, CEGAR based on
the interpolation method [17] is applied with counterexamples
being returned from model checking following [18].

II. P RELIMINARIES
A. Probabilistic system models
Definition 1. [2] An MDP is a tuple M = (S, s̄, A, T ) where
• S is a finite set of states;
• s̄ ∈ S is the initial state;
• A is a finite set of actions;
• T : S × A × S → [0, 1] is a transition function
Here the probability of making a transition from state s ∈ S
to state s0 ∈ S under action aP∈ A is given by T (s, a, s0 ).
0
For MDP, it is required that
s0 ∈S T (s, a, s ) = 1, ∀s ∈
S, a ∈ A. Under this requirement, the terminating states can
be modeled by adding a self-loop with the probability 1 [2].
As a special case, DTMC is an MDP with only one action

3

defined for each state s ∈ S and the transition function can
be reduced as T : S × S → [0, 1]. To analyze the behavior
of MDP with additional information, we can define a labeling
function L : S → 2AP that assigns each state s ∈ S with a
subset of atomic propositions AP .
For MDPs, the states are assumed to be fully observable. As
a generalization, POMDPs consider system states with partial
observability.
Definition 2. A POMDP is a tuple P = {M, Z, O} where
• M is an MDP;
• Z is a finite set of observations;
• O : S × Z → [0, 1] is an observation function.
Instead of direct observability, POMDP assigns a probability
distribution over the observation set Z for every state s ∈ S,
which is described by the observation function O. Here the
probability of observing z ∈ Z at state s ∈ S is given by
O(s, z).
In this paper, we consider finite POMDPs, in which S, A, Z
and AP are finite sets.
B. Paths and adversaries
In the MDP M = (S, s̄, A, T ), a path ρ is a non-empty
sequence of states and actions in the form
ρ = s0 a0 s1 a1 s2 . . . ,
where s0 = s̄, si ∈ S, ai ∈ A and T (si , ai , si+1 ) ≥ 0 for
all i ≥ 0 [2]. Let ρ(i) denote the ith state si of a path ρ, ρ−
i
denote the prefix ending in the ith state si and ρ+
i denote the
suffix starting from the ith state si . Let |ρ| denote the length
of ρ which is the number of transitions. The set of paths in M
is denoted as P athM and its set of corresponding prefixes is
denoted as P refM . Let P rρ (i, j) (i ≤ j) stand for the product
of the transition probabilities from the ith state to the jth state
(i < j) on path ρ. Thus
P rρ (i, j) =

j−1
Y

T (sk , ak , sk+1 ), i < j,

k=i

and P rρ (i, j) = 1 if i = j.
To synthesize about an MDP, an adversary resolves the
system nondeterminism given system executions. A pure adversary is a function σ : P refM → A, which maps every
finite path of M onto an action in A. A randomized adversary
is a function σ : P refM → Dist(A), which maps every
finite paths of M onto a distribution over action set A. Under
an adversary function σ, the set of possible system paths is
denoted as P athσM . While the pure adversary is a special case
of the randomized adversary, in this paper we consider pure
adversaries and we will discuss in the next subsection that pure
adversaries are as powerful as randomized adversaries for the
type of system properties we consider.
Compared with MDPs, POMDPs do not have direct observability over the states. For a POMDP P = {S, s̄, A, Z, T, O},
define the observation sequence of a path ρ = s0 a0 s1 a1 s2 . . .
as a unique sequence obs(ρ) = z0 a0 z1 a1 z2 . . . where zi ∈ Z
and O(si , zi ) > 0 for all i ≥ 0. The observation sequence

is also known as the history information. To synthesize about
POMDP, the adversary is required to be observation-based,
where for all ρ, ρ0 ∈ P refM , σ(ρ) = σ(ρ0 ) if obs(ρ) =
obs(ρ0 ).
C. Probabilistic computation tree logic
To represent and synthesize the design requirements or control objectives, Probabilistic Computation Tree Logic (PCTL)
[2] is considered in this paper. As the probabilistic extension
of the Computation Tree Logic (CTL) [21], PCTL adds the
probabilistic operator P , which is a quantitative extension of
CTL’s A (always) and E (exist) operators [3], [22].
Definition 3. [2] The syntax of PCTL is defined as
• State formula φ ::= true | α | ¬φ | φ ∧ φ |P./p [ψ],
≤k
• Path formula ψ ::= Xφ | φ U
φ | φ U φ,
where α ∈ AP , ./∈ {≤, <, ≥, >}, p ∈ [0, 1] and k ∈ N.
Here ¬ stands for "negation", ∧ for "conjunction", X for
"next", U ≤k for "bounded until" and U for "until". Specially,
P./p [ψ] takes a path formula ψ as its parameter and describes
the probabilistic constraint. Note that a PCTL formula is
always a state formula and path formulas only occur in P
operator.
Definition 4. [2], [23] For an labeled MDP M =
(S, s̄, A, T, L), the satisfaction relation  for any states s ∈ S
is defined inductively as follows
s  true, ∀s ∈ S;
s  α ⇔ α ∈ L(s);
s  ¬φ ⇔ s 2 φ;
s  φ1 ∧ φ2 ⇔ s  φ1 ∧ s  φ2 ;
s  P./p [ψ] ⇔ P r({ρ ∈ P athσM | ρ  ψ}) ./ p, ∀σ ∈ ΣM ,
where ΣM is the set of all adversaries and for any path ρ ∈
P athM
ρ  Xφ ⇔ ρ(1)  φ;
ρ  φ1 U ≤k φ2 ⇔ ∃i ≤ k, ρ(i)  φ2 ∧ ρ(j)  φ1 , ∀j < i;
ρ  φ1 Uφ2 ⇔ ∃k ≥ 0, ρ  φ1 U ≤k φ2 .
Compared with MDPs, the adversaries for POMDPs must
be observation-based. Therefore the PCTL satisfaction relation
for s  P./p [ψ] is limited to consider observation-based
adversaries for POMDPs, while other satisfaction relations can
be inherited from MDP cases.
In this paper, we consider the safety fragment of PCTL
(safe-PCTL) [8] which is given in conjunction with the liveness fragment as follows.
• φS := true | α | φS ∧ φS | φS ∨ φS |PEp [φL U φL ],
• φL := true | α | φL ∧ φL | φL ∨ φL |¬PEp [φL U φL ],
where α ∈ AP , E ∈ {≤, <}, p ∈ [0, 1]. If we restrict E
to be ≤ in the above grammar, we will get strict liveness
and weak safety fragments of PCTL. While reasoning some
logic properties for POMDPs is undecidable [24], we focus on
safe-PCTL with finite-horizon which is decidable. And without
losing generality, in the rest part of the article, we will mainly

4

consider the safe-PCTL for bounded until φ = PEp [φ1 U ≤k φ2 ]
as the type of specifications to illustrate our framework.
Generally, a randomized adversary is more powerful than a
pure adversary, its special case. But for the PCTL fragment
considered in this paper, the pure adversaries and randomized
adversaries have the same power for MDPs and POMDPs
in the sense that restricting the set of adversaries to pure
strategies will not change the satisfaction relation of the PCTL
fragment [25]. The intuitive justification of this claim is that
if we are just interested in upper and lower bounds to the
probability of some events to happen, any probabilistic combination of these events stays within the bounds. Moreover,
deterministic adversaries are sufficient to achieve the bounds
[25].
D. Model checking and counterexample selection
For MDPs, the probabilistic model checking of PCTL
specification has been extensively studied [2]. Depending on
whether ./ in the specification gives upper or lower bound,
PCTL model checking of MDPs solves an optimization problem by computing either the minimum or maximum probability over all adversaries [2]. Due to its full observability, MDP
model checking can be solved generally in polynomial time in
the size of the state space and the computational complexity
has been discussed extensively in [3]. There also exist model
checking software tools for MDPs, such as PRISM [26] and
storm [27].
As a generalization of MDPs to consider uncertainties in
both transitions and observations, POMDPs model system
more accurate but the model checking of POMDPs is more
expensive [1]. Generally, the solution for POMDP model
checking is in exponential time in the size of the state space
or even undecidable for lots of properties [4], [5], [6]. To
solve the POMDP model checking problem for specification
φ = PEp [φ1 U ≤k φ2 ] considered in this article, one possible
approach is modifying the transition structure of POMDP to
make states s |= ¬φ1 and states s |= φ2 absorbing, and
designing the reward scheme that assigns 0 to intermediate
transitions and 1 to the final transitions on s |= φ2 when depth
k is reached [28]. Then the model checking problems can be
formulated as a classic POMDP optimization problem that can
be solved by, for example, value iteration method [29], [30].
While model checking answers whether or not a given
specification can be satisfied, an adversary will be returned
as the witness if the specification is violated. As one step
further, counterexample selection gives a particular system
path or set of paths in the system that violate the specification as a detailed evidence. Such a path or set of paths
is called counterexample. For non-probabilistic systems, finding counterexamples is done by finding a path that violates
the specification. However, for the probabilistic systems, the
probabilities of the paths also need to be considered. Given
an adversary, the nondeterminism of MDPs and POMDPs
can be solved which give the induced DTMCs. Then the
counterexample selection for MDPs and POMDPs can be
considered as for DTMCs since model checking problem will
generate the witness adversary if the specification is violated.

For DTMCs, in [15] the counterexamples are considered to
be a finite set of executions and finding the counterexamples
that carry enough evidence is equivalent to solve shortest path
problem on the graph generated from DTMCs. But for some
properties, e.g., P<1 (true U φ), there may not exist a finite
set of paths that witnesses the violation as shown in [8]. While
there are different counterexample forms proposed to reason
different properties and cases, readers may refer to [8] for a
comprehensive summary.
For the finite horizon safe-PCTL considered in this paper,
counterexample can always be represented by a finite set of
finite paths. In the case of ≤, this is clear since it belongs
to the weak safety fragment of PCTL, which is a subset of
properties considered in [15]; in the case of <, the set of
paths as the counterexample is finite since the specification is
only on the finite horizon for a finite system. Therefore in this
paper we apply the framework and algorithms from [15] and
COMICS tool [31] is used as the software package to generate
counterexamples.
III. A BSTRACTION AND SIMULATION RELATION
For CEGAR in MDPs, different abstract system forms are
proposed [7], [8], [14] depending on the verification goals
and considered specifications. For POMDP with partial observability, we present 0/1-WAz as the abstract system form,
which is extended from 0/1-WA considered in [12]. Based
on 0/1-WAz , we further propose a simulation relation —
safe simulation that can preserve the finite horizon safe-PCTL
specification between the abstract 0/1-WAz system and the
concrete POMDP system. These give the foundation of our
sound and complete CEGAR framework for POMDP.
A. z-labeled 0/1-weighted automata
Definition 5. A z-labeled 0/1-weighted automaton 0/1-WAz
Mz is a tuple {S, s̄,
A, T, Z, L, Lz },
• S is a finite set of states;
• s̄ is the initial state;
• A is a finite set of actions;
• T : S × A × S → [0, 1] is a transition function;
• Z is a finite set of observation labels;
AP
• L : S → 2
is a atomic proposition labeling function
with AP being a finite set of atomic propositions;
z
• L : S → Z is a z-labeling function.
With Lz describing the observable information for each
state, the system execution of 0/1-WAz behaves in the same
way of POMDP after we embed the transition and observation
function in POMDP into transition function in 0/1-WAz . From
this point of view, 0/1-WAz can naturally be an abstraction
form for POMDP. Due to the partial observability of states
in 0/1-WAz , its adversaries must be also observation-based
and the model checking for 0/1-WAz can be inherited from
POMDP model checking, which is further discussed in the
appendix section.
Remark: Compared with 0/1-WA model described in [12],
0/1-WAz adds an observation set Z and a z-labeling function

5

seven

seven zeven
s1 zeven
a : 0.5, b : 1

5
0.2
a:

a:

sn−1

start

s0

5
0.02

a : 0.475

sodd

a : 0.5

sf

5
.2
:0

5
.2
:0

0.5

a

a : 0.25

a
a:

a : 0.475

s1 zodd

···

0.25

:0
.2
5

a : 0.5

a : 0.25

a : 0.25

a

···

5

a : 0.5

:0
.2

s1

a

a : 0.5

5
0.47

s0

start

a:

:0
.2
5

b:1

a

b:1

a:

a

5
.2
:0

a
5
.2
:0

a:

0.5

a : 0.5

sodd zodd

sf zf

Fig. 1: The POMDP model P in Example 1
Lz to represent the observable information on each state in S.
But the definition of cylinder set and σ algebra in 0/1-WAz
can still be straightforwardly inherited from 0/1-WA.
Given a POMDP, we can define its corresponding 0/1-WAz ,
which can be seen as adding observation labels directly to its
guided MDP proposed in our previous work [23], [32].
Definition 6. [23] Given a POMDP P = {S, s̄, A, Z, T, O},
its guided MDP M+ is a tuple {X + , x̄+ , A, T + },
•
•
•
•
•

X + = {x+ |x+ = [s, z], s ∈ S, z ∈ Z} ∪ {s̄} is a finite
set of states;
x̄+ = s̄ is the initial state;
A is a finite set of actions;
T + (s̄, a, [s0 , z 0 ]) := T (s̄, a, s0 ) · O(s0 , z 0 );
T + ([s, z], a, [s0 , z 0 ]) := T (s, a, s0 ) · O(s0 , z 0 ).

Given a POMDP P = {S, s̄, A, Z, T, O}, we define the
corresponding 0/1-WAz Mz : {M+ , Z z , Lz } where
•
•
•

M+ is the
S guided MDP for P;
Z z = Z {init};
Lz (s̄) = init and Lz ([s, z]) = z, s ∈ S, z ∈ Z.

Here the special observation init is used to label the initial
state s̄. While we assume the initial state of POMDP is known,
if the initial condition given for the POMDP is a distribution
over S, a dummy state can be added as the new initial state
with transition links to all other s ∈ S at the probability
specified by the initial distribution [23].
Example 1. Consider a POMDP P = {S, s̄, A, Z, T, O}1 ,
where
•
•
•
•

S consists of n + 3 states (n is an even number and
n ≥ 2). S = {sf , seven , sodd } ∪ {s0 , s1 , ..., sn−1 };
s̄ = s0 ;
A = {a, b};
Z = {zf , zeven , zodd }.

1 This

POMDP model is extended from the MDP model considered in [8]

Fig. 2: The corresponding 0/1-WAz Mz for P in Example 1
TABLE I: Observation matrix
O(s, z)
sf
seven
sodd
si : even
si : odd

zf
1

zeven

zodd

1
0.95
0.05

1
0.05
0.95

The transition probability under both actions are given in
Fig. 1, where
T (si , b, si ) = 1, i ∈ [0, n − 1],
T (si , a, si+1 ) = 0.5, i ∈ [0, n − 2],
T (sn−1 , a, sn−1 ) = 0.5,
T (si , a, sf ) = 0.25, i ∈ [0, n − 1],
T (si , a, seven ) = 0.25, for i: even and i ∈ [0, n − 1],
T (si , a, sodd ) = 0.25, for i: odd and i ∈ [0, n − 1],
T (sodd , a, sf ) = 0.5,
T (sodd , a, sodd ) = 0.5.
The observation matrix is shown as follows in Table I. Among
S, the state sf represents a failure state with label f ail and is
colored by orange in Fig. 1. No other states has proposition
labels.
For POMDP P, the corresponding 0/1-WAz Mz is shown
in Fig. 2.
Based on the definition of Mz , the paths from POMDP
P and paths from Mz build a one-to-one mapping under a
same observation-based adversary. This makes POMDP and its
corresponding 0/1-WAz equivalent and convertible for formal
verification purposes. Notice that the parallel production of
POMDP’s state space and observation space during the gener-

6

ation of 0/1-WAz Mz is mainly for the usage of theoretical
proof of our CEGAR framework. Though the cross production generates a larger state space in 0/1-WAz , the random
processes for state transitions and observation selections in
POMDP have been encoded in the state transitions in 0/1WAz . Therefore it will not introduce lots of computational
expenses in our refinement algorithm introduced later.
B. Simulation relation for 0/1-WAz
With 0/1-WAz as the possible form of the abstract systems
for POMDP, we need to define the property preservation
relation between the abstract system and the concrete system.
For MDPs, simulation relations are widely used and discussed
[16], [8]. Based on the strong simulation relation [16] that preserves safe-PCTL for MDPs, we propose the safe simulation
relation for 0/1-WAz to preserve finite horizon safe-PCTL
specifications.
Consider two 0/1-WAz Mz1 = {S1 , s̄1 , A, T1 , Z, L1 , Lz1 }
and Mz2 = {S2 , s̄2 , A,
a
T2 , Z, L2 , Lz2 }. For a ∈ A, s1 ∈ S1 and s2 ∈ S2 , let s1 −
→ µ1
a
and s2 −
→ µ2 with µi (s0 ) = Ti (si , a, s0 ), s0 ∈ Si , i ∈ {1, 2}.
Let Supp(µ) := {s| µ(s) > 0}. Note that we still call µi a
probability distribution for convenience but it is non-stochastic
since its total probability mass can be larger than 1. Let R ⊆
S1 × S2 denote a binary relation between the state spaces of
Mz1 and Mz2 .
Definition 7. µ1 vR µ2 if and only if there is a weight
function w : P
S1 × S2 → [0, 1] such that
1. µ1 (s1 ) = Ps2 ∈S2 w(s1 , s2 ), ∀ s1 ∈ S1 ,
2. µ2 (s2 ) ≥ s1 ∈S1 w(s1 , s2 ), ∀ s2 ∈ S2 ,
3. w(s1 , s2 ) = 0 if Lz1 (s1 ) 6= Lz2 (s2 ) or L1 (s1 ) 6= L2 (s2 ),
4. w(s1 , s2 ) > 0 implies s1 Rs2 , ∀ s1 ∈ S1 , s2 ∈ S2 .
Definition 8. R is a safe simulation relation between two 0/1a
WAz Mz1 and Mz2 if and only if for every s1 Rs2 and s1 −
→
a
µ1 , there exists a µ2 with s2 −
→ µ2 and µ1 vR µ2 .
For s1 ∈ S1 and s2 ∈ S2 , s2 safely simulates s1 , denoted
s1  s2 , if and only if there exists a safe simulation T such
that s1 T s2 .
Mz2 safely simulated Mz1 , also denoted Mz1  Mz2 , if and
only if s̄1  s̄2 .
Lemma 1. µ1 vR µ2 implies, µ1 (S) ≤ µ2 (R(S)), for every
S ⊆ Supp(µ1 ).
Proof. Let w be the associated weight function, then
X X
µ1 (S) =
w(s, t)

Theorem 1. Let φ be a safe-PCTL specification with finite
horizon. For a POMDP P and its corresponding 0/1-WAz
Mz1 , if Mz1  Mz2 with Mz2 being 0/1-WAz , then Mz2 |= φ
implies P |= φ.
Proof. For finite horizon safe-PCTL specifications without
probabilistic operator P , this theorem holds trivially since the
initial states of Mz2 and P have the same atomic proposition
labels.
Consider the specifications containing probabilistic operator
with constraint, φ = PEp [ ]. Assume Mz2 |= φ but P 6|= φ. For
Mz1 , there must exist an observation-based adversary, which
generates a witness DTMC M1 that violates the specification
φ. We want to show, under the same adversary, the corresponding weighted DTMC M2 for Mz2 also violates φ. Thus M2
can serve as the witness of Mz2 ’s violation and show Mz2 6|= φ.
Then by contradiction the theorem can be proved.
Let R be the safe simulation relation between Mz1 and Mz2 .
Since Mz1 6|= φ, there exists a finite set of finite paths that
satisfy φ and their accumulated probability masses 5 p.
To show the contradiction, we first prove that for a finite
set of paths with length n, P aths = {ρs |ρs = s0 ...sn }
in Mz1 , the corresponding set of paths P atht = {ρt |ρt =
t0 ...tn , s.t. ∃ρs = s0 ...sn , ∈ P aths , si Rti } in Mz2 satisfies
P r(P atht ) ≥ P r(P aths ). For i = 0, . . . , n, let si ∈ S(i)
where S(i) = {s|s = ρs (i), ρs ∈ P aths }. For paths in
P aths , let µsi denote the (non-stochastic) probability distribution over S(i) at step i. Correspondingly we could define
Ti , µti for P atht . By the definition of P atht , we have
T (i) = R(S(i))). Clearly, P r(P aths ) = µsn (S(n)) and
P r(P atht ) = µtn (T (n)). Now we are proving µsj vR µtj
for j = 0, . . . , n by induction, which will lead to the proof of
Theorem 1 following Lemma 1.
For j = 0, P r(P atht ) ≥ P r(P aths ) holds trivially. For
j = 1, we have µs1 vR µt1 since µs0 and µt0 are generated
directly from µs0 and µt0 , respectively.
Assume µsi vR µti for j = i. Then for j = i + 1,
X
µsi+1 (sy ) =
µsi (sx ) · µsx (sy ), ∀sy ∈ S(i + 1),
sx ∈S(i)

µti+1 (ty )

X

=

µti (tx ) · µtx (ty ), ∀ty ∈ T (i + 1).

tx ∈T (i)

Since µsi vR µti , there exists a weight function w, such that


X
X

µsi+1 (sy ) =
w(sx , t1 ) · µsx (sy ) ,
sx ∈S(i)

=

X X

t1 ∈R(sx )



s∈S t∈R(S)

w(s, t) ≤ µ2 (R(S)).

t∈R(S) s∈S

µti+1 (ty ) ≥

X


X


tx ∈T (i)

w(s1 , tx ) · µtx (ty ) .

s1 ∈R(tx )

Since w(s, t) > 0 if and only if sRt,
Lemma 1 states that the safe simulation relation for probability distributions enlarges the probability masses over the
support. In the next theorem, we prove that the safe simulation
preserves of the finite horizon safe-PCTL specifications, where
its enlargement effect for the sets of paths is shown.

µsi+1 (sy ) =

XX
sx

µti+1 (ty ) ≥

XX
sx

[w(sx , tx ) · µsx (sy )] ,

tx

tx

[w(sx , tx ) · µtx (ty )]

7

with sx Rtx . Because sx Rtx , we have µsx vR µtx with a
weight function wx . Thus


XX
X
w(sx , tx ) ·
µsi+1 (sy ) =
wx (sy , t2 )
sx

=

tx

X

t2 ∈R(sy )

XX

t2 ∈R(sy ) sx

w(sx , tx ) · wx (sy , t2 ),

tx


µti+1 (ty ) ≥

XX
sx

=



w(sx , tx ) ·

tx

X

X

wx (s2 , ty )

s2 ∈R(ty )

XX

s2 ∈R(ty ) sx

w(sx , tx ) · wx (s2 , ty ).

tx

Based on Definition 7, µsi+1 vR µti+1 . By induction, we have
proved µsj vR µtj for j = 0, . . . , n. Thus we have µsk (S(k)) ≤
µtk (T (k)) following Lemma 1 given T (k) = R(S(k)). This
also proves P r(P aths ) ≤ P r(P atht ). Because n stands
for an arbitrary length, by applying this proof to paths with
different lengths in the counterexample path set from Mz1 , we
know that there always exists a finite set of paths in Mz2 with a
larger accumulative probability that violates the specification.
Then this corresponding set of paths is the witness of Mz2
violating φ, which contradicts to our initial assumption. This
concludes our proof for Theorem 1.

Fig. 3: Illustration of the quotient construction for 0/1-WAz :
the circles stand for the concrete states s ∈ S and the rectangles stand for the abstract states generated by a given partition
Π. Different colors stand for different atomic propositions.
Based on Definition 9, the concrete states can belong to a
same abstract state only if they have the same observation
label.
Definition 9. Given a 0/1-WAz Mz = {S, s̄, A, T, Z, L, Lz }
and a consistent partition Π, define the quotient 0/1-WAz
Mz /Π = {Π, [s̄]Π , A, TΠ , Z, LzΠ , LΠ } where
X
TΠ ([s]Π , a, [s]0Π ) = max
T (si , a, sj ),
si ∈[s]Π

LzΠ ([s]Π )

sj ∈[s]0Π

z

= L (s),

LΠ ([s]Π ) = L(s).
With Theorem 1, we have shown that safe simulation
preserves finite horizon safe-PCTL specification φ between
POMDP and the possible 0/1-WAz as the abstract system.
In next section, we present our CEGAR framework to find a
proper 0/1-WAz as the abstract system.

Note that based on the requirement of the consistent partition,
[s̄]Π = s̄. By Definition 8, It follows straight forwardly that
Mz /Π  Mz with safe simulation relation R = {(s, c)|s ∈
c, c ∈ Π}.
B. CEGAR

IV. C OUNTEREXAMPLE GUIDED ABSTRACTION
REFINEMENT

In order to find a 0/1-WAz Mz that can safely simulate the
corresponding 0/1-WAz of a POMDP P and capture enough
properties from P to prove or disprove the satisfaction relation,
we develop a novel CEGAR scheme. Since the model checking
of specifications without probabilistic operators can be trivial,
we focus on finite-horizon safe-PCTL with probabilistic operator P and probability threshold.
A. Quotient construction for 0/1-WAz
We first define the quotient 0/1-WAz by partitioning
the state space of the corresponding 0/1-WAz Mz =
{S, s̄, A, T, Z, L, Lz } generated for POMDP P. This process
is called quotient construction. Let Π denote a partition
of S and [s]Π denote the equivalence class (abstract state)
containing s (concrete state). Here Π can be viewed as a set of
abstracted states and [s]Π ∈ Π. Comparing with the quotient
construction presented in the non-probabilistic case and MDP,
we require ∀s1 , s2 ∈ [s]Π , Lz (s1 ) = Lz (s2 ), L(s1 ) = L(s2 ).
Such a partition Π is called a consistent partition.

In order to find a quotient 0/1-WAz Mz /Π that either
shows Mz /Π |= φ or provides the counterexample to show
Mz 6|= φ, we follow a CEGAR approach.
Initially, we construct the quotient 0/1-WAz Mz /Π0 based
on the coarsest partition Π0 that groups any states with the
same observation and atomic proposition labels together in
Mz . In each iteration i, if the model checking of the specification φ on Mz /Πi returns yes, the CEGAR terminates with
a proper quotient 0/1-WAz Mz /Πi as the abstract system
that Mz /Πi |= φ, which further implies P |= φ. Otherwise,
we can get the counterexample as a finite set of finite paths
P athCE and their accumulated probability mass 5 p. Given
the counterexample, we check whether this counterexample is
spurious or not where the realizable probability of the counterexample is checked. If this counterexample is not spurious,
the CEGAR terminates with the real counterexample that witnesses the violation of the given specification. Otherwise, we
will use this spurious counterexample to refine the state space
partition to get a finer state space partition. This process keeps
going until the counterexample (CE) checking returns "No" in
the sense that the previously found counterexample has been
removed. After that, with the finer state space partition, we reconstruct the quotient 0/1-WAz for the iteration i + 1 and do
model checking again. The overview of our CEGAR approach

8

Initialization
Coarsest
partition
Quotient
Construction

Satisfied

Model checking

Proper abstract
system

Not satisfied

No

Spurious checking

Not Spurious

Real
counterexample

Spurious

CE checking

Yes

Find abstract states
for refinement

Refine the state
space partition

Fig. 4: The overview of the CEGAR approach for POMDP

is shown in Fig. 4 and we illustrate our algorithms step-by-step
as follows.
1) Check spuriousness of counterexample: Given the counterexample, we calculate the achievable probability in its realization in Mz . For a abstract path ρΠ = c0 a0 ...cn ∈ P athCE ,
we define its realization in Mz as a set of concrete state paths
denoted by π(ρΠ ) = {ρ|ρ = s0 a0 ...sn , sj ∈ cj , j = 0, ..., n}.
If the accumulative probability mass of all realizations for
P athCE 5 p, we have found a real counterexample showing
P 6|= φ. Otherwise, P athCE is spurious and introduced
by a too coarse quotient partition, in which case we need
to refine the state space partition and get a finer abstract
system. The algorithm for spuriousness checking of a given
counterexample is summarized in Algorithm 1.
Algorithm 1: Check spuriousness of the counterexample
Data: Counterexample as a set of paths P athCE and the
probability threshold p for the specification φ
Result: true if the counterexample is spurious.
1 sum ← 0
2 for ρΠ = c0 a0 ...cn ∈ P athCE do
3
for ρ ∈ π(ρΠ ) do
4
sum = sum + P rρ (0, |ρ|)
5
if sum 5 p then
6
return f alse
7
end
8
end
9 end
10 return true
2) Find the set of abstract states for refinement: Given a
spurious counterexample P athCE as a set of abstract state
paths in Mz /Π, the refinement algorithm first finds a set of
abstract states needed to be refined then analyzes the splitting
policy for certain abstract states to reduce the spuriousness
of the counterexample. Based on the splitting policy, the

Fig. 5: Illustration of finding Bj . Starting from the end of
a counterexample path, j will separate this path into two
parts. For the accumulative probability, we use the transition
probability from the abstract state path to get p+
j for the last
j steps and the transition probability from the concrete state
paths to get p−
j for the first n − j steps.
refinement algorithm generates a new partition Π for next
iteration.
To find a set of abstract states needed to be refined, we
initialize j = 0 and get a set of abstract states Bj that
contains the (pivot)th state for each ρΠ ∈ P athCE with
pivot = max(|ρΠ | − j, 0):
Bj = {c ∈ Π|c = ρΠ (pivot), ρΠ ∈ P athCE }.
For each ρΠ ∈ P athCE , we calculate
ρΠ
p+
(pivot, |ρΠ |).
j = Pr

For each ρ ∈ π(ρΠ ), we calculate
ρ
p−
j = P r (0, pivot).
−
Given p+
j and pj for each ρΠ ∈ P athCE and ρ ∈
π(ρΠ ), we can
summation SPj =
P
P get the −accumulated
+
p
·
p
and
check
whether SPj E p
j
ρΠ ∈P athCE
ρ∈π(ρΠ ) j
or not. If yes, we increase j by 1 and go to the next
iteration. If not, Bj contains the abstract state needed to be
refined. Notice that SPj is monotonic increasing and when
jPreaches the maximum path length in P athCE , SPj =
ρΠ
(0, |ρΠ |) 5 p because P athCE is a counρΠ ∈P athCE P r
terexample. Also because P athCE is spurious, SP1 E p.
These two facts guarantee the termination of the algorithm
for some j > 0. If Bj is returned as a set of abstract states
needed to refine, Bj must have at least one abstract state that
contains more than one concrete states; otherwise sum will be
the same for j and j − 1 which will make the algorithm end
in iteration j − 1. A direct implementation of the algorithm
for this part is summarized in Algorithm 2.
Remark: While the calculation of p−
j requires the projection
of an abstract state path to a set of concrete state paths, we
only need to do the calculation once when j = 0. In the
initial iteration with j = 0, we will calculate the probability of
reaching each concrete state following the projection paths of
the counterexample and these values can be saved to memory.
In later iterations, the projection paths are still the same so we
just need to load p−
j from memory. And since the counterexample paths have already solved the nondeterminism, solving

9

p−
j can be done very efficiently by, for example, dynamic
programming.
Algorithm 2: Find the set of abstract states for refinement
Data: spurious counterexample as a set of paths P athCE
and the probability threshold p for the
specification φ
Result: a set of abstracted states Bj .
1 j ← −1
2 do
3
j ←j+1
4
sum ← 0
5
Bj ← {c ∈ Π|c = ρΠ (max(|ρΠ | − j, 0)), ρΠ ∈
P athCE }
6
for ρΠ ∈ P athCE do
7
pivot ← max(|ρΠ | − j, 0)
ρΠ
8
p+
(pivot, |ρΠ |)
j ← Pr
9
for ρ ∈ π(ρΠ ) do
ρ
10
p−
j ← P r (0, pivot)
+
11
sum = sum + p−
j · pj
12
if sum 5 p then
13
return Bj
14
end
15
end
16
end
17 while sum E p
3) Refine the state space partition: After finding Bj , we
have a set of abstract states showing that the state space
partition Πi is too coarse. We want to find a new partition
to reduce the spuriousness of the counterexample.
Assume the spurious counterexample P athCE contains
only one abstract path ρΠ with the corresponding abstract state
in Bj having more than one concrete states. Let c = ρΠ (pivot)
and cnext = ρΠ (pivot + 1) with pivot = max(|ρΠ | − j, 0)
and a ∈ A the selected action for the transition between c
and cnext . We want to find the split policy that splits the
equivalent class c into two abstract states to reduce the value of
SPj . Based on the quotient construction rules for the abstract
system, we could first get
Pthe array of transition probabilities
from s ∈ c to cnext ( s0 ∈cnext T (s, a, s0 )), then sort this
array in descendingPorder to get G+ . Here the nth element
0
of G+ stands for
s0 ∈cnext T (s[n], a, s ), n = 1, 2, ..., |c|.
If we split c into two parts that the first abstract state c1
contains concrete states {s[1], ..., s[n − 1]} and the second
abstract state c2 contains concrete states {s[n], ..., s[|c|]}, then
TΠ (c1 , a, cnext ) = G+ [1] and TΠ (c2 , a, cnext ) = G+ [n].
Let G− represent an array
P of transition probabilities that its
nth element is G− [n] = ρ∈π(ρΠ ),ρ(pivot)=s[n] P rρ (0, pivot).
Since we want to reduce the value of SPj , we can go through
the possible split policy by selecting the separation point n
(n = 2, 3, ..., |c|) such that
argn min

n−1
X
d=1

G− [d] · G+ [1] +

|c|
X

G− [d] · G+ [n],

d=n

with the minimization goal describing the potential new SPj .

Algorithm 3: Refine the state space partition
Data: spurious counterexample as a set of paths P athCE
in Mz /Π and a set of abstracted states Bj
Result: new partition Π
1 P ath ← {ρΠ |ρΠ ∈ P athCE , |ρΠ (pivot)| >
1 with pivot = max(|ρΠ | − j, 0)}
2 M = |P ath|
3 for m = 1, ..., M do
4
ρm
Π ← the mth path in P ath
5
pivotm = max(|ρm
Π | − j, 0)
m
m
6
cm = ρm
(pivot
),
m cnext = ρΠ (pivotm + 1)
Π
7
am ← the selected action between cm and cm
next on
ρm
Π
−
8
generate G+
mmand Gm
+
ρΠ
9
pj|ρm = P r (pivotm , |ρm
Π |);
Π
m
10
for n = 2, ..., |c | do
11
rmn
P=

P|c|
n−1 −
+
−
+
d=1 Gm [d] · Gm [1] +
d=n Gm [d] · Gm [n] ·
p+
j|ρm
Π
m
TΠ (c ,am ,cm
next )
12
13
14
15
16

end
end
m, n ← argm,n min rmn
update Π by splitting cm with the separation point n
return Π

If we have multiple abstract paths like ρΠ , in this case
we can go through each path, find the split policy based on
that path, then compare and select the split policy that gives
the best reduction for the potential new SPj . Given a set
of abstract state paths P athCE as the spurious counterexample and Bj , we first get a subset of abstract state paths
P ath = {ρΠ |ρΠ ∈ P athCE , |ρΠ (pivot)| > 1 with pivot =
max(|ρΠ | − j, 0)}. Basically we extract a set of abstract state
paths with the corresponding abstract state in Bj containing
more than one concrete state. Let |P ath| = M . For each
m
m
ρm
Π ∈ P ath, m = 1, ..., M , we have pivotm , c , cnext , am ,
+
−
Gm and Gm , respectively. If the mth path is selected with
separation point n, the potential new SPj can be captured by


|c|
n−1
X
X
+
+

rmn = 
G−
G−
m [d] · Gm [1] +
m [d] · Gm [n]
d=1

d=n

·

p+
j|ρm
Π

TΠ (cm , am , cm
next )

,

and the selected m and n should minimize rmn . The algorithm
for this part is summarized in Algorithm 3.
With the m and n minimizing the potential new SPj ,
we have a split policy that splits the select abstract state
into two. Under the new partition rule, we check the new
counterexample paths. If these abstract state paths do not have
enough accumulative probability of violation, we will move to
the next iteration i+1 with the new state space partition Πi+1 ;
otherwise, we will apply Algorithm 2 to update Bj then run
a new round of refinement.

10

,b

0.
05
b:
5,
:0
.4
7
a

:0
.4
75
a
a:

b
75,
0.4

95
: 0.

a : 0.475, b : 0.95

5
.2
:0

t3

a

a : 0.25

t2

t1

a : 0.275, b : 0.95

5
.2
:0

a : 0.475, b : 0.95

:1

a

a : 0.275, b : 0.95

5, b

Partition Π1
t0 : {s0 }
t1 : {si zodd }
t2 : {si zeven , seven zeven }
t3 : {sf zf }
t4 : {sodd zodd }

t0

start

:0
.0
5

t0

start

0.
a:

Partition Π0
t0 : {s0 }
t1 : {si zodd , sodd zodd }
t2 : {si zeven , seven zeven }
t3 : {sf zf }

a : 0.25

t2

t1

a : 0.475, b : 0.95

t3

a : 0.475, b : 0.95

a : 1, b : 1

a : 1, b : 1

a
a : 0.25

5
.2
:0

a : 0.5

t4

a:

for P

z∗ , a

5

t2

t1

.2
:0

b

a : 0.475, b : 0.95

t5

a

a : 0.05, b : 0.95

75,
0.4
a:

95
: 0.

a : 0.25

t0

start

a:

5
0.2

a : 0.25

t3

a : 0.475, b : 0.95
a : 0.475, b : 0.95

a
a : 0.25

5
.2
:0

Proof. Soundness: we initialize the coarsest assumption as a
quotient 0/1-WAz Mz /Π. For every iteration i ∈ N, the new
generated abstract system Mz /Πi is also a quotient 0/1-WAz .
Follow the definition of quotient 0/1-WAz and Theorem 1, the
soundness can be concluded.
Completeness: Since the newly generated abstract system
is guaranteed to be finer than the older one in the previous
iteration and the original concrete system Mz is the finest
abstract system for itself, the convergence of the CEGAR
is guaranteed. This shows in the worst case we find the
original concrete system as its assumption, which concludes
the completeness.

Partition Π2
t0 : {s0 }
t1 : {si zodd }
t2 : {si zeven }
t3 : {sf zf }
t4 : {sodd zodd }
t5 : {seven zeven }

0.
05

Theorem 2. The CEGAR framework is sound and complete.

Fig. 8: The 0/1-WAz Mz1

b:

Fig. 7: The adversary that witnesses M0 6|= φ

0.5

a : 0.5, b : 1

:0
.4
75
,

start

Mz0

a

Fig. 6: The 0/1-WA

z

t4

a:

0.5

a : 0.5, b : 1

V. E XAMPLE
For POMDP system P described in Example 1, consider
the bounded until specification φ = P≤0.45 (true U ≤n f ail)
and we want to check whether P |= φ. Let n =
20. Based on the corresponding 0/1-WAz Mz of P, we
get the initial coarsest abstraction for P by partitioning the state space of Mz into four equivalence classes
{s0 }, {si zodd , sodd zodd }, {si zeven , seven zeven } and {sf zf }
with i ∈ [0, n). The resulting 0/1-WAz Mz0 is shown in Fig.
6 with four abstract states. Here Mz0 does not satisfy φ with
the witness adversary shown in Fig. 7, which basically choose
action a for whatever history sequences. The counterexample
is returned as a set of two paths: {t0 → t3 , t0 → t1 → t3 } with
the accumulative probability of 0.4875, which is larger than
required 0.45. It turns out that this CE is spurious. By checking
the abstracted states backward in CE, we find B1 = {t0 , t1 }
that includes the over abstracted state and requires further
refinement. The selected splitting policy splits sodd zodd out
of t1 . The generated abstract paths from the previous counterexample only have the accumulative probability of 0.36875,

Fig. 9: The 0/1-WAz M2

which implies the counterexample paths have been removed
and the newly generated abstract system Mz1 is shown in Fig.
8.
By reusing the adversary found in the previous iteration, we
can show Mz1 does not satisfy φ neither. The counterexample
is returned as a set of four paths: {t0 → t3 , t0 → t1 →
t3 , t0 → t2 → t3 , t0 → t2 → t2 → t3 } with the
accumulated probability of 0.50625. This counterexample is
also spurious. After finding B1 = {t0 , t1 , t2 } that contains
the over abstracted states, we choose the splitting policy that
splits seven zeven out of t2 . And the generated abstract paths
from the previous counterexample only have the accumulative
probability around 0.3775, which implies the counterexample
paths have been removed and the newly generated abstract
system Mz2 is shown in Fig. 9.
Still with the adversary in Fig. 7, the dissatisfaction of
Mz2 on φ is witnessed. This time the returned counterexample
contains four paths: {t0 → t3 , t0 → t1 → t3 , t0 → t1 → t2 →

11

t3 , t0 → t1 → t4 → t3 } with the accumulative probability
around 0.4845. It turns out that the realizable probability of
the counterexample is larger than 0.45, which means we have
found the real counterexample showing that P 6|= φ.
VI. C ONCLUSION AND F UTURE W ORK
In this article, a CEGAR framework for POMDPs is proposed with the proof of the soundness and completeness.
Inspired by strong simulation relation for probabilistic systems
and CEGAR frameworks for MDPs, we define 0/1-WAz as
the form of the abstract system for POMDP and use safe simulation relation to preserving safe-PCTL with finite horizon.
With 0/1-WAz and safe simulation relation, the abstraction
refinement algorithm is given to find a proper abstract system
for POMDP based on counterexamples returned from model
checking on the abstract systems iteratively.
In the future, we will extend our results to other temporal
logic specifications and relax the requirement on the specification to have a finite horizon. Meanwhile, we will completely
implement the software package for our CEGAR framework.
A PPENDIX
C ONNECTION BETWEEN MODEL CHECKING AND OPTIMAL
POLICY COMPUTATION FOR 0/1-WA z
In the optimal policy computation problem for POMDP
P = {S, s̄, A, Z, T, O}, a reward function R(s, a) : S × A →
R is defined to assign a numerical value quantifying the reward
of performing an action a at state s [30]. The objective is
to compute a policy (adversary) for selecting actions based
on histories. The optimal policy σ maximizes the expected
future accumulative reward and usually the future rewards
are discounted by a factor γ : 0 ≤ γ < 1 to guarantee the
accumulative reward is finite. Formally, given a history ht =
a0 z1 , ..., zt−1 at−1 zt , the belief distribution b(·|ht ) over S is
the sufficient statistic [33]. Here b(s|ht ) = P r(st = s|ht , b0 )
stands for the conditional probability that the domain is in
state s at time t, given history ht and initial state distribution
b0 . With the initial value function being defined as
X
V0 (b|h) = max
R(s, a)b(s|h),
a

s∈S

the tth value function can be calculated from the (t − 1)th
following
"
X
Vt (b|h) = max
R(s, a)b(s|h)
a

transitions on s |= φ2 when depth k is reached [28], [34]. Since
the future accumulative rewards are collected from the finite
horizon, the discount factor is not needed. Under this reward
scheme, the value function Vk (b) stands for the accumulative
probability of paths satisfying φ1 U ≤k φ2 with initial belief
state b under the optimal policy. Then the model checking
problems can be answered by finding the optimal policy and
checking whether Vk (b0 ) E p or not. This classic POMDP
optimal policy computation problem that can be solved by, for
example, value iteration method [29], [30]. Among different
solvers for POMDP optimization problems, partially observable Monte-Carlo planning (POMCP) is a promising method
based on Monte-Carlo simulation to find the optimal policy
with convergence guarantee in large POMDPs [34], [35].
In Section III, we introduce 0/1-WAz which is an extension
of 0/1-WA. With the requirement of the adversaries being
observation-based, 0/1-WAz can be seen as a special POMDP
with the observation function for each state being Dirac delta
function. For this special POMDP, the transition functions for
some states satisfy T (s, a, s0 ) ∈ [0, 1], s, s0 ∈ S, a ∈ A but
P
0
s0 ∈S T (s,
P a, s ) can be 0larger than 1 while in the traditional
POMDP s0 ∈S T (s, a, s ) must be equal (or less) to 1. We
call this special kind of POMDP the weighted-POMDP. For
weighted-POMDP, we can still design a reward scheme to
connect its model checking problem with the optimal policy computation problem for the bounded until safe-PCTL
specification φ = PEp [φ1 U ≤k φ2 ]. To illustrate this reward
scheme, we notice that in the standard POMDP, the optimal
policy computation problem can be understood as the planning
problem on a derived MDP where the states of this MDP
are the belief states in POMDP and the transition function is
given by belief state updating function. Since the belief state
corresponds to the history, the states of the derived MDP can
also be understood as histories. Following this idea, we first
present the construction of the derived MDP for weightedPOMDP then give the reward scheme for the derived MDP.
For weighted-POMDP, the belief state distribution b(·|ht ) is
no longer the sufficient statistic for a history ht because at each
time instance
the carried probability mass over S is enlarged
P
when s0 ∈S T (s, a, s0 ) > 1. To represent the total probability
mass over S for a history h, we define a coefficient function
C() that maps a history in weighted-POMDP to a positive real
value. Formally, given initial state s̄ we have C(h0 ) = 1 and
(
1, s = s̄;
b(s|h0 ) =
0, otherwise.

s∈S

#
+γ

X

P r(z|a, b)Vt−1 (τ (b, a, z)) ,

The updates of the belief state b and the coefficient function
C follow

z∈Z

where τ () stands for the belief state update function following Bayesian rules [30]. For the bounded until safe-PCTL
specification φ = PEp [φ1 U ≤k φ2 ] considered in this article,
one can convert the model checking problem to the optimal
policy computation problem for POMDP by modifying the
transition structure of POMDP to make states s |= ¬φ1 and
states s |= φ2 absorbing, and designing the reward scheme
that assigns 0 to intermediate transitions and 1 to the final

b(s0 |ht )
O(s0 , z)T (s, a, s0 )b(s|ht−1 )C(ht−1 )
,
00
00
s00 ∈S
s∈S O(s , z)T (s, a, s )b(s|ht−1 )C(ht−1 )
XX
C(ht ) = C(ht−1 )
b(s|ht−1 )T (s, a, s0 ), t = 1, 2, ...
P

=P

s∈S

P

s∈S s0 ∈S

Given a weighted-POMDP, its derived MDP M with histories
as states is defined as M = {H, A, TM } where H is the state

12

space of histories and
TM (h, a, haz)
P
P
00
00
s00 ∈S
s∈S O(s , z)T (s, a, s )b(s|h)C(h)
P
P
=P
00
00
00 ∈S
z∈Z
s∈S O(s , z)T (s, a, s )b(s|h)C(h)
P sP
00
00
O(s , z)T (s, a, s )b(s|h)C(h)
00
= s ∈S s∈S
,
C(haz)
where
the second equality is established following the fact that
P
z∈Z O(s, z) = 1. Apparently TM (h, a, haz) is a standard
transition
function for MDP with
P
T
z∈Z M (h, a, haz) = 1, ∀a ∈ A, h ∈ H.
Given φ = PEp [φ1 U ≤k φ2 ] as the specification for a
weighted-POMDP, we still modify the transition structure to
make states s |= ¬φ1 and states s |= φ2 absorbing. Instead
of assigning reward for intermediate transitions, an immediate
reward is assigned at the end for a history. Let ∆ denote the
set of s |= φ2 , s ∈ S. Then the initial value function is defined
as
X
V0 (h) = C(h)
b(s|h)
s∈∆

and the tth value function can be calculated from the (t−1)th:
X
Vt (h) = max
TM (h, a, haz)Vt−1 (haz).
a

z∈Z

Theorem 3. Vk (h) equals to the maximum accumulative
probability of paths satisfying φ1 U ≤k φ2 with initial history
h following the optimal policy.
Proof. We give an induction proof for this theorem.
For the base case of k = 0, the theorem holds trivially with
X
V0 (h) = C(h)
b(s|h).
s∈∆

Assume the theorem is true for k = i, i ≥ 0. Then we have
X
i
Vi (h) =
b(s0 |h)C(h)P r{s0 z →
− ∆|h},
s0 ∈S
i

where P r{s0 z →
− ∆|h} represents the maximum probability
mass of reaching ∆ in less or equal to i steps from s0
conditional on history h with z as the latest observation.
For k = i + 1, the maximum accumulative path probability
mass of reaching ∆ in less or equal to i + 1 steps for history
h can be written as
XXX
P rob = max
O(s0 , z)T (s, a, s0 )b(s|h)C(h)
a

z∈Z s0 ∈S s∈S
i
0

P r{s z →
− ∆|haz}
XX
= max
b(s0 |haz)TM (h, a, haz)C(haz)
a

z∈Z s0 ∈S
i
0

P r{s z →
− ∆|haz}.
Following the expression of Vi (h), we can get
X
P rob = max
TM (h, a, haz)Vi (haz) = Vi+1 (h).
a

z∈Z

Thus Vi+1 (h) is the maximum probability mass of reaching
∆ in less or equal to i + 1 steps for the history h, which
concludes the proof.
Then the model checking problems for the weightedPOMDP P on
φ = PEp [φ1 U ≤k φ2 ] can be answered by finding the optimal
policy that maximize Vk (h0 ) and checking whether Vk (h0 )Ep
or not. This optimal policy computation problem can be solved
using, for example, POMCP.
R EFERENCES
[1] Z. Ma and M. Kwiatkowska, “Modelling with prism of intelligent
system,” Ph.D. dissertation, Citeseer, 2008.
[2] J. J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker, Mathematical
techniques for analyzing concurrent and probabilistic systems. American Mathematical Soc., 2004.
[3] C. Baier and J. Katoen, Principles of Model Checking. MIT Press,
2008.
[4] O. Madani, S. Hanks, and A. Condon, “On the undecidability of
probabilistic planning and infinite-horizon partially observable markov
decision problems,” in AAAI/IAAI, 1999, pp. 541–548.
[5] J. Goldsmith and M. Mundhenk, “Complexity issues in markov decision
processes.” in IEEE Conference on Computational Complexity, 1998, pp.
272–280.
[6] K. Chatterjee, M. Chmelík, and M. Tracol, “What is decidable about
partially observable markov decision processes with ω-regular objectives,” Journal of Computer and System Sciences, vol. 82, no. 5, pp.
878–911, 2016.
[7] H. Hermanns, B. Wachter, and L. Zhang, “Probabilistic cegar,” in
International Conference on Computer Aided Verification. Springer,
2008, pp. 162–175.
[8] R. Chadha and M. Viswanathan, “A counterexample-guided abstractionrefinement framework for markov decision processes,” ACM Transactions on Computational Logic (TOCL), vol. 12, no. 1, p. 1, 2010.
[9] L. Feng, M. Kwiatkowska, and D. Parker, “Compositional verification
of probabilistic systems using learning,” in Quantitative Evaluation of
Systems (QEST), 2010 Seventh International Conference on the. IEEE,
2010, pp. 133–142.
[10] M. Kwiatkowska, G. Norman, D. Parker, and H. Qu, “Assume-guarantee
verification for probabilistic systems,” in International Conference on
Tools and Algorithms for the Construction and Analysis of Systems.
Springer, 2010, pp. 23–37.
[11] ——, “Compositional probabilistic verification through multi-objective
model checking,” Information and Computation, vol. 232, pp. 38–65,
2013.
[12] F. He, X. Gao, M. Wang, B.-Y. Wang, and L. Zhang, “Learning weighted
assumptions for compositional verification of markov decision processes,” ACM Transactions on Software Engineering and Methodology
(TOSEM), vol. 25, no. 3, p. 21, 2016.
[13] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counterexampleguided abstraction refinement,” in International Conference on Computer Aided Verification. Springer, 2000, pp. 154–169.
[14] A. Komuravelli, C. S. Păsăreanu, and E. M. Clarke, “Assume-guarantee
abstraction refinement for probabilistic systems,” in International Conference on Computer Aided Verification. Springer, 2012, pp. 310–326.
[15] T. Han, J.-P. Katoen, and D. Berteun, “Counterexample generation in
probabilistic model checking,” IEEE Transactions on Software Engineering, vol. 35, no. 2, pp. 241–257, 2009.
[16] R. Segala and N. Lynch, “Probabilistic simulations for probabilistic
processes,” Nordic Journal of Computing, vol. 2, no. 2, pp. 250–273,
1995.
[17] T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan,
“Abstractions from proofs,” SIGPLAN Not., vol. 39, no. 1, pp.
232–244, Jan. 2004. [Online]. Available: http://doi.acm.org/10.1145/
982962.964021
[18] T. Han and J.-P. Katoen, “Counterexamples in probabilistic model
checking,” in International Conference on Tools and Algorithms for the
Construction and Analysis of Systems. Springer, 2007, pp. 72–86.
[19] C. Baier, B. Engelen, and M. Majster-Cederbaum, “Deciding bisimilarity
and similarity for probabilistic processes,” Journal of Computer and
System Sciences, vol. 60, no. 1, pp. 187–231, 2000.

13

[20] L. Feng, T. Han, M. Kwiatkowska, and D. Parker, “Learning-based
compositional verification for synchronous probabilistic systems,” in
International Symposium on Automated Technology for Verification and
Analysis. Springer, 2011, pp. 511–521.
[21] E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic. Springer, 1982.
[22] M. Kwiatkowska, G. Norman, and D. Parker, “Stochastic model checking,” in International School on Formal Methods for the Design of
Computer, Communication and Software Systems. Springer, 2007, pp.
220–270.
[23] X. Zhang, B. Wu, and H. Lin, “Learning based supervisor synthesis
of pomdp for pctl specifications,” in 2015 54th IEEE Conference on
Decision and Control (CDC). IEEE, 2015, pp. 7470–7475.
[24] K. Chatterjee, L. Doyen, and T. A. Henzinger, “A survey of partialobservation stochastic parity games,” Formal Methods in System Design,
vol. 43, no. 2, pp. 268–284, 2013.
[25] K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger, “Randomness
for free,” in International Symposium on Mathematical Foundations of
Computer Science. Springer, 2010, pp. 246–257.
[26] M. Kwiatkowska, G. Norman, and D. Parker, “Prism 4.0: Verification
of probabilistic real-time systems,” in Computer aided verification.
Springer, 2011, pp. 585–591.
[27] C. Dehnert, S. Junges, J.-P. Katoen, and M. Volk, “The probabilistic
model checker storm,” arXiv preprint arXiv:1610.08713, 2016.
[28] R. Sharan, “Formal methods for control synthesis in partially observed
environments: application to autonomous robotic manipulation,” Ph.D.
dissertation, California Institute of Technology, 2014.
[29] N. L. Zhang and W. Zhang, “Speeding up the convergence of value
iteration in partially observable markov decision processes,” Journal of
Artificial Intelligence Research, vol. 14, no. 1, pp. 29–51, 2001.
[30] J. Pineau, G. Gordon, and S. Thrun, “Anytime point-based approximations for large pomdps,” Journal of Artificial Intelligence Research, pp.
335–380, 2006.
[31] N. Jansen, E. Ábrahám, M. Volk, R. Wimmer, J.-P. Katoen, and
B. Becker, “The comics tool–computing minimal counterexamples for
dtmcs,” in International Symposium on Automated Technology for Verification and Analysis. Springer, 2012, pp. 349–353.
[32] X. Zhang, B. Wu, and H. Lin, “Assume-guarantee reasoning framework
for mdp-pomdp,” in Decision and Control (CDC), 2016 IEEE 55th
Conference on. IEEE, 2016, pp. 795–800.
[33] K. J. Astrom, “Optimal control of markov processes with incomplete
state information,” Journal of mathematical analysis and applications,
vol. 10, no. 1, pp. 174–205, 1965.
[34] D. Silver and J. Veness, “Monte-carlo planning in large pomdps,” in
Advances in neural information processing systems, 2010, pp. 2164–
2172.
[35] L. Kocsis and C. Szepesvári, “Bandit based monte-carlo planning,” in
European conference on machine learning. Springer, 2006, pp. 282–
293.

