On timed models and full abstraction

Gavin Lowe and Joël Ouaknine

In this paper we study a denotational model for a discrete-time version of CSP. We give a compositional semantics for the language. The model records refusal information at the end of each time unit; we believe this model to be simpler than existing models. We also show that the model is fully abstract: equivalence in the model corresponds to the natural equivalence of may testing; and all members of the denotational model are syntactically expressible. We also consider a slightly weaker model, containing no refusal information; we show that this model corresponds to an alternative form of may testing. We briefly discuss the application of these models to the study of information flow in multi-level secure systems.

Proceedings of MFPS 05, ENTCS 155, 2006. 21 pages.

PostScript / PDF © 2006 Elsevier Science B.V.

Imprint / Data Protection