Open Systems Laboratory at Illinois

A theory of may testing for asynchronous calculi with locality and no name matching

By Prasannaa Thati, Reza Ziaei, and Gul Agha. In AMAST, volume 2422 of Lecture Notes in Computer Science, 223–238. Springer, 2002.

Full Text:
Download PDF
Publisher Link:
http://dx.doi.org/10.1007/3-540-45719-4_16

Abstract

We present a theory of may testing for asynchronous calculi with locality and no name matching. Locality is a non-interference property that is common in systems based on object-paradigm. Concurrent languages such as Join and Pict disallow name matching, which is akin to pointer comparison in imperative languages, to provide for an abstract semantics that would allow useful program transformations. May testing is widely acknowledged to be an effective notion for reasoning about safety properties. We provide a trace-based characterization of may testing for versions of asynchronous π-calculus with locality and no name matching, which greatly simplifies establishing equivalences between processes. We also exploit the characterization to provide a complete axiomatization for the finitary fragment of the calculi.

BibTeX

@inproceedings{conf/amast/ThatiZA02,
    author = "Thati, Prasannaa and Ziaei, Reza and Agha, Gul",
    editor = "Kirchner, Hélène and Ringeissen, Christophe",
    title = "A Theory of May Testing for Asynchronous Calculi with
             Locality and No Name Matching",
    booktitle = "AMAST",
    crossref = "conf/amast/2002",
    ee = "http://dx.doi.org/10.1007/3-540-45719-4_16",
    keywords = "formal methods",
    pages = "223-238",
    year = "2002",
}

@proceedings{conf/amast/2002,
    editor = "Kirchner, Hélène and Ringeissen, Christophe",
    title = "Algebraic Methodology and Software Technology, 9th
             International Conference, AMAST 2002, Saint-Gilles-les-Bains,
             Reunion Island, France, September 9-13, 2002, Proceedings",
    isbn = "3-540-44144-1",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    volume = "2422",
    year = "2002",
}