Mini project 2 MAE 6740 – Fall ‘11 Assigned Oct. 25th, Due November 10th by 5 PM Verification of robot motion A robot is moving around an environment partitioned by a 4x4 grid, where each cell has length and width of 1 and the bottom left corner is the origin. The velocity of the robot is given by the vector [Vx, Vy] which is different for each grid cell. The grid has four specially marked cells: Init is the initial set (the robot starts somewhere in this set), G1 and G2 represent goal sets and B represents the unsafe set. Each grid cell also contains the value of [Vx, Vy] in that cell. Init [1,-1] [0.5,-2] [1,0] [0.1,-1] [0.1,-1] [0.1,-1] G2 [0.1,1] [-1,-1] [2,0.5] [1,-0.2] G1 [0,0] [-1,0.05] [0.5,2] [0.2,1] [0.1,1] B (0,0) x → 1. Model the motion of the robot as a Hybrid system. You may choose a graphical representation or a definition. What should the guards be? 2. The values for [Vx, Vy] in cell (1,2) (values indicated in bold) may cause problems when analyzing the system. Why? In the following, replace the values with [2,-0.3] 3. For the following statements, write the property as a temporal logic formula and then verify/falsify it. You may need extra variables: ↑ ya. The goal G1 is reachable from Init (there exists a trajectory originating in the set Init that reaches set G1) b. All trajectories originating in Init reach the goal G1. c. The goal G1 can be reached within 1 time unit d. The goal G1 can be reached within 10 time units e. The goal G2 is reachable from Init (there exists a trajectory originating in the set Init that reaches set G2) f. All trajectories originating in Init reach the goal G2. g. The system is safe (all trajectories originating in the set Init do not enter the unsafe set B) 4. Did you abstract the hybrid system? If so, how? Is it the right abstraction for the specification? Consider two robots moving in the 3x3 grid shown below Init1 [1,-1] Init2 [0.5,-2] [1,0] [0.1,-1] [0.1,-1] [0.1,1] [2,-0.3] [1,-0.2] G1 (0,0) x → Robot 1 starts somewhere in the set Init1 and Robot 2 starts somewhere in the set Init2. The robots are considered “in collision” if they are in the same cell at the same time. 5. How would you model the system of two robots? 6. Specify the requirement that the robots never be in collision (in temporal logic, with respect to the model of part 5) ↑ y7. Verify the property defined in part 6. You may use any of the tools and techniques discussed in class. Tools that might be useful: • UPPAAL: http://www.uppaal.org/ (better maintained than HyTech) • HyTech: http://embedded.eecs.berkeley.edu/research/hytech/ Note: Feel free to discuss the problem with others; however, writing and coding is to be done individually. Turn in your written answers (either hard copy or electronically) and email your code by the deadline. Final Project proposal 8. Describe (in approx. half a page) what you would like to do as a final project for the course. Define the problem, what will be done and how it is relevant to the class. Ideally, this project will be connected to your ongoing