Weak bisimulation is sound and complete for pCTL*

DOI10.1007/3-540-45694-5_24MaRDI QIDQ4484498zbMATH OpenFDO

Authors Josée Desharnais, Vineet Gupta, Radha Jagadeesan, Prakash Panangaden

Publication date 12 June 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2421/24210355.htm

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Weak bisimulation is sound and complete for pCTL\(^*\)
• Weak bisimulation for probabilistic systems
• Bisimulations meet PCTL equivalences for probabilistic automata
• Bisimulation for labelled Markov processes
• Exploring probabilistic bisimulations. I

Cited in

(21)

• SOS specifications for uniformly continuous operators
• Probabilistic divide \& congruence: branching bisimilarity
• Weak bisimulation is sound and complete for pCTL\(^*\)
• Comparative branching-time semantics for Markov chains
• Branching bisimulation for probabilistic systems: characteristics and decidability
• Logical characterizations of behavioral relations on transition systems of probability distributions
• Compositional bisimulation metric reasoning with Probabilistic Process Calculi
• A spectrum of behavioral relations over LTSs on probability distributions
• Testing Finitary Probabilistic Processes
• Quantifying Vulnerability of Secret Generation Using Hyper-Distributions
• A pseudometric in supervisory control of probabilistic discrete event systems
• On Compositionality, Efficiency, and Applicability of Abstraction in Probabilistic Systems
• Deciding probabilistic bisimilarity distance one for probabilistic automata
• Separable GPL: decidable model checking with more non-determinism
• Monads and Quantitative Equational Theories for Nondeterminism and Probability
• Compositional weak metrics for group key update
• Bisimulation and Simulation Relations for Markov Chains
• Explainability of probabilistic bisimilarity distances for labelled Markov chains
• Partial order reduction for probabilistic branching time
• Branching bisimulation congruence for probabilistic systems
• Parametric probabilistic transition systems for system design and analysis

This page was built for publication: Weak bisimulation is sound and complete for pCTL*

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