Trustworthy Systems

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,
    address          = {Portsmouth, USA},
    author           = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael},
    booktitle        = {Workshop on Knowledge Engineering for Planning and Scheduling},
    keywords         = {automated planning, upper bounds},
    month            = jun,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8205.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/8205.pdf},
    title            = {Mechanising Theoretical Upper Bounds in Planning},
    year             = {2014}
  }

Download