Deciding bisimilarity and similarity for probabilistic processes.

DOI10.1006/JCSS.1999.1683zbMath1073.68690OpenAlexW1963619740MaRDI QIDQ1975973

Christel Baier, Bettina Engelen, Mila E. Majster-Cederbaum

Publication date: 2000

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jcss.1999.1683

Mathematics Subject Classification ID

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

Related Items (42)

Weak bisimulations for fuzzy automata ⋮ An Algorithm for Probabilistic Alternating Simulation ⋮ A General Framework for Probabilistic Characterizing Formulae ⋮ A space-efficient simulation algorithm on probabilistic automata ⋮ An efficient algorithm to determine probabilistic bisimulation ⋮ Stochastic equivalence for performance analysis of concurrent systems in dtsiPBC ⋮ Weighted Bisimulation in Linear Algebraic Form ⋮ Comparative branching-time semantics for Markov chains ⋮ Unnamed Item ⋮ Converging from branching to linear metrics on Markov chains ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Computing Behavioral Relations for Probabilistic Concurrent Systems ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ Differential Bisimulation for a Markovian Process Algebra ⋮ A Hemimetric Extension of Simulation for Semi-Markov Decision Processes ⋮ Exploring probabilistic bisimulations. I ⋮ Deciding Simulations on Probabilistic Automata ⋮ On well-founded and recursive coalgebras ⋮ Unnamed Item ⋮ Three-valued abstraction for probabilistic systems ⋮ Discrete time stochastic and deterministic Petri box calculus dtsdPBC ⋮ Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation ⋮ Unnamed Item ⋮ A Space-Efficient Probabilistic Simulation Algorithm ⋮ Verifying quantum communication protocols with ground bisimulation ⋮ Polynomial time decision algorithms for probabilistic automata ⋮ From generic partition refinement to weighted tree automata minimization ⋮ Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation ⋮ Bisimulation relations for weighted automata ⋮ Formal Verification of Differential Privacy for Interactive Systems (Extended Abstract) ⋮ Unnamed Item ⋮ The How and Why of Interactive Markov Chains ⋮ Symbolic computation of differential equivalences ⋮ Deciding probabilistic bisimilarity distance one for probabilistic automata ⋮ Bisimulations Meet PCTL Equivalences for Probabilistic Automata ⋮ Quantitative Abstractions for Collective Adaptive Systems ⋮ Probabilistic weak simulation is decidable in polynomial time ⋮ Efficient Coalgebraic Partition Refinement ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory ⋮ Improved algorithms for computing the greatest right and left invariant Boolean matrices and their application ⋮ Bisimulation and Simulation Relations for Markov Chains ⋮ Automatic verification of real-time systems with discrete probability distributions.

Cites Work

• An implementation of an efficient algorithm for bisimulation equivalence
• Verification of multiprocess probabilistic protocols
• A calculus of communicating systems
• An \(O(IVI^3)\) algorithm for finding maximum flows in networks
• A logic for reasoning about time and reliability
• Processes with probabilities, priority and time
• Testing equivalences for processes
• Axiomatizing probabilistic processes: ACP with generative probabilities
• Generating BDDs for symbolic model checking in CCS
• Model checking of probabilistic and nondeterministic systems
• A Theory of Communicating Sequential Processes
• Three Partition Refinement Algorithms
• Symbolic model checking for probabilistic processes
• Bisimulation for probabilistic transition systems: A coalgebraic approach
• Termination of Probabilistic Concurrent Program
• Testing preorders for probabilistic processes
• Binary Search Trees of Bounded Balance
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Deciding bisimilarity and similarity for probabilistic processes.