We present a computationally attractive technique to study the reachability of rectangular regions by trajectories of continuous multi-affine systems. The method is iterative. At each step, finer partitions and finite quotients that over-approximate the reachability properties of the initial system are produced. We exploit some convexity properties of multi-affine functions on rectangles to show that the construction of the quotient at each step requires only the evaluation of the vector field at the set of all vertices of all rectangles in the partition and finding the roots of a finite set of scalar affine functions. This methodology can be used for formal analysis of biochemical networks, aircraft and underwater vehicles, where multi-affine models are widely used.
Alur, R., Courcoubetis, C., Henzinger, T.A. and Ho, P.H.1993: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Grossman, R.L., Nerode, A., Ravn, A.P. and Rischel, H., editors, Lecture notes in computer science, Vol. 736. Springer-Verlag, New York, 209-29.
2.
Alur, R., Dang, T. and Ivancic, F.2002: Predicate abstraction for reachability analysis of hybrid systems. ACM Transactions on Embedded Computing Systems5(1), 152-99.
3.
Alur, R. and Dill, D.L.1994: A theory of timed automata. Theoretical Computer Science126, 183-235.
4.
Batt, G., Belta, C. and Weiss, R.2008: Temporal logic analysis of gene networks under parameter uncertainty. IEEE Transactions on Circuits and Systems and IEEE Transactions on Automatic Control, Joint Special Issue on Systems Biology53, 215-29.
5.
Belta, C. and Habets, L.C.G.J.M. 2006: Control of a class of nonlinear systems on rectangles . IEEE Transactions on Automatic Control51(11), 1749-59.
6.
Ghosh, R.Tiwari, A. and Tomlin, C.2003: Automated symbolic reachability analysis; with application to delta-notch signaling automata. In Maler, O. and Pnueli, A., editors, Lecture notes in computer science, Vol. 2623. Springer-Verlag, New York, 233-48.
7.
Habets, L.C.G.J.M. and van Schuppen, J.H.2004: A control problem for affine dynamical systems on a full-dimensional polytope. Automatica40, 21-35.
8.
Haghverdi, E.Tabuada, P. and Pappas, G.2005: Bisimulation relations for dynamical, control, and hybrid systems. Theoretical Computer Science342(2-3), 229-61.
9.
Henzinger, T.A., Kopke, P.W., Puri, A. and Varaiya, P.1998: What is decidable about hybrid automata? Journal of Computer System and Sciences57, 94-124.
10.
Kloetzer, M. and Belta, C.2008: A fully automated framework for control of linear systems from temporal logic specifications. IEEE Transactions on Automatic Control53(1), 287-97.
11.
Lafferriere, G., Pappas, G.J. and Sastry, S.2000: O-minimal hybrid systems. Mathametics of Control, Signals, and Systems13(1), 1-21.
12.
Lotka, A.1925: Elements of physical biology. Dover Publications, Inc., New York.
13.
Milner, R.1989: Communication and concurrency Prentice-Hall, Englewood CliDs, NJ.
14.
Nicolin, X., Olivero, A., Sifakis, J. and Yovine, S.1993: An approach to the description and analysis of hybrid automata. In Grossman, R.L., Nerode, A., Ravn, A.P. and Rischel, H. editors, Lecture notes in computer science, Vol. 736. Springer-Verlag, New York, 149-78.
15.
Pappas, G.J.2003: Bisimilar linear systems. Automatica39(12), 2035-47.
16.
Park, D.M.R.1981: Concurrency and automata on infinite sequences. In Peter Deussen, editor, Lecture notes in computer science, Vol. 104. Springer-Verlag, London, UK, 167-83.
17.
Puri, A. and Varaiya, P.1994: Decidability of hybrid systems with rectangular differential inclusions. In David L. Dill, editor, Lecture notes in computer science, Vol. 818. Springer-Verlag, London, UK, 95-104.
18.
Tiwari, A. and Khanna, G.2002: Series of abstractions for hybrid automata. In Tomlin, C. and Greenstreet, M.R., editors, Lecture notes in computer science, Vol. 2289. Springer-Verlag, London, UK, 465-78.
19.
Volterra, V.1926: Fluctuations in the abundance of a species considered mathematically. Nature118, 558-60.
