Integrated Static and Dynamic Modeling of Processes
Dissertation/PhD thesis, Wolfgang May,
Freiburg, Mai 1998
Prof. Dr. Georg Lausen,
Prof. Dr. Peter H. Schmitt,
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
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.
Published by logos Verlag,
Berlin, 1998, ISBN 3-89722-153-5.