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 | Inf. Comput. |
| Volume | 249 |
| Pagination | 76–109 |
| 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://dx.doi.org/10.1016/j.ic.2016.03.009 |
| DOI | 10.1016/j.ic.2016.03.009 |
PDF (Full text):
