Bisimulations Meet PCTL Equivalences for Probabilistic Automata

DOI10.1007/978-3-642-23217-6_8zbMath1344.68170OpenAlexW2103972329MaRDI QIDQ3090825

Lei Song, Jens Chr. Godskesen, Li-jun Zhang

Publication date: 2 September 2011

Published in: CONCUR 2011 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-23217-6_8

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (3)

A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ Relating strong behavioral equivalences for processes with nondeterminism and probabilities ⋮ Group-by-Group Probabilistic Bisimilarities and Their Logical Characterizations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Probabilistic logical characterization
• Bisimulation through probabilistic testing
• A logic for reasoning about time and reliability
• Deciding bisimilarity and similarity for probabilistic processes.
• Weak bisimulation is sound and complete for pCTL\(^*\)
• Comparative branching-time semantics for Markov chains
• Model checking of probabilistic and nondeterministic systems
• A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains
• Game Refinement Relations and Metrics
• Algebraic laws for nondeterminism and concurrency
• Branching time and abstraction in bisimulation semantics
• Bisimulations Meet PCTL Equivalences for Probabilistic Automata
• Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking

This page was built for publication: Bisimulations Meet PCTL Equivalences for Probabilistic Automata