Roberto Segala. A Compositional Trace-Based Semantics for Probabilistic Automata. In Insup Lee and Scott A. Smolka, editors, 6th International Conference on Concurrency Theory (CONCUR'95, Philadelphia, Pennsylvania, August 1995), volume 962 of Lecture Notes in Computer Science, pages 234-248. Springer-Verlag 1995. .pdf

Abstract

Compositionality is one key aspects of the observational semantics defined on nondeterministic labeled transition systems for the study of concurrency. Recently, randomization has started to play an important role in the development and analysis of concurrent systems, and, although some models that integrate nondeterminism and probability were developed, not much attention was paid to the development of compositional observational semantics for such models. The main problem is that compositionality is not easy to achieve: the interplay between probability and nondeterminism creates subtle and unexpected dependencies between events.

In this paper we tackle the problem by extending the trace semantics for labeled transition systems to a randomized model of concurrent computation. The role of a trace in the randomized model is played by a probability distribution over traces, called a trace distribution. We show that the preorder based on trace distribution inclusion is not a precongruence, and we build an elementary context, called the principal context, that is sufficiently powerful to characterize the coarsest precongruence that is contained in the trace distribution preorder. Finally, we introduce a notion of a probabilistic forward simulation and we prove that it is sound for the trace distribution precongruence. An important characteristic of a probabilistic forward simulation is that it relates states to probability distributions over states.