Case Studies of Continuous and Hybrid Systems

(A) 3-dimensional stable model

tyle="text-align: center;">Constructing Flowpipes for Continuous and Hybrid Systems: Case-Studies.

 

Introduction

We present a set of benchmarks of continuous and hybrid systems as long as their running results on the tool Flow* of version 1.0.0. These studies are intended to benchmark the performance of Flow* tool and serve as a basis of comparison with other tools.

All these studies are run on the following computational platform.

CPU:      Intel Core i7-860 Processor (2.80 GHz)
Memory:  4096 MB
System:    Ubuntu 12.04 LTS

Con

Continuous-Time Case Studies

h3>

(A)

(A) Brusselator

Brusselator system is a “chemical oscillator” (see here for more details).

The dynamics of a Brusselator are given by
Brusselator
wherein A=1 and B=1.5 in our tests. We let Flow* compute the Taylor model flowpipes for the time horizon [0,15]. We first choose the initial set x in [0.9,1] and y in [0,0.1], Flow* costs 7 seconds to generate the flowpipes shown in the figure below. (model file)
Brusselator_reach_small
Then, we enlarge the initial set to x in [0.8,1] and y in [0,0.2]. To control the wrapping effect, we slightly adjust the reachability parameters in the model file. The total time cost is 16 seconds, a grid paving of the flowpipes is shown as follows. (model file)
Brusselator_reach_large

(B)

(B) Lorenz system

Lorenz System is a three variable dynamical system that can exhibit chaotic behavior (see here for more details). It can be modeled by the following 3-dimensional ODE
Lorentz
wherein the parameters A,B,C are in their typical values: A=10, B=28, C=8/3. First, we choose the initial set x in [14.99,15.01], y in [14.99,15.01] and z in [35.99,36.01]. The tool Flow* spent 9 seconds to compute the flowpipes in [0,1]. A grid paving of the flowpipes in the x-y plane is as below. (model file)
Lorentz_reach_short
Then, we perform a long-term reachability computation, say [0,6.5], from a smaller initial set x in [14.999,15.001], y in [14.999,15.001] and z in [35.999,36.001]. The total time cost is 642 seconds. The projection of the results in the x-y plane is as follows. (model file)
Lorentz_reach_long

(C)

(C) Model of a biological system

consider a dynamical system described in [1] modeled as an ODE with 7 system variables:
biology_7
We choose the initial set which is a box of [0.1,0.105] in each dimension. Flow* spent 394 seconds to compute 1000 flowpipes for the time horizon [0,2]. We present the octagon enclosures of the flowpipe projections in the x2-x6 plane and x3-x4 plane. (model file)
biology_7_x2_x6biology_7_x3_x4

(D)

(D) Another model of a biological system

consider another model from  [1], which has 9 variables. biology_9
The initial set is a box of [0.09,0.11] in each dimension. Because of the large coefficients in the ODE, we have to choose a very small time step, say 0.001. We compute the first 200 flowpipe segments using Flow*, the time taken is 282 seconds. Some projections of the flowpipes are shown below. (model file)
biology_9_x1_x5
biology_9_x2_x6
biology_9_x7_x8

Hybrid

Hybrid case studies

-dimensional stable model

To evaluate the performance of a reachability tool, we design a hybrid system consists of 2 modes and 1 jump. The ODE in the first mode l1 defines a stable vector field whose unique equilibrium is (2,-2,1).
hybrid_stable_l1
In the second mode l2, the ODE is also stable, and the unique equilibrium is (0,0,0).
hybrid_stable_l2
The only jump is from l1 to l2. The guard is a box x in [1.7,2.3], y in [-2.3,1.7] and z in [0.7,1.3]. We let Flow* perform the flowpipe construction from the initial set x in [3,3.5], y in [-3,-2.5], z in [0.7,1.3] for the time horizon [0,10]. The time cost is 61 seconds. Some projections of the flowpipes are shown as follows.
hybrid_stable_x_y
hybrid_stable_x_z
It can be seen that the flowpipes converge to the equilibrium in both of the modes. (model file)

