Structural Operational Semantics for Stochastic Process Calculi

Abstract. A syntactic framework called SGSOS, for defining well-behaved Markovian stochastic transition systems, is introduced by analogy to the GSOS congruence format for nondeterministic processes. Stochastic bisimilarity is guaranteed a congruence for systems defined by SGSOS rules. Associativity of parallel composition in stochastic process algebras is also studied within the framework.

• Type: Conference
• Year: 2008
• Where: FOSSACS
• Authors: Bartek Klin, Vladimiro Sassone
• Keywords: FOSSACS 2008, GSOS Congruence Format, Markovian Stochastic Transition, Software Engineering, Stochastic