Characterising Probabilistic Processes Logically

Yuxin Deng, Rob van Glabbeek

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010, Proceedings
EditorsChristian G. Fermüller, Andrei Voronkov
Place of PublicationBerlin, Heidelberg
PublisherSpringer
Pages278-293
Number of pages16
ISBN (Electronic)978-3-642-16242-8
ISBN (Print)978-3-642-16241-1
DOIs
Publication statusPublished - 15 Oct 2010
Event17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010 - Yogyakarta, Indonesia
Duration: 10 Oct 201015 Oct 2010

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin, Heidelberg
Volume6397
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010
Country/TerritoryIndonesia
CityYogyakarta
Period10/10/1015/10/10

Fingerprint

Dive into the research topics of 'Characterising Probabilistic Processes Logically'. Together they form a unique fingerprint.

Cite this