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. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1007/978-3-642-16242-8_20 | international conference on logic programming |
Keywords | DocType | Volume |
fixpoint operator,characterising probabilistic,finite-state process,probabilistic mu-calculus,various simulation-like preorders,behavioural relation,modal mu-calculus,probabilistic extension,simulation semantics,probabilistic behaviour,characteristic formula | Journal | abs/1007.5188 |
Issue | ISSN | ISBN |
null | 0302-9743 | 3-642-16241-X |
Citations | PageRank | References |
7 | 0.46 | 25 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Yuxin Deng | 1 | 413 | 30.41 |
Rob J. van Glabbeek | 2 | 1930 | 134.34 |