Skip to main content

TS

Mechanising theoretical upper bounds in planning

Authors

Mohammad Abdulaziz, Charles Gretton and Michael Norrish

NICTA

Australian National University

Griffith University

Abstract

We examine the problem of computing upper bounds on the lengths of plans. Tractable approaches to calculating such bounds are based on a decomposition of state-variable dependency graphs (causal graphs). Our contribution follows an existing formalisation of concepts in that setting, reporting our efforts to mechanise bounding inequalities in HOL. Our primary contribution is to identify and repair an important error in the original formalisation of bounds. We also develop novel bounding results and compare them analytically with existing bounds.

BibTeX Entry

  @inproceedings{Abdulaziz_GN_14,
    author           = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael},
    month            = {jun},
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/8205.pdf},
    year             = {2014},
    keywords         = {automated planning, upper bounds},
    title            = {Mechanising Theoretical Upper Bounds in Planning},
    booktitle        = {Workshop on Knowledge Engineering for Planning and Scheduling},
    address          = {Portsmouth, USA}
  }

Download