|
KEYWORDS process calculus, true concurrency, resource, consumption, recycling,
quantification, pomset, denotational and structural
operational semantics, full abstraction. PURPOSE We combine a truly concurrent approach
on the denotational side with a weighted automata view on the operational
side, by developing a truly concurrent
semantical approach to modelling CSP and CCS without choice based on a
programming semantics using particular kinds of pomsets, according to the new stream of weighted automata theory consisting in attaching weights to
transitions which express their cost in terms of some available resources.
The developed approach formalizes the consumption
and recycling of resources by
processes, presenting a processes language similar to both CSP
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. PROJECTS After having clarified the obvious
algebraic interaction of residuation with the operators of the process language one
would easily check the essential fact that the denotational semantics of all
operators is linear even using weights from an algebra. This approach would enable to
interpret a substitution and a replication operator as a more modern
alternative to the recursion operator. Applications
in Computer Science and Management The theoretical work already developed
should be followed by prospection of the applications in engineering and economy,
where the notion of consumable or recyclable resource is ubiquitous, for
instance in transactional systems and workflow management. Developing a Residuational Denotational
Semantics We
also care to note that the residuation operator whose properties underlie
most of the main results of this semantical work over complex multi-pomsets has been axiomatized in
a much more general setting by Panangaden and
Stark. Quite general domains and corresponding automata based on residues
have furthermore been considered in the extensive work of Droste
and Kuske. Residuation is
moreover axiomatised in modal logics (for example
in arrow logics) which have a rich denotational semantics. We venture stating
that part, if not the whole semantics, may be cast in that setting, thus
providing an approach which is more algebraic and richer in semantical models
than the one we have presented and therefore more amenable to modelling
complex examples and applications. Checking the Stability and Linearity
of the Denotational Semantics Much
of the theory required for complex multi-pomsets
can be clarified by using the domain-theoretic machinery developed for stable/linear embedding-projection pairs,
for instance in the case of Berry's category of dI-domains.
Apart from the benefit of tightening the present discourse, this would also
offer the opportunity to extend the interpretational framework by drawing on
the already well-developed experience with models for substructural
logics (arrow logics, resource logics, linear logic). Replacing Recursion with Replication 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 replication
operator that would be more modern and easy to comprehend in order to have a
universal (Turig-complete) process language that is
more expressive regarding different concurrency paradigms and easier to
model-check than the \pi-calculus. Enriching
the Process Calculus with a Choice
Operator The
sole operator customary in other process languages which,
as for now, has been intentionally left out in ours is the non-deterministic choice. Using
power-domains over complex multi-pomsets should
provide a clear way of expressing the necessary notion of non-determinism in
order to model choice at the expectable expense of rendering the
domain-theoretic tools more involved. Another possibility to achieve the same
result could reside in enriching complex multi-pomsets
with a further relation on trace events expressing conflict of choices, thus
imposing a modellig view closer to event
structures. Simplifying the Dirty Semantics of
the Alphabetized Parallel Operator 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 plain parallel operator
would perform only the necessary space-parallel synchronization, as compared
to the partitional operator that spatially
completely separates the processes. Such an operator seems difficult to define
denotationally, but is easy to define and to reason
upon operationally either by synchronization which expresses common progress
on identical actions (as in CSP) or communication which expresses common
progress on dual actions (as in CCS). Also, there is operationally little
need in imposing a synchronization alphabet $S$ distinguishing between
private as opposed to common actions/resources, the three operational rules
of the alphabetized parallel operator already being in mutual exclusion of
assertions and therefore offering deterministic processing alternatives even
if dropping all assertions on the synchronization alphabet $S$. This is the
case for the defined plain parallel operator. We note that the latter rules
cannot be obtained from the former for any particular choice of the
synchronization alphabet $S$ and, therefore, do not represent a special case
of the alphabetized parallel operator. This plain parallel operator allows
processes not only to commonly progress but moreover each process to also
perform local tasks provided that they do not interfere with the rest. It
only blocks the local activity of a process that is conflicting with other
processes while enabling joint progress through synchronization in the case
of coincidence of purposes and communication in the case of complementarity
of purposes. Due to the condition on the resource semantics, the operational
rules for the plain parallel operator described above already represent
operationally disjoint choices and, therefore, do not introduce
non-determinism. Note that this is not the case for the classical operational
rules of the parallel operator obtained from these ones by dropping the
precondition pertaining to resources, this being the very reason why the
classical parallel operator is customary expanded to a non-deterministic
choice of alternatives. Independence versus Parallelism Using the equivalence $\a \disj p$ iff $a \parl p \trans{a} p$ could make the resource semantics
operationally entirely superfluous by replacing independence with the already present parallelism. The interesting question is whether this approach
may also enable a more abstract denotational semantics which does not make
use of resources at all in order to define a semantical domain of processes,
thereby substantially simplifying and generalizing the denotation of the
operators. An Enriched Categorial Semantics 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 enriched
categorical framework along the unifying lines drawn by the work of Lawvere concerning orders and metrics. This would allow
define a completion of enriched categories trough formal balls along the line
of results mentioned above. A Distributed
Operational Semantics The
denotational semantics that we have defined over complex multi-pomsets should better be matched with a distributed structural operational
semantics, by specifying separate transition rules for processes running
on each resource. This step should be similar to the one employed in Mazurkiewicz trace theory when going over from sequential
diamond automata to asynchronous Zielonka automata. Complexity of Labelled Partial Orders and Expressiveness of Process Languages An interesting question would be
to formally inquire the expressiveness
of the process language by defining a complexity
measure for the language terms and subsequently complexity classes of
labelled partial orders. Abstracting
Weight Arithmetics to an Equational Ordered Algebra 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 equational ordered
algebra as labels of the partial orders, in order to naturally combine
domain theory and weighted automata theory. Defining a Substitution
Operator on the Domain Substituting
the labels of a pomset by pomsets
allows defining a powerful substitution
operator that could be used to interpret an operation similar to the
application of \lambda-calculus and would render the process language
universal (Turing-complete) as is for instance the \pi- calculus. Time and Space as Resources 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