Structural Operational Semantics for Continuous State Stochastic Transition Systems

Giorgio Bacci, Marino Miculan

Research output: Contribution to journalJournal articleResearchpeer-review

12 Citations (Scopus)

Abstract

In this paper we show how to model syntax and semantics of stochastic processes with continuous states, respectively as algebras and coalgebras of suitable endofunctors over the category of measurable spaces Meas. Moreover, we present an SOS-like rule format, called MGSOS , representing abstract GSOS over Meas, and yielding fully abstract universal semantics , for which behavioral equivalence is a congruence. An MGSOS specification defines how semantics of processes are composed by means of measure terms , which are expressions specifically designed for describing finite measures. The syntax of these measure terms, and their interpretation as measures, are part of the MGSOS specification. We give two example applications, with a simple and neat MGSOS specification: a “quantitative CCS”, and a calculus of processes living in the plane R2
whose communication rate depends on their distance. The approach we follow in these cases can be readily adapted to deal with other quantitative aspects.
Original languageEnglish
JournalJournal of Computer and System Sciences
Volume81
Issue number5
Pages (from-to)834–858
ISSN0022-0000
DOIs
Publication statusPublished - Aug 2015

Fingerprint

Dive into the research topics of 'Structural Operational Semantics for Continuous State Stochastic Transition Systems'. Together they form a unique fingerprint.

Cite this