Robust SOS Specifications of Probabilistic Processes

Daniel Gebler

promotor: prof.dr. W. Fokkink (VUA)
copromotor: dr. P.R. D’Argenio (FaMAF, Universidad Nacional de Córdoba)
Vrije Universiteit Amsterdam
Date: 13 November, 2015, 09:45


We develop a language specification theory for probabilistic nondeterministic systems in the context of metric bisimulation semantics. This theory generalizes and extends ordinary Plotkin-style Structural Operational Semantics language specification theory of nondeterministic systems. The main contributions are:

  • unification and generalization of existing metric compositionality concepts
  • language specification formats for all metric compositionality concepts
  • language meta-theoretical results for metric compositional language specifications
  • denotational model of metric compositionality of language operators and programs
  • axiomatization of the bisimulation distance of language operators and programs

We introduce the notion of uniformly continuous language operators as canonical metric compositionality concept that generalizes earlier proposals like non-extensive and non- expansive operators and allows us now to reason also about recursive programs. Then we develop a spectrum of language specification formats for the spectrum of compositionality properties formed by uniform continuity, Lipschitz continuity, non-expansiveness and non-extensiveness that allows us to specify simultaneously unbounded recursive, bounded recursive, non-recursive and choice operators. We derive for each language specification format compositionality results that allow us to determine the distance between programs and provide methods to verify if a program specification satisfies some compositionality property. Complementary to the structural specification results we develop a denotational model that formalizes in a stratified manner the primitive program behavior that determines the compositionality property of language operators. Finally, an equational axiomatization of the behavioral distance of language operators derived from their respective specifications provides an algorithmic approach to deduce algebraic properties such as the distance between programs.