## A Compositional Trace-Based Semantics for Probabilistic AutomataAuthor: Roberto Segala
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 an author-created copy of the paper (© Springer-Verlag).
homepage |