Collaborative Research on Systems and Security

2006 
Abstract : There are two areas where the research conducted under this grant was focused: (1) research on models of concurrency, and in particular on true concurrency, and (2) models for probabilistic choice. In the first area, we collaborated with Professor Paul Gastin, then of the Universite de Paris VII, over a period of years on devising domain-theoretic models to support true concurrency. This approach to modeling concurrent computation differs from the usual approach, where parallel composition is modeled by synchronization and interleaving of non-synchronized actions. In true concurrency, the approach is different, with an attempt to model actions occurring concurrently, rather in a specified order. The results of this research are reported in the journal papers 1) and 3) above. The summary of the results are that we devised a denotational model for a simple parallel programming language that supports prefixing, sequential composition, hiding, restriction, parallel composition using true concurrency, and recursion. We also showed that the denotational model is fully abstract with a natural operational model for the process calculus we devised, where one observes only unsynchronized atomic actions. The second area of research focused on models for probability. Our interest in this area was inspired by results of our colleague A. W. Roscoe, who showed that there is no information flow in a system where Low's view of the system is deterministic. The idea was to devise a more comprehensive model where probabilistic choice could replace nondeterminism, thus allowing a differentiation between the choices of the system and those of the users. Our first results along this line provided a model for probabilistic choice that also supports nondeterminism, in a setting in which the expected laws for both operations are obeyed in the model. This work is reported in paper 3) under papers in conference proceedings.
    • Correction
    • Cite
    • Save
    • Machine Reading By IdeaReader
    0
    References
    0
    Citations
    NaN
    KQI
    []