@techreport{atr16,
 author      = {Ralf Wimmer and Holger Hermanns 
                            and Marc Herbstritt 
			    and Bernd Becker},
 title       = {{Towards Symbolic Stochastic Aggregation}},
 editor      = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle 
	                     and Ernst-R{\"u}diger Olderog 
  	                     and Andreas Podelski 
	                     and Reinhard Wilhelm},
 subproject  = {S3},
 year        = {2007},
 month       = aug,
 type        = {Reports of SFB/TR 14 AVACS},
 series      = {ATR},
 number      = 16,
 note        = {ISSN: 1860-9821, {\tt http://www.avacs.org}},
 access      = {open},
 abstract    = {
  Bisimulations are one of the classical means to fight
  the state explosion problem. Especially in combination
  with symbolic methods, like BDD-based data representation
  and algorithms that exploit the compact BDD representation,
  they enable the minimization of very large state spaces without
  losing relevant properties.

  In this report, we show how a symbolic algorithm,
  that was originally developed for non-stochastic 
  systems, can be extended to compute strong and
  branching bisimulations on interactive Markov chains (IMCs).
  An IMC is a very general model that combines the stochastic
  behavior of traditional Markov chains with action-labeled
  transition systems. To the best of our knowledge,
  our suggested algorithm is the first symbolic algorithm for 
  both stochastic \emph{strong} bisimulation and stochastic 
  \emph{branching} bisimulation on IMCs.
               },
}