@inproceedings{b847fa29f59346929574d473ca96e89a,
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.",
author = "Yuxin Deng and {van Glabbeek}, Rob",
year = "2010",
month = oct,
day = "15",
doi = "10.1007/978-3-642-16242-8_20",
language = "English",
isbn = "978-3-642-16241-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "278--293",
editor = "Ferm{\"u}ller, {Christian G.} and Andrei Voronkov",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings",
address = "United Kingdom",
note = "17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010 ; Conference date: 10-10-2010 Through 15-10-2010",
}