We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation.\parWe provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.

References in zbMATH (referenced in 12 articles , 1 standard article )

Showing results 1 to 12 of 12.
Sorted by year (citations)

  1. Boulgakov, Alexandre; Gibson-Robinson, Thomas; Roscoe, A.W.: Computing maximal weak and other bisimulations (2016)
  2. Noll, Thomas: Safety, dependability and performance analysis of aerospace systems (2015)
  3. Turrini, Andrea; Hermanns, Holger: Polynomial time decision algorithms for probabilistic automata (2015)
  4. Yatapanage, Nisansala; Winter, Kirsten: Next-preserving branching bisimulation (2015)
  5. Turrini, Andrea; Hermanns, Holger: Cost preserving bisimulations for probabilistic automata (2014)
  6. Dehnert, Christian; Katoen, Joost-Pieter; Parker, David: SMT-based bisimulation minimisation of Markov models (2013)
  7. Hermanns, Holger; Katoen, Joost-Pieter: The how and why of interactive Markov chains (2010)
  8. Böde, Eckard; Peikenkamp, Thomas; Rakow, Jan; Wischmeyer, Samuel: Model based importance analysis for minimal cut sets (2008)
  9. Derisavi, Salem: A symbolic algorithm for optimal Markov chain lumping (2007)
  10. Katoen, Joost-Pieter; Kemna, Tim; Zapreev, Ivan; Jansen, David N.: Bisimulation minimisation mostly speeds up probabilistic model checking (2007)
  11. Katoen, Joost-Pieter; Klink, Daniel; Leucker, Martin; Wolf, Verena: Three-valued abstraction for continuous-time Markov chains (2007)
  12. Wimmer, Ralf; Herbstritt, Marc; Hermanns, Holger; Strampp, Kelley; Becker, Bernd: SIGREF -- a symbolic bisimulation tool box (2006)

Further publications can be found at: