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
JournalInformation and Computation
Volume249
Pagination76-109
Date Published08/2016
ISSN0890-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.
URLhttp://www.sciencedirect.com/science/article/pii/S0890540116000468
DOI10.1016/j.ic.2016.03.009
PDF (Full text):