DOC PREVIEW
Berkeley ELENG C149 - Controller Synthesis

This preview shows page 1-2-3-4-5 out of 15 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 15 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

1Introduction toEmbedded SystemsEdward A. Lee & Sanjit A. SeshiaUC BerkeleyEECS 149Spring 2009Copyright © 2008-09, Edward A. Lee & Sanjit A. Seshia, All rights reservedLecture 19: Controller SynthesisEECS 149, UC Berkeley: 2A Robot delivery service, with moving obstacles φ = destination for robot At any time step:Robot can move Left, Right, Up, Down, Stay PutEnvironment can move one obstacle Up or Down or Stay Put But only total of 2 times over all time stepsCan model Robot and Env as FSMsRobot state = its position, Env state = positions of obstacles and countφφφφstart2EECS 149, UC Berkeley: 3Recap of topics covered last time 1. Stated the goal in temporal logic: F φ The problem is a “reachability problem”2. Gave an algorithm to solve a version of the reachabilityproblem3. Considered some alternative goals:F φ1∧ F φ2∧ … ∧ F φnF( φ1∧ F ( φ2∧ … ∧ F φn))φφφφstartEECS 149, UC Berkeley: 4Reachability Analysis, RevisitedThe reachability problem:Given an FSM M = (Q, δ, Q0), and a state φ, is s reachable from some q0∈ Q0by following δ ?System evolution according to δ is a sequence: robot step, env step, robot step, env step, …φ is reachable if there is some sequence of robot and env steps from q0to φ This seq need not have the worst-case env steps! It’s optimistic – assumes helpful environment (not adversarial)3EECS 149, UC Berkeley: 5. . .QkQ2Visualizing ‘Optimistic’ Controller SynthesisQ1Q0SSSφS – obstacles “stay put”D – obstacle “moves down”DEECS 149, UC Berkeley: 6Synthesis with an Adversarial EnvironmentSuppose at every step, an adversary picks the worst possible action to stop the robot’s progressThis is a game between the system and its adversarial environmentWe want to modify the search performed by the reachability algorithm to handle this worst-case behavior.Any ideas?4EECS 149, UC Berkeley: 7Controllable StatesIdea:Compute the set of states from which, no matter what the environment does, the robot can reach the red square φ.Such states are called controllable states.What are some examples of controllable states for our robot example?EECS 149, UC Berkeley: 8Examples of Controllable Statesφφφφstartrobot5EECS 149, UC Berkeley: 9Examples of Controllable StatesφφφφstartEnv_Moves = MAX_MOVESEECS 149, UC Berkeley: 10Examples of Controllable StatesφφφφstartEnv_Moves = MAX_MOVES6EECS 149, UC Berkeley: 11Synthesis Algorithm1.Start with the set of trivially controllable states S02.Add all states from which the robot can reach S0in one combined step (robot step, env step), no matter what the environment does3.Repeat until no new states added 4.Check if this set contains a start state. If yes, then we found a strategy. If no, then no strategy exists against the worst-case environment (adversary).EECS 149, UC Berkeley: 12Synthesis Algorithm: Formal DescriptionInput: Description of M: (Q0, δ), Goal state φEach state q = (q1, q2), δ1updates q1, δ2updates q2Output: Does Q0contain a controllable state?Init: S := Snew:= φ; /* Note φ != ∅ */while (Snew!= ∅) {if (Snew∩ Q0!= ∅) return YES;S’ := { q | ∀ p1∈ δ1(q) ∃ p2∈ δ2(p1) s.t. p2∈ S } ∪ SSnew:= S’ \ S; S := S’;} return NO;S is the set of controllable statesenvrobot7EECS 149, UC Berkeley: 13Controller Synthesis for G pSuppose we want the system to always satisfy property p alternatively, we want the system to never satisfy ¬ pE.g. robot should never hit an obstacle; aircraft should never collide; etc.How can we use the previous algorithm to synthesize a control strategy for G p?[Idea: switch the roles of the environment and the system (robot) –now the environment is trying to reach a goal state. Avoid the states controllable by the environment]EECS 149, UC Berkeley: 14Recap of ConceptsSynthesis is a Game between the Robot (“System”) and its EnvironmentGoal for robot: F φRobot wins if it reaches φEnvironment wins otherwise Zero-sum gameGoal for env: G ¬ φEnvironment wins if φ is always falseRobot wins otherwise8EECS 149, UC Berkeley: 15Rest of today’s lecture Discuss synthesis for G F p How to synthesize a continuous trajectory EECS 149, UC Berkeley: 16Handling other kinds of Temporal Logic GoalsG F pExample: The iRobot must visit the charging station infinitely often Consider the FSM formed by composing the iRobot FSM with its Environment FSM Visualize this FSM as a directed graph Suppose that “visiting the charging station” is a state p in this graphWhat graph property corresponds to visiting the state p infinitely often?9EECS 149, UC Berkeley: 17Winning Strategy for G F pThe system must visit state p infinitely oftenFor benign environment (optimistic synthesis):The state graph must contain a cycle with state pHow can we detect this if we have to build the graph on the fly? EECS 149, UC Berkeley: 18Finding Winning Strategy for G F pThe system must visit state p infinitely oftenFor benign environment (optimistic synthesis):The state graph must contain a cycle with state pHow can we detect this if we have to build the graph on the fly? Two steps:1. Check if p is reachable from the initial state2. Check if p is reachable from itself10EECS 149, UC Berkeley: 19Winning Strategy for G F p: Adversarial SettingThe system must visit state p infinitely oftenHow do we check this for an adversarial environment?EECS 149, UC Berkeley: 20Perform “Adversarial Reachability”!Checking that p is reached infinitely often for an adversarial environment:Two steps:1. Check if p is reachable from the initial state, no matter what the adversary does2. Check if p is reachable from itself, no matter what the adversary doesFor each of these steps, use the algorithm we used on slide 12 of this lecture11EECS 149, UC Berkeley: 21Synthesizing a Continuous TrajectoryφφφφstartSuppose we have a discrete trajectory (path) to φHow do we transform that into the desired continuous trajectory?(assume static obstacles)EECS 149, UC Berkeley: 22Necessary ConditionφφφφstartφφφφstartIf there exists a discrete trajectory, then there must also exist a continuous trajectory12EECS 149, UC Berkeley: 23The Other ConditionφφφφstartφφφφstartIf there isn’t a discrete trajectory, it is possible/OK fora continuous trajectory to exist? EECS 149, UC Berkeley: 24Bisimulation (revisited)The property we need is


View Full Document
Download Controller Synthesis
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Controller Synthesis and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Controller Synthesis 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?