Independence, name-passing and constraints in models for concurrency

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.