eTheses Repository

On the compositionality of round abstraction

Menaa, Mohamed Nabih (2012)
Ph.D. thesis, University of Birmingham.

PDF (1174Kb)


Game Semantics is an approach to denotational semantics that has been successful in providing accurate, fully abstract models for various programming languages. It has thereafter been applied, amongst other things, to model checking, access control analysis, information flow analysis, and recently, hardware synthesis.

While the roots of modern Game Semantics are sequential, several game models of asynchronous concurrency have since been devised. However, synchronous concurrency has not been considered hitherto.

This thesis studies synchronous concurrency in game-like models. The central idea is to investigate deriving such synchronous models from their asynchronous counterparts using round abstraction--a technique that allows aggregating a sequence of computational steps to form a larger, more abstract macro-step.

We define round abstraction within a trace-semantic setting that generalises game semantic models. We note that, in general, round abstraction is not compositional. We then identify sufficient conditions to guarantee correct composition, thereby proposing a framework for round abstraction that is sound when applied to synchronous and asynchronous behaviours.

We explore extensions of our synchronous model with causality, global clocks and determinism.

Type of Work:Ph.D. thesis.
Supervisor(s):Ghica, Dan
School/Faculty:Colleges (2008 onwards) > College of Engineering & Physical Sciences
Department:School of Computer Science
Subjects:QA75 Electronic computers. Computer science
QA76 Computer software
T Technology (General)
Institution:University of Birmingham
ID Code:3381
This unpublished thesis/dissertation is copyright of the author and/or third parties. The intellectual property rights of the author or third parties in respect of this work are as defined by The Copyright Designs and Patents Act 1988 or as modified by any successor legislation. Any use made of information contained in this thesis/dissertation must be in accordance with that legislation and must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the permission of the copyright holder.
Export Reference As : ASCII + BibTeX + Dublin Core + EndNote + HTML + METS + MODS + OpenURL Object + Reference Manager + Refer + RefWorks
Share this item :
QR Code for this page

Repository Staff Only: item control page