From: Ioannis F. <jfi...@gm...> - 2021-04-11 00:24:52
|
Hi Rishabh, TLA+ ==== TLA+ is a language for writing mathematics, including specifications. TLA+ is described in the book (PDF available there): http://lamport.azurewebsites.net/tla/book.html?back-link=learning.html#book More about it, including tools, can be found at: http://lamport.azurewebsites.net/tla/tla.html Raw TLA+ includes more temporal formulas than TLA+. The raw logic and how it differs is described in the paper: http://lamport.azurewebsites.net/pubs/pubs.html#lamport-actions Below I use raw TLA+. Temporal formula form ===================== At the temporal logic level of `tulip` there is no predefined variable that counts time. Such a variable could be defined in your specification, but the first complication that would arise would be due to the finiteness of the set of values that that variable can take. Instead of defining such a variable, the prime operator can be used to describe how the system can change. For example, in raw TLA+: ``` (* Initial condition *) Init == obs_loc = 1 (* How the obstacle can change locations. *) Transitions == /\ (obs_loc = 1) => \/ obs_loc' = 2 \/ obs_loc' = 4 /\ (obs_loc = 2) => (obs_loc' = 3) /\ (obs_loc = 3) => (obs_loc' = 4) /\ (obs_loc = 4) => (obs_loc' = 4) (* Which regions to avoid, depending on the current location of the obstacle. *) WhatToAvoid == /\ (obs_loc = 1) => ~ region_1 /\ (obs_loc = 2) => ~ region_2 /\ (obs_loc = 3) => ~ region_3 /\ (obs_loc = 4) => ~ region_4 Prop == /\ Init /\ [] /\ Transitions /\ WhatToAvoid ``` where `obs_loc` is a variable that describes the location of the obstacle (as an index), and `region_1`, .., `region_4` are variables that name polytopes in the workspace (`region_1` for example means `x \in Region1`, where `x` would be the continuous state of the system). More about using the prime operator to describe obstacle movement can be found in the references that I linked to in my previous email. polytope representation ======================= The function `polytope.polytope.box2poly` is a convenience interface. Currently, the class `polytope.polytope.Polytope` represents covex polytopes, and the class `polytope.polytope.Region` polytopes (including nonconvex ones). https://en.wikipedia.org/wiki/Polytope The half-space representation is used for convex polytopes. More about this representation can be read at: https://en.wikipedia.org/wiki/Convex_polytope#Definitions The minimal vertex representation can be computed from the half-space representation using the function `polytope.polytope.extreme`: https://github.com/tulip-control/polytope/blob/f981f434a270ee005076b9c534383aeaba314f40/polytope/polytope.py#L1480 A half-space representation can be computed from a vertex representation using the function `polytope.polytope.qhull`: https://github.com/tulip-control/polytope/blob/f981f434a270ee005076b9c534383aeaba314f40/polytope/polytope.py#L1567 An example that demonstrates these two functions is: https://github.com/tulip-control/polytope/blob/f981f434a270ee005076b9c534383aeaba314f40/examples/randplot.py The geometry of the half-space representation is that it describes the intersection of a collection of half-spaces, by describing the hyperplane that bounds each half-space, which is done via a distance and a vector normal to the hyperplane. Deciding whether a point is in the half-space is (roughly) done by taking the inner product between the point's location vector and the half-space's normal vector, and comparing this with the distance. (A normalization step is needed to make the "distances" appear in the numbers.) By your wording ("a series of vertices in a 2d plane"), you probably do not mean the polytope defined as the convex hull of those vertices, but the set of points "enclosed" by a simple closed polygonal chain: https://en.wikipedia.org/wiki/Polygonal_chain in other words, a simple polygon: https://en.wikipedia.org/wiki/Simple_polygon A simple polygon can be nonconvex, so the class `polytope.polytope.Region` needs to be used to represent it. One way to do this is to first triangulate the polygon, forming a mesh of simplices https://en.wikipedia.org/wiki/Triangle_mesh then to convert the mesh to a `list` of convex polytopes using the function `polytope.polytope.simplices2polytopes`: https://github.com/tulip-control/polytope/blob/f981f434a270ee005076b9c534383aeaba314f40/polytope/polytope.py#L2256 which can be used to instantiate a `polytope.polytope.Region`. More about simplices can be found at: https://en.wikipedia.org/wiki/Simplex Python packages like `shapely` or `pymesh` can probably be used for computing the triangulation: https://github.com/Toblerity/Shapely https://github.com/PyMesh/PyMesh Another resource is the documentation of the package `polytope`: https://github.com/tulip-control/polytope/blob/master/doc/tutorial.md Best regards, Ioannis On 4/8/21 10:42 PM, Rishabh Thakkar wrote: > Hi Ioannis, > > > > Thanks for the suggestions. I still had a few lingering questions. > > So my first thought was I could indeed define an "obstacle" to avoid for each individual timestep, but I was not able to see or understand how I would generate an LTL formula for avoiding the unsafe region at each time step. In other words, does there exist an internal state variable such as "t" representing time or a specific time step that I can access while generating the LTL formula as something like "[] (t=1 -> ~obstacle_t1 && t=2 -> ~obstacle_t2 && ... && t=n -> ~obstacle_tn)"? I realize worst case I can have something in the dynamics that increments by 1 at each step, but I was wondering if there was something already built in? > > Furthermore, I am also confused about defining a polytope that is not in the shape of a box. All of the examples use this box2poly function, but I don't see one defined with a series of vertices. I see that the constructor for a polytope asks for a matrix A and vector b denoted as hyperplane normals and offsets, but I don't exactly understand that terminology. Is there any reference that explains how I can take a series of vertices in a 2d plane represent them as a polytope? > > Thank you, > Rishabh > > On Thu, Apr 8, 2021 at 10:28 AM Ioannis Filippidis <jfi...@gm... <mailto:jfi...@gm...>> wrote: > > Hi Rishabh, > > It would possible to describe moving obstacles in discrete time > by using an LTL formula that mentions the names of polytopic regions > in the workspace. For example, if the formula requires that the system > not be in region_1 at one point in time, and not in a nearby region_2 > at a consecutive point in time, etc., this would correspond to an > obstacle that moved from occupying region_1 to occupying region_2, etc. > > Such a formula would probably better be formed programmatically by > operating on strings in Python (and defining the corresponding > polytopic regions). Writing the formula by hand may not be practical, > due to its size and complexity. > > This approach also allows using discrete-valued environment variables > that determine how the obstacles move, thus enabling also the modeling of > an unknown behavior for how the obstacles will move, subject to > assumptions. More information about this approach can be found in > TuLiP's references, in particular: > https://github.com/tulip-control/tulip-control/blob/bb004422b575dccea8d19c33acfeb04b37c62a5a/doc/bib.txt#L57-L68 > The resulting interaction between system and environment can be > regarded as a game. > > About discretizing continuous movement in this way: by either > enlarging the obstacle regions, or using appropriate continuous-state > uncertainties in the system dynamics, it could be possible to > account for the intermediate positions that the obstacles occupy in > continuous time. This may be a conservative approximation of the > continuous-time planning problem. > > I am not sure whether by "dynamic" obstacles you mean obstacles that > have continuous dynamics (besides moving). > > Best regards, > Ioannis > > On 4/8/21 2:31 AM, Rishabh Thakkar wrote: > > Hi there, > > > > I was browsing through the TuLiP examples, but it wasn't clear to me how or > > whether there was support for designing an environment with dynamic > > obstacles for a continuous environment. If that is not, is it possible to > > input a list of polytopes representing safe or unsafe regions for each > > discrete time step? Ultimately, I am trying to model a moving obstacle in > > the continuous world. I'm hoping to start with a deterministic path of the > > obstacle, but eventually transition it to something that behaves as an > > adversary to the primary system being controlled effectively creating a > > game. To what extent could TuLiP support modeling this type of system. > > > > Thanks, > > Rishabh > > -------------- next part -------------- > > An HTML attachment was scrubbed... > > > > _______________________________________________ > > tulip-control-users mailing list > > tul...@li... <mailto:tul...@li...> > > https://lists.sourceforge.net/lists/listinfo/tulip-control-users > > > |