Trustworthy Systems

Characterising probabilistic processes logically (extended abstract)

Authors

Yuxin Deng and Rob van Glabbeek

Shanghai Jiao Tong University

NICTA

UNSW

Abstract

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.

BibTeX Entry

  @inproceedings{Deng_Glabbeek_10,
    address          = {Yogyakarta, Indonesia},
    author           = {Deng, Yuxin and van Glabbeek, Robert},
    booktitle        = {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}
  }

Download