IEEE Robotics & Automation Magazine - September 2011 - 86

motion in the form of Markov decision processes and
partially observed Markov decision processes. The specifications will be in the form of formulas of probabilistic
temporal logics. One of the main challenges will be to
extend the existing distributed formal synthesis algorithms
to probabilistic frameworks.
Acknowledgment
This work was partially supported by Office of Naval
Research MURI N00014-09-1051, Army Research Office
W911NF-09-1-0088, AFOSR YIP FA9550-09-1-020, and
National Science Foundation CNS-0834260 at Boston
University, and by the CNCSIS (in Romanian) grant
PN-II-RU PD 333/2010 at the Technical University of
Iasi, Romania.

[15] L. Habets, M. Kloetzer, and C. Belta, "Control of rectangular multiaffine hybrid systems," in Proc. IEEE Conf. Decision and Control, 2006,
pp. 2619-2624.
[16] L. Habets, P. Collins, and J. van Schuppen, "Reachability and control
synthesis for piecewise-affine hybrid systems on simplices," IEEE Trans.
Automat. Contr., vol. 51, no. 6, pp. 938-948, 2006.
[17] R. Milner, Communication and Concurrency. Englewood Cliffs, NJ:
Prentice-Hall, 1989.
[18] M. Kloetzer and C. Belta, "Automatic deployment of distributed
teams of robots from temporal logic motion specifications," IEEE Trans.
Robot., vol. 26, no. 1, pp. 48-61, 2010.
[19] H. Kress-Gazit, D. Conner, H. Choset, A. Rizzi, and G. Pappas,
"Courteous cars," IEEE Robot. Automat. Mag., vol. 15, no. 1, pp. 30-38,
2008.
[20] M.

Mukund,

"From

global

specifications

to

distributed

implementations," in Synthesis and Control of Discrete Event Systems,
B. Caillaud, P. Darondeau, and L. Lavagno, Eds. Norwell, MA: Kluwer,

References
[1] J.C. Latombe, Robot Motion Planning. Norwell: MA: Kluwer, 1991.

2002, pp. 19-34.

[2] S. LaValle, Planning Algorithms. Cambridge, MA: Cambridge Univ.
Press, 2006.

[21] Y. Chen, X. Ding, A. Stefanescu, and C. Belta, "A formal approach to
deployment of robotic teams in an urban-like environment," Proc. 10th

[3] S. Karaman and E. Frazzoli, "Sampling-based motion planning with

Int. Symp. Distributed Autonomous Robotics Systems, 2010, to be

deterministic l-calculus specifications," in Proc. IEEE Conf. Decision and
Control, 2010, pp. 2222-2229.

published.
[22] J. Hopcroft, R. Motwani, and J.D. Ullman, Introduction to Automata

[4] M. Kloetzer and C. Belta, "A fully automated framework for control

Theory, Languages, and Computation. Reading, MA: Addison-Wesley,
2007.

of linear systems from temporal logic specifications," IEEE Trans. Automat. Contr., vol. 53, no. 1, pp. 287-297, 2008.
[5] H. Kress-Gazit, G. Fainekos, and G.J. Pappas, "Where's Waldo? Sensor-based temporal logic motion planning" in Proc. IEEE Int. Conf.

[23] M.A. Memon, "Computational logic: Linear-time vs. branching-time
logics," Simon Fraser Univ., Burnaby: Canada, Apr. 2003.
[24] C. Belta, V. Isler, and G.J. Pappas, "Discrete abstractions for robot

Robotics and Automation, 2007, pp. 3116-3121.

planning and control in polygonal environments," IEEE Trans. Robot.,

[6] S.G. Loizou and K.J. Kyriakopoulos, "Automatic synthesis of multiagent motion tasks based on LTL specifications," in Proc. IEEE Conf.

vol. 21, no. 5, pp. 864-874, 2005.
[25] S. Lindemann, I. Hussein, and S. LaValle, "Real time feedback con-

Decision and Control, 2004, pp. 153-158.

trol for nonholonomic mobile robots with obstacles," in Proc. IEEE Conf.

[7] M.M. Quottrup, T. Bak, and R. Izadi-Zamanabadi, "Multi-robot
motion planning: A timed automata approach," in Proc. IEEE Int. Conf.

Decision and Control, 2007, pp. 2406-2411.
[26] A. Stefanescu, "Automatic synthesis of distributed transition sys-

Robotics and Automation, 2004, pp. 4417-4422.

tems," Ph.D. dissertation, Univ. Stuttgart, Germany, 2006.

[8] T. Wongpiromsarn, U. Topcu, and R.M. Murray, "Receding horizon
temporal logic planning for dynamical systems," in Proc. IEEE Conf. Deci-

[27] Y. Chen, A. Stefanescu, and C. Belta, "A hierarchical approach to
automatic deployment of robotic teams with communication con-

sion and Control, 2009, pp. 5997-6004.

straints," in Proc. IEEE/RSJ Int. Conf. Intelligent Robots and Systems,

[9] E.M. Clarke, D. Peled, and O. Grumberg, Model Checking. Cambridge, MA: MIT Press, 1999.

Taipei, Taiwan, 2010, pp. 5079-5084.

[10] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pis-

Xu Chu Ding, Department of Mechanical Engineering, Boston University, Boston, MA 02215, USA. E-mail:
xcding@bu.edu.

tore, M. Roveri, R. Sebastiani, and A. Tacchella, "Nusmv 2: An
open-source tool for symbolic model checking," Lecture Notes Comput. Sci., vol. 2404, pp. 359-364, 2002 [Online]. Available: http://
www.springerlink.com/content/7hrq3m38utrrgywb/.
[11] G. Holzmann, The SPIN Model Checker: Primer and Reference
Manual. Reading, MA: Addison-Wesley, 2004.
[12] R. Alur, T.A. Henzinger, G. Lafferriere, and G.J. Pappas, "Discrete
abstractions of hybrid systems," Proc. IEEE, vol. 88, no. 7, pp. 971-984,
2000.
[13] R. Burridge, A. Rizzi, and D. Koditschek, "Sequential composition of

Marius Kloetzer, Department of Automatic Control and
Applied Informatics, Technical University "Gheorghe Asachi"
of Iasi, Romania. E-mail: kmarius@ac.tuiasi.ro.
Yushan Chen, Department of Electrical Engineering, Boston
University, Boston, MA 02215, USA. E-mail: yushanc@
bu.edu.

dynamically dexterous robot behaviors," Int. J. Robot. Res., vol. 18, no. 6,
pp. 534-555, 1999.
[14] J. Desai, J. Ostrowski, and V. Kumar, "Controlling formations of
multiple mobile robots," in Proc. IEEE Int. Conf. Robotics and Automation, 1998, pp. 2864-2869.

86

*

IEEE ROBOTICS & AUTOMATION MAGAZINE

*

SEPTEMBER 2011

Calin Belta, Department of Mechanical Engineering, Boston
University, Boston, MA 02215, USA. E-mail: cbelta@
bu.edu.
http://http:// http://www.springerlink.com/content/7hrq3m38utrrgywb/
Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - September 2011
