Analysing Input/Output-Capabilities of Mobile Processes with a ...


Barbara König. Analysing input/output-capabilities of mobile processes with a generic type system. In Proc. of ICALP '00, pages 403–414. Springer-Verlag, 2000. LNCS 1853.


We introduce a generic type system for the synchronous polyadic -calculus, allowing us to mechanize the analysis of input/output capabilities of mobile processes. The parameter of the generic type system is a lattice-ordered monoid, the elements of which are used to describe the capabilities of channels with respect to their input/output-cabilities. The type system can be instantiated in order to check process properties such as upper and lower bounds on the number of active channels, confluence and absence of blocked processes.

Suggested BibTeX entry:

    author = {Barbara K{\"o}nig},
    booktitle = {Proc. of ICALP '00},
    note = {{LNCS} 1853},
    pages = {403--414},
    publisher = {{Springer-Verlag}},
    title = {Analysing Input/Output-Capabilities of Mobile Processes with a Generic Type System},
    year = {2000}

GZipped PostScript (42 kB)PDF (123 kB)Journal version, Tech report version
© University of Duisburg-Essen, Theoretical Computer Science group