Trustworthy Systems

Mechanising theoretical upper bounds in planning


Mohammad Abdulaziz, Charles Gretton and Michael Norrish


Australian National University

Griffith University


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

    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         = {},
    slides           = {},
    title            = {Mechanising Theoretical Upper Bounds in Planning},
    year             = {2014}