Optimal Observation Mode Scheduling for Systems
under Temporal Constraints

arXiv:1602.08260v1 [cs.LO] 26 Feb 2016

Eva Tesařová, Mária Svoreňová, Jiřı́ Barnat, Ivana Černá

Abstract— Autonomous control systems use various sensors
to decrease the amount of uncertainty under which they
operate. While providing partial observation of the current
state of the system, sensors require resources such as energy,
time and communication. We consider discrete systems with
non-deterministic transitions and multiple observation modes.
The observation modes provide different information about
the states of the system and are associated with non-negative
costs. We consider two control problems. First, we aim to
construct a control and observation mode switching strategy
that guarantees satisfaction of a finite-time temporal property
given as a formula of syntactically co-safe fragment of LTL
(scLTL) and at the same time, minimizes the worst-case cost
accumulated until the point of satisfaction. Second, the bounded
version of the problem is considered, where the temporal
property must be satisfied within given finite time bound. We
present correct and optimal solutions to both problems and
demonstrate their usability on a case study motivated by robotic
applications.

I. I NTRODUCTION
Embedded systems used in transportation, medical and
other safety critical applications typically operate under
uncertainty. The source of the uncertainty can be of two
types. The internal uncertainty is bounded to the system’s
control inputs such as noisy actuators in mobile robots. The
external uncertainty arises from the system’s interaction with
the environment such as other robots or people operating in
the same space. In order to lower the amount of uncertainty,
sensors are deployed to provide information about the current
state of the system. Individual sensors and their combinations
may provide varying, partial observation of the current state
of the system. At the same time, their deployment requires
resources such as energy, time or communication.
The field of sensor scheduling studies the problem of the
deployment of sensors in order to optimize estimation of a
signal connected to the system’s state. There is a wide range
of results, e.g., for linear systems [20], hybrid systems [9]
and for applications in robot motion planning [14]. The
related field of information gathering assumes a fixed set
of sensors and aims to find a control strategy for the
system that optimizes estimation of the signal. Recently, a
problem combining optimization with temporal objectives
has been considered in information gathering for discrete
systems [10].
Partial observability has been extensively studied for
discrete systems in artificial intelligence and game theory.
The authors are with Faculty of Informatics, Masaryk
University, Brno, Czech Republic, xtesaro2@fi.muni.cz,
svorenova@mail.muni.cz, barnat@fi.muni.cz,
cerna@muni.cz. This work has been partially supported by the
Czech Science Foundation grant No. 15-08772S.

The main focus is typically on partially observable Markov
decision processes (POMDPs) that model both partial observation and probabilistic uncertainties. The optimization
objectives include expected total cost over finite horizon [3],
and expected average or discounted total cost over infinite
horizon [11], [15]. Besides optimization objectives, many
systems also operate under temporal constraints. Recently,
temporal logics such as Linear Temporal Logic (LTL) or
Computation Tree Logic (CTL) have been increasingly used
to specify temporal properties of systems such as reachability, safety, stability of response. The overview of results
for partially observable stochastic games (with POMDPs
as a subclass) with respect to various classes of temporal
objectives can be found in [5]. It is important to note that
most of the problems of quantitative nature formulated for
POMDPs are undecidable to solve precisely or even to
approximate [5], [13]. All the above results consider systems
with one fixed observation mode that can be seen as a
deployment of a single sensor.
Comparing to the aforementioned fields of study, in this
work we focus on a problem that combines the optimal
and temporal control for systems with multiple observation
modes. We present a discrete system for modeling the above
setting referred to as a non-deterministic transition system
(NTS) with observation modes. The non-determinism can be
used to model both the internal and external uncertainty of
the system whereas observation modes capture the sensing
capabilities. In every step of an execution of the system,
one decides which mode of partial observation to activate.
Activation of each observation mode is associated with a
non-negative cost. An example of a robotic system with
limited energy resources and multiple sensing capabilities
is a planetary rover. In [14], the authors design an optimal
schedule for the use of a localization system in a rover
that minimizes energy consumption while at the same time
guarantees safe path following. While sensor readings are
typically continuous, in this work we assume that the set of
readings that affect decision-making can be represented by a
finite set, e.g., sets of values satisfying the same constraints.
We consider the following two problems. First, the aim
is to construct a control and observation mode switching
strategy for an NTS with observation modes that (i) guarantees satisfaction of a finite-time temporal property given as a
formula of syntactically co-safe fragment of LTL (scLTL)
and (ii) minimizes the worst-case cost accumulated until
the point of satisfaction. The second problem considers the
bounded version of the above problem, where the temporal
property is required to be satisfied in at most k ≥ 1 steps.

Leveraging techniques from automata-based model checking
and graph theory, we present correct and optimal solutions
to both problems. While in this work, we restrict ourselves
to objectives over finite time horizon, the aim is to use
these results as a basis for solving more intriguing problems
in our future work, e.g., involving infinite-time temporal
properties and cost functions, and probabilistic models. At
the same time, temporal properties over finite horizon offer
lower computational and strategy complexity compared to
the general class of temporal properties and cover many
interesting properties typically considered, e.g., in robotic
applications [12], [10], [19].
To the best of our knowledge, discrete systems with
multiple modes were first considered only recently in [7], [6],
where the authors focus on control with respect to properties
in infinite time horizon. The most related work to ours is [2]
that considers a variation of POMDPs, where at each step
the user can either choose to use the partial information or
pay a fixed cost and receive the full information about the
current state of the system. The authors discuss the problems
of minimizing the worst-case or expected total cost before
reaching a designated goal state with probability 1. While the
former problem has optimal, polynomial solution, the latter
proves undecidable. The main contribution of our work is
twofold. First, we introduce a new model that extends the
one in [2] in the sense that we allow multiple observation
modes with varying costs. Second, we design correct and
optimal strategies to control such models to guarantee an
scLTL formula while minimizing the corresponding cost,
over bounded or unbounded time horizon.
The rest of this paper is organized as follows. In Sec. II,
we introduce NTS with observation modes and necessary
definitions from temporal logic and automata theory. The
two problems of interest are stated in Sec. III and solved in
Sec. IV and V, respectively. For better readability, we use an
illustrative example to demonstrate the presented framework.
In Sec. VI, we evaluate the proposed algorithms on a case
study motivated by robotic applications. We conclude with
final remarks and future directions in Sec. VII.
II. P RELIMINARIES
A. Notation
For a set X, we use X ∗ to denote the set of all finite sequences of elements of X. A finite sequence σ = x0 . . . xn ∈
X ∗ has length |σ| = n + 1, σ(i) = xi is the i-th element
and σ i = σ(i) . . . σ(n) is the suffix starting with the i-th
element, for 0 ≤ i ≤ n. Similarly, for an infinite sequence
ρ = x0 x1 . . . ∈ X ω , ρ(i) = xi for all i ≥ 0. A prefix of a
finite sequence σ or an infinite sequence ρ is any sequence
σ(0) . . . σ(k) for 0 ≤ k ≤ |σ| or ρ(0) . . . ρ(k) for k ≥ 0,
respectively.

is the initial state, AP is a set of atomic propositions, and
L : S → 2AP is a labeling function.
A run of a NTS is an infinite sequence s0 s1 . . . ∈ S ω such
that for every i ≥ 0 there exists a ∈ A with si+1 ∈ T (si , a).
A finite run is a finite prefix of a run of the NTS.
Definition 2 (NTS with observation modes): A NTS with
observation modes is a tuple (N , O, M ), where N =
(S, A, T, sinit , AP , L) is NTS, O is a non-empty finite set of
observations and M is a non-empty finite set of observation
modes. Every observation mode m ∈ M is associated with
an observation function γm : S → 2O and a cost gm ∈ R+
0.
A run of a NTS with observation modes is an infinite
sequence ρ = (s0 , m0 )(s1 , m1 ) . . . ∈ (S × M )ω such
that s0 s1 . . . is a run of the NTS. A finite run σ =
(s0 , m0 ) . . . (sn , mn ) ∈ (S × M )∗ of the NTS with observation modes is a finite prefix of a run. A pair (s, m) ∈ S × M
of a state and an observation mode is called a configuration.
Given a finite run σ = (s0 , m0 ) . . . (sn , mn ), we define
the cost of σ as follows
n
X
g(σ) =
gmi .
(1)
i=0

The observational trace of a run ρ = (s0 , m0 )(s1 , m1 ) . . .
is the sequence γ(ρ) = γm0 (s0 )γm1 (s1 ) . . . ∈ (2O )ω
and the propositional trace of ρ is the sequence L(ρ) =
L(s0 )L(s1 ) . . . ∈ (2AP )ω . The observational and propositional traces of finite runs are defined analogously.
Definition 3 (Strategy): Given a NTS with observation modes, a (observation-based control and observation
scheduling) strategy is a function C : (2O )∗ → A × M that
defines the action and the observation mode to be applied in
the next step based only on the sequence of past observations.
We use σC and ρC to denote finite and infinite runs of
the NTS N induced by a strategy C, respectively. Note that
for every configuration (s, m), the strategy C induces a nonempty set of runs ρC with ρC (0) = (s, m).
Example 1: Consider
an
NTS
N
=
(S, A, T, sinit , AP , L), where S = {s1 , . . . , s7 }, A = {a, b},
sinit = s1 and the transition function is as depicted in Fig. 1.
We let AP = {?} and the labeling function is indicated in
Fig. 1, i.e., L(s6 ) = {?} and L(si ) = ∅ for every i 6= 6.
Consider three observation modes M = {m1 , m2 , m3 } for
N such that their respective observation functions γ1 , γ2 , γ3
report neither the shape nor the color, only the shape and
both the shape and the color of the state as shown in Fig. 1.
Hence, the set of observations is
O = {white, blue, red,
circle, rectangle, diamond}

B. System with observation modes

For example, for state s2 the observation functions are
defined as γ1 (s2 ) = ∅, γ2 (s2 ) = {rectangle}, γ3 (s2 ) =
{rectangle, blue}. The costs of the observation modes
are g1 = 0, g2 = 1, g3 = 2.

Definition 1 (NTS): A non-deterministic transition system
(NTS) is a tuple N = (S, A, T, sinit , AP , L), where S is a
non-empty finite set of states, A is a non-empty finite set of
actions, T : S × A → 2S is a transition function, sinit ∈ S

C. Specification
Linear temporal logic (LTL) is a modal logic with modalities referring to time [16]. Formulas of LTL are interpreted
over infinite words such as the propositional traces generated

start

s1

a
a
a

s2

a
b

s3

a
b

a

s4

b
a

∅, {?}

∅

s5
start

s6

a

s7

a

Fig. 2.

Fig. 1. Example of an NTS with observation modes. For full description
see Ex. 1.

by runs of a NTS with observation modes. Co-safe fragment
of LTL, or co-safe LTL, contains all LTL formulas such that
every satisfying infinite word has a good finite prefix [12]. A
good finite prefix is a finite word such that every its extension
to an infinite word satisfies the formula. A class of co-safe
LTL formulas that are easy to characterize are syntactically
co-safe LTL formulas [12].
Definition 4 (scLTL): Syntactically co-safe LTL (scLTL)
formulas over AP are the LTL formulas formed as follows:
ϕ :: p | ¬p | ϕ ∧ ϕ | ϕ ∨ ϕ | X ϕ | ϕ U ϕ | F ϕ,
where p ∈ AP , ∧ (conjunction) and ∨ (disjunction) are
Boolean operators, and X (next), U (until) and F (future
or eventually) are temporal operators.
The satisfaction relation |= is recursively defined as follows. For a word w ∈ (2AP )ω , we let:
w |= p
⇔ p ∈ w(0),
w |= ¬p
⇔ p 6∈ w(0),
w |= ϕ1 ∧ ϕ2 ⇔ w |= ϕ1 and w |= ϕ2 ,
w |= ϕ1 ∨ ϕ2 ⇔ w |= ϕ1 or w |= ϕ2 ,
w |= X ϕ
⇔ w1 |= ϕ,
w |= ϕ1 U ϕ2 ⇔ there exists i ≥ 0 : wi |= ϕ2 ,
and for all 0 ≤ j < i : wj |= ϕ1
w |= F ϕ
⇔ there exists i ≥ 0 : wi |= ϕ.
Remark 1: To express properties over bounded time horizon, bounded temporal opeators U≤k , F≤k are often used
in the literature. Note that these can be encoded using the
operators from Def. 4.
Even though scLTL formulas have infinite-time semantics,
their satisfaction is guaranteed in finite time through the
concept of good finite prefixes as explained above. We
represent scLTL formulas with finite automata.
Definition 5 (DFA): A deterministic finite automaton
(DFA) is a tuple A = (Q, 2AP , δ, q0 , F ), where Q is a nonempty finite set of states, 2AP is the alphabet, δ : Q×2AP →
Q is a transition function, q0 ∈ Q is the initial state and
F ⊆ Q is a non-empty set of accepting states.
A run of a DFA is a finite sequence q0 q1 . . . qn ∈ Q∗
such that for every i ≥ 0, there exists X ∈ 2AP such that
qi+1 = δ(qi , X). Every finite word w ∈ (2AP )∗ induces a
run of the DFA. A run is called accepting if its last state is
an accepting state. A word w is accepted by the DFA if it
induces an accepting run.
Given an scLTL formula ϕ, one can construct a minimal
(in the number of states) DFA that accepts all and only good
finite prefixes of ϕ using a translation algorithm from [12]
and automata theory techniques [17].

