» Download Article

Authors
Girard, Antoine, Le Guernic, Colas

Identifier
10.3182/20080706-5-KR-1001.01514

Index Terms
Verification

Abstract
This work is concerned with the algorithmic reachability analysis of linear systems with constrained initial states and inputs. In this paper, we present a new approach for the computation of tight polyhedral over-approximations of the reachable sets of a linear system. The main contribution over our previous work is that it makes it possible to consider systems whose sets of initial states and inputs are given by arbitrary compact convex sets represented by their support functions. We first consider the discrete-time setting and then we show how our algorithm can be extended to handle continuous-time linear systems. Finally, the effectiveness of our approach is demonstrated through several examples.

References

E. Asarin, T. Dang, O. Maler, and O. Bournez. Approximate
reachability analysis of piecewise-linear dynamical
systems. In Hybrid Systems: Computation and Control,
volume 1790 of LNCS, pages 20-31. Springer, 2000.

A. Bemporad and M. Morari. Verification of hybrid
systems via mathematical programming. In Hybrid
Systems: Computation and Control, volume 1569 of
LNCS, pages 31-45. Springer, 1999.

D.P. Bertsekas. Dynamic programming and optimal control.
Athena Scientific, 2000.

D.P. Bertsekas, A. Nedic, and A.E. Ozdaglar. Convex
analysis and optimization. Athena Scientific, 2003.

S. Boyd and L. Vandenberghe. Convex optimization.
Cambridge University Press, 2004.

A. Chutinan and B.H. Krogh. Verification of polyhedralinvariant
hybrid automata using polygonal flow pipe
approximations. In Hybrid Systems: Computation and
Control, volume 1569 of LNCS, pages 76-90. Springer,
1999.

E.M. Clarke, O. Grumberg, and D.A. Peled. Model
Checking. MIT Press, 2000.

T. Dang. V�erification et Synth`ese des Syst`emes Hybrides.
PhD thesis, Institut National Polytechnique de Grenoble,
2000.

A. Girard. Reachability of uncertain linear systems using
zonotopes. In Hybrid Systems: Computation and Control,
volume 3414 of LNCS, pages 291-305. Springer,
2005.

A. Girard, C. Le Guernic, and O. Maler. Efficient computation
of reachable sets of linear time-invariant systems
with inputs. In Hybrid Systems: Computation and Control,
volume 3927 of LNCS, pages 257-271. Springer,
2006.

Z. Han. Formal Verification of Hybrid Systems using
Model Order Reduction and Decomposition. PhD thesis,
Department of ECE, Carnegie Mellon University, 2005.

W. K�uhn. Towards an optimal control of the wrapping effect.
In SCAN 98, Developments in Reliable Computing,
pages 43-51. Kluwer, 1999.

A.B. Kurzhanski and P. Varaiya. Ellipsoidal techniques for
reachability analysis. In Hybrid Systems: Computation
and Control, volume 1790 of LNCS, pages 202-214.
Springer, 2000.

A. Kurzhanskiy and P. Varaiya. Ellipsoidal techniques
for reachability analysis of discrete time linear systems.
IEEE Trans. Automatic Control, 52(1):26-38, 2007.

I. Mitchell and C. Tomlin. Level set methods for computation
in hybrid systems. In Hybrid Systems: Computation
and Control, volume 1790 of LNCS, pages 310-323.
Springer, 2000.

O. Stursberg and B.H. Krogh. Efficient representation and
computation of reachable sets for hybrid systems. In
Hybrid Systems: Computation and Control, volume 2623
of LNCS, pages 482-497. Springer, 2003.

C. Tomlin, I. Mitchell, A. Bayen, and M. Oishi. Computational
techniques for the verification and control
of hybrid systems. Proc. of the IEEE, 91(7):986-1001,
2003.

P. Varaiya. Reach set computation using optimal control.
In Proc. KIT Workshop on Verification of Hybrid Systems.
Verimag, Grenoble, 1998.