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

Direct link
HD-Automata for Open Bisimulation
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Mobility)
2005 (English)Report (Other academic)
Place, publisher, year, edition, pages
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2005-037
URN: urn:nbn:se:uu:diva-93877OAI: oai:DiVA.org:uu-93877DiVA: diva2:167504
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2009-11-30Bibliographically approved
In thesis
1. Relations in Models of Calculi and Logics with Names
Open this publication in new window or tab >>Relations in Models of Calculi and Logics with Names
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. viii + 128 p.
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 132
Process Calculi, Syntax, Semantics, HD-automata, Logic, Category theory
National Category
Computer Engineering
urn:nbn:se:uu:diva-6245 (URN)91-554-6426-2 (ISBN)
Public defence
2006-01-16, Room 1211, Polacksbacken, Lägerhyddsvägen 2F, Uppsala, 10:15 (English)
Available from: 2005-12-22 Created: 2005-12-22 Last updated: 2011-02-18Bibliographically approved

Open Access in DiVA

No full text

Other links

By organisation
Computer Systems

Search outside of DiVA

GoogleGoogle Scholar
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

Total: 196 hits
ReferencesLink to record
Permanent link

Direct link