{?}

q0

q1

A minimal DFA for the scLTL formula from Ex. 2.

A run ρ of a NTS with observation modes satisfies an
scLTL formula ϕ if L(ρ) |= ϕ or, equivalently, if there exists
a finite prefix ρϕ of ρ such that L(ρϕ ) is a good finite prefiex
for the formula ϕ. We refer to prefixes ρϕ as the good finite
prefixes of the run ρ for the formula ϕ. We say that a strategy
C satisfies ϕ starting from a configuration (s, m) if ρC |= ϕ
for every run ρC such that ρC (0) = (s, m).
Example 2: Consider the set of atomic propositions
AP = {?}. An example of an scLTL formula over AP is
ϕ = F ?. A corresponding minimal DFA A for ϕ is shown
in Fig. 2.
III. P ROBLEM FORMULATION
Consider a NTS with observation modes (N , O, M ). The
main motivation for the problem formulated in this section
is a robotic system, e.g., an autonomous car driving in an
urban-like environment, that involves uncertainty originating,
e.g., from the motion of the robot such as noisy actuators of
the car or from interaction with dynamic elements in the
environment such as pedestrians on streets. Typically, the
system is equipped with a set of sensors, where each sensor
provides a partial information about the uncertainties. In such
a case, an NTS can be used to model the motion capabilities
of the robot in a partitioned environment and its interaction
with the dynamic elements. The observation modes of the
NTS then represent possible subsets of sensors and the
cost of an observation mode corresponds to the amount of
resources such as energy or communication needed to deploy
the chosen set of sensors for a single step. During executions
of the system, only the observations associated with the
current state of the NTS and the chosen observation mode
are available. Hence, the current state of the system might
not be uniquely recognized.
We assume that the system is given a temporal objective
in the form of an scLTL formula ϕ over the set of atomic
propositions AP . Given a starting configuration (s, m) and
a strategy C that satisfies the formula ϕ, we define the
following cost function:
V (C, (s, m), ϕ) =

max
ρC ,ρC (0)=(s,m)

min g(ρϕ ).

ρϕ ρ0 =ρC

(2)

Intuitively, the cost V (C, (s, m), ϕ) of a strategy C with
respect to the formula ϕ and the configuration (s, m) is the
worst-case cumulative cost of the (earliest) satisfaction of ϕ
using C starting from configuration (s, m).
In this work, we aim to synthesize strategies that optimize
the above cost, while at the same time guarantee satisfaction
of the scLTL formula. We consider both general and bounded
version of this problem, formulated as follows.
Problem 1 (Optimal scLTL control): Given
NTS with observation modes (N , O, M ),

a
where

N
= (S, A, T, sinit , AP , L), an initial observation
mode minit ∈ M , and an scLTL formula ϕ over
AP , find an observation-based control and observation
scheduling strategy C such that (1) C satisfies ϕ starting
from the configuration (sinit , minit ), and (2) the cost
V (C, (sinit , minit ), ϕ) is minimized over all strategies
satisfying ϕ starting from the configuration (sinit , minit ).
Problem 2 (Bounded optimal scLTL control): Given
a NTS with observation modes (N , O, M ), where
N = (S, A, T, sinit , AP , L), an initial observation mode
minit ∈ M , an scLTL formula ϕ over AP , and a finite bound
k ≥ 0, find an observation-based control and observation
scheduling strategy C such that (1) C satisfies ϕ starting
from the configuration (sinit , minit ) in at most k steps,
and (2) the cost V (C, (sinit , minit ), ϕ) is minimized over
all strategies satisfying ϕ starting from the configuration
(sinit , minit ) in at most k steps.
In Sec. IV, we propose an algorithm to solve the general
Problem 1 and prove its correctness and optimality. The
algorithm builds on techniques from automata-based model
checking and graph theory. The bounded Problem 2 can
be solved using an alternation of the above algorithm as
proposed in Sec. V. Both algorithms are demonstrated in
Sec. VI on an illustrative case study of a mobile robot in an
indoor environment equipped with a set of sensors.
Example 3: Consider the NTS with observation modes
introduced in Ex. 1 with initial observation mode m1 and
the scLTL formula from Ex. 2 that requires to reach the
state labeled with ? , i.e., state s6 . Note that only in states
s2 , s3 , s4 there is more than one action allowed and hence
it suffices to discuss strategies based on their decision in
these states. No strategy C with C(∅) = (a, m1 ), i.e., a
strategy that applies action a starting from the initial state
s1 and activates observation mode m1 in the next state, can
guarantee satisfaction of the formula. The reason is that the
three states s2 , s3 , s4 cannot be told apart using mode m1
and both actions a, b always in at least one case lead to state
s7 from which s6 cannot be reached. Consider strategy C1
that recognizes the shape of the three states s2 , s3 , s4 , i.e.,
C1 (∅) = (a, m2 ),
C1 (∅{rectangle}) = (a, m1 ),
C1 (∅{diamond}) = (b, m1 ).
Strategy C1 guarantees a visit to s6 in at most 3 steps and
its cost V (C1 , (sinit , m1 ), ϕ) = 1. Alternatively, consider
strategy C2 that recognizes both the shape and the color of
the three states s2 , s3 , s4 , i.e.,
C1 (∅) = (a, m3 ),
C1 (∅{rectangle, blue}) = (b, m1 ),
C1 (∅{rectangle, red}) = (a, m1 ),
C1 (∅{diamond,white}) = (b, m1 ).
Strategy C2 guarantees a visit to s6 in 2 steps and its cost
V (C2 , (sinit , m1 ), ϕ) = 2. Strategy C1 is the solution to the
optimal scLTL control Problem 1 as its cost is lower than
the cost of C2 . However, if we consider the bounded optimal

