Characterising Probabilistic Processes Logically (Extended Abstract)

Select |


Deng, Yuxin; van Glabbeek, Robert

Deng, Yuxin; van Glabbeek, Robert


Conference Material

17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning

Yogyakarta, Indonesia


In this paper we work on (bi)simulation semantics of processes that exhibit both nondeterministic and probabilistic behaviour. We propose a probabilistic extension of the modal mu-calculus and show how to derive characteristic formulae for various simulation-like preorders over finite-state processes without divergence. In addition, we show that even without the fixpoint operators this probabilistic mu-calculus can be used to characterise these behavioural relations in the sense that two states are equivalent if and only if they satisfy the same set of formulae.


Concurreny, Probabilistic Processes, Modal mu-calculus, simulation, bisimulation, characteristic formulae

The Author may self-archive an author-created version of his Contribution on his own website and his institution's repository, including his final version; however he may not use the publisher's PDF version which is posted on, LNCS online. Furthermore, the author may only post his version provided acknowledgement is given to the original source of publication and a link is inserted to the published article on Springer-Verlag's website. The link must be accompanied by the following text: "The original publication is available at".



Deng, Yuxin; van Glabbeek, Robert. Characterising Probabilistic Processes Logically (Extended Abstract). In: Christian Fermüller & Andrei Voronkov Editor, editor/s. 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning; Yogyakarta, Indonesia. Springer; 2010-10-10. 278-293.

Loading citation data...

Citation counts
(Requires subscription to view)