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

DOI10.1016/J.IC.2009.11.002zbMath1189.68080OpenAlexW2056928795MaRDI QIDQ2266992

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

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)

Related Items (11)

A General Framework for Probabilistic Characterizing Formulae ⋮ A space-efficient simulation algorithm on probabilistic automata ⋮ A Semantics for Every GSPN ⋮ Probabilistic bisimulation for realistic schedulers ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ On the probabilistic bisimulation spectrum with silent moves ⋮ Sound approximate and asymptotic probabilistic bisimulations for PCTL ⋮ On the Semantics of Markov Automata ⋮ Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes ⋮ Probabilistic Bisimulation for Realistic Schedulers ⋮ Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Weak bisimulation is sound and complete for pCTL\(^*\)