@techreport{atr21,
   author = {W. Damm and S. Disch and H. Hungar and S. Jacobs and J. Pang and F. Pigorsch and C. Scholl and U. Waldmann and B. Wirtz},
   title = {Exact State Set Representation in the Verification of Linear Hybrid Systems with Large Discrete State Space},
   editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard Wilhelm},
   institution = {SFB/TR 14 AVACS},
   subproject = {H3},
   year = {2007},
   month = {June},
   type = {Reports of SFB/TR 14 AVACS},
   series = {ATR},
   number = 21,
   note = {ISSN: 1860-9821, http://www.avacs.org.},
   access        = {open},
   abstract =     {We propose algorithms significantly extending the
limits for maintaining exact representations in the verification of
linear hybrid systems with large discrete state spaces. We use
AND-Inverter Graphs (AIGs) extended with linear constraints ({\Laig}s)
as symbolic representation of the hybrid state space, and show how
methods for maintaining compactness of AIGs can be lifted to support
model-checking of linear hybrid systems with large discrete state
spaces. This builds on a novel approach for eliminating sets of
redundant constraints in such rich hybrid state representations by a
suitable exploitation of the capabilities of SMT solvers, which is of
independent value beyond the application context studied in this paper.
We used a benchmark derived from an Airbus flap control system
(containing $2^{20}$ discrete states) to demonstrate the relevance of
the approach.},
  bibtex        = {atr021.bib},
  pdf           = {avacs_technical_report_021.pdf}
}