a

(s2 , q0 )

(s5 , q0 )

b
a

a
start

(s1 , q0 )

a

a

(s3 , q0 )

(s6 , q0 )

a

(s7 , q1 )

a

b

a
b

(s4 , q0 )

Fig. 3.

a

(s7 , q0 )

a

Product of the NTS from Ex. 1 and the DFA from Ex. 2.

scLTL control Problem 2 with k = 2, then C2 is the solution
as C1 may need more than 2 steps to reach s6 .
IV. O PTIMAL SC LTL CONTROL
In this section, we describe the algorithm to solve Problem 1 in detail. To approach the problem, we leverage
automata-based model checking techniques that analyze the
state space using graph algorithms. We first construct a
synchronous product of the NTS N and a DFA A for the
scLTL formula ϕ, where the runs of the NTS satisfying
the formula can be easily identified through accepting states
of the DFA. Next, to account for the non-determinism and
partial observation, we use a belief construction over the
product that determines the set of possible current states of
the product given any finite sequence of past observations.
Using graph algorithms, we construct a strategy for the belief
product that guarantees a visit of an accepting state and
minimizes a function derived from the costs of the associated
observation modes. Finally, we map the strategy from the
belief product to the original NTS and prove that the resulting
strategy is a solution to Problem 1.
A. Constructing the product
Definition 6 (Product): Let N = (S, A, T, sinit , AP , L)
be a NTS and A = (Q, 2AP , δ, q0 , F ) be a DFA. The
synchronous product is a tuple
P = N × A = (S × Q, A, TP , (sinit , q0 ), AP , LP , FP ),
where
• S × Q is the set of states,
• A is the alphabet,
S×Q
• TP : S × Q × A → 2
is a transition function such
0 0
that (s , q ) ∈ TP ((s, q), a) if and only if s0 ∈ T (s, a)
and δ(q, L(s)) = q 0 ,
• (sinit , q0 ) is the initial state,
AP
• LP : S × Q → 2
is the labeling function such that
LP ((s, q)) = L(s),
• FP = {(s, q) | q ∈ F } is the set of product accepting
states.
Note that the product can be seen as an NTS with a set of
accepting states. This allows us to adopt the definitions of
an infinite and finite runs for the product as well as a notion
of an accepting finite run.
Example 4: In Fig.. 3, we depict the product constructed
for the NTS with observation modes presented in Ex. 1 and
the DFA from Ex. 2.

start

(a, m0 ), 0

{(s1 , q0 )}

{(s2 , q0 ), (s3 , q0 ), (s4 , q0 )}

(a, m

1 ), 1

(a
,m
),

2

2

(a, m2 ), 2

{(s3 , q0 )}

(a,
m
1 ),
(a,
1
m
2 ),
2

{(s2 , q0 ), (s3 , q0 )}

{(s2 , q0 )}

{(s4 , q0 )}

Definition 8 (Strategy): Given a weighted belief product
B = (B, A, TB , binit , O, FB , w), a strategy for B is a
function C : B∗ → A.
We call a strategy C memoryless if it can be defined as
a function C : B → A. If the context is clear, we use σC
and ρC to denote finite and infinite runs of B induced by a
strategy C, respectively.
C. Constructing a strategy for the belief product

Fig. 4. Part of the weighted belief product for the NTS with observation
modes presented in Ex. 1 and the DFA from Ex. 2. The costs of individual
belief actions are written in bold.

We abuse the notation by using γα to denote the observation function of a sensor α ∈ Θ as well as its extension to
S × Q, i.e., γα ((s, q)) = γα (s) for all (s, q) ∈ S × Q.
B. Constructing the belief product
The belief construction over the product follows the standard principles used for partially observable systems. Besides
keeping track of the states that the product can currently be
in, we also keep track of the observation mode deployed in
the current state.
Definition 7 (Weighted belief product): Given a product
P and a set of observation modes M with the initial observation mode minit , we define the weighted belief product
B = (B, A, TB , binit , O, FB , w)
over P, where
S×Q
• B⊆2
is the set of all belief states, where a belief
state b ∈ B is a set of product states such that there
exists an observation mode m ∈ M such that all states
in b have the same observations in mode m,
• A = A × M is the set of belief actions of the form
a = (a, m), where a ∈ A is an action of P and m ∈ M
is an observation mode,
B
• TB : B × A → 2
is the transition function such that
0
a belief state b ∈ TB (b, (a, m0 )) if and only if b0 is
the set of all product states that can be reached in one
step from a state in b using action a and have the same
observations in mode m0 ,
• binit = {(sinit , q0 )} is the initial state,
• FB = {b | b ⊆ FP } is the set of accepting belief states,
+
• w : B × A → R0 is the weight function such that
w(b, (a, m)) = gm .
Weighted belief product can be seen as a NTS with a
set of accepting states and a weight function on transitions.
We adopt definitions of finite and infinite runs of the belief
product and an accepting finite run.
Corollary 1: From the definition of the weighted belief
product B it follows that every finite run of B corresponds
to exactly one finite sequence of observations in (2O )∗ and
at the same time, every finite sequence of observations in
(2O )∗ corresponds to at most one finite run of B.
Example 5: In Fig.. 4, we depict part of the weighted
belief product constructed for the NTS with observation
modes presented in Ex. 1 and the DFA from Ex. 2.

