Weak bisimulation is sound and complete for pCTL^*

DOI10.1016/J.IC.2009.11.002MaRDI QIDQ2266992zbMATH OpenOpenAlexFDO

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

Publication date 26 February 2010

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2009.11.002

zbMATH Keywords

image finiteness'

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*
• Probabilistic Bisimulation: Naturally on Distributions
• Weak bisimulation for probabilistic systems
• Notes on generative probabilistic bisimulation
• Bisimulation for labelled Markov processes

Cites work

• Algebraic laws for nondeterminism and concurrency
• An algorithm for quantitive verification of probabilistic transition systems
• Axiomatizations for probabilistic bisimulation
• Bisimulation for labelled Markov processes
• Bisimulation metrics for continuous Markov decision processes
• Bisimulation through probabilistic testing
• Continuous Capacities on Continuous State Spaces
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Finite Continuous Time Markov Chains
• Full abstraction for a shared-variable parallel language
• Fully abstract denotational models for nonuniform concurrent languages
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• scientific article; zbMATH DE number 3223983 (Why is no real title available?)
• scientific article; zbMATH DE number 3228101 (Why is no real title available?)
• scientific article; zbMATH DE number 3390061 (Why is no real title available?)
• Logical Characterizations of Bisimulations for Discrete Probabilistic Systems
• Metrics for labeled Markov systems
• Probability and Nondeterminism in Operational Models of Concurrency
• Theory of capacities
• Weak bisimulation for probabilistic systems
• Weak bisimulation is sound and complete for pCTL*

Cited in

(15)

• Probabilistic bisimulation for realistic schedulers
• On the probabilistic bisimulation spectrum with silent moves
• Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes
• A space-efficient simulation algorithm on probabilistic automata
• A general framework for probabilistic characterizing formulae
• On the semantics of Markov automata
• Bisimulations meet PCTL equivalences for probabilistic automata
• A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences
• Weak bisimulation is sound and complete for pCTL*
• Probabilistic bisimulation for realistic schedulers
• Bisimulations meet PCTL equivalences for probabilistic automata
• A semantics for every GSPN
• Sound approximate and asymptotic probabilistic bisimulations for PCTL
• A spectrum of approximate probabilistic bisimulations
• Trace semantics for stochastic systems with nondeterminism

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 Q2266992)