A Compositional Trace-Based Semantics for Probabilistic Automata

Appears: Proceedings of the 6th International Conference on Concurrency Theory (CONCUR '95), Philadelphia, PA, USA, LNCS 962, pages 234-248, 1995.

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.

Download:
Download the paper from the publisher.

Download an author-created copy of the paper (© Springer-Verlag).