Extending dynamic logic with refinements of abstract actions

Humans can make a plan by refining abstract actions. Dynamic logic, which enables reasoning about the dynamics of actions, does not support this form of planning. This paper investigates the extension of dynamic logic with a refinement relation that specifies how an abstract action can be refined into a more specific (composite) action. The paper investigates the properties of the refinement relation, the derivation of the refinement relation and a proof system based on a prefixed-tableau.