Testing Probabilistic Automata

Appears: Proceedings of the 7th International Conference on Concurrency Theory (CONCUR '96), Pisa, Italy, LNCS 1119, pages 299--314, 1996.

Abstract: We study testing preorders for probabilistic automata and we characterize them in terms of relations that are based on inclusion of trace and failure distributions, i.e., probability distributions over failures and traces that can arise in a probabilistic computation. The novelty of our approach to testing is the use of multiple success actions rather than a single action. This allows us to observe the relative probabilities of different traces within a computation.

We define and characterize two kinds of testing preorders: preorders sensitive to infinite traces, and preorders sensitive to finite traces only. The second kind of preorder is an extension to the probabilistic framework of the testing preorders of De Nicola and Hennessy. We show that under assumptions of finite branching and strong convergence the two kinds of preorders coincide.

Download the paper from the publisher.

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