Weak bisimulation is sound and complete for pCTL\(^*\)
From MaRDI portal
Publication:2266992
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
Related Items
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