In this section, we propose an algorithm that constructs
a memoryless strategy for the weighted belief product that
guarantees a visit to an accepting state (if such a strategy
exists) and minimizes the worst-case cumulative weight. We
prove that such a strategy then maps to a strategy for the
original NTS with observation modes that solves Problem 1.
The algorithm can be seen as a combination of the standard
algorithm for computing winning states in non-deterministic
systems [1] and Dijkstra’s algorithm for computing shortest
paths in a weighted graph [8].
In the algorithm, we incrementally compute a value
wtg(b) (weight-to-go) for every belief state b that is the
minimum worst case weight of reaching an accepting state
starting from b. Initially, the value is 0 for accepting belief
states and ∞ otherwise. We use Wi to denote the set of belief
states for which the value wtg(b) 6= ∞ after i-th iteration. In
i-th iteration, we consider the belief state bmin ∈ B \ Wi−1
and its action abmin that leads to the set Wi−1 and minimizes
the worst-case sum of the weight of the action and the value
wtg of a successor state. The algorithm terminates when the
initial belief state binit is added to the set Wi or when there
exists no state b ∈ B \ Wi with an action leading to Wi .
If the resulting set Wi contains the initial belief state, the
strategy consisting of the above actions for each belief state
in Wi is returned. The algorithm is summarized in Alg. 1.
Proposition 1 (Correctness): Alg. 1 results in a strategy
C for the weighted belief product such that every run under
C that starts in binit eventually visits an accepting belief
state, if such a strategy exists.
Proof: The property can be proved by induction on the
iteration counter i and proving that starting from the state
bi ∈ Wi , bi 6∈ Wi−1 , strategy C guarantees a visit to an
accepting belief state in at most i steps.
Proposition 2 (Optimality): Let C be the strategy resulting from Alg. 1. Then among all strategies that guarantee a
visit to an accepting belief state, C minimizes the value
VB (C, binit ) =

max
ρC ,ρC (0)=binit

min

ρacc ρ0 =ρC

w(ρacc , C)

(3)

where ρacc is a finite run ending in an accepting state and
|ρacc |−2

w(ρ

acc

, C) =

X


w ρacc (i), C(ρacc (0) . . . ρacc (i)) .

i=0

Intuitively, the value VB (C, b) of a strategy C with respect
to a belief state b is the worst-case cumulative weight of the
(earliest) visit to an accepting state using C starting from b.
Proof: We show by induction that after every iteration
i ≥ 1, it holds that VB (C, bi ) = wtg(bi ) for all states
bi ∈ Wi , i.e., the strategy C realizes the values wtg(bi ),

Algorithm 1 Constructing a strategy for the weighted belief
product that maps to a solution of Problem 1.
Input: B = (B, A, TB , binit , O, FB , w)
Output: memoryless strategy C for the belief product B
1: W0 := FB
2: ∀ b ∈ W0 : wtg(b) := 0
∀ b ∈ (B\W0 ) : wtg(b) := ∞
3: i := 1
4: while binit 6∈ Wi and exist b ∈ B\Wi−1 and a ∈ A such that
∅ 6= TB (b, a) ⊆ Wi−1 do
5:
bmin := ⊥
amin := ⊥
∆min := ∞
6:
for every b ∈ B\Wi−1 and a ∈ A such that ∅ 6=
TB (b, a) ⊆ Wi−1 do
7:
∆ := 0 max {w(b, a) + wtg(b0 )}
b ∈TB (b,a)

8:
9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:

if ∆ < ∆min then
bmin := b
amin := a
∆min := ∆
end if
end for
Wi := Wi−1 ∪ {bmin }
C(bmin ) := amin
wtg(bmin ) := ∆min
i := i + 1
end while
if binit ∈ Wi then
return C
else
return no suitable strategy exists
end if

and that the strategy C minimizes the value VB (·, bi ) among
all strategies that guarantee visit to an accepting state.
Assume that the strategy C is computed in n iterations
of the “while” cycle in line 4, i.e., Wn is the resulting
fixed point set. Consider a belief state bi that was added
to the set Wn in i-th iteration, i.e., bi 6∈ Wi−1 , bi ∈ Wi .
Assume that for all j < i it holds that C minimizes the value
VB (·, bj ) for every bj ∈ Wj and that VB (C, bj ) = wtg(bj ).
Trivially, C minimizes the value for all accepting belief states
b ∈ FB as VB (C, b) = 0 = wtg(b). We show that C then
also minimizes the value VB (·, bi ) over all strategies and
VB (C, bi ) = wtg(bi ).
Assume by contradiction that there exists a (possibly not
memoryless) strategy C 0 for B such that VB (C 0 , bi ) <
VB (C, bi ). As C is optimal for all bj , j < i, it must hold
that
VB (C 0 , bj ) = wtg(bj ) = VB (C, bj ).

(4)

Let b ∈
/ Wi−1 be a belief state such that there exists a run
σC 0 under C 0 that leads from bi through b to an accepting
b
b
belief state and TB (b, C 0 (σC
0 )) ⊆ Wi−1 , where σC 0 is a
prefix of σC 0 ending in the state b. Note that such b must
exist since C 0 guarantees a visit to an accepting state and
FB ⊆ Wi−1 (be aware that b can be bi itself). Since
b
0
the cumulative weight w(σC
0 , C ) is non-negative and the
action C(bi ) minimizes the value in line 7, it holds that
the cumulative weight w(σC 0 , C 0 ) is higher or equal to the
cumulative weight of any run σC under C starting in bi
leading to an accepting belief state. Hence VB (C 0 , bi ) ≥
VB (C, bi ) and strategy C is optimal.

D. Constructing a strategy for the NTS
Let CB be the strategy for the weighted belief product B
resulting from Alg. 1. Consider the following (observationbased control and observation scheduling) strategy C for the
NTS N with observation modes M . For a finite sequence of
observations σO ∈ (2O )∗ , we define
C(σO ) = CB (b),

(5)

where b is the last state of the finite run σB of the belief
product that corresponds to σO as described in Cor. 1, if such
run exists.
Theorem 1: Let CB be the strategy for the weighted belief
product B resulting from Alg. 1. Then the strategy C for the
NTS with observation modes constructed according to Eq. 5
is a solution to Problem 1.
Proof: The correctness with respect to the scLTL
formula ϕ follows directly from Prop. 1. The optimality of C follows from Prop. 2 and the fact that
V (C, (sinit , minit ), ϕ) = VB (CB , binit ).
Complexity. Given an scLTL formula ϕ the number of
states of a corresponding minimal DFA A is in general
doubly exponential in the size of the formula. However,
compared to the size of the NTS, the size of the automaton typically does not play a crucial role in the overall
complexity. The product P of the NTS N and A is then
of size O(|S| × |Q|). The belief product B involves a
subset construction over the product, hence its size is in
O(2|S|×|Q| ). In order to minimize the complexity in practice,
only the reachable states of both the product and the belief
product are constructed. With a proper choice of a data
structure storing the belief product B, Alg. 1 runs in time
O(|B| · log |B| + |A| · dn), where dn is the degree of nondeterminism of the NTS N , i.e., the maximum number of
possible successors given a state and an action. Note that
while the algorithms are polynomial with respect to their
input, i.e., the belief product, they are exponential in the
size of the original NTS.
V. B OUNDED OPTIMAL SC LTL CONTROL
In order to solve the bounded version of Problem 1, i.e.,
Problem 2, we proceed as follows. As in the case for the
general problem, we first construct the product P of the
NTS N with a DFA A for the scLTL formula ϕ and the
corresponding belief product B as proposed in Sec. IV-A
and IV-B, respectively. To compute a strategy for the belief
product from Sec. IV-C, we use an alternation of Alg. 1
presented below and summarized as Alg. 2. Intuitively, as
Alg. 1 builds on the principles of Dijkstra’s algorithm, Alg. 2
follows the idea behind Bellman-Ford algorithm for solving
the bounded shortest path problem in weighted graphs [8].
We prove properties of the resulting strategy CB for the belief
product and argue that when mapped to the original system
as described in Sec. IV-D, we obtain a correct and optimal
solution to Problem 2.
A. Constructing a strategy for the belief product
In this section, we describe an algorithm that constructs
a strategy for the weighted belief product that guarantees

Algorithm 2 Constructing a strategy for the weighted belief
product and the given bound that maps to a solution of
Problem 2.
Input: B = (B, A, TB , binit , O, FB , w), bound k ≥ 1
Output: strategy C for the belief product B
1: W0 := FB
2: ∀ b ∈ W0 : wtg(b) := 0
∀ b ∈ (B\W0 ) : wtg(b) := ∞
3: i := 1
4: while i ≤ k do
5:
for every b ∈ B do
6:
ab
∆b
min := ⊥
min := wtg(b)
7:
for every a ∈ A such that ∅ =
6 TB (b, a) ⊆ Wi−1 do
8:
∆ := 0 max {w(b, a) + wtg(b0 )}
b ∈TB (b,a)

9:
10:
11:
12:
13:
14:
15:
16:
17:
18:
19:
20:
21:
22:
23:
24:
25:
26:
27:
28:

if ∆ < ∆b
min then
ab
∆b
min = a
min := ∆
end if
end for
end for
Wi := Wi−1
for every state b ∈ B do
C(b) := ab
min
wtg(b) := ∆b
min
if wtg(b) < ∞ then
Wi := Wi ∪ {b}
end if
end for
i := i + 1
end while
if binit ∈ Wi then
return C
else
return no suitable strategy exists for given bound
end if

a visit to an accepting belief state within k steps (if such
a strategy exists) and minimizes the worst-case cumulative
weight.
Instead of computing the weight-to-go value wtg(b) for
a single well-chosen belief state b at a time as in Alg. 1,
in Alg. 2 we update the value in parallel for all states
in every iteration. We show that the set Wi which is the
set of all belief states for which wtg(b) 6= ∞ after i-th
iteration, consists of all belief states b that can reach an
accepting belief state in at most i steps and with the worstcase cumulative weight wtg(b). The algorithm terminates
after k, but at most |B| − 1, iterations. If the resulting set
Wi contains the initial belief state, the strategy consisting of
the chosen actions for each belief state in Wi is returned.
Proposition 3 (Correctness): Alg. 2 results in a strategy
C for the weighted belief product such that every run under
C that starts in binit visits an accepting belief state in at
most k steps, if such a strategy exists.
Proof: The property can be proved by induction on the
iteration counter i and proving that starting from any state
bi ∈ Wi , strategy C guarantees a visit to an accepting belief
state in at most i steps.
Proposition 4 (Optimality): Let C be the strategy resulting from Alg. 2. Then among all strategies that guarantee
a visit to an accepting belief state in at most k steps, C
minimizes the value in Eq. 3.

