Affordable Access

A specification structure for deadlock-freedom of synchronous processes

Publication Date
  • Qa75 Electronic Computers. Computer Science
  • Computer Science
  • Linguistics


Many different notions of “program property”, and many different methods of verifying such properties, arise naturally in programming. We present a general framework of Specification Structures for combining different notions and methods in a coherent fashion. We then apply the idea of specification structures to concurrency in the setting of Interaction Categories. As a specific example, a certain specification structure defined over the interaction category GProc yields a new category GProcD in which morphisms are deadlock-free concurrent processes and composition is process interaction. GProcD is obtained from GProc by adding specification information to the objects which is strong enough to guarantee deadlock-freedom. The main technical contribution is to show that this can be done in a way which is preserved by composition. The methods used to achieve this can be seen as a semantic analogue of those used to prove strong normalization in classical linear logic.

There are no comments yet on this publication. Be the first to share your thoughts.