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/2MotivationActions with multiple possibleoutcomesAction failures»e.g., gripper drops its loadExogenous events»e.g., road closedNondeterministic systems are like Markov Decision Processes (MDPs), but without probabilities attached to the outcomesUseful 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 SystemsNondeterministic system: a triple = (S, A, ) S = finite set of states A = finite set of actions : S A 2sLike in the previous chapter, the book doesn’t commit to any particular representationIt only deals with the underlying semanticsDraw the state-transition graph explicitlyLike in the previous chapter, a policy is a function from states into actionsπ: S ANotation: Sπ = {s | (s,a) π}In some algorithms, we’ll temporarily have nondeterministic policies»Ambiguous: multiple actions for some statesπ: S 2A, or equivalently, π S AWe’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/4GoalStart2Robot r1 startsat location l1Objective 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/5GoalStart2Robot r1 startsat location l1Objective 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/6GoalStart2Robot r1 startsat location l1Objective 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 StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (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 StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (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 StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (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 StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (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 StructuresExecution structurefor a policy π:The graph of all ofπ’s execution pathsNotation: π = (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