-
Notifications
You must be signed in to change notification settings - Fork 32
EP: Documentation
Enhancement proposal for the LazySets documentation.
LazySets is a library for set-based computations in the Euclidean space. The library can handle the most common operations between sets, such as Minkowski sum, cartesian product, convex hull and intersection, to mention a few. Moreover, several set representations are defined, such as polyhedra in constraint and in vertex representation, ellipsoids, balls in different norms, and specific classes of polyhedra (such as intervals, zonotopes or hyperrectangles) for which specialized methods apply. Applications that use LazySets can explore different approaches with minimal changes in their code, because conversion between set representations as well as overapproximation or underapproximation algorithms are implemented.
One of the key features of LazySets is specialization. On a more technical level, the
library is highly optimized to get the best possible performance given the following two
restrictions: the set type and the set dimension. For instance, consider the linear map
transformation, that is, to compute Y = \{y : y = Ax for some x ∈ X\}.
In LazySets, linear_map(A, X) returns a set representation of Y and the algorithm that is
actually used, as well as the type of Y, depends on the types of its arguments and the dimension of
X (in programming jargon, this is called multiple dispatch). In particular,
if X is a polygon in vertex representation (VPolygon) then the linear map is applied to
each vertex. However, if X is a 30-dimensional polyhedron in halfspace representation (HPolyhedron),
then the halfspace representation is used (if possible), because the cost of computing the vertex
representation increases exponentially with the dimension.
Moreover, in LazySets set operations can be performed in two possible (complementary) ways:
concretely or lazily, where concrete computation means that the result is a set, and in the
lazy computation the result is an object that represents the operation between the given sets.
For instance, while linear_map(A, X) computes the concrete linear map as explained in the previous
paragraph, LinearMap(A, B), or simply A * X, computes the lazy linear map, which is just
a new object which "holds" the linear map computation until it is
actually needed. In other words, LinearMap(A, X) can be used to reason about
the linear map even if X is very high-dimensional, since this command just
builds an object representing the linear map of X by A. In Julia, Unicode
symbols such as A * X, X ⊕ Y, X ⊖ Y, X × Y, all default to lazy operations by design.
Unicode is input using the latex name of the symbol followed by the TAB key,
such as \oplus[TAB] for the (lazy) Minkowski sum ⊕.
Furthermore, one can combine lazy set operations to build lazy expressions that represent several
operations between sets, such as eg. Q = (Z ⊕ A*X) × T.
By means of the basic tools of convex geometry, mainly support function theory, useful information
about Q can be obtained without actually computing the linear map, minkowski sum and cartesian product
in the above computation. For example, if the computation only involves querying information
about Q in a small number of directions, the lazy approach can be done very efficiently.
LazySets is a recent and actively developed academic library and it has been applied by its developers to the problem of the reachability analysis of ordinary differential equations with uncertain parameters and inputs. LazySets was the library used to successfully verify for the first time a 10,000-dimensional system, using lazy set-based matrix exponentiation techniques. We refer to [1-5] for applications and for experimental evaluations.
<<< links to some publications ?? >>>
- HOME << short. aim of the library. where is it used.
- Installation and troubleshooting << talk on dependencies. etc
- A Tour of LazySets << guide plenty of examples. take some of what we have in "intro to convex sets .."
- Polyhedral approximations << theory on support functions
- Convex set types
- Non-convex set types
- Closure properties << operations that preserve the set type
- Lazy Intersections
- Projections
- Distance computations
- Plotting