From Explicit to Symbolic Types for Communication Protocols in CCS

Hanne Riis Nielson; Flemming Nielson; Jörg Kreiker; Henrik Pilegaard

doi:10.1007/978-3-642-24933-4_5

From Explicit to Symbolic Types for Communication Protocols in CCS

Hanne Riis Nielson
, Flemming Nielson
, Jörg Kreiker
, Henrik Pilegaard

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Abstract

We study communication protocols having several rounds and expressed in value passing CCS. We develop a type-based analysis for providing an explicit record of all communications and show the usual subject reduction result. Since the explicit records can be infinitely large, we also develop a type-based analysis for providing a finite, symbolic record of all communications. We show that it correctly approximates the explicit record and prove an adequacy result for it.

Original language	English
Title of host publication	Formal Modeling: Actors, Open Systems, Biological Systems : Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday
Publisher	Springer
Publication date	2012
Pages	74-89
ISBN (Print)	978-3-642-24932-7
DOIs	https://doi.org/10.1007/978-3-642-24933-4_5
Publication status	Published - 2012
Event	Symposium in honor of Carolyn Talcott - Menlo Park, United States Duration: 3 Nov 2011 → 4 Nov 2011

Conference

Conference	Symposium in honor of Carolyn Talcott
Country/Territory	United States
City	Menlo Park
Period	03/11/2011 → 04/11/2011

Series	Lecture Notes in Computer Science
Number	7000
ISSN	0302-9743

Access to Document

10.1007/978-3-642-24933-4_5

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{69a079c254c942d4ab30157fd284de7b,

title = "From Explicit to Symbolic Types for Communication Protocols in CCS",

abstract = "We study communication protocols having several rounds and expressed in value passing CCS. We develop a type-based analysis for providing an explicit record of all communications and show the usual subject reduction result. Since the explicit records can be infinitely large, we also develop a type-based analysis for providing a finite, symbolic record of all communications. We show that it correctly approximates the explicit record and prove an adequacy result for it.",

author = "Nielson, \{Hanne Riis\} and Flemming Nielson and J{\"o}rg Kreiker and Henrik Pilegaard",

year = "2012",

doi = "10.1007/978-3-642-24933-4\_5",

language = "English",

isbn = "978-3-642-24932-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

number = "7000",

pages = "74--89",

booktitle = "Formal Modeling: Actors, Open Systems, Biological Systems",

note = "Symposium in honor of Carolyn Talcott ; Conference date: 03-11-2011 Through 04-11-2011",

}

Nielson, HR, Nielson, F, Kreiker, J & Pilegaard, H 2012, From Explicit to Symbolic Types for Communication Protocols in CCS. in Formal Modeling: Actors, Open Systems, Biological Systems: Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. Springer, Lecture Notes in Computer Science, no. 7000, pp. 74-89, Symposium in honor of Carolyn Talcott, Menlo Park, California, United States, 03/11/2011. https://doi.org/10.1007/978-3-642-24933-4_5

From Explicit to Symbolic Types for Communication Protocols in CCS. / Nielson, Hanne Riis; Nielson, Flemming; Kreiker, Jörg et al.
Formal Modeling: Actors, Open Systems, Biological Systems: Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. Springer, 2012. p. 74-89 (Lecture Notes in Computer Science; No. 7000).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - From Explicit to Symbolic Types for Communication Protocols in CCS

AU - Nielson, Hanne Riis

AU - Nielson, Flemming

AU - Kreiker, Jörg

AU - Pilegaard, Henrik

PY - 2012

Y1 - 2012

N2 - We study communication protocols having several rounds and expressed in value passing CCS. We develop a type-based analysis for providing an explicit record of all communications and show the usual subject reduction result. Since the explicit records can be infinitely large, we also develop a type-based analysis for providing a finite, symbolic record of all communications. We show that it correctly approximates the explicit record and prove an adequacy result for it.

AB - We study communication protocols having several rounds and expressed in value passing CCS. We develop a type-based analysis for providing an explicit record of all communications and show the usual subject reduction result. Since the explicit records can be infinitely large, we also develop a type-based analysis for providing a finite, symbolic record of all communications. We show that it correctly approximates the explicit record and prove an adequacy result for it.

U2 - 10.1007/978-3-642-24933-4_5

DO - 10.1007/978-3-642-24933-4_5

M3 - Article in proceedings

SN - 978-3-642-24932-7

T3 - Lecture Notes in Computer Science

SP - 74

EP - 89

BT - Formal Modeling: Actors, Open Systems, Biological Systems

PB - Springer

T2 - Symposium in honor of Carolyn Talcott

Y2 - 3 November 2011 through 4 November 2011

ER -

From Explicit to Symbolic Types for Communication Protocols in CCS

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this