A Tableau Calculus For First-Order Branching Time Logic
Wolfgang May, Peter H. Schmitt
Abstract:
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.