Title
Characterising probabilistic processes logically
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 Deng141330.41
Rob J. van Glabbeek21930134.34