IEEE Robotics & Automation Magazine - September 2011 - 90

these propositions as observations. The pose propositions fp1 , . . . , p9 g for each leg are satisfied only when
that leg is in the corresponding pose. State q10 is a slight
variation of state q4 and in this two-dimensional framework,
we represent them with the same pose. (The pose we call
coupe, more formally known as sur le cou-de-pied, has two
variations: in one, the foot of the working leg is wrapped
around the ankle, while in the other, it is fully pointed and
placed next to the ankle. While two states are necessary to
prevent nonsense barre sequences from being accepted by
the system, the resolution of our model is not intended to
capture such subtle differences in pose.) Hence, proposition
p4 is true at states q4 and q10 . The additional propositions,
Roffground (the right leg is off the ground) and Rcoronal
(the right leg is in a coro* nal extension away from
the body), help script
The soft specifications
statements about the system more concisely as
tweak the viable output
they apply to several states
and have corresponding
sequence by enumerating
meaning for the left-leg
system. When needed, a
aesthetic guidelines that
script R or L is added to
the system is encouraged to the states and propositions corresponding to
TR and TL , respectively;
achieve.
however, generally speak* ing, moves valid (or
invalid) on one leg are
likewise allowed (or disallowed) on the other so often
that these scripts will be neglected as our specifications
are symmetrical.
Our next task is to compose these two systems using a
synchronous product; this composition is liberal and naive
because it incorporates every available joint state and
transition (some of which are no longer physically possible
and/or aesthetically desirable) without taking into consideration whether the composed system is still appropriate.
In the next section, we whittle away which of these joint
states and transitions the system will inhabit.
More formally, the synchronous product of the two
transition systems TL and TR , denoted as TL TR , is a
new transition system with (QP , q0P , !P , PP , hP ): (Asynchronous transitions of the original single leg systems are
also allowed since the reflexive transitions defined in (1)
3) establish self-loops at each state.) The states are Cartesian pairs of the single leg states, i.e., QP QL 3 QR , likewise q0P ¼ (q0L , q0R ). Transitions exist between these joint
states if and only if a transition existed between both single states, i.e., !P QP 3 QP is defined by (q, q0) 2 !P if
and only if q 6¼ q0, (qL , q0L ) 2 !L , and ðqR ; q0R Þ 2 !R ,
where q ¼ (qL , qR ) and q0 ¼ (q0L , q0R ). The set of propositions, PP , becomes the union of the single leg transitions
for the left and right legs with an added proposition,
Spose, which is satisfied when both legs are in the same
90

IEEE ROBOTICS & AUTOMATION MAGAZINE

SEPTEMBER 2011

positions. The labeling function associates any proposition that was true for either single leg state with the
joint state.
Methods for Behavior Specification
Since the one-leg transition system does not contain all the
information about the physical capabilities of the robot
(TR assumes that the left leg is static and vice versa), it is
entirely possible that the product TP accepts runs that are
not physically possible to execute and not within the range
of our goal aesthetic. Hence, we formulate specifications
that enable our system to make discrete decisions about
viable trajectories (that is, accept or reject various runs
through the transition system), where viable is defined in
terms of both physical and aesthetic constraints.
To define our problem, we assume that our system is
required to satisfy physical constraints of a bipedal geometry and aesthetic requirements of basic classical ballet.
Specifically, we want to prevent the robot from executing
any physically infeasible runs and are interested in applying aesthetic conditions to the accepted runs of TP to
make them adhere to our chosen dance style. For example, we may disallow a list of two-legged body poses that
are perhaps considered ugly as judged by the metric of
ballet. We may further influence our output so as to only
produce a specific type of movement phrase within the
genre that, for example, is typified by more frequent use
of certain movements.
Thus, we consider two types of specifications to express
the restrictions: 1) hard specifications and 2) soft specifications. A hard specification incorporates physical constraints and aesthetic requirements that the robotic system
must satisfy, whereas a soft specification captures certain
additional aesthetic requirements that the robotic system
is encouraged to achieve. The general philosophy and
method for implementing these specifications is provided
here; the next section covers our specific choices to generate ballet phrases.
Hard Specifications
Recently, there has been an increasing interest in developing computational frameworks that enable rich specification languages for robotics. In particular, temporal
logics, such as linear temporal logic (LTL) and computation tree logic (CTL) have been suggested as motion
specification languages [20], [18], [8], [11], [5]. The use
of such logics allows for a large spectrum of specifications that include choice of a goal ("go to either A or B"),
convergence to a region ("reach A eventually and stay
there for all future times"), visiting targets sequentially
("reach A, then B, and then C"), surveillance ("reach A
and then B infinitely often"), and the satisfaction of more
complicated temporal and logic conditions about the
reachability of regions of interest ("Never go to A. Don't
go to B unless C or D were visited"). Such robot motion
planning and control objectives are achieved based on

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