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