Process modeling deals with several aspects of a process: the static, dynamic, and hierarchical aspects describe properties of its states, computations, and actions, respectively. This thesis aims to integrate these aspects in a single semantical concept which is based on labeled Kripke structures.

Starting from first-order logic for describing individual states, elements of labeled transition systems are integrated. For modeling sequences of actions, a branching time model is used where states and actions are modeled by first-order structures.

Additionally, the structural aspect of actions deals with abstraction and refinement: elementary actions can be used to define complex actions, or complex actions can be decomposed into their subactions, leading to a hierarchical state space.

The temporal relationships between states and actions on the same level, forming computation sequences, and the relationships between states on different levels of abstraction are combined into a labeled Kripke structure. Different accessibility relations are used for representing the temporal successor relation and relating states on different levels of abstraction of the model. To cover the intended refinement semantics of the hierarchical state space, the temporal successor relation contains additional information about the Kripke subframe which represents the refined action. The frame problem is solved by distinguishing procedure knowledge and frame knowledge. An axiomatization based on inheritance along the accessibility relations is given which describes the intended semantics.

For reasoning about labeled Kripke structures, two complementary logics are defined, extending first-order logic by temporal modalities and temporal connectives, respectively: for specification of individual actions, frame axioms, eventualities, and guarantee properties, a modal logic for branching time, LCTL, is defined based on CTL, whereas for reasoning about action sequences, a logic with temporal connectives, ECL, is defined. The combination of both logics provides a powerful formal instrument for describing static and dynamic aspects of a process.

For both logics, tableau calculi are given which share a common tableau representation, also leading to an integrated calculus.