Skip to content

Commit

Permalink
Added missing examples for Chapter 7 of the manual
Browse files Browse the repository at this point in the history
  • Loading branch information
pgagarinov committed May 16, 2014
1 parent 1bba21b commit d55a9fe
Show file tree
Hide file tree
Showing 67 changed files with 5,269 additions and 1,296 deletions.
2 changes: 1 addition & 1 deletion doc/_build/html/.buildinfo
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: 9cb5c1e55f016cf97bb882dc74d49254
config: bd338c293b4d7773267227655f05ebf8
tags: 645f666f9bcd5a90fca523b33c5a78b7
2 changes: 1 addition & 1 deletion doc/_build/html/chap_acknowledge.html
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ <h3>Navigation</h3>
</ul>
</div>
<div class="footer">
&copy; Copyright 2011-2013 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
&copy; Copyright 2011-2014 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
Created using <a href="http://sphinx-doc.org/">Sphinx</a> 1.2.2.
</div>
</body>
Expand Down
1,918 changes: 1,906 additions & 12 deletions doc/_build/html/chap_ellTube.html

Large diffs are not rendered by default.

920 changes: 460 additions & 460 deletions doc/_build/html/chap_ellcalc.html

Large diffs are not rendered by default.

216 changes: 108 additions & 108 deletions doc/_build/html/chap_examples.html

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion doc/_build/html/chap_functions.html
Original file line number Diff line number Diff line change
Expand Up @@ -10472,7 +10472,7 @@ <h3>Navigation</h3>
</ul>
</div>
<div class="footer">
&copy; Copyright 2011-2013 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
&copy; Copyright 2011-2014 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
Created using <a href="http://sphinx-doc.org/">Sphinx</a> 1.2.2.
</div>
</body>
Expand Down
146 changes: 73 additions & 73 deletions doc/_build/html/chap_implement.html

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions doc/_build/html/chap_install.html
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ <h2>Installation and Quick Start<a class="headerlink" href="#installation-and-qu
<ol class="arabic simple">
<li>At this point, the directory tree of the <em>Ellipsoidal Toolbox</em> is
added to the MATLAB path list. In order to save the updated path
list, in your MATLAB window menu go to File <span class="math">\rightarrow</span> Set
list, in your MATLAB window menu go to File <img class="math" src="_images/math/a9c4c6156d25f42923975ce449aadad9848ed7dc.png" alt="\rightarrow"/> Set
Path... and click Save.</li>
<li>To get an idea of what the toolbox is about, type</li>
</ol>
Expand Down Expand Up @@ -230,7 +230,7 @@ <h3>Navigation</h3>
</ul>
</div>
<div class="footer">
&copy; Copyright 2011-2013 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
&copy; Copyright 2011-2014 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
Created using <a href="http://sphinx-doc.org/">Sphinx</a> 1.2.2.
</div>
</body>
Expand Down
78 changes: 39 additions & 39 deletions doc/_build/html/chap_intro.html
Original file line number Diff line number Diff line change
Expand Up @@ -81,19 +81,19 @@ <h1>Introduction<a class="headerlink" href="#introduction" title="Permalink to t
calculating their convex hull. MPT’s convex hull algorithm is based on
the Double Description method <a class="reference internal" href="#motz1953" id="id3">[MOTZ1953]</a> and implemented in
the CDD/CDD+ package <a class="reference internal" href="#cddhp" id="id4">[CDDHP]</a>. Its complexity is
<span class="math">V^n</span>, where <span class="math">V</span> is the number of vertices and <span class="math">n</span> is
<img class="math" src="_images/math/5cf1ead08d0d7fda7f71d5e6228edcbc9f7b2e4c.png" alt="V^n"/>, where <img class="math" src="_images/math/c99df7a209495334da442b1ec998abaabfa320d8.png" alt="V"/> is the number of vertices and <img class="math" src="_images/math/413f8a8e40062a9090d9d50b88bc7b551b314c26.png" alt="n"/> is
the state space dimension. Hence the use of MPT is practicable for low
dimensional systems. But even in low dimensional systems the number of
vertices in the reach set polytope can grow very large with the number
of time steps. For example, consider the system,</p>
<div class="math">
<p><span class="math">x_{k+1} = Ax_k + u_k ,</span></p>
</div><p>with <span class="math">A=\left[\begin{array}{cc}\cos 1 &amp; -\sin 1\\ \sin 1 &amp; \cos 1\end{array}\right]</span>,
<span class="math">\ u_k \in \{u\in {\bf R}^2 ~|~ \|u\|_{\infty}\leqslant1\}</span>,
and <span class="math">x_0 \in \{x\in {\bf R}^2 ~|~ \|x\|_{\infty}\leqslant1\}</span>.</p>
<p><img src="_images/math/475800963f211b68178d44849f87661603b95a78.png" alt="x_{k+1} = Ax_k + u_k ,"/></p>
</div><p>with <img class="math" src="_images/math/723a7f8cb2ace0920d908d01c86420373b48e8ca.png" alt="A=\left[\begin{array}{cc}\cos 1 &amp; -\sin 1\\ \sin 1 &amp; \cos 1\end{array}\right]"/>,
<img class="math" src="_images/math/750490dafc28eb1175e6bf5f15083953bafabf1d.png" alt="\ u_k \in \{u\in {\bf R}^2 ~|~ \|u\|_{\infty}\leqslant1\}"/>,
and <img class="math" src="_images/math/ae1be594cdd66a2ccb79190913273784e5c201b6.png" alt="x_0 \in \{x\in {\bf R}^2 ~|~ \|x\|_{\infty}\leqslant1\}"/>.</p>
<p>Starting with a rectangular initial set, the number of vertices of the
reach set polytope is <span class="math">4k + 4</span> at the <span class="math">k</span>th step.</p>
<p>In <span class="math">d/dt</span> <a class="reference internal" href="#ddthp" id="id5">[DDTHP]</a>, the reach set is approximated by
reach set polytope is <img class="math" src="_images/math/f22656e16328ce7f7b5af269ab2256888d2354be.png" alt="4k + 4"/> at the <img class="math" src="_images/math/e9203da50e1059455123460d4e716c9c7f440cc3.png" alt="k"/>th step.</p>
<p>In <img class="math" src="_images/math/91fe3e396a3aba8f5ff5f521d0b3f4008b4e0966.png" alt="d/dt"/> <a class="reference internal" href="#ddthp" id="id5">[DDTHP]</a>, the reach set is approximated by
unions of rectangular polytopes <a class="reference internal" href="#asar2000" id="id6">[ASAR2000]</a>.</p>
<div class="figure align-center" id="ddtfig" style="width: 50%">
<img alt="approximation" src="_images/chapter01_ddt.png" />
Expand All @@ -102,15 +102,15 @@ <h1>Introduction<a class="headerlink" href="#introduction" title="Permalink to t
<p>The algorithm works as follows. First, given the set of initial
conditions defined as a polytope, the evolution in time of the
polytope’s extreme points is computed (<a href="#ddtfig">figure 14</a> (a)).</p>
<p><span class="math">R(t_1)</span> in <a href="#ddtfig">figure 14</a> (a) is the reach set of the system at
time <span class="math">t_1</span>, and <span class="math">R[t_0, t_1]</span> is the set of all points that
can be reached during <span class="math">[t_0, t_1]</span>. Second, the algorithm computes
<p><img class="math" src="_images/math/088e22e395ff0b8f6cde149172e52590852bcebf.png" alt="R(t_1)"/> in <a href="#ddtfig">figure 14</a> (a) is the reach set of the system at
time <img class="math" src="_images/math/44780f0598b4d22c6888cfca27deb04115f7fa88.png" alt="t_1"/>, and <img class="math" src="_images/math/1a3e51473c097540a265ee70575abb8038230e74.png" alt="R[t_0, t_1]"/> is the set of all points that
can be reached during <img class="math" src="_images/math/85674382bfceecdd6e6d6bdfbc6cff246ef47ef9.png" alt="[t_0, t_1]"/>. Second, the algorithm computes
the convex hull of vertices of both, the initial polytope and
<span class="math">R(t_1)</span> (<a href="#ddtfig">figure 14</a> (b)). The resulting polytope is then
bloated to include all the reachable states in <span class="math">[t_0,t_1]</span> (<a href="#ddtfig">figure 14</a> (c)).
<img class="math" src="_images/math/088e22e395ff0b8f6cde149172e52590852bcebf.png" alt="R(t_1)"/> (<a href="#ddtfig">figure 14</a> (b)). The resulting polytope is then
bloated to include all the reachable states in <img class="math" src="_images/math/3ad5575eeecc18f7013d14bb6ac8e07d4a611af3.png" alt="[t_0,t_1]"/> (<a href="#ddtfig">figure 14</a> (c)).
Finally, this overapproximating polytope is in its turn
overapproximated by the union of rectangles (<a href="#ddtfig">figure 14</a> (d)). The
same procedure is repeated for the next time interval <span class="math">[t_1,t_2]</span>,
same procedure is repeated for the next time interval <img class="math" src="_images/math/d82d790d123640183a6478ccd2fca6d3dbbb5cc0.png" alt="[t_1,t_2]"/>,
and the union of both rectangular approximations is taken (<a href="#ddtfig">figure 14</a> (e,f)),
and so on. Rectangular polytopes are easy to represent
and the number of facets grows linearly with dimension, but a large
Expand All @@ -128,21 +128,21 @@ <h1>Introduction<a class="headerlink" href="#introduction" title="Permalink to t
uses a special class of polytopes (see <a class="reference internal" href="#zonohp" id="id12">[ZONOHP]</a>)
of the form,</p>
<div class="math">
<p><span class="math">Z=\{x \in {\bf R}^n ~|~
x=c+\sum_{i=1}^p\alpha_ig_i,~ -1\leqslant\alpha_i\leqslant1\},</span></p>
</div><p>wherein <span class="math">c</span> and <span class="math">g_1, ..., g_p</span> are vectors in
<span class="math">{\bf R}^n</span>. Thus, a zonotope <span class="math">Z</span> is represented by its
center <span class="math">c</span> and ‘generator’ vectors <span class="math">g_1, ..., g_p</span>. The
value <span class="math">p/n</span> is called the order of the zonotope. The main benefit
<p><img src="_images/math/079103ca2d8d2b4f2f1a11895f4e0777515a4655.png" alt="Z=\{x \in {\bf R}^n ~|~
x=c+\sum_{i=1}^p\alpha_ig_i,~ -1\leqslant\alpha_i\leqslant1\},"/></p>
</div><p>wherein <img class="math" src="_images/math/65868d23a5bfe5b3b2d819386b19c14fa36af134.png" alt="c"/> and <img class="math" src="_images/math/5a5dba513d884860270a37e8a093a04413a047c1.png" alt="g_1, ..., g_p"/> are vectors in
<img class="math" src="_images/math/e1ece5563e1c134d935af18b692ffc3fde4f2fd6.png" alt="{\bf R}^n"/>. Thus, a zonotope <img class="math" src="_images/math/c4563e7ecec2336a3934447a6c10ef8519b0b452.png" alt="Z"/> is represented by its
center <img class="math" src="_images/math/65868d23a5bfe5b3b2d819386b19c14fa36af134.png" alt="c"/> and ‘generator’ vectors <img class="math" src="_images/math/5a5dba513d884860270a37e8a093a04413a047c1.png" alt="g_1, ..., g_p"/>. The
value <img class="math" src="_images/math/7e48764f6022209e2a9d41cdb3350b01bd3e1283.png" alt="p/n"/> is called the order of the zonotope. The main benefit
of zonotopes over general polytopes is that a symmetric polytope can be
represented more compactly than a general polytope. The geometric sum of
two zonotopes is a zonotope:</p>
<div class="math">
<p><span class="math">Z(c_1, G_1)\oplus Z(c_2, G_2) = Z(c_1+c_2, [G_1 ~ G_2]),</span></p>
</div><p>wherein <span class="math">G_1</span> and <span class="math">G_2</span> are matrices whose columns are
generator vectors, and <span class="math">[G_1 ~ G_2]</span> is their concatenation. Thus,
<p><img src="_images/math/8b15416140d9a6317080962cc6f3e97cb091c2f9.png" alt="Z(c_1, G_1)\oplus Z(c_2, G_2) = Z(c_1+c_2, [G_1 ~ G_2]),"/></p>
</div><p>wherein <img class="math" src="_images/math/7fb876996f317119f4a67c585344c9d153432a9b.png" alt="G_1"/> and <img class="math" src="_images/math/576bb52be38d16b35d99d553a68e3632c764b41f.png" alt="G_2"/> are matrices whose columns are
generator vectors, and <img class="math" src="_images/math/d465e46fed499e62fd8331e3c6c2d9ba9fc46aa2.png" alt="[G_1 ~ G_2]"/> is their concatenation. Thus,
in the reach set computation, the order of the zonotope increases by
<span class="math">p/n</span> with every time step. This difficulty can be averted by
<img class="math" src="_images/math/7e48764f6022209e2a9d41cdb3350b01bd3e1283.png" alt="p/n"/> with every time step. This difficulty can be averted by
limiting the number of generator vectors, and overapproximating
zonotopes whose number of generator vectors exceeds the limit by lower
order zonotopes. The benefits of the compact zonotype representation,
Expand Down Expand Up @@ -179,28 +179,28 @@ <h1>Introduction<a class="headerlink" href="#introduction" title="Permalink to t
linear system, the set of initial conditions and control bounds,
symbolically computes the exact reach set, using the experimental
quantifier elimination package. Quantifier elimination is the removal of
all quantifiers (the universal quantifier <span class="math">\forall</span> and the
existential quantifier <span class="math">\exists</span>) from a quantified system. Each
all quantifiers (the universal quantifier <img class="math" src="_images/math/f9c9bedb8f4996f937e5accd1b8c65158eead225.png" alt="\forall"/> and the
existential quantifier <img class="math" src="_images/math/aef07bc4ffa497327bb3d282cd8b9fd21a4be2fc.png" alt="\exists"/>) from a quantified system. Each
quantified formula is substituted with quantifier-free expression with
operations <span class="math">+</span>, <span class="math">\times</span>, <span class="math">=</span> and <span class="math">&lt;</span>. For
operations <img class="math" src="_images/math/3e41c598147b003fe1c720cafa073d83ccdd84bd.png" alt="+"/>, <img class="math" src="_images/math/c69691d64985442217922c8d34e835a9dea60178.png" alt="\times"/>, <img class="math" src="_images/math/eceeddfc4750d4fd271778cbd91090d6476c4a04.png" alt="="/> and <img class="math" src="_images/math/c1063a458139235d94b43817ed8d89dab9f9f811.png" alt="&lt;"/>. For
example, consider the discrete-time system</p>
<div class="math">
<p><span class="math">x_{k+1} = Ax_k + Bu_k</span></p>
</div><p>with <span class="math">A=\left[\begin{array}{cc}0 &amp; 1\\0 &amp; 0\end{array}\right]</span>
and <span class="math">B=\left[\begin{array}{c}0\\1\end{array}\right]</span>.</p>
<p>For initial conditions <span class="math">x_0\in\{x\in {\bf R}^2 ~|~ \|x\|_{\infty} \leqslant1\}</span> and
controls <span class="math">u_k\in\{u\in {\bf R} ~|~ -1\leqslant u\leqslant1\}</span>, the
reach set for <span class="math">k\geqslant0</span> is given by the quantified formula</p>
<p><img src="_images/math/0e8bce0949a2fbbe0993fbff7d4b895350df342c.png" alt="x_{k+1} = Ax_k + Bu_k"/></p>
</div><p>with <img class="math" src="_images/math/eeef52417b85996d354fb4e6654848ebfb513fad.png" alt="A=\left[\begin{array}{cc}0 &amp; 1\\0 &amp; 0\end{array}\right]"/>
and <img class="math" src="_images/math/8d047e64eceb1d63ca54023f66232e5861ca1d65.png" alt="B=\left[\begin{array}{c}0\\1\end{array}\right]"/>.</p>
<p>For initial conditions <img class="math" src="_images/math/531dda07a2dabeeaa9be97a75a5bb2c34c7058cb.png" alt="x_0\in\{x\in {\bf R}^2 ~|~ \|x\|_{\infty} \leqslant1\}"/> and
controls <img class="math" src="_images/math/4ae17ef1aa815763c1305aaa3aa46398363f4933.png" alt="u_k\in\{u\in {\bf R} ~|~ -1\leqslant u\leqslant1\}"/>, the
reach set for <img class="math" src="_images/math/dbe643040d34260bc1e3129b8853db23abe5e3b5.png" alt="k\geqslant0"/> is given by the quantified formula</p>
<div class="math">
<p><span class="math">\{ x\in{\bf R}^2 ~|~ \exists x_0, ~~ \exists k\geqslant0, ~~
<p><img src="_images/math/e2e51eb287a8f16ad4eb5aa87458072eeb94ac60.png" alt="\{ x\in{\bf R}^2 ~|~ \exists x_0, ~~ \exists k\geqslant0, ~~
\exists u_i, ~ 0\leqslant i\leqslant k: ~~
x = A^kx_0+\sum_{i=0}^{k-1}A^{k-i-1}Bu_i \},</span></p>
x = A^kx_0+\sum_{i=0}^{k-1}A^{k-i-1}Bu_i \},"/></p>
</div><p>which is equivalent to the quantifier-free expression</p>
<div class="math">
<p><span class="math">-1\leqslant[1 ~~ 0]x\leqslant1 ~ \wedge ~ -1\leqslant[0 ~~ 1]x\leqslant1.</span></p>
<p><img src="_images/math/cc0c6c57f34e206e04e9293909fcf1290c78df3f.png" alt="-1\leqslant[1 ~~ 0]x\leqslant1 ~ \wedge ~ -1\leqslant[0 ~~ 1]x\leqslant1."/></p>
</div><p>It is proved in <a class="reference internal" href="#laff2001" id="id19">[LAFF2001]</a> that for
continuous-time systems, <span class="math">\dot{x}(t) = Ax(t) + Bu(t)</span>, if
<span class="math">A</span> is constant and nilpotent or is diagonalizable with rational
continuous-time systems, <img class="math" src="_images/math/922627e82772d0c59364db1fa301dc616d34af3b.png" alt="\dot{x}(t) = Ax(t) + Bu(t)"/>, if
<img class="math" src="_images/math/0acafa529182e79b4f56165ec677554fba7fcf98.png" alt="A"/> is constant and nilpotent or is diagonalizable with rational
real or purely imaginary eigenvalues, and with suitable restrictions on
the control and initial conditions, the quantifier elimination package
returns a quantifier free formula describing the reach set. Quantifier
Expand Down Expand Up @@ -267,7 +267,7 @@ <h2>References</h2><table class="docutils citation" frame="void" id="motz1953" r
<table class="docutils citation" frame="void" id="ddthp" rules="none">
<colgroup><col class="label" /><col /></colgroup>
<tbody valign="top">
<tr><td class="label"><a class="fn-backref" href="#id5">[DDTHP]</a></td><td><span class="math">d/dt</span> homepage. <a class="reference external" href="http://www-verimag.imag.fr/~tdang/ddt.html">http://www-verimag.imag.fr/~tdang/ddt.html</a>.</td></tr>
<tr><td class="label"><a class="fn-backref" href="#id5">[DDTHP]</a></td><td><img class="math" src="_images/math/91fe3e396a3aba8f5ff5f521d0b3f4008b4e0966.png" alt="d/dt"/> homepage. <a class="reference external" href="http://www-verimag.imag.fr/~tdang/ddt.html">http://www-verimag.imag.fr/~tdang/ddt.html</a>.</td></tr>
</tbody>
</table>
<table class="docutils citation" frame="void" id="asar2000" rules="none">
Expand Down Expand Up @@ -442,7 +442,7 @@ <h3>Navigation</h3>
</ul>
</div>
<div class="footer">
&copy; Copyright 2011-2013 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
&copy; Copyright 2011-2014 Moscow State University, Faculty of Computational Mathematics and Computer Science, System Analysis Department, 2004-2011 The Regents of the University of California.
Created using <a href="http://sphinx-doc.org/">Sphinx</a> 1.2.2.
</div>
</body>
Expand Down
Loading

0 comments on commit d55a9fe

Please sign in to comment.