Hostname: page-component-6898cfcb55-cbk24 Total loading time: 0 Render date: 2026-11-11T03:15:23.196Z Has data issue: false hasContentIssue false

Pointwise extensions of GSOS-defined operations

Published online by Cambridge University Press:  25 March 2011

HELLE HVID HANSEN
Affiliation:
Technische Universiteit Eindhoven and Centrum Wiskunde & Informatica, P.O. Box 513, 5300 MB Eindhoven, The Netherlands Email: h.h.hansen@tue.nl
BARTEK KLIN
Affiliation:
University of Cambridge and University of Warsaw, 15 JJ Thomson Avenue, Cambridge CB3 0FD, U.K. Email: klin@mimuw.edu.pl
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Final coalgebras capture system behaviours such as streams, infinite trees and processes. Algebraic operations on a final coalgebra can be defined by distributive laws (of a syntax functor Σ over a behaviour functor F). Such distributive laws correspond to abstract specification formats. One such format is a generalisation of the GSOS rules known from structural operational semantics of processes. We show that given an abstract GSOS specification ρ that defines operations σ on a final F-coalgebra, we can systematically construct a GSOS specification ρ that defines the pointwise extension σ of σ on a final FA-coalgebra. The construction relies on the addition of a family of auxiliary ‘buffer’ operations to the syntax. These buffer operations depend only on A, so the construction is uniform for all σ and F.

Information

Type
Paper
Copyright
Copyright © Cambridge University Press 2011