Independence, name-passing and constraints in models for concurrency

Håkon Normann

    Publikation: AfhandlingerPh.d.-afhandling

    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.
    OriginalsprogEngelsk
    KvalifikationDoktor i filosofi (ph.d.)
    Vejleder(e)
    • Hildebrandt, Thomas, Hovedvejleder
    Bevillingsdato22 dec. 2017
    Udgiver
    ISBN'er, trykt978-87-7949-010-9
    StatusUdgivet - 2017

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Independence, name-passing and constraints in models for concurrency'. Sammen danner de et unikt fingeraftryk.

    Citationsformater