» Download Article

Authors
Mitchell, Ian M.; Chen, Mo; Oishi, Meeko

Digital Object Identifier (DOI)
10.3182/20120606-3-NL-3011.00018

Page Numbers:
108-114

Index Terms
Reachability; Verification; Numerical tools

Abstract
In sampled data systems the controller receives periodically sampled state feedback about the evolution of a continuous time plant, and must choose a constant control signal to apply between these updates; however, unlike purely discrete time models the evolution of the plant between updates is important. In contrast, for systems with nonlinear dynamics existing reachability algorithms - based on Hamilton-Jacobi equations or viability theory - assume continuous time state feedback and the ability to instantaneously adjust the input signal. In this paper we describe an algorithm for determining an implicit surface representation of minimal backwards reach tubes for nonlinear sampled data systems, and then construct switched, set-valued feedback controllers which are permissive but ensure safety for such systems. The reachability algorithm is adapted from the Hamilton-Jacobi formulation proposed in Ding and Tomlin [2010]. We show that this formulation is conservative for sampled data systems. We implement the algorithm using approximation schemes from level set methods, and demonstrate it on a modified double integrator.

References

Jean-Pierre Aubin, Alexandre M. Bayen, and Patrick
Saint-Pierre. Viability Theory: New Directions. Systems
& Control: Foundations & Applications. Springer, 2011.
doi: 10.1007/978-3-642-16684-6.
Michael S. Branicky and Gang Zhang. Solving hybrid control
problems: Level sets and behavioral programming.
In Proceedings of the American Control Conference,
pages 1175{1180, Chicago, IL, 2000.
M.S. Branicky, M.M. Curtiss, J. Levine, and S. Morgan.
Sampling-based planning, control and verication of
hybrid systems. IEE Proceedings Control Theory and
Applications, 153(5):575 { 590, 2006.
P. Cardaliaguet, M. Quincampoix, and P. Saint-Pierre.
Set-valued numerical analysis for optimal control and
dierential games. In M. Bardi, T. E. S. Raghavan, and
T. Parthasarathy, editors, Stochastic and Dierential
Games: Theory and Numerical Methods, volume 4 of
Annals of International Society of Dynamic Games,
pages 177{247. Birkhauser, 1999.
Jerry Ding and Claire J. Tomlin. Robust reach-avoid
controller synthesis for switched nonlinear systems. In
Proceedings of the IEEE Conference on Decision and
Control, pages 6481{6486, Atlanta, GA, 2010. doi: 10.
1109/CDC.2010.5717115.
Steven M. LaValle. Planning Algorithms. Cambridge
University Press, New York, 2006.
John Lygeros. On reachability and minimum cost optimal
control. Automatica, 40(6):917{927, 2004. doi: 10.1016/
j.automatica.2004.01.012.
John Lygeros, Claire Tomlin, and Shankar Sastry. Controllers
for reachability specications for hybrid systems.
Automatica, 35(3):349{370, 1999. doi: 10.1016/
S0005-1098(98)00193-9.
Ian M. Mitchell. Comparing forward and backward reachability
as tools for safety analysis. In Alberto Bemporad,
Antonio Bicchi, and Giorgio Buttazzo, editors, Hybrid
Systems: Computation and Control, number 4416 in
Lecture Notes in Computer Science, pages 428{443.
Springer Verlag, 2007. doi: 10.1007/978-3-540-71493-4
34.
Ian M. Mitchell and Jeremy A. Templeton. A toolbox of
Hamilton-Jacobi solvers for analysis of nondeterministic
continuous and hybrid systems. In Manfred Morari and
Lothar Thiele, editors, Hybrid Systems: Computation
and Control, number 3414 in Lecture Notes in Computer
Science, pages 480{494. Springer Verlag, 2005. doi: 10.
1007/978-3-540-31954-2 31.
Ian M. Mitchell, Alexandre M. Bayen, and Claire J.
Tomlin. A time-dependent Hamilton-Jacobi formulation
of reachable sets for continuous dynamic games.
IEEE Transactions on Automatic Control, 50(7):947{
957, 2005. doi: 10.1109/TAC.2005.851439.
Ian M. Mitchell, Mo Chen, and Meeko Oishi. Ensuring
safety of nonlinear sampled data systems through
reachability (extended version). Technical Report TR-
2012-01, Department of Computer Science, University of
British Columbia, Vancouver, BC, Canada, April 2012.
Stanley Osher and Ronald Fedkiw. Level Set Methods
and Dynamic Implicit Surfaces. Springer, 2002. doi:
10.1007/b98879.
Erion Plaku, Lydia Kavraki, and Moshe Vardi. Hybrid
systems: from verication to falsication by combining
motion planning and discrete search. Formal Methods
in System Design, 34:157{182, 2009. doi: 10.1007/
s10703-008-0058-5.
James A. Sethian and Alexander Vladimirsky. Ordered
upwind methods for hybrid control. In C. J. Tomlin
and M. R. Greenstreet, editors, Hybrid Systems: Com-
putation and Control, number 2289 in Lecture Notes
in Computer Science, pages 393{406. Springer Verlag,
2002.