Skip to main content


Scalar outcomes suffice for finitary probabilistic testing


Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang




The question of equivalence has long vexed research in concurrency, leading to many different denotational- and bisimulation-based approaches; a breakthrough occurred with the insight that tests expressed within the concurrent framework itself, based on a special ``success action'', yield equivalences that make only inarguable distinctions.

When probability was added, however, it seemed necessary to extend the testing framework beyond a direct probabilistic generalisation in order to remain useful. An attractive possibility was the extension to multiple success actions that yielded vectors of real-valued outcomes.

Here we prove that such vectors are unnecessary when processes are finitary, that is finitely branching and finite-state: single scalar outcomes are just as powerful. Thus for finitary processes we can retain the original, simpler testing approach and its direct connections to other naturally scalar-valued phenomena.

BibTeX Entry

    publisher        = {Lecture Notes in Computer Science},
    author           = {Deng, Yuxin and van Glabbeek, Robert and Morgan, Carroll and Zhang, Chenyi},
    issn             = {0302-9743},
    month            = mar,
    editor           = {{R. De Nicola}},
    year             = {2007},
    keywords         = {probabilistic processes, nondeterminism, probabilistic automata, testing equivalences, reward
                        testing, hyperplanes, compactness, markov decision processes.},
    title            = {Scalar Outcomes Suffice for Finitary Probabilistic Testing},
    booktitle        = {16th European Symposium on Programming, ESOP 2007},
    pages            = {363-378},
    address          = {Braga, Portugal}