A general SOS theory for the specification of probabilistic transition systems
Title | A general SOS theory for the specification of probabilistic transition systems |
Publication Type | Journal Article |
Year of Publication | 2016 |
Authors | D'Argenio, PR, Gebler, D, Lee, MD |
Journal | Information and Computation |
Volume | 249 |
Pagination | 76-109 |
Date Published | 08/2016 |
ISSN | 0890-5401 |
Abstract | This article focuses on the formalization of the structured operational semantics approach for languages with primitives that introduce probabilistic and non-deterministic behavior. We define a general theoretic framework and present the ntμfθ/ntμxθ rule format that guarantees that bisimulation equivalence (in the probabilistic setting) is a congruence for any operator defined in this format. We show that the bisimulation is fully abstract w.r.t. the ntμfθ/ntμxθ format and (possibilistic) trace equivalence in the sense that bisimulation is the coarsest congruence included in trace equivalence for any operator definable within the ntμfθ/ntμxθ format (in other words, bisimulation is the smallest congruence relation guaranteed by the format). We also provide a conservative extension theorem and show that languages that include primitives for exponentially distributed time behavior (such as IMC and Markov automata based language) fit naturally within our framework. |
URL | http://www.sciencedirect.com/science/article/pii/S0890540116000468 |
DOI | 10.1016/j.ic.2016.03.009 |
PDF (Full text):