For modeling structured processes with different levels of atomic
actions, classical linear or branching time Kripke structures with
first-order states are insufficient:
They do not provide any means for modeling independent parallel
threads of activity which have to be joined at some point,
action refinement, or procedure concepts.
In all three cases, it is important to distinguish facts resp.
knowledge derived in the current thread of activity from
facts which are not concerned in this activity.
This problem is also closely related to the frame problem.
In this paper, hierarchical Kripke structures are introduced for
modeling hierarchically structured processes, also coping with
the different qualities of knowledge arising in this context:
every state consists of a total first-order interpretation, which
gives the state as-is, and a partial first-order interpretation
containing all procedure knowledge which has been derived in the
current thread of activity.
A correct and complete set of axioms is presented for reasoning
about hierarchical Kripke structures.
