Scalar Outcomes Suffice for Finitary Probabilistic Testing

Select |




Print


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

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


2007-03-24


Conference Material


16th European Symposium on Programming, ESOP 2007


Braga, Portugal


363-378


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.


LNCS 4421, Springer


Probabilistic processes, nondeterminism, probabilistic automata, testing equivalences, reward testing, hyperplanes, compactness, Markov Decision Processes.


http://www.cse.unsw.edu.au/~rvg/pub/scalar.pdf


0302-9743


nicta:147


Deng, Yuxin; van Glabbeek, Robert; Morgan, Carroll; Zhang, Chenyi. Scalar Outcomes Suffice for Finitary Probabilistic Testing. In: R. De Nicola Editor, editor/s. 16th European Symposium on Programming, ESOP 2007; Braga, Portugal. LNCS 4421, Springer; 2007-03-24. 363-378.



Loading citation data...

Citation counts
(Requires subscription to view)