Integrating processes in temporal logic

In this paper we propose a technique to integrate process models in
classical structures for quantified temporal (modal) logic. The idea
is that in a temporal logic processes are ordinary syntactical objects
with a specific semantical representation. So we want to achieve a
`temporal logics of processes' to adequately describe aspects of
systems dealing with data structures, reactive and time-critical
behavior, environmental influences, and their interaction in a single
frame. Thus the structural information of processes can be captured
and exploited to guide proofs. As an instance of this scheme we
present a quantified, metric, linear temporal logic containing
processes and conjunctions of processes explicitly. Like a predicate a
process can be regarded as a special kind of atomic formula with its
own intension, a family of sets collecting the observable behavior as
`runs'. A run is comparable with a Hoare-traces or a timed
observational sequence it is a sequence of sequences of values taken
from a set of objects. Each single value can be regarded as a
snapshot of an observable feature at a moment in time, e.g. a value
transmitted through a channel. ... mehr Such a set has to respects the
structure of the underlying temporal logic, but not one to one, we do
not require that for a path in the time structure there is exactly one
possible run. Since each run has a certain length, the view of a run
is in particular associated with a time interval. The difference
between moments and intervals of time is expressed by several kinds of
modal operators each of them with restrictions in the shape of
annotated equations and predicates to determined the relevant time
slices. We describe syntax and semantic of this logic especially with
a focus on the process part. Finally we sketch a calculus and give
some examples.