Bisimulations Meet PCTL Equivalences for Probabilistic Automata

DOI10.1007/978-3-642-23217-6_8zbMath1344.68170MaRDI 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

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

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

03B44: Temporal logic

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Related Items

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