Proof: Let Ci and wtgi denote the strategy and the
weight-to-go computed by Alg. 2 before start of the (i + 1)th iteration. We show by induction that after every iteration
i ≥ 1, it holds that VB (Ci , bi ) = wtgi (bi ) for all states
bi ∈ Wi , and that strategy Ci minimizes the value VB (·, bi )
among all strategies that guarantee visit to an accepting state
in at most i steps.
Assume that for all j < i it holds VB (Cj , bj ) = wtgj (bj )
for all states bj ∈ Wj , and that strategy Cj minimizes
the value VB (·, bj ) among all strategies that guarantee visit
to an accepting state in at most j steps. Trivially, C0
minimizes the value for all accepting belief states b ∈ FB as
VB (C0 , b) = 0 = wtg0 (b). We show that Ci then minimizes
the value VB (·, bi ) over all strategies that guarantee visit
to an accepting state in at most i steps and VB (Ci , bi ) =
wtgi (bi ).
Assume by contradiction that there exists a strategy C 0
for B such that VB (C 0 , bi ) < VB (Ci , bi ) and guarantee
visit to an accepting state for all bi ∈ Wi in at most i
steps. Recall that Wi−1 contains exactly those states that
guarantee visit to an accepting state in at most i − 1 steps
(see proof of Prop. 3). Let bi be an arbitrary belief state
from Wi . Since C 0 is winning in at most i steps, it holds
TB (bi , C 0 (bi )) ⊆ Wi−1 . From the induction hypothesis and
the fact the action Ci (bi ) minimizes the value in line 7 it
follows that VB (C 0 , bi ) ≥ wtgi (bi ) = VB (Ci , bi ) implying
strategy Ci is optimal strategy among all strategies that
guarantee visit to an accepting state in at most i steps.
Theorem 2: Let CB be the strategy for the weighted belief
product B resulting from Alg. 2. Then the strategy C for the
NTS with observation modes constructed according to Eq. 5
is a solution to Problem 2.
Proof: The correctness with respect to the scLTL
formula ϕ follows directly from Prop. 3 and the optimality of C follows from Prop. 4 and the fact that
V (C, (sinit , minit ), ϕ) = VB (CB , binit ).
Complexity. The size of a minimal DFA for ϕ, the product
and the belief product are discussed in Sec. IV-D. Similarly
as for Alg. 1, with a proper choice of a data structure storing
the belief product B, Alg. 2 runs in time O(k · |B| · |A| · dn),
where dn is the degree of non-determinism of N , i.e., the
maximum number of possible successors given a state and an
action. Here, the value |B|·|A|·dn serves as the upper bound
on the number of all edges in the belief product. Note that
Alg. 2 can be terminated prematurely if the current iteration
i of the while loop in line 4 did not imply any change in the
function wtg or if i ≥ |B|−1 as every strategy for the belief
product that guarantees a visit to an accepting belief state
must do so in at most |B| − 1 steps due to non-determinism.
Remark 2: Note that Alg. 2 can be used not only to solve
the bounded Problem 2, but also the general Problem 1 by
considering k = |B|−1. However, this solution to Problem 1
has higher computational complexity in practice than the one
presented in Sec. IV using Alg. 1.
VI. C ASE S TUDY
We implemented the algorithms from Sec. IV and V in
C++. In this section, we demonstrate their use on a case

1

2

3

Fig. 5. The environment of a mobile robot partitioned into a grid of
5 × 5 equally sized regions. The three grids correspond to three possible
placements of dangerous regions, shown in red. The locations of the starting
region, in green, and the target region, in blue, are known and hence their
placement is the same in all three grids.

NW

NE
det

SW

SE

(a)

NW

N

NE

W

det

E

SW

S

SE

(b)

(c)

Fig. 6.
Two sensors that provide information about the presence of
dangerous regions in robot’s immediate surroundings. We also show the
names of the corresponding observations learned by the robot. For the first
sensor in (a), the surrounding area is divided into quadrants and the sensor
reports all quadrants containing a dangerous region. For the second sensor
in (b), the exact set of dangerous regions is reported. For example, let (c)
show the immediate surroundings of the robot with it’s current position in
the middle and dangerous regions in red. The first sensor reports the set of
observations {NW, NE, SE, det} and the second sensor reports {N, SE, det}.

study motivated by examples in [4], [18]. All executions were
performed on Mac OS X 10.10.3 with 2.6 GHz Intel Core
i5 processor and 8 GB 1600 MHz DDR3 memory.
Consider a mobile robot moving in an environment partitioned into a grid of 5 × 5 equally sized regions. The grid
contains a starting, a target and possibly multiple dangerous
regions, where the robot is detected and captured. The robot
knows the locations of the starting and the target regions
but it does not know the exact locations of dangerous
regions. Nevertheless, the robot knows that the grid takes
one of the three forms depicted in Fig. 5. The robot moves
deterministically in (up to) four directions corresponding
to the movement in the four compass directions. To learn
the presence of dangerous regions in it’s immediate surroundings, the robot can deploy one of the two sensors in
Fig. 6. The first sensor partitions the neighboring area into
quadrants and reports the set of all quadrants that contain
at least one dangerous region. The second sensor reports
the exact regions in robot’s immediate surroundings that
are dangerous. In every step, the robot can decide which
sensor to activate, if any. The costs of deployment of the two
sensors is 1 and 2, respectively. The cost can be interpreted
as the amount of resources needed for the use of each
sensor. Alternatively, it may model the amount of information
received by the enemy in dangerous regions. The goal of the
robot is to reach the target region from the starting region
without being detected, while minimizing the cost.
The NTS with observation modes that models the above
system has 76 states S = {sinit , sijk | 1 ≤ i ≤ 3, 1 ≤
j, k ≤ 5} and 5 actions A = {a, N, S, E, W}. States sijk

correspond to the regions in the three grids, where 1 ≤ i ≤ 3
is the grid identifier and 1 ≤ j, k ≤ 5 determine the row
and column coordinate, respectively. For example, s111 is
the top left corner of the first grid. The initial state sinit
has only one transition T (sinit , a) = {s111 , s211 , s311 } that
corresponds to the enemy choosing one of the three grids
in Fig. 5. The transitions of all sijk are deterministic and
correspond to moving in compass directions N, S, E, W. The
set AP = {dang, target} and the labeling function is
such that L(sinit ) = ∅ and L(sijk ) indicates the target and
dangerous regions as in Fig. 5. The set of observations is O =
{N, S, W, E, NW, NE, SW, SE, det}. The NTS has 3 observation
modes corresponding to not activating any sensor, activating
the first sensor and activating the second sensor, respectively.
The respective observation functions γ1 , γ2 , γ3 are defined in
Fig. 6 and g1 = 0, g2 = 1, g3 = 2. Note that in every step of
an execution of the system, we know the robot’s position in
the grid precisely, only the identifier of the grid is unknown.
The scLTL formula specifying the robot’s mission is
(¬dang) U target and the corresponding minimal DFA A
has 3 states. The product P of N and A has 208 states
and 667 (possibly non-deterministic) transitions, and was
constructed in less than 0.1 seconds. The weighted belief
product B has 375 states and 2634 transitions, and was
constructed in 1.5 seconds.
Using Alg. 1, we computed an optimal solution to Problem 1 for this system in 7 seconds. The corresponding
strategy for the robot is as follows. In the starting region, use
the first sensor. If the reported observations are SE and SW,
then the robot is in grid 1 from Fig. 5. If the set of reported
observations is empty, the robot is moving either in grid 2 or
grid 3. In the former case, do not deploy any sensors anymore
and move in directions E, S, S, S, S, W to reach the target
region. In the latter case, do not use any sensor anymore and
move in directions S, E, E, E, E, S, S, S, W, W, N, W, W, S.
The worst-case cost of the strategy is 1 and the maximum
number of transitions performed by the robot to reach the
target region is 14, i.e., in the NTS N it is 15 including the
first step for choosing the grid.
Next, we used Alg. 2 to solve the bounded version of
the problem for bounds k < 15, where the mission must be
satisfied faster than using the strategy above. For all choices
of k below, the algorithm terminated in less than 3 seconds.
For k ≤ 8, there does not exist a suitable strategy. For k = 13
and k = 14, the optimal strategy has the same structure as
the one resulting from Alg. 1 with the following exception.
If the robot learns that it moves either in grid 2 or 3, the
sequence of directions is S, E, E, E, E, S, S, W, W, W, W, S.
The maximum number of steps needed to reach the target
region is 13 and the worst-case cost of the strategy is 1.
Finally, for 9 ≤ k ≤ 12 there exists a solution and the
corresponding optimal strategy for the robot is as follows.
From the starting region, move in directions E and then S
without deploying any sensor. Then move in direction E and
activate the second sensor. If the reported observations are S
and SE then the robot is moving in grid 1. In such a case,
do not use any sensors anymore and move in directions

