## 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. Name-passing 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 namepassing,

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

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

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.

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. Name-passing 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 namepassing,

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

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

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.

Originalsprog | Engelsk |
---|

Forlag | IT-Universitetet i København |
---|---|

Antal sider | 102 |

ISBN (Trykt) | 978-87-7949-010-9 |

Status | Udgivet - 2017 |

Navn | ITU-DS |
---|---|

Nummer | 143 |

ISSN | 1602-3536 |