Trustworthy Systems

Scalar outcomes suffice for finitary probabilistic testing

Authors

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

UNSW\ NICTA

Abstract

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

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

Download