Abstract
In this thesis we look at independence, name-passing and constraints in models for concurrency, with the goal of obtaining models that encompass all three aspects.
With independence we mean that two actions are independent if they have no impact on each other. Namepassing is that names or terms are communicated around in the process by actions, and can give rise to new actions or synchronizations. Constraints are when some conditions have to be met by the state of the process in order for some action to be enabled or disabled. We choose Psi-calculus as a common frame as this is a meta-model that
encompass name-passing, constraints and parallel composition, but lack the notion of independence.
For the initial look on constraints we provide instantiations of event structures and DCR-graphs into Psi-calculi to prove that the assertions and constraints of Psi can encompass known constraint-based models with independence.
We provide a notion of syntactically correct processes for each of the instantiations and a mapping from the event structure or DCR-graph into a syntactically correct process. We also show that any syntactically correct process is a mapping of an event structure or DCR-graph. For the event structure instantiation we give a notion of refinement of the process, which takes a syntactically correct process and generate a new syntactically correct process in the same style of standard event structure action refinement.
We then go on to provide non-interleaving semantics for the guarded early pi-calculus. Our starting point here is the non-interleaving semantics for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject)
causality and events are defined from a notion of locations derived from the syntactic structure of the process term.
The semantics are conservatively extended with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the name-passing topology of the pi-calculus. We prove
that these semantics give rise to a labelled asynchronous transition system.
We finally introduce the logical causality that is generated by the assertions, conditions and enabling mechanics of the Psi-calculus, and what the obstacles that have to be overcome in order to get non-interleaving semantics for
the full Psi-calculi framework.
With independence we mean that two actions are independent if they have no impact on each other. Namepassing is that names or terms are communicated around in the process by actions, and can give rise to new actions or synchronizations. Constraints are when some conditions have to be met by the state of the process in order for some action to be enabled or disabled. We choose Psi-calculus as a common frame as this is a meta-model that
encompass name-passing, constraints and parallel composition, but lack the notion of independence.
For the initial look on constraints we provide instantiations of event structures and DCR-graphs into Psi-calculi to prove that the assertions and constraints of Psi can encompass known constraint-based models with independence.
We provide a notion of syntactically correct processes for each of the instantiations and a mapping from the event structure or DCR-graph into a syntactically correct process. We also show that any syntactically correct process is a mapping of an event structure or DCR-graph. For the event structure instantiation we give a notion of refinement of the process, which takes a syntactically correct process and generate a new syntactically correct process in the same style of standard event structure action refinement.
We then go on to provide non-interleaving semantics for the guarded early pi-calculus. Our starting point here is the non-interleaving semantics for CCS by Mukund and Nielsen, where the so-called structural (prefixing or subject)
causality and events are defined from a notion of locations derived from the syntactic structure of the process term.
The semantics are conservatively extended with a notion of extruder histories, from which we infer the so-called link (name or object) causality and events introduced by the name-passing topology of the pi-calculus. We prove
that these semantics give rise to a labelled asynchronous transition system.
We finally introduce the logical causality that is generated by the assertions, conditions and enabling mechanics of the Psi-calculus, and what the obstacles that have to be overcome in order to get non-interleaving semantics for
the full Psi-calculi framework.
| Original language | English |
|---|
| Publisher | IT-Universitetet i København |
|---|---|
| Number of pages | 102 |
| ISBN (Print) | 978-87-7949-010-9 |
| Publication status | Published - 2017 |
| Series | ITU-DS |
|---|---|
| Number | 143 |
| ISSN | 1602-3536 |