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 language | English |
---|---|
Pages (from-to) | 113-151 |
Number of pages | 39 |
Journal | Journal of Computer and System Sciences |
Volume | 92 |
Issue number | March |
Early online date | 9 Oct 2017 |
DOIs | |
Publication status | Published - Mar 2018 |
Keywords
- Compositional reasoning
- Probabilistic process algebras
- SOS specification formats
- Structural operational semantics
- Uniform continuity