Benchmarks and Competitions on Formal Methods for Robotics

about domains documentation events FAQ

scaling chains of integrators

\( \DeclareMathOperator{\Feventually}{\Diamond} \DeclareMathOperator{\Galways}{\Box} \DeclareMathOperator{\Uuntil}{\mathbf{U}} \)

Illustration of a trajctory in 3-dimensional Euclidean space.  It avoids two gray rectangles (obstacles) and reaches a green goal rectangle.
The scaling chains of integrators domain is the simplest in terms of dynamics and specifications, yet unlike the other domains, the system to be controlled can be scaled easily to arbitrarily many dimensions. While this problem is abstract in the sense that it is not modeling a specific physical system, it is well-motivated because the double-integrator is just the basic force equation \( F=ma \) of Newtonian mechanics, up to a scaling factor. Informally, this problem domain concerns controlling acceleration or a higher order derivative of a point-mass in high-dimensional spaces so as to visit goal regions and avoid obstacles.

Dynamics and constraints

Let \( n \) and \( m \) be positive integers. Consider the differential equation \begin{equation} D^{m}q = u ,\label{eq:minteg} \end{equation} where \( q: [0,\infty [ \rightarrow \mathbb{R}^{n} \) and \( D \) is the differential operator. The input \( u \) is bounded as \( \lVert u(t) \rVert_1 \leq u_{\mathrm{max}} \). The system is called a chain of integrators because it can be rewritten as a linear control system \begin{equation} \begin{split} \dot{x}_1 &= x_2 \\ \dot{x}_2 &= x_3 \\ &\vdots \\ \dot{x}_{m-1} &= x_m \\ \dot{x}_m &= u \\ y &= x_1 \end{split}\label{eq:cintegdyn} \end{equation} where for time \( t \), each \( x_{i}(t)\in \mathbb{R}^n \) for \( i=1,\ldots,m \), and \( x(t)=\left( x_{1}(t) , \ldots , x_{m}(t)\right)\in \mathbb{R}^{nm} \). The output trajectories of \eqref{eq:cintegdyn} are exactly those of \eqref{eq:minteg}, given the same input, and thus we call them equivalent. In \eqref{eq:minteg}, control input is applied as the \( m \)-th derivative of an \( n \)-dimensional variable \( q \), and the intermediate derivatives are made explicit in \eqref{eq:cintegdyn}. A notable particular case is \( m=2 \), which is called the "double integrator". If \( n \leq 3 \) then \( q \) may be referred to as the "position".

To introduce process and sensor noise, consider the 2-dimensional system \begin{align} \dot{x} &= \left( \begin{array}{cc} 0 & 1 \\ 0 & 0 \end{array} \right) x + \left( \begin{array}{c} 0 \\ 1 \end{array} \right) u + \xi \label{eq:dintegdyn}\\ y &= \left( \begin{array}{cc} 1 & 0 \end{array} \right) x + \eta \label{eq:dintegobs}, \end{align} where \( \xi \) and \( \eta \) are either bounded disturbances (nondeterministic) or stochastic processes. Equivalence with \eqref{eq:minteg} in the case of \( n=1, m=2 \) and \( \xi=\eta=0 \) is apparent using \( x_1 = q \) and \( x_2 = \dot{q} \). For \( n > 1 \), the matrices in \eqref{eq:dintegdyn} and \eqref{eq:dintegobs} can be repeated in block diagonal form to yield a new linear time-invariant system of dimension \( 2n \) and which is again equivalent to \eqref{eq:minteg} for \( m=2 \).

Specifications

Task specifications will require visitation of regions while avoiding obstacles. These can be regarded as a slight extension beyond classical motion planning. There are two forms of specifications: \begin{equation}\label{eq:dinteg-surveillance} q(0) = \mathrm{init} \wedge \Galways \left( q(t) \notin \mathrm{Obs} \right) \wedge \bigwedge_{i} \Galways \Feventually \mathrm{goal}_i \end{equation} and \begin{equation}\label{eq:dinteg-timedreach} q(0) = \mathrm{init} \wedge \Galways \left( q(t) \notin \mathrm{Obs} \right) \wedge \bigwedge_{i} \left( \mathrm{counter}_i \leq T_{i} \right) \Uuntil \mathrm{goal}_i , \end{equation} where \( \mathrm{Obs} \subset \mathbb{R}^n \) is the obstacle set, which is represented by a finite union of polytopes. For each \( i \), \( \mathrm{counter}_i \) is a discrete clock that enforces the real-time deadline \( T_i \) of reaching region \( \mathrm{goal}_i \). Goal region \( \mathrm{goal}_i \) is defined by a convex polytope. The initial position is a single point, \( \mathrm{init}\in \mathbb{R}^n \). As part of the specification form \eqref{eq:dinteg-timedreach}, a time of initialization and rate of progression of the discrete counters is specified. These are significant because they determine in what order and how quickly the goal regions must be reached.