@techreport{atr8,
 author      = {Marc Herbstritt and Ralf Wimmer and Thomas Peikenkamp and Eckard B{\"o}de and Michael Adelaide and Sven Johr and Holger Hermanns and Bernd Becker},
 title       = {{Analysis of Large Safety-Critical Systems: A quantitative Approach}},
 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        = {2006},
 month       = {Feb},
 type        = {Reports of SFB/TR 14 AVACS},
 series      = {ATR},
 number      = 8,
 note        = {ISSN: 1860-9821, {\tt http://www.avacs.org}},
 access      = {open},
 abstract    = {
The ever increasing complexity of systems requires combined efforts
with respect to analysis and verification to close the so-called
verification gap. On the modeling side, to face this problem, expressive
high-level methodologies are used to manage system complexity. From the
analysis side it is therefore essential to also start at this level. Due to
powerful symbolic tools -- often based on BDDs -- consistent high-level
representations can be generated. The bottleneck for subsequent
system analysis, however, is still the incredible state space of
such representations. This fact gains even more importance when the
intended analysis is bound to explicit tools, e.g.,~for a quantitative
analysis using stochastic model checking.

In this work, we are bridging the gaps between high-level system descriptions
of safety-critical systems and corresponding explicit state space
representations that can be handled by explicit quantitative analysis tools.
In a first step, our approach safely integrates failure behavior of
safety-critical systems into their high-level description. Then, structural
reductions are applied. Manageable explicit representations are finally
obtained by a novel BDD-based symbolic branching bisimulation algorithm.

We provide experimental data demonstrating the efficiency of our methods:
safety-critical systems whose size seems to be prohibitive for any explicit
analysis tool at the beginning are reduced  by orders of magnitude,
thus paving the way to quantitative analysis without losing relevant
information.
               },
}