(B) In

(B) Insulin Infusion Control in Diabetic Patients

namics of insulin glucose in a type I diabetic patient is modeled by the Bergman minimal model with three state variables (G,I,X) wherein G is plasma glucose concentration above the basal value G_B, I is the plasma insulin concentration above the basal value I_B, and X is the insulin concentration in an interstitial chamber.

diabetic

g(t) is the uncontrolled (meal) glucose input and i(t) is the controlled insulin input. We consider two controllers suggested by Fisher et al. and Furler et al. (see our paper [2] for further details).

The  choice of the constant parameters  for the  two control schemes  are described in [2]. The first control scheme generates a 9-mode hybrid automaton, and the second a 6-mode one. Start from the initial set G in [-2,2], I in [-0.1,0.1] and X in [0,0], Flow* took  63 and 28 seconds  to compute the flowpipes for the first and second model respectively in the time horizon [0,360]. The results are shown below.  The model files are also available (diabetic_1, diabetic_2)
diabetic_1
diabetic_2

(C) Non-linea

(C) Non-linear navigation benchmarks

linear navigation benchmarks introduced by Fehnker and Ivancic [4] by adding non-linear drags to the velocities vx and vy. The drag force in the x and y direction is given as -0.1*vx^3 and -0.1*vy^3 respectively. We apply Flow* to do the reachability analysis for the non-linear NAV04 to NAV09 such that the initial sets of NAV05 and NAV09 are slightly contracted. The time cost and model files are listed as follows.

benchmarks time (s)
NAV04 14.5
NAV05 20.8
NAV06 40.4
NAV07 26.1
NAV08 25.6
NAV09 50.1

(D) Water-Tan

(D) Water-Tank System.

a ball shaped water tank is half governed by a PI controller. When the water level achieves a specified high value, the controller is turned off and the inflow valve starts to close. If the level reaches the specified low value, then the inflow valve will be opened and the controller will be turned on afterwards (description). We start from the initial water level [10,10.5] and let Flow* compute the flowpipes covering the time horizon [0,1000]. The total time taken for flowpipe computations is 270 seconds, and the result is as follows. (model file)
watertank

Future Work o

Future Work on Flow*

ong>not a finished product: it is not perfect and we appreciate feedback.

We are continuously under development! Future directions for our tool are too numerous to list here. A few main limitations that we hope to fix in the subsequent versions are

  • Support for trigonometric and rational functions.
  • Automatic inference of flowpipe construction parameters from simulations (simplifying the input model file).
  • Quantifying the accuracy of flowpipe constructions.
  • Flowpipe computations targettted to an unsafe region.

People

<

People

int effort undertaken by RWTH Aachen University, Germany and University of Colorado, Boulder.

The lead developer of this tool is Xin Chen (PhD student at RWTH Aachen University).  Please contribute bug reports directly to Xin Chen.

Other contributors are Profs. Sriram Sankaranarayanan (Colorado) and Erika Abraham (RWTH Aachen University)

Acknowledgments

Acknowledgments

arayanan acknowledges support from the US National Science Foundation (NSF) under NSF CAREER Award (Award # 0953941) and NSF CPS Award (Award # 1035845).

References

References

. Herwig, A. Kowald, C. Wierling and H. Lehrach. Systems Biology in Practice: Concepts, Implementation and Application. Wiley-Blackwell, 2005.
[2] X. Chen, E. Abraham and S. Sankaranarayanan. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. IEEE Real-Time Systems Symposium (RTSS), 2012.
[3] X. Chen, E. Abraham and S. Sankaranarayanan. Flow*: An Analyzer for Non-Linear Hybrid Systems. Computer Aided Verification (CAV), 2013.
[4] A. Fehnker and F. Ivancic. Benchmarks for Hybrid Systems Verification. Hybrid systems: computation and control (HSCC) 2004