process calculus, true concurrency, resource, consumption, recycling,
quantification, pomset, denotational and structural
operational semantics, full abstraction.
We combine a truly concurrent approach
on the denotational side with a weighted automata view on the operational
side, by developing a and CCS without choice, using
a trace-based operational
semantics over sets of strings of actions, a truly concurrent denotational semantics over pomsets
of actions, obtaining a full
abstraction result relating the
denotational and the operational semantics. One should note that the model
allows defining a continuous denotational semantics, being a good model
candidate even for a stable and linear denotational semantics, for all
operators defined so far namely serial,
sequential, parallel, partitional, restriction,
hiding and recursion. The benefit and purpose of the interpretational
extensions, especially the binary and
real number enrichment by resources, resides in the increased modelling
power of the process language. If continued, this line of development would thus deliver a linear universal (Turing-complete)
process language that is more
expressive and easier to
model-check than the pi calculus, theoretically and applicationally.
After having clarified the obvious
algebraic interaction of
The theoretical work already developed
should be followed by prospection of the applications in
We
also care to note that the
Much
of the theory required for complex multi-pomsets
can be clarified by using the domain-theoretic machinery developed for
After having proven that the
denotational semantics of all operators of the process language is linear one
should be able to easily define an alternative to the recursion operator
basing it on a
The
sole operator customary in other process languages which,
as for now, has been intentionally left out in ours is the
Although its operational semantics
is rather straightforward to understand its denotational semantics is
considerably more involved than that of any of the other operators presented
in this semantical work. The complex denotational definition
of the alphabetized parallel is concededly tailored in order to match the
operational definition, whose own justification as an essential form of
parallelism does not seem to be acquired, which is why we consider it to be a
complicated and dirty semantics of deterministic parallelism, which has to be
reconsidered in order to have a clear and clean semantics. Just as the serial
operator performs only the necessary time-serial synchronization as compared
to the sequential operator that temporally completely separates the
processes, a
Using the equivalence $\a \disj p$ iff $a \parl p \trans{a} p$ could make the resource semantics
operationally entirely superfluous by replacing
The
non-contractive metric semantics can be obtained as the maximal points of the
order semantics through the universal construction of formal balls defined by
Flagg & Koppermann for ultra-metrics and
extended to metrics by Edalat & Heckmann. It a posteriori clarified the manifest
connections between the order and metric properties of the underlying
semantical domains established by Diekert in 1992
and subsequently extended and enriched to the present models. A common order
and metric approach seems feasible by generalizing the ground domain of
labeled partial orders to an
The
denotational semantics that we have defined over complex multi-pomsets should better be matched with
An interesting question would be
to formally inquire the
The present models use vectors
of real weights as labels of the partial orders. Nevertheless, the underlying
intuition of modelling resources and the developed theory so far are largely
independent of this particular choice and could be enriched even further by
using weights of an
Substituting
the labels of a pomset by pomsets
allows defining a powerful
Time
and space should be considered as representing just two notable but
particular dual instances of the notion of resource. Precedence in time would
express causality between event-stamps while precedence in space would express
relocation between event-addresses. Serial and parallel composition would
represent just two forms of process combination with respect to particular
dual resources but otherwise be similar, the former
effecting ordered time exclusion the latter ordered space exclusion of
events. Just as serial composition sums time-stamps and joins space-addresses
the parallel composition would sum space-addresses and join time-stamp of
events in a dual way. In this view the parallel composition would cease to be
symmetric but a symmetrized version of the parallel composition could be
explicitly regained. Newer axiomatic approaches to the parallel composition
showing that the unsymmetrical parallel composition is essential in finite
axiomatizations could deliver the motivation for inquiring into the above
view. |

**©
Dan TEODOSIU**