Dana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 1 Chapter 10 Control Rules in Planning Dana S. Nau University of Maryland 5:01 PM April 4, 2012 Lecture slides for Automated Planning: Theory and PracticeDana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 2 Motivation ● Often, planning can be done much more efficiently if we have domain-specific information ● Example: ◆ classical planning is EXPSPACE-complete ◆ block-stacking can be done in time O(n3) ● But we don’t want to have to write a new domain-specific planning system for each problem! ● Domain-configurable planning algorithm ◆ Domain-independent search engine (usually a forward state-space search) ◆ Input includes domain-specific information that allows us to avoid a brute-force search » Prevent the planner from visiting unpromising statesDana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 3 Motivation (Continued) ● If we’re at some state s in a state space, sometimes a domain- specific test can tell us that ◆ s doesn’t lead to a solution, or ◆ for any solution below s, there’s a better solution along some other path ● In such cases we can to prune s immediately ● Rather than writing the domain-dependent test as low-level computer code, we’d prefer to talk directly about the planning domain ● One approach: ◆ Write logical formulas giving conditions that states must satisfy; prune states that don’t satisfy the formulas ● Presentation similar to the chapter, but not identical ◆ Based partly on TLPlan [Bacchus & Kabanza 2000]Dana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 4 Quick Review of First Order Logic ● First Order Logic (FOL): ◆ constant symbols, function symbols, predicate symbols ◆ logical connectives (∨, ∧, ¬, ⇒, ⇔), quantifiers (∀, ∃), punctuation ◆ Syntax for formulas and sentences on(A,B) ∧ on(B,C) ∃x on(x,A) ∀x (ontable(x) ⇒ clear(x)) ● First Order Theory T: ◆ “Logical” axioms and inference rules – encode logical reasoning in general ◆ Additional “nonlogical” axioms – talk about a particular domain ◆ Theorems: produced by applying the axioms and rules of inference ● Model: set of objects, functions, relations that the symbols refer to ◆ For our purposes, a model is some state of the world s ◆ In order for s to be a model, all theorems of T must be true in s ◆ s |= on(A,B) read “s satisfies on(A,B)” or “s entails on(A,B)” » means that on(A,B) is true in the state sDana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 5 Linear Temporal Logic ● Modal logic: FOL plus modal operators to express concepts that would be difficult to express within FOL ● Linear Temporal Logic (LTL): ◆ Purpose: to express a limited notion of time » An infinite sequence 〈0, 1, 2, …〉 of time instants » An infinite sequence M= 〈s0, s1, …〉 of states of the world ◆ Modal operators to refer to the states in which formulas are true: ¡ f - next f - f holds in the next state, e.g., ! on(A,B) ♢ f - eventually f - f either holds now or in some future state  f - always f - f holds now and in all future states f1 ∪ f2 - f1 until f2 - f2 either holds now or in some future state, and f1 holds until then ◆ Propositional constant symbols TRUE and FALSEDana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 6 Linear Temporal Logic (continued) ● Quantifiers cause problems with computability ◆ Suppose f(x) is true for infinitely many values of x ◆ Problem evaluating truth of ∀x f(x) and ∃x f(x) ● Bounded quantifiers ◆ Let g(x) be such that {x : g(x)} is finite and easily computed ∀[x:g(x)] f(x) • means ∀x (g(x) ⇒ f(x)) • expands into f(x1) ∧ f(x2) ∧ … ∧ f(xn) ∃[x:g(x)] f(x) • means ∃x (g(x) ∧ f(x)) • expands into f(x1) ∨ f(x2) ∨ … ∨ f(xn)Dana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 7 Models for LTL ● A model is a triple (M, si, v) ◆ M = 〈s0, s1, …〉 is a sequence of states ◆ si is the i’th state in M, ◆ v is a variable assignment function » a substitution that maps all variables into constants ● To say that v(f ) is true in si , write (M,si,v) |= f ● Always require that (M, si,v) |= TRUE (M, si,v) |= ¬FALSE ● For planning, need to augment LTL to refer to goal states ◆ Include a GOAL operator such that GOAL(f) means f is true in every goal state ◆ ((M,si,V),g) |= GOAL(f) iff (M,si,V) |= f for every si ∈ gDana Nau: Lecture slides for Automated Planning Licensed under the Creative Commons Attribution-NonCommercial-ShareAlike License: http://creativecommons.org/licenses/by-nc-sa/2.0/ 8 ● Suppose M= 〈s0, s1, …〉 (M,s0,v) |= ¡¡ on(A,B) means A is on B in s2 ● Abbreviations: (M,s0) |= ¡¡ on(A,B) no free variables, so v is irrelevant: M |= ¡¡ on(A,B) if we omit the state, it defaults to s0 ● Equivalently, (M,s2,v) |= on(A,B) same meaning with no modal operators s2 |= on(A,B) same thing in ordinary FOL ● M |= ¨¬holding(C) ◆ in every state in M, we aren’t holding C ● M |= ¨(on(B, C) ⇒ (on(B, C) ∪ on (A, B))) ◆ whenever we enter a state in which B is on C, B remains on C until A is on B. ExamplesDana Nau: Lecture slides for Automated Planning Licensed under the