Shanghai Jiao Tong University
NICTA
UNSW
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.
@inproceedings{Deng_Glabbeek_10, address = {Yogyakarta, Indonesia}, author = {Deng, Yuxin and van Glabbeek, Robert}, booktitle = {Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning}, editor = {{Christian Ferm\"uller \& Andrei Voronkov}}, issn = {0302-9743}, keywords = {concurreny, probabilistic processes, modal mu-calculus, simulation, bisimulation, characteristic formulae}, month = oct, pages = {278--293}, paperurl = {https://trustworthy.systems/publications/nicta_full_text/784.pdf}, publisher = {Springer}, title = {Characterising Probabilistic Processes Logically (Extended Abstract)}, year = {2010} }