CORA computes reachable sets for linear systems, nonlinear systems as well as for systems with constraints. Continuous as well as discrete time models are supported. Uncertainty in the system inputs as well as uncertainty in the model parameters can be explicitly considered. In addition, CORA also provides capabilities for the simulation of dynamical models.
The following dynamic systems are implemented in CORA. More information can be found in Section 4 in the CORA manual.
In CORA, linear systems have the form
where \(x(t) \in \mathbb{R}^n\) is the system state, \(u(t)\in \mathbb{R}^m\) is the system input, \(w(t) \in \mathbb{R}^n\) is the disturbance, \(y(t) \in \mathbb{R}^p\) is the system output, \(v(t) \in \mathbb{R}^p\) is the sensor noise, and \(A \in \mathbb{R}^{n \times n}\), \(B \in \mathbb{R}^{n \times m}\), \(c \in \mathbb{R}^n\), \(C \in \mathbb{R}^{p \times n}\), \(D \in \mathbb{R}^{p \times m}\), \(k \in \mathbb{R}^p\).
More information can be found in Section 4 in the CORA manual.
The code below gives a reachability analysis example for linear systems in CORA.
All dynamic systems share a set of identical
operations, such as
reach
to compute the reachable set and simulateRandom
for
random simulations.
Further examples can be found at ./examples/contDynamics
on GitHub.
This class extends linear systems by uncertain parameters. We provide two implementations, one for uncertain parameters that are fixed over time and one for parameters that can arbitrarily vary over time. For the case with fixed parameters, a linear parametric system is defined as
which can be equivalently formulated as
where \(x(t) \in \mathbb{R}^n\) is the system state, \(u(t)\in \mathbb{R}^m\) is the system input, \(p \in \mathbb{R}^p\) is the parameter vector, and \(\mathcal{P} \subset \mathbb{R}^p\) is the set of parameters. For the case with fixed parameters, a linear parametric system is defined as
More information can be found in Section 4 in the CORA manual.
In addition to continuous-time linear systems, CORA also supports discrete-time linear systems defined as
where \(x[i] \in \mathbb{R}^n\) is the system state, \(u[i] \in \mathbb{R}^m\) is the system input, \(w[i] \in \mathbb{R}^n\) is the disturbance, \(y[i] \in \mathbb{R}^p\) is the system output, \(v[i] \in \mathbb{R}^p\) is the sensor noise, and \(A \in \mathbb{R}^{n \times n}\), \(B \in \mathbb{R}^{n \times m}\), \(c \in \mathbb{R}^n\), \(C \in \mathbb{R}^{p \times n}\), \(D \in \mathbb{R}^{p \times m}\), \(k \in \mathbb{R}^p\).
More information can be found in Section 4 in the CORA manual.
In contrast to all other systems, we consider stochastic properties here. The system under consideration is defined by the following linear stochastic differential equation (SDE), which is also known as the multivariate Ornstein-Uhlenbeck process:
where \(A\) and \(C\) are matrices of proper dimension and \(A\) has full rank. There are two kinds of inputs: the first input \(u\) is Lipschitz continuous and can take any value in \(\mathcal{U} \subset \mathbb{R}^n\) for which no probability distribution is known. The second input \(\xi\in\mathbb{R}^m\) is white Gaussian noise. The combination of both inputs can be seen as a white Gaussian noise input, where the mean value is unknown within the set \(\mathcal{U}\).
More information can be found in Section 4 in the CORA manual.
Discrete-time Autoregressive Moving Average models with exogenous Input (ARMAX models) are considered in the \(linearARMAX\) class. They can be described by the following equation:
where \([i] \in \mathbb{R}^o\) is the system output at time step \(i\) and \(u[i] \in \mathbb{R}^m\) is the system input which can also include disturbances and measurements noise.
More information can be found in Section 4 in the CORA manual.
Although a fairly large group of dynamic systems can be described by linear systems, the extension to nonlinear systems is an important step towards the analysis of more complex systems. We consider general nonlinear continuous systems defined by the differential equation
where \(x(t) \in \mathbb{R}^n\) is the system state, \(u(t) \in \mathbb{R}^m\) is the system input, \(y(t) \in \mathbb{R}^o\) is the system output, and \(f:\mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}^n\) and \(g:\mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}^o\) are sufficiently smooth.
More information can be found in Section 4 in the CORA manual.
The code below gives a reachability analysis example for nonlinear systems in CORA.
Further examples can be found at ./examples/contDynamics
on GitHub.
Nonlinear parametric systems extend nonlinear systems by additionally considering uncertain parameters \(p\):
where \(x(t) \in \mathbb{R}^n\) is the system state, \(u(t) \in \mathbb{R}^m\) is the system input, \(p \in \mathbb{R}^p\) is the parameter vector, \(y(t) \in \mathbb{R}^o\) is the system output, and \(f: \mathbb{R}^n \times \mathbb{R}^m \times \mathbb{R}^p \to \mathbb{R}^n\) and \(g: \mathbb{R}^n \times \mathbb{R}^m \times \mathbb{R}^p \to \mathbb{R}^o\) are sufficiently smooth. As for linear parametric systems, the parameters \(p \in \mathcal{P}\) can be constant over time or time-varying.
More information can be found in Section 4 in the CORA manual.
We consider nonlinear discrete-time systems defined as
where \(x[i] \in \mathbb{R}^n\) is the system state, \(u[i] \in \mathbb{R}^m\) is the system input, \(y[i]\) is the system output, and \(f:\mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}^n\) and \(g:\mathbb{R}^n \times \mathbb{R}^m \to \mathbb{R}^o\) are continuous functions.
More information can be found in Section 4 in the CORA manual.
We consider time-invariant, semi-explicit, index-1 differential-algebraic systems defined as
where \(x(t) \in \mathbb{R}^n\) is the vector of differential variables, \(y(t) \in \mathbb{R}^q\) is the vector of algebraic variables, \(u(t) \in \mathbb{R}^m\) is the vector of inputs, \(z(t) \in \mathbb{R}^o\) is the system output, and \(f: \mathbb{R}^n \times \mathbb{R}^q \times \mathbb{R}^m \to \mathbb{R}^n\), \(g: \mathbb{R}^n \times \mathbb{R}^q \times \mathbb{R}^m \to \mathbb{R}^q\), and \(h: \mathbb{R}^n \times \mathbb{R}^q \times \mathbb{R}^m \to \mathbb{R}^o\) are sufficiently smooth continuous functions. The initial state is consistent when \(g(x(0),y(0),u(0)) = 0\), while for DAEs with an index greater than 1, further hidden algebraic constraints have to be considered. For an implicit DAE, the index-1 property holds if and only if \(\forall t: \, \det(\frac{\partial g(x(t),y(t),u(t))}{\partial y})\neq 0\), i.e., the Jacobian of the algebraic equations is non-singular. Loosely speaking, the index specifies the distance to an ODE (which has index 0) by the number of required time differentiations of the general form \(0 = F(\dot{\tilde{x}}, \tilde{x}, u, t)\) along a solution \(\tilde{x}(t)\), in order to express \(\dot{\tilde{x}}\) as a continuous function of \(\tilde{x}\) and \(t\).
More information can be found in Section 4 in the CORA manual.
Due to the current trend towards artificial intelligence, the system class of neural network controlled system is gaining more and more importance. In CORA, we consider neural network controlled systems with discrete feedback, where the neural network controller updates the control input at the end of the time steps defined by the sampling time \(\Delta t\). The dynamic system \(\dot{x} = f(x,u)\) can be any of the above dynamic systems.
More information can be found in Section 4 in the CORA manual or read more here.