Article contents
Pointwise extensions of GSOS-defined operations
Published online by Cambridge University Press: 25 March 2011
Abstract
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.
- Type
- Paper
- Information
- Mathematical Structures in Computer Science , Volume 21 , Special Issue 2: Coalgebraic Logic , April 2011 , pp. 321 - 361
- Copyright
- Copyright © Cambridge University Press 2011
References
- 5
- Cited by