Characterising probabilistic processes logically (extended abstract)

DOI10.1007/978-3-642-16242-8_20MaRDI QIDQ4933311zbMATH OpenOpenAlexFDO

Authors Yuxin Deng, Rob van Glabbeek

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.5188

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Modal logic (including the logic of norms) (03B45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Group-by-group probabilistic bisimilarities and their logical characterizations
• Exploring probabilistic bisimulations. I
• Bisimulation through probabilistic testing
• Characterising Testing Preorders for Finite Probabilistic Processes
• A general framework for probabilistic characterizing formulae

Cited in

(16)

• Probabilistic divide \& congruence: branching bisimilarity
• SOS-based modal decomposition on nondeterministic probabilistic processes
• Probabilistic bisimilarity as testing equivalence
• A spectrum of behavioral relations over LTSs on probability distributions
• Exploring probabilistic bisimulations. I
• Explainability of probabilistic bisimilarity distances for labelled Markov chains
• Group-by-group probabilistic bisimilarities and their logical characterizations
• Logical characterization of bisimulation metrics
• Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
• Logical characterization of branching metrics for nondeterministic probabilistic transition systems
• Characterisations of testing preorders for a finite probabilistic \(\pi\)-calculus
• Raiders of the lost equivalence: probabilistic branching bisimilarity
• Logical characterization of branching bisimilarity over random processes
• Bisimulations for probabilistic and quantum processes (invited paper)
• Logical characterizations of behavioral relations on transition systems of probability distributions
• A general framework for probabilistic characterizing formulae

This page was built for publication: Characterising probabilistic processes logically (extended abstract)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4933311)