SOS specifications for uniformly continuous operators

Daniel Gebler, Simone Tini*

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

Behavioral metric semantics provide formal notions to compare probabilistic systems, giving a notion of behavioral distance characterizing how far the behavior of two systems is apart. Compositional reasoning over probabilistic systems with respect to behavioral metric semantics requires the language operators to be uniformly continuous, which ensures that a limited change in the behavior of a subsystem implies a smooth and limited change in the behavior of the whole system. We consider a hierarchy of uniform continuity properties for process algebra operators and, for each of these properties, we propose a Structural Operational Semantics specification format (namely a set of syntactical constraints on the form of the SOS rules) ensuring that the property is satisfied by construction by all operators captured by the format.

Original languageEnglish
Pages (from-to)113-151
Number of pages39
JournalJournal of Computer and System Sciences
Volume92
Issue numberMarch
Early online date9 Oct 2017
DOIs
Publication statusPublished - Mar 2018

Keywords

  • Compositional reasoning
  • Probabilistic process algebras
  • SOS specification formats
  • Structural operational semantics
  • Uniform continuity

Fingerprint

Dive into the research topics of 'SOS specifications for uniformly continuous operators'. Together they form a unique fingerprint.

Cite this