SOS specifications for uniformly continuous operators

Daniel Gebler, Simone Tini

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

Fingerprint

Uniformly continuous
Semantics
Specification
Specifications
Operator
Structural Operational Semantics
Uniform Continuity
Metric
Algebra
Formal Semantics
Process Algebra
Mathematical operators
Subsystem
Reasoning
Imply

Keywords

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

Cite this

Gebler, Daniel ; Tini, Simone. / SOS specifications for uniformly continuous operators. In: Journal of Computer and System Sciences. 2018 ; Vol. 92, No. March. pp. 113-151.
@article{2c57d2b983334acdb9653d74d7bf9bc3,
title = "SOS specifications for uniformly continuous operators",
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.",
keywords = "Compositional reasoning, Probabilistic process algebras, SOS specification formats, Structural operational semantics, Uniform continuity",
author = "Daniel Gebler and Simone Tini",
year = "2018",
month = "3",
doi = "10.1016/j.jcss.2017.09.011",
language = "English",
volume = "92",
pages = "113--151",
journal = "Journal of Computer and System Sciences",
issn = "0022-0000",
publisher = "Elsevier",
number = "March",

}

SOS specifications for uniformly continuous operators. / Gebler, Daniel; Tini, Simone.

In: Journal of Computer and System Sciences, Vol. 92, No. March, 03.2018, p. 113-151.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - SOS specifications for uniformly continuous operators

AU - Gebler, Daniel

AU - Tini, Simone

PY - 2018/3

Y1 - 2018/3

N2 - 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.

AB - 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.

KW - Compositional reasoning

KW - Probabilistic process algebras

KW - SOS specification formats

KW - Structural operational semantics

KW - Uniform continuity

UR - http://www.scopus.com/inward/record.url?scp=85032193371&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85032193371&partnerID=8YFLogxK

U2 - 10.1016/j.jcss.2017.09.011

DO - 10.1016/j.jcss.2017.09.011

M3 - Article

VL - 92

SP - 113

EP - 151

JO - Journal of Computer and System Sciences

JF - Journal of Computer and System Sciences

SN - 0022-0000

IS - March

ER -