Plan Verification in HTN Planning

In HTN planning, plans don't only need to be executable, they also need to be a refinement of the initial plan. The following systems perform that reasoning.

• Plan Correction Approach:

  • URL: https://github.com/siprog/PlanCorrectionKR2021
  • Further Info: This approach is technically not performing plan verification. It performs plan corrections in case a plan is not a solution. (So it's performing verification as a substep.) The 'base approach' that only performs verification will be available soon. See details on the project page. However, it the plan serving as input plan is a solution already, then this approach likely states so (so it is acting as verification system as a special case), but it's less efficient than the specialized version of this that only performs plan verification.

• Plan Verification via Encoding into SAT:

  • URL: http://panda3.hierarchical-task.net
  • Further info: This plan verifier verifies plans just based on the plan alone, i.e., no decomposition hierarchy (e.g., sequence of decomposition methods) is not used or even provided. In fact, the main task is to figure out whether the plan can be produced by the model's task hierarchy. This is done via an encoding into SAT. (This is only available in the the now outdated PANDA-3 planner. The code is not longer maintained.)

• Plan Verification via Encoding into HTN Planning:

  • URL: https://github.com/panda-planner-dev/pandaPIpgrRepairVerify
  • Further info: This plan verifier also verifies plans just based on the plan alone, just like the encoding into SAT. This approach does however not create a SAT problem, but an HTN problem so that standard HTN planners can be used to solve the problem. These are two implementations of the same transformation, where the second is slightly newer and also supports plan repair and plan recognition.

• Plan Verification via Parsing:

  • URLs:
    • https://github.com/siprog/HTNPLanValidationThesis
    • https://github.com/panda-planner-dev/pandaPIpgrRepairVerify
  • Further info: There are actually two verifiers that verify plans based on parsers. Both adapt a parsing approach, since verifying an HTN plan corresponds to checking the word problem of a formal grammar.
    • The first approach bases on the Rete parsing appraoch. Note that the version linked here is not the newest one as its (newest) code has not yet been publicly released. Please contact the authors (see repository) if you need the newest version. It finds any compound task from the domain that decomposes into the given action sequence, not a given goal task or initial task network. This was changed in later versions, to be released soon. If until then you want to use this code to verify whether an action sequence is a plan, i.e., can be obtained from a given initial task network, you can edit the model by introducing a new compound task and a single method decomposing it into the problem's initial task network. (It works for TO and PO domains.)
    • The second one extends the standard CYK algorithm and hence only works for TO HTN domains.

• Simple Plan Verification with Plan and method sequence given:

  • URL: See output specification page of IPC 2020
  • Further info: This plan verifier was created for the IPC 2020. It requires the applied methods leading to the plan in question as additional input. The syntax of that hierarchy output follows that of the IPC 2020 and is specified on the given webpage.