**Author:** N. Lynch,
R. Segala,
F. Vaandrager
**Appears:** *SIAM Journal on Computing*, 37(4), pages 977-1013,
2007.

**Also:** This paper extends [LSV03].

**Abstract:**
Probabilistic automata (PAs) constitute a general framework for modeling and analyzing
discrete event systems that exhibit both nondeterministic and probabilistic behavior, such as
distributed algorithms and network protocols. The behavior of PAs is commonly defined using
schedulers (also called adversaries or strategies), which resolve all nondeterministic choices based
on past history. From the resulting purely probabilistic structures, trace distributions can be
extracted, whose intent is to capture the observable behavior of a PA. However, when PAs
are composed via an (asynchronous) parallel composition operator, a global scheduler may
establish strong correlations between the behavior of system components and, for example,
resolve nondeterministic choices in one PA based on the outcome of probabilistic choices in the
other. It is well known that, as a result of this, the (linear-time) trace distribution precongruence
is not compositional for PAs. In his PhD thesis from ’95, Segala has shown that the (branchingtime)
probabilistic simulation preorder is compositional for PAs. In this paper, we establish
that the simulation preorder is in fact the coarsest refinement of the trace distribution preorder
that is compositional.

We prove our characterization result by providing (1) a context of a given PA A, called
the tester, that may announce the state of A to the outside world, and (2) a specific global
scheduler, called the observer, which ensures that the state information that is announced is
actually correct. Now when another PA B is composed with the tester, it may generate the same
external behavior as the observer only when it is able to simulate A in the sense that whenever
A goes to some state s, B can go to a corresponding state u from which it may generate the same
external behavior. Our result shows that probabilistic contexts together with global schedulers
are able to exhibit the branching structure of PAs.

**Download:**

Download the paper from the publisher.

Download an author-created copy
of the paper.