IEEE Robotics & Automation Magazine - September 2011 - 91

algorithms inspired from model checking [3] and temporal logic games [17].
Here, we use LTL to express robotic tasks that include
an aesthetic component, e.g., "go to goal with grace" or,
more specifically, "move in the quick, staccato style of
allegro ballet." These tasks have an objective component,
such as "take ten steps" and also incorporate subjective
qualities like intention and aesthetics, such as "make ten
movements that give the impression of being happy."
Thus, in this article, through a particular approach to
modeling and formal synthesis, we begin to quantify subjective qualities, which are a significant missing link in
human-like robot interaction, by scripting them in the
established language of LTL.
LTL formulas are built from a set of atomic propositions P, Boolean operators : (negation), _ (disjunction),
^ (conjunction), and ! (implication), and temporal operators X (next), U (until), F (eventually), and G (always).
The semantics of LTL formulas are given over infinite
words generated by transition systems, such as TR , TL , and
TP defined in the "A Discrete Model" section. For simplicity, in what follows, we will denote a general transition system and its set of propositions by T and P, respectively. A
word of T is an infinite sequence over the power set of P
that satisfies the transition relation of T. For example,
fp2 gfp7 , Roffground, Rcoronalgfp4 , Roffgroundgfp2 g . . .
is the word generated by a run of TR that starts at qR2 , goes
to qR7 , next to qR10 , and then keeps looping among these
three states.
A word satisfies an LTL formula / if / is true at the first
position of the word; X/ states that at the next state, an
LTL formula / is true; F/ means that / eventually
becomes true in the word; G/ means that / is true at all
positions of the word; and /1 U/2 means /2 eventually
becomes true and /1 is true until this happens. More
expressivity can be achieved by combining the above
temporal and Boolean operators (several examples are
given later in the article). For example, the word given
above satisfies the following LTL formulas: Xp7 À p7 is true
at the next state, Fp4 À p4 will be true eventually, and
GF(p4 ^ Roffground) À p4 and Roffground are always
eventually true.
We use LTL formulas to represent the hard specification. The physical restrictions of the robot and aesthetic
requirements of ballet can be translated to LTL formulas
as is shown in the "Generating Ballet Phrases" section. To
ensure that the hard specifications are achieved in our
system output, we augment the product transition system
defined in the "A Discrete Model" section with an automata-theoretic representation of the specifications. The
resulting structure ensures that a run of our system,
which models a movement phrase, obeys both the physical dynamics (represented by TP ) and LTL specification
(represented by a formula /). More formally, such a
desired movement phrase is a sequence of transitions of
TP that produces a corresponding word satisfying /.

Such a run can be found using techniques inspired
by LTL model checking [3], which checks whether all
the words of a transition system satisfy an LTL formula
/ over its set of propositions. Central to LTL modelchecking problem is the construction of a B€
uchi automaton that accepts all and only words satisfying /. An
off-the-shelf software tool, such as LTL2BA [7], can be
used to generate such a B€
uchi automaton. The product
automaton, A, between the transition system and B€
uchi
automaton accepts all and only the runs of the transition system whose words satisfy /. In other words, this
product automaton captures the movement phrases
satisfying the hard specification; thus, we call these balletic phrases.
Soft Specifications
The soft specifications tweak the viable output sequence
by enumerating aesthetic guidelines that the system is
encouraged (instead of forced) to achieve. We define our
first type of soft specification, denoted by S 1 , as a collection of subsets of PP : S 1 & 2PP [12]. This encodes a set of
desired states as follows: we say a state q 2 QP satisfies S 1
if and only if hP (q) 2 S 1 . To broaden this ability to tweak
the output, we need to specify desired transitions.
Accordingly, we define a new, second type of soft specification as:
S 2 ¼ f(propi , prop0i )g, where propi , prop0i 2 2PP :

(3)

Again, we say a transition (q, q0) 2 !P satisfies S 2 if and
only if (hP (q), (hP (q0)) 2 S 2 . Hence, the collections S 1 and
S 2 model a desire for the robotic system to prefer certain
states (poses) and transitions (movements) more than
others. The technique that allows these specifications to
guide our output is outlined next; the faculty this adds to
our framework is demonstrated in the "Generating Ballet
Phrases" section.
Implementation
We design a (local, real time) receding-horizon controller to find a run that maximizes rewards collected based
on local information obtained at the current state while
guaranteeing the satisfaction of the hard specification.
Using an approach similar to that in [5], where a receding-horizon controller was designed, we employ a
measure of progress toward satisfying the LTL formula
/. If the controller is designed to always increase this
progress, as defined by our measure, then we can show
that / is satisfied. The proposed approach relied on an
assignment of 1) a suitable cost to each state of A (to
ensure that the output sequence adheres to / as the
sequence is selected) and 2) rewards on states and transitions that satisfy the propositions in S1 and S2 (to influence the poses and motions in the output sequence).
As previously discussed, the product automaton A is
uchi
constructed from the transition system TP and B€
SEPTEMBER 2011

IEEE ROBOTICS & AUTOMATION MAGAZINE

Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - September 2011