This page contains supplementary material for the following paper:

General Notes

These multi-agent animations were implemented and generated using CHARON, a general-purpose tool for the specification and simulation of hybrid systems.

In the animations, actors (colored yellow) navigate around obstacles (red) to reach targets (green).

Crowd simulation

In this animation (MPEG, size: 1.1M), a crowd of actors moves from the bottom of the screen to a target at the top, navigating around a crowd of actors simultaneously crossing from the top of the screen to a target at the bottom.

Three-segment animation

In our paper, we mention a three-segment animation (MPEG, size: 1.1M) in which an agent: uses complex steering to avoid obstacles in segment 1; uses simple linear steering in segment 2; and celebrates in segment 3. The celebration consists of waiting, then moving off the final target and changing size. (We chose a simple celebration. For the purpose of demonstrating discrete transitions between behaviors, a more complex celebration would have been no more effective.)

We generated a similar animation (MPEG, size: 1.3M) to demonstrate how the agent's course would differ if it did not switch to the simpler linear steering in segment 2.

Verifying collision-avoidance for a race-style game

As reported in the paper, we specified the rudiments of a race-like game in the hybrid system model checking tool HyTech.

Our game contains three agents, two racing actors and one obstacle, each moving at constant speed around a square, two-lane track. The rules of the race encode that each actor (naturally) prefers to race on the inside lane, and must do so whenever possible. Because one racer is slower than the other and the obstacle is slower than both, racers may move to the outside lane to pass slower agents, moving promptly back to the inside lane when they are done passing.

Consider an infinite race, an endless execution of this animation system. Will the two racers ever collide? As described in the paper, collisions were indeed possible the way we specified it in HyTech. We thought we had specified collision-avoidant behavior, but HyTech demonstrated our mistake.

We here present an animation (MPEG, size: 2.3M) of a system similar to the one we specified in HyTech. As with our other animations, we generated this by specifying and simulating an animation system in CHARON and then supplying the simulation output (in altered form) to a graphical viewer. The CHARON specification of the race, however, differs in significant ways from the HyTech one. The racers in CHARON are spheres, not cubes. Further, due to differences in the specification languages of HyTech and CHARON, racers in our CHARON animation do not collide; it would have required significant contrivance to create collisions in the CHARON animated race.

Even though this animation system is not completely identical to the one we implemented in HyTech, it does demonstrate a closely related race-like scenario about which we can reason using logics of hybrid systems.

For curious readers, we also present the HyTech trace that we did not include in our paper. By manually backtracking through the trace, we can expose aspects of our HyTech system, such as the location where a collision occurs. The trace displays values of certain variables (x1, y1, etc.) at certain times in the race-system execution; a full explanation of how to interpret the trace is beyond the scope of this supplementary material.

Back to Eric Aaron's home page
Eric Aaron, eaaron@cs.rutgers.edu