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 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.




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.




Return to homepage