A general SOS theory for the specification of probabilistic transition systems

TitleA general SOS theory for the specification of probabilistic transition systems
Publication TypeJournal Article
Year of Publication2016
AuthorsD'Argenio, PR, Gebler, D, Lee, MD
JournalInf. Comput.
Volume249
Pagination76–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.
URLhttp://dx.doi.org/10.1016/j.ic.2016.03.009
DOI10.1016/j.ic.2016.03.009
PDF (Full text): 
Powered by Drupal