UMD CMSC 722 - Chapter 17 Planning Based on Model Checking

Unformatted text preview:

Chapter 17 Planning Based on Model CheckingMotivationNondeterministic SystemsExampleSlide 5Slide 6Execution StructuresSlide 8Slide 9Slide 10Slide 11Slide 12Types of SolutionsFinding Strong SolutionsSlide 15Slide 16Slide 17Slide 18Slide 19Slide 20Slide 21Slide 22Slide 23Finding Weak SolutionsSlide 25Slide 26Slide 27Finding Strong-Cyclic SolutionsSlide 29Example 1Slide 31Slide 32Slide 33Example 2: no applicable actions at s5Slide 35Slide 36Slide 37Slide 38Slide 39Slide 40Planning for Extended GoalsSlide 42Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/1Chapter 17Planning Based on Model CheckingDana S. NauUniversity of Maryland09:34 AM January 14, 2019Lecture slides forAutomated Planning: Theory and PracticeDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/2MotivationActions with multiple possibleoutcomesAction failures»e.g., gripper drops its loadExogenous events»e.g., road closedNondeterministic systems are like Markov Decision Processes (MDPs), but without probabilities attached to the outcomesUseful if accurate probabilities aren’t available, or if probability calculations would introduce inaccuraciesacbgrasp(c)acbIntendedoutcomea bcUnintendedoutcomeDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/3Nondeterministic SystemsNondeterministic system: a triple  = (S, A, ) S = finite set of states A = finite set of actions : S  A  2sLike in the previous chapter, the book doesn’t commit to any particular representationIt only deals with the underlying semanticsDraw the state-transition graph explicitlyLike in the previous chapter, a policy is a function from states into actionsπ: S  ANotation: Sπ = {s | (s,a)  π}In some algorithms, we’ll temporarily have nondeterministic policies»Ambiguous: multiple actions for some statesπ: S  2A, or equivalently, π  S  AWe’ll always make these policies deterministic before the algorithm terminatesDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/4GoalStart2Robot r1 startsat location l1Objective is toget r1 to location l4 π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4)), (s5, move(r1,l3,l4))} π3 = {(s1, move(r1,l1,l4))}ExampleDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/5GoalStart2Robot r1 startsat location l1Objective is toget r1 to location l4 π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4)), (s5, move(r1,l3,l4))} π3 = {(s1, move(r1,l1,l4))}ExampleDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/6GoalStart2Robot r1 startsat location l1Objective is toget r1 to location l4 π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4)), (s5, move(r1,l3,l4))} π3 = {(s1, move(r1,l1,l4))}ExampleDana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/7GoalStart2Execution StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (Q,T)Q  S T  S  S π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4)), (s5, move(r1,l3,l4))} π3 = {(s1, move(r1,l1,l4))}s2s1s5s3s4Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/8Execution StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (Q,T)Q  S T  S  S π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4)), (s5, move(r1,l3,l4))} π3 = {(s1, move(r1,l1,l4))}s2s1s5s3s4Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/9GoalStart2Execution StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (Q,T)Q  S T  S  S π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4)), (s5, move(r1,l3,l4))} π3 = {(s1, move(r1,l1,l4))}s2s1s5s3s4Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/10Execution StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (Q,T)Q  S T  S  S π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4)), (s5, move(r1,l3,l4))} π3 = {(s1, move(r1,l1,l4))}s2s1s5s3s4Dana Nau: Lecture slides for Automated PlanningLicensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/11GoalStart2Execution StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (Q,T)Q  S T  S  S π1 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3, move(r1,l3,l4))} π2 = {(s1, move(r1,l1,l2)), (s2, move(r1,l2,l3)), (s3,


View Full Document
Download Chapter 17 Planning Based on Model Checking
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 Chapter 17 Planning Based on Model Checking 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 Chapter 17 Planning Based on Model Checking 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?