An efficient algorithm to determine probabilistic bisimulation
Summary: We provide an algorithm to efficiently compute bisimulation for probabilistic labeled transition systems, featuring non-deterministic choice as well as discrete probabilistic choice. The algorithm is linear in the number of transitions and logarithmic in the number of states, distinguishing both action states and probabilistic states, and the transitions between them. The algorithm improves upon the proposed complexity bounds of the best algorithm addressing the same purpose so far by \textit{C. Baier} et al. [J. Comput. Syst. Sci. 60, No. 1, 187--231 (2000; Zbl 1073.68690)]. In addition, experimentally, on various benchmarks, our algorithm performs rather well; even on relatively small transition systems, a performance gain of a factor 10,000 can be achieved.
- Deciding bisimilarity and similarity for probabilistic processes.
- Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation
- Probabilistic bisimulation and simulation algorithms by abstract interpretation
- scientific article; zbMATH DE number 1927574
- An efficient algorithm for computing bisimulation equivalence
- A logic for reasoning about time and reliability
- A space-efficient simulation algorithm on probabilistic automata
- An O(m n) algorithm for computing stuttering equivalence and branching bisimulation
- An overview of the mCRL2 toolset and its recent advances
- Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Bisimulation through probabilistic testing
- CCS expressions, finite state processes, and three problems of equivalence
- Deciding bisimilarity and similarity for probabilistic processes.
- Exploring probabilistic bisimulations. I
- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
- scientific article; zbMATH DE number 1927574 (Why is no real title available?)
- scientific article; zbMATH DE number 1754605 (Why is no real title available?)
- Modeling and analysis of communicating systems
- Optimal state-space lumping in Markov chains
- Polynomial time decision algorithms for probabilistic automata
- Problem solving using process algebra considered insightful
- Simple O(m n) time Markov chain lumping
- Simple bisimilarity minimization in O(m n) time
- SMT-based bisimulation minimisation of Markov models
- Stochastic model checking
- Three Partition Refinement Algorithms
- Deciding bisimilarity and similarity for probabilistic processes.
- From generic partition refinement to weighted tree automata minimization
- Probabilistic bisimulation and simulation algorithms by abstract interpretation
- A Space-Efficient Probabilistic Simulation Algorithm
- scientific article; zbMATH DE number 1927574 (Why is no real title available?)
- Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation
- scientific article; zbMATH DE number 7559464 (Why is no real title available?)
- Efficient and modular coalgebraic partition refinement
- Lowerbounds for Bisimulation by Partition Refinement
- Equivalence checking 40 years after: a review of bisimulation tools
- Generic partition refinement and weighted tree automata
- Explicit Hopcroft's trick in categorical partition refinement
- A cancellation law for probabilistic processes
- An implementation of an efficient algorithm for bisimulation equivalence
This page was built for publication: An efficient algorithm to determine probabilistic bisimulation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2633253)
