-
Notifications
You must be signed in to change notification settings - Fork 0
IJCAI 19
Discussion on Plan-Property Dependencies 1 and 2.
- Plan property: polytime-computable Boolean fn of task Pi and applicable action sequence vec_a
- Basic dependency: p entails q if, for every applicable action sequence vec_a, if p(veca)=true then q(veca)=true, We say in this case that the basic dependency "p entails q" is valid in Pi.
- (Complex/general) dependency: propositional formula phi over plan properties. phi holds if, for every applicable action sequence vec_a, phi evaluates to true on vec_a. We say in this case that phi is valid in Pi. Basic dependencies are the special case "p ==> q". Motivation: this could be inside a single new plan prop. However, plan props are black boxes to the framework; in the exploration of composed dependencies, i.e. when solving the explanation problem specified below, the explanation facility will establish the interesting combinations across these blackboxes.
Entailment over two dependencies phi and psi: phi entails psi if, for every action sequence, if phi evaluates to true then so does psi. Note that this is equivalent to validity of the dependency "phi ==> psi".
show that dependencies, and entailment thereover, are more than standard propositional logic: even if a formula is not universally true, iot may be true for all action sequences due to the underlying planning task. In fact this will typically be the case, e.g. in a simple mutex where reaching one fact A excludes reaching another fact B.
- basic: find all pairwise dependencies, ie, compute the graph whose nodes are the properties and whose edges are the basic dependencies
- general: find all strongest dependencies: the root nodes in the DAG over equivalence classes of dependencies
Needs to be done carefully!
Place our approach and the kinds of explanations it provides relative to the literature (contrastive explanations). Which are the kinds of user questions that we can answer?
All this relates closely to propositional logic, to mutex analysis, to invariants more generally.
Relation to model checking ie asking questions about properties of planning task? Joerg thinks it's basically a special case, formulating a relevant analysis and implementing that effectively.
Use trucks/packs with fuel as canonical simple running example; but also more complex ones/beyond, inspired by proposal
as per draft (Rebecca + Michael)
more general plan props and how they can be compiled into previous.
given task Pi = (V,A,I) and plan property phi. design in polynomial time a task Pi' = (V',A',I') where V subseteq V' and A subseteq A' so that:
- for every applicable action sequence veca' in Pi' leading to state s', the A-subsequence veca of veca' is applicable in Pi and leads to a state s that agrees with s' on V;
- there is a state var v' in V' \setminus V such that, for every applicable action sequence veca' in Pi' leading to state s', v' is true in s' if and only if veca as per 1. satisfies phi in Pi.
research question: which known compilations can be done in this way?
- LTL over state variables: presumably only safety properties ie representable by finite automaton; is there a syntactic characterization of that fragment? Compilation into PDDL-style planning prior work Edelkamp (for MIPS IPC 2006), McIlraith (a few papers after 2005/6); presumably the compilations there can be used as-is, possibly with adaptations to fit the single-state-var v' setup we need here. Actually Edelkamp's compilation seems to work out of the box: add Buechi property automaton to task, force an automaton-advancing action after each regular action, check at end whether automaton is in accepting state.
- action subsets used in plan: eg is an instance of some action schema used? are actions from two different subset classes (eg using truck1 and using truck2) used? general formulation: propositional logic whose atoms are "plan uses at least one action from A_i" where A_i subseteq A. Compilation: one flag for each A_i, set by actions from A_i in plan; formula checking step at end. Strictly dominated by LTL, counting or ordering can not be expressed using action subsets. The atom "plan uses at least one action from A'" you can encode as (<> a_0 or .... or <> a_n) with a_i in A'. in experiments, only consider sub-clkasses of LTL anyhow; action subsets could be one of them; action reordering another; to be decided whether to implement the full compilation in front of the FD search phase, or only simpler/effective compilations for our special cases of interest.
on both simple instantiation (oplan properties are goal facts), and on compiled more general plan props.
should be done relative to solving simpler problems, specifically a) oversubscription planning ie finding a maximum-size solvable goal subset, and/or b) classical planning for a solvable goal set.
RCP (resource-constrained planning) domains from Marcel's previous work: NoMystery, TPP, Rovers.
Ideally, we should actually do something with existing oversubscription planning benchmarks. Carmel and Mirkis generated ones in their work (http://iew3.technion.ac.il/~dcarmel/Papers/Sources/ecai14b.pdf), from IPC benchmarks, by restricting plan cost to 25%, 50%, 75%, and 100% of optimal plan cost for all goals. Emulate this, for unit action costs, in a way that makes our current technology applicable. Question: what about the nogood learning here? does the search just prune against the g function? or do we represent a discrete g function through a discrete state variable treating it like a resource?
===> Should use all RCP benchmarks; and as many IPC benchmarks as feasible, preferring the ones from more recent IPCs (probably/possibly sklipping the ones with conditiona effects).
NoMystery: extension of the above where the new plan property is using only one specific truck (truck1, truck2), or using only a single truck (no matter which one). Another possibility: package1 and package2 should be delivered using the same truck (load/unload package1 on truckX excludes löoad/unload package2 on truckY).
Similar in TPP, Rovers; so far as there is >1 vehicle. Maybe variants with just one central fuel/energy store so we don't get into the pareto-optimality issue? Also an idea is to restrict to particular scalable instance family where the optimal amount of fuel/energy is known by construction; could be much easier to write generators for this.
Plan property of the form "plan uses an action from B and does not use an action from A" (because user is asking "why does the plan include an action from A rather than one from B?"): eg Logistics why is packageX transported with truckA not with truckB? why image with RoverA not RoverB?
===> Use the RCP benchmarks for this, extended with this kind of property.
IPC 2006 planning with temporal goals; make these oversubscribed problems and do the same as above. does this work with those benchmarks? IPC'06 TPP Storage and Rovers have non-temporal non-metric versions with trajectory constraints. In case all these constraints are satisfiable together, make oversubscribed by same method as in IPC ie impose bound on permitted plan cost. ==> TODO: read PDDL3 JAIR paper for terminology/variants; check which benchmarks we can use.
Temporal ordering over actions: plan uses A before B etc, easily expressed by/compiled into LTL over state variables. eg Logistics: why are you delivering packageA before packageB?
===> Use IPC'06 TPP Storage and Rovers, probably in oversubscribed version