Weak bisimulation is sound and complete for pCTL\(^*\)

DOI10.1016/j.ic.2009.11.002zbMath1189.68080MaRDI QIDQ2266992

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

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

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

Related Items

A Semantics for Every GSPN, A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences, Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes, A General Framework for Probabilistic Characterizing Formulae, On the Semantics of Markov Automata, Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Bisimulation through probabilistic testing
• Fully abstract denotational models for nonuniform concurrent languages
• Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes.
• Full abstraction for a shared-variable parallel language
• Bisimulation for labelled Markov processes
• Theory of capacities
• Bisimulation Metrics for Continuous Markov Decision Processes
• Algebraic laws for nondeterminism and concurrency
• Finite Continuous Time Markov Chains
• Continuous Capacities on Continuous State Spaces
• Probability and Nondeterminism in Operational Models of Concurrency
• Logical Characterizations of Bisimulations for Discrete Probabilistic Systems