Probability and Nondeterminism
- 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).
- Collaboration: Shanghai Jiao Tong University, Trinity College Dublin.
People
Past
|
Publications
2019
|
 |
Carroll Morgan, Annabelle McIver and Tahiry Rabehaja Abstract hidden markov models: A monadic account of quantitative information flow Mathematical Structures in Computer Science, Volume 15, Issue 1, pp. 36:1-36:50, March, 2019 |
|
|
|
Nick Fischer and Rob van Glabbeek Axiomatising infinitary probabilistic weak bisimilarity of finite-state behaviours Journal of Logical and Algebraic Methods in Programming, Volume 102, pp. 64-102, January, 2019 |
2018
|
|
|
Annabelle McIver, Carroll Morgan, Benjamin Kaminski and Joost-Pieter Katoen A new proof rule for almost-sure termination ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, January, 2018 |
2014
|
|
|
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
|
|
|
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
|
|
|
Yuxin Deng and Rob van Glabbeek Characterising probabilistic processes logically (extended abstract) International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 278–293, Yogyakarta, Indonesia, October, 2010 |
2009
|
|
|
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy and Carroll Morgan Testing finitary probabilistic processes (extended abstract) International Conference on Concurrency Theory (CONCUR), pp. 274–288, Bologna, Italy, August, 2009 |
2008
|
|
|
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
|
|
|
Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, Carroll Morgan and Cuicui Zhang Characterising testing preorders for finite probabilistic processes Annual IEEE Symposium on Logic in Computer Science, pp. 313–322, Wroclaw, Poland, July, 2007 |
|
|
|
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 |
|
|
|
Yuxin Deng, Rob van Glabbeek, Carroll Morgan and Chenyi Zhang Scalar outcomes suffice for finitary probabilistic testing European Symposium on Programming, pp. 363–378, Braga, Portugal, March, 2007 |