IEEE Robotics & Automation Magazine - September 2011 - 64

[46] P. Tabuada, "Approximate simulation relations and finite abstrac-

[63] P. Tabuada and G. J. Pappas, "Linear time logic control of discrete-

tions of quantized control systems," in Hybrid Systems: Computation and
Control (LNCS 4416), A. Bemporad, A. Bicchi, and G. C. Buttazzo, Eds.,

time linear systems," IEEE Trans. Automat. Contr., vol. 51, no. 12,
pp. 1862-1877, 2006.

Berlin: Springer, 2007, pp. 529-542.
[47] A. Girard and G. J. Pappas, "Approximation metrics for discrete and

[64] O. Kupferman and M. Y. Vardi, "Model checking of safety properties," Formal Meth. Syst. Des., vol. 19, pp. 291-314, 2001.

continuous systems," IEEE Trans. Automat. Contr., vol. 52, no. 5,

[65] E. Y. Chang, Z. Manna, and A. Pnueli, "Characterization of temporal

pp. 782-798, May 2007.
[48] A. Girard, "Approximately bisimilar finite abstractions of stable lin-

property classes," in Proc. 19th Int. Colloquium Automata Languages and
Programming (ICALP'92), W. Kuich, Ed., London, U.K. Berlin: Springer-

ear systems," in Hybrid Systems: Computation and Control (LNCS 4416),

Verlag, 1992, pp. 474-486.

A. Bemporad, A. Bicchi, and G. C. Buttazzo, Eds., Berlin: Springer-Verlag,
2007, pp. 231-244.

[66] R. Armoni, S. Egorov, R. Fraer, D. Korchemny, and M. Y. Vardi,
"Efficient LTL compilation for SAT-based model checking," in Proc.

[49] A. Girard, A. A. Julius, and G. J. Pappas, "Approximate simulation

IEEE/ACM Int. Conf. Computer-Aided Design. Washington, DC: IEEE

relations for hybrid systems," Discrete Event Dyn. Syst., vol. 18, no. 2,
pp. 163-179, 2008.

Computer Society, 2005, pp. 877-884.
[67] S. M. LaValle, M. S. Branicky, and S. R. Lindemann, "On the rela-

[50] G. Pola, A. Girard, and P. Tabuada, "Approximately bisimilar sym-

tionship between classical grid search and probabilistic roadmaps," Int. J.

bolic models for nonlinear control systems," Automatica, vol. 44, no. 10,
pp. 2508-2516, 2008.

Robot. Res., vol. 23, no. 7-8, pp. 673-692, 2004.
[68] J. Matousek, Geometric Discrepancy. Berlin: Springer-Verlag, 1999.

[51] A. Girard, G. Pola, and P. Tabuada, "Approximately bisimilar

[69] S. Tezuka, "Quasi-Monte Carlo: The discrepancy between theory

symbolic models for incrementally stable switched systems," in Hybrid
Systems: Computation and Control (LNCS 4981), M. Egerstedt and

and practice," in Monte Carlo and Quasi-Monte Carlo Methods 2000,
K.-T. Fang, F. J. Hickernell, and H. Niederreiter, Eds., Berlin: Springer-

B. Mishra, Eds., Berlin: Springer-Verlag, 2008, pp. 201-214.

Verlag, 2002, pp. 124-140.

[52] A. Bhatia and E. Frazzoli, "Incremental search methods for reachability analysis of continuous and hybrid systems," in Hybrid Systems:

[70] S. R. Lindemann, A. Yershova, and S. M. LaValle, "Incremental grid
sampling strategies in robotics," in Algorithmic Foundations of Robotics,

Computation and Control (LNCS 2993), R. Alur and G. J. Pappas, Eds.,
Berlin: Springer-Verlag, 2004, pp. 142-156.

VI, M. Erdmann, D. Hsu, M. Overmars, and A. F. van der Stappen, Eds.,
Berlin: Springer-Verlag, 2005, pp. 313-328.

[53] J. Kim, J. M. Esposito, and V. Kumar, "An RRT-based algorithm for

[71] J. Shewchuk, "Triangle: Engineering a 2D quality mesh generator

testing and validating multi-robot controllers," in Proc. RSS'05, 2005,
pp. 249-256.

and Delaunay triangulator," in Applied Computational Geometry
Towards Geometric Engineering (LNCS 1148), M. Lin and D. Manocha,

[54] M. S. Branicky, M. M. Curtiss, J. Levine, and S. Morgan, "Sampling-

Eds., Berlin: Springer-Verlag, 1996, ch. 23, pp. 203-222.

based planning, control and verification of hybrid systems," in IEEE Proc.
Control Theory Applicat., 2006, vol. 153, no. 5, pp. 575-590.

[72] 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.

[55] A. Bhatia and E. Frazzoli, "Sampling-based resolution-complete

[73] T. Latvala, "Efficient model checking of safety properties," in Model

algorithms for safety falsification of linear systems," in Hybrid Systems:
Computation and Control (LNCS 4981), M. Egerstedt and B. Mishra,

Checking Software (LNCS 2648), T. Ball and S. K. Rajamani, Eds., Berlin:
Springer-Verlag, 2003, pp. 74-88.

Eds., Berlin: Springer-Verlag, 2008, pp. 606-609.

[74] F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella,

[56] T. Dang, A. Donze, O. Maler, and N. Shalev, "Sensitive state-space
exploration," in Proc. IEEE CDC'08, pp. 4049-4054, Dec. 2008.

and M. Y. Vardi, "Benefits of bounded model checking at an industrial
setting," in Proc. 13th Int. Conf. Computer Aided Verification (CAV '01),

[57] T. Dang and T. Nahhal, "Coverage-guided test generation for

G. Berry, H. Comon, and A. Finkel, Eds., London, U.K. Berlin: Springer-

continuous and hybrid systems," Formal Meth. Syst. Des., vol. 34, no. 2,
pp. 183-213, 2009.

Verlag, 2001, pp. 436-453.
[75] E. M. Clarke and H. Veith, "Counter examples revisited: Principles,

[58] E. Plaku, L. E. Kavraki, and M. Y. Vardi, "Hybrid systems: from

algorithms, applications, in Verification: Theory and Practice (LNCS

verification to falsification by combining motion planning and
discrete search," Formal Meth. Syst. Des., vol. 34, no. 2, pp. 157-182,

2772), N. Dershowitz, Ed., Berlin: Springer-Verlag, 2003, pp. 208-224.

2009.
[59] E. Plaku, L. E. Kavraki, and M. Y. Vardi, "Motion planning with

Amit Bhatia, Department of Computer Science, Rice University, Houston, TX 77005, USA. E-mail: abhatia@rice.edu.

dynamics by a synergistic combination of layers of planning," IEEE Trans.
Robot., vol. 26, no. 3, pp. 469-482, 2010.
[60] P. Cheng and V. Kumar, "Sampling-based falsification and verification of controllers for continuous dynamic systems," Int. J. Robot. Res.,
vol. 27, no. 11-12, pp. 1232-1245, Nov./Dec. 2008.
[61] R. Alami, J. P. Laumond, and T. Simeon, "Two manipulation planning algorithms," in Proc. Algorithmic Foundations of Robotics, 1995,
pp. 109-125.
[62] C. L. Nielsen and L. E. Kavraki, "A two level fuzzy PRM for manipulation planning," in Proc. IEEE/RSJ Int. Conf. Intelligent Robots and Systems, 2000, vol. 3, pp. 1716-1721.

64

*

IEEE ROBOTICS & AUTOMATION MAGAZINE

*

SEPTEMBER 2011

Matthew R. Maly, Department of Computer Science, Rice
University, Houston, TX 77005, USA. E-mail: mmaly@
rice.edu.
Lydia E. Kavraki, Department of Computer Science, Rice
University, Houston, TX 77005, USA. E-mail: kavraki@rice.edu.
Moshe Y. Vardi, Department of Computer Science, Rice
University, Houston, TX 77005, USA. E-mail: vardi@
rice.edu.
http://www.rice.edu http://www.rice.edu
Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - September 2011