W, S, S, S, W to reach the target region. Similarly, if the
observations are S an N then the robot is in grid 2, do not use
any sensors anymore and move in directions W, S, S, W, S.
Finally, if the observations are SW, SE and N then the robot
is in grid 3, do not use any sensors and move in directions
S, S, S, W, W. While the maximum number of steps needed
to reach the target region is 9, the worst-case cost of the
strategy is 2.
VII. C ONCLUSION AND F UTURE W ORK
We consider non-deterministic transition systems with
multiple observation modes with fixed non-negative costs.
We present correct and optimal algorithms to solve two
optimal temporal control problems. The first aims to construct a control and observation mode switching strategy
that guarantees satisfaction of a finite-time temporal property
given as a formula of scLTL and minimizes the worst-case
cost accumulated until the point of satisfaction. Second, we
consider the bounded version of the problem with a bound
on the time of satisfaction. Both algorithms are demonstrated
on a case study motivated by robotic application.
In our future work, we aim to use the results presented
in this work as a basis for solving more intriguing problems
of observation scheduling under temporal constraints. The
extensions include infinite-time temporal properties, infinitetime optimization objectives and probabilistic models.
R EFERENCES
[1] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT
Press, 2008.
[2] N. Bertrand and B. Genest. Minimal Disclosure in Partially Observable
Markov Decision Processes . In Proc. of FSTTCS, volume 13, pages
411–422, 2011.
[3] K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia. Optimal Cost
Almost-Sure Reachability in POMDPs. In Proc. of AAAI, pages 3496–
3502, 2015.
[4] K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia. Qualitative
analysis of POMDPs with temporal logic specifications for robotics
applications. In Proc. of ICRA, pages 325–330, 2015.
[5] K. Chatterjee, L. Doyen, and T. A. Henzinger. A survey of partialobservation stochastic parity games. Formal Methods in System
Design, 43(2):268–284, 2013.
[6] K. Chatterjee and R. Majumdar. Minimum Attention Controller
Synthesis for Omega-Regular Objectives. In Proc. of FORMATS,
volume 6919 of Lecture Notes in Computer Science, pages 145–159,
2011.
[7] K. Chatterjee, R. Majumdar, and T. Henzinger. Controller Synthesis
with Budget Constraints. In Proc. of HSCC, volume 4981 of Lecture
Notes in Computer Science, pages 72–86, 2008.
[8] T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson. Introduction
to Algorithms. McGraw-Hill Higher Education, 2nd edition, 2001.
[9] Z. Feng, K. Teo, and V. Rehbock. Hybrid method for a general optimal
sensor scheduling problem in discrete time. Automatica, 44(5):1295
– 1303, 2008.
[10] A. Jones, M. Schwager, and C. Belta. A receding horizon algorithm
for informative path planning with temporal logic constraints. In Proc.
of ICRA, pages 5019–5024, 2013.
[11] L. P. Kaelbling, M. L. Littman, and A. R. Cassandra. Planning
and acting in partially observable stochastic domains. Artificial
Intelligence, 101(12):99 – 134, 1998.
[12] O. Kupferman and M. Y. Vardi. Model Checking of Safety Properties.
Formal Methods in System Design, 19(3):291–314, 2001.
[13] O. Madani, S. Hanks, and A. Condon. On the undecidability of
probabilistic planning and related stochastic optimization problems.
Artificial Intelligence, 147(12):5 – 34, 2003.
[14] P. Ondruska, C. Gurau, L. Marchegiani, C. H. Tong, and I. Posner.
Scheduled Perception for Energy-Efficient Path Following. In Proc.
of ICRA, 2015.

[15] J. Pineau, G. Gordon, and S. Thrun. Point-based Value Iteration: An
Anytime Algorithm for POMDPs. In Proc. of IJCAI, pages 1025–
1030, 2003.
[16] A. Pnueli. The temporal logic of programs. In 18th Annual Symposium
on Foundations of Computer Science, pages 46–57, Oct 1977.
[17] M. Sipser. Introduction to the theory of computation. PWS Publishing
Company, 1997.
[18] M. Svorenova, M. Chmelik, K. Leahy, H. F. Eniser, K. Chatterjee,
I. Cerna, and C. Belta. Temporal logic motion planning using
POMDPs with parity objectives: case study paper. In Proc. of HSCC,
pages 233–238, 2015.
[19] A. Ulusoy, T. Wongpiromsarn, and C. Belta. Incremental Controller
Synthesis in Probabilistic Environments with Temporal Logic Constraints. Int. Journal of Robotics Research, 33(8):1130–1144, 2014.
[20] M. Vitus, W. Zhang, A. Abate, J. Hu, and C. Tomlin. On efficient
sensor scheduling for linear dynamical systems. In Proc. of ACC,
pages 4833–4838, 2010.

