uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Relations in Models of Calculi and Logics with Names
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2006 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In this thesis we investigate two operational models of name-passing calculi: one based on coalgebra, and one based on enriched automata. We develop a semantic framework for modelling the open bisimulation in π-calculus, hyperbisimulation in Fusion calculus, and the first semantic interpretation of FOλ(nabla) logic.

We consider a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of atoms. The key aspect of this model is to consider functors over the category of irreflexive and symmetric finite relations. The models previously proposed for the separate notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter.

Moreover, the new model admits a definition of distinction-aware simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu's FOλ(nabla) logic. FOλ(nabla) logic is designed for reasoning about operational semantics of languages with binding.

On the operational level, a contribution of the thesis is to extend an automata-based model for a variety of name-passing calculi with their associated notion of equivalence. HD-automata, a syntax-independent operational model, has been successfully applied for modelling e.g. early and late bisimulation in π-calculus and hyperbisimulation in Fusion calculus. However, current HD-automata are not adequate for modelling open bisimulation because they can not handle distinction-preserving substitutions. We solve this technical problem by integrating the notion of distinction into the definition of named sets, the basic building blocks of HD-automata. Finally, we discuss the relationship between HD-automata with distinctions, and D-LTS.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis , 2006. , p. viii + 128
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 132
Keywords [en]
Process Calculi, Syntax, Semantics, HD-automata, Logic, Category theory
National Category
Computer Engineering
Identifiers
URN: urn:nbn:se:uu:diva-6245ISBN: 91-554-6426-2 (print)OAI: oai:DiVA.org:uu-6245DiVA, id: diva2:167505
Public defence
2006-01-16, Room 1211, Polacksbacken, Lägerhyddsvägen 2F, Uppsala, 10:15 (English)
Opponent
Supervisors
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2018-01-13Bibliographically approved
List of papers
1. Relationally Staged Computations in Calculi of Mobile Processes
Open this publication in new window or tab >>Relationally Staged Computations in Calculi of Mobile Processes
2004 (English)In: Proc. 7th Workshop on Coalgebraic Methods in Computer Science / [ed] J. Adámek, S. Milius, Elsevier , 2004, p. 105-120Conference paper, Published paper (Refereed)
Abstract [en]

We apply the recently developed techniques of higher order abstract syntax and functorial operational semantics to give a compositional and fully abstract semantics for the π-calculus equipped with open bisimulation. The key novelty in our work is the realisation that the sophistication of open bisimulation requires us to move from the usual semantic domain of presheaves over subcategories of Set to presheaves over subcategories of Rel. This extra structure is crucial in controlling the renaming of extruded names and in providing a variety of different dynamic allocation operators to model the different binders of the π-calculus.

Place, publisher, year, edition, pages
Elsevier, 2004
Series
Electronic Notes in Theoretical Computer Science, ISSN 1571-0661 ; 106
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-93874 (URN)10.1016/j.entcs.2004.02.027 (DOI)
Conference
Workshop on Coalgebraic Methods in Computer Science (CMCS), Barcelona, Spain, 27–29 March 2004
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2018-01-13Bibliographically approved
2. A unifying model of variables and names
Open this publication in new window or tab >>A unifying model of variables and names
2004 (English)Report (Other academic)
Place, publisher, year, edition, pages
Department of Mathematics and Computer Science, University of Udine, 2004
Series
Research Report UDMI ; 15/2004/RR
Identifiers
urn:nbn:se:uu:diva-93875 (URN)
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2009-11-30Bibliographically approved
3. Modelling Fusion Calculus using HD-Automata
Open this publication in new window or tab >>Modelling Fusion Calculus using HD-Automata
Show others...
2005 (English)Report (Other academic)
Abstract [en]

We propose a coalgebraic model of the Fusion calculus based on HD-automata. The main advantage of the approach is that the partition refinement algorithm designed for HD-automata is easily adapted to handle Fusion calculus processes. Hence, the transition systems of Fusion calculus processes can be minimised according to the notion of observational semantics of the calculus. As a beneficial side effect, this also provides a bisimulation checker for Fusion calculus.

Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2005-038
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:uu:diva-93876 (URN)
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2018-01-13Bibliographically approved
4. HD-Automata for Open Bisimulation
Open this publication in new window or tab >>HD-Automata for Open Bisimulation
2005 (English)Report (Other academic)
Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2005-037
Identifiers
urn:nbn:se:uu:diva-93877 (URN)
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2009-11-30Bibliographically approved

Open Access in DiVA

fulltext(873 kB)865 downloads
File information
File name FULLTEXT01.pdfFile size 873 kBChecksum MD5
481795b34f414225116ceae63693e876e48f76198be3cb42e13e9273e19d72d7182b5ed8
Type fulltextMimetype application/pdf
cover(452 kB)38 downloads
File information
File name COVER01.pdfFile size 452 kBChecksum MD5
18455d646f1868c03d9f05da8d3ff8ee5c68d8bc0bfb8caed7fa8f43de4c026102a22ba3
Type coverMimetype application/pdf
Buy this publication >>

By organisation
Division of Computer SystemsComputer Systems
Computer Engineering

Search outside of DiVA

GoogleGoogle Scholar
Total: 865 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1584 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf