IEEE Robotics & Automation Magazine - September 2016 - 24

(India), Autobots (India), and MavDetectors (United States) (Figure 1). After
two intense days, Team Autobots was
declared the grand winner.
We believe that our challenge is a
good first step toward a better world
without land mines. We are hopeful
that, with continuous improvement in
each edition, we are on the right path
toward a version that could be deployed
in real scenarios with real land mines!
References

Figure 1. The HRATC finalists together with Edson Prestes (HRATC co-organizer, fourth
from the right) and Raj Madhavan (RAS-SIGHT chair, fifth from the left).

arbitrary area defined by a list of positions provided by the global positioning system in search of land mines
placed in a nonuniform distribution.
The HRACT 2016 received nine entries

from five countries: Bangladesh,
France, India, Italy, and the United
States. After the simulation and testing
phases, four teams qualified for the
finals: DISHARI (Bangladesh), Tushar

[1] R. Madhavan, L. Marques, E. Prestes, P.
Dasgupta, G. Cabrita, D. Portugal, B. Gouveia,
V. Jorge, R. Maffei, G. Franco, and J. Garcia,
"2014 Humanitarian Robotics and Automation Technology Challenge," IEEE Robot.
Autom. Mag., vol. 21, no. 3, pp. 10-16, 2014.
[2] R. Madhavan, L. Marques, E. Prestes, R.
Maffei, V. Jorge, B. Gil, S. Dogru, G. Cabrita,
R. Neuland, and P. Dasgupta, "2015 Humanitarian Robotics and Automation Technology
Challenge," IEEE Robot. Autom. Mag., vol. 22,
no. 3, pp. 182-184, 2015.

The 2016 Formal Methods for
Robotics Challenge
By Vasumathi Raman

obotic systems demand a high
standard of safety and correctness of behavior. There is a
large body of algorithmic work
addressing the principled design of
correct-by-construction controllers for
robots, drawing on formal methods for
verification and automatic synthesis of
transition systems satisfying desired
properties. The first of its kind, the
FMRC was developed to address the
lack of large-scale demonstrations of
current capabilities in this domain and
of benchmarks and metrics for
evaluating novel algorithms.
Digital Object Identifier 10.1109/MRA.2016.2587958
Date of publication: 13 September 2016

IEEE ROBOTICS & AUTOMATION MAGAZINE

At ICRA 2016, teams from four
universities-California Institute of
Technology (Caltech), Carnegie Mellon University (CMU), Cornell University, and Worcester Polytechnic
Institute (WPI)-competed across two
problem domains designed to test various challenges faced during the practical deployment of controller synthesis
approaches. The first domain involved
controlling a dynamical system modeled as a chain of integrators to satisfy
a reach-avoid temporal logic specification. This domain was designed to
test scalability of the submitted controller synthesis methods on problem
instances of increasing dimension
and order of highest derivative. The

september 2016

second domain was a road network
containing vehicles modeled as
Dubins cars. The objective was to control a single "ego" vehicle to achieve
safety (i.e., to not collide and to always
stay in its lane) and liveness (i.e., to
always eventually visit the goal
region) specifications while interacting with the remaining vehicles,
whose behavior was uncontrolled but
simulated subject to certain assumptions (e.g., to always eventually vacate
the goal region).
To allow maximum flexibility of
solution format, the solutions were
evaluated by running them in a
black-box fashion rather than requiring, e.g., solutions compatible with

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