A Formal Approach to the Automatic Generation of Ballet Phrases

This paper presents a novel example where formal methods can be used to generate a type of human behavior. Drawing inspiration from classical ballet, poses are cast as discrete states and movements as the transitions between these states. Using Linear Temporal Logic (LTL), we are able to further constrain the set of possible sequences through the transition system and thus prevent it from evolving through a sequence of states that is physically impossible or aesthetically undesirable. Thus, a given movement style is encoded in the availability of transitions at each state, and the dynamics of a complex physical trajectory are abstracted as a system which moves between these states. Our overarching objective is to facilitate subtle degrees of control over systems through a useful parameterization for human movement. Such subtleties are required, for example, by humanoid robots to interact in and analyze a social and aesthetically driven world.