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

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

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