Skip to main content

Probability and Nondeterminism

Probability and Nondeterminism

Separating hyperplane
  • Aim: The goal of this project is to build a theory of processes that faithfully integrates probabilities and nondeterminism.
  • Context: A satisfactory semantic theory for processes which encompass both nondeterministic and probabilistic behaviour has been a long-standing research problem. Such a theory is indispensable for the successful modelling, analysis and verification of systems where the interplay of probability and nondeterminism plays an essential role.
           In 1992 Wang & Larsen posed the problems of finding complete axiomatisations and alternative characterisations for a natural generalisation of the standard testing preorders to such processes. Recently, we solved both for finite processes, by providing a detailed account of both may- and must testing preorders for a finite version of the process calculus CSP extended with probabilistic choice. Further work deals with infinite processes, and generalisations to other testing disciplines, such as reward testing.
  • Approach: We bring together techniques from process algebra, Markov decision processes and Euclidean geometry (e.g. separating hyperplane lemmas). Probabilistic automaton
  • Collaboration: University of New South Wales, Shanghai Jiao Tong University, Trinity College Dublin.

People


Publications

2014

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Real reward testing for probabilistic processes
Theoretical Computer Science, Volume 538, pp. 16-36, July, 2014

2011

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Real reward testing for probabilistic processes (extended abstract)
Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL 2011), pp. 61-73, Saarbr├╝cken, Germany, July, 2011

2010

Abstract PDF Yuxin Deng and Rob van Glabbeek
Characterising probabilistic processes logically (extended abstract)
Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 278-293, Yogyakarta, Indonesia, October, 2010

2009

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Testing finitary probabilistic processes (extended abstract)
20th International Conference on Concurrency Theory (CONCUR 2009), pp. 274-288, Bologna, Italy, August, 2009

2008

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan
Characterising testing preorders for finite probabilistic processes
Logical Methods in Computer Science, Volume 4, Number 4, pp. 1-33, October, 2008

2007

Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang
Characterising testing preorders for finite probabilistic processes
22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 313-322, Wroclaw, Poland, July, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang
Remarks on testing probabilistic processes
Electronic Notes in Theoretical Computer Science, Volume 172, Number , pp. 359-397, April, 2007
Abstract PDF Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang
Scalar outcomes suffice for finitary probabilistic testing
16th European Symposium on Programming, ESOP 2007, pp. 363-378, Braga, Portugal, March, 2007

Contact

Rob van Glabbeek, Robert.van Glabbeek <at> data61.csiro.au
Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.