This is a project to develop benchmark problems for research in so-called formal methods for robotics. The repositories are hosted on GitHub at https://github.com/fmrchallenge.

Below is a summary of *problem domains*, each of which is the basis
for particular *problem instances*. With such a taxonomy, we are able to
provide parameterized benchmarks that can be arbitrarily scaled, randomly
generated, etc. Of course, there is also support for fixed benchmarks, e.g., as
proposed from specific industrial applications. Normative
descriptions are given at `fmrchallenge.org/norm`.

The *scaling chains of integrators* domain is the simplest in terms of
dynamics, yet unlike the other domains, the system to be controlled can be
scaled easily to arbitrarily many dimensions. While this problem is abstract in
the sense that it is not modeling a specific physical system, it is
well-motivated because the double-integrator is just the basic force equation
\( F=ma \) of Newtonian mechanics, up to a scaling factor. Informally, this
problem domain concerns controlling acceleration or a higher order derivative of
a point-mass in high-dimensional spaces so as to visit goal regions and avoid
obstacles.

The *traffic network of Dubins cars* domain involves navigation in a small network of
two-lane roads with vehicles that have Dubins car dynamics. There is an
adversary that selects the motion of other cars. The adversary is subject to
assumptions such as obeying traffic rules and not parking unfairly at locations
that must be eventually reached by the controller.

The *factory cart clearing* domain concerns dexterous manipulation tasks
motivated by assembly line activities. The robot is required to process objects
laid out on a cart that is brought to it and sort them into bins. Carts arrive
after the robot indicates that it is ready, and carts are removed once a robot
declares that it is done. Scoring will be based on how many carts can be
processed correctly (described below) in a fixed amount of time.