info:eu-repo/semantics/article
A general SOS theory for the specification of probabilistic transition systems
Fecha
2016-03Registro en:
D'argenio, Pedro Ruben; Gebler, Daniel; Lee, Matias David; A general SOS theory for the specification of probabilistic transition systems; Academic Press Inc Elsevier Science; Information and Computation; 249; 3-2016; 76-109
0890-5401
CONICET Digital
CONICET
Autor
D'argenio, Pedro Ruben
Gebler, Daniel
Lee, Matias David
Resumen
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.