MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Damm, Werner
Disch, Stefan
Hungar, Hardi
Jacobs, Swen
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris
dblp
dblp
dblp
dblp
dblp
dblp
dblp
dblp
dblp
Not MPG Author(s):
Damm, Werner
Disch, Stefan
Hungar, Hardi
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Wirtz, Boris
Editor(s):
Namjoshi, Kedar S.
Yoneda, Tomohiro
Higashino, Teruo
Okamura, Yoshio
dblp
dblp
dblp
dblp
Not MPII Editor(s):
Namjoshi, Kedar S.
Yoneda, Tomohiro
Higashino, Teruo
Okamura, Yoshio
BibTeX cite key*:
DammDischHungarJacobsPangPigorschSchollWaldmannWirtz2007
Title, Booktitle
Title*:
Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space
Booktitle*:
Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Tokyo, Japan
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
22 October 2007
Event End Date:
25 October 2007
Publisher
Name*:
Springer
URL:
http://www.springer.de
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
4762
Number:
Month:
Pages:
425-440
Year*:
2007
VG Wort Pages:
30
ISBN/ISSN:
3-540-75595-1
Sequence Number:
DOI:
10.1007/978-3-540-75596-8_30
Note, Abstract, ©
(LaTeX) 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
(LinAIGs) 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.
Keywords:
First-Order Model Checking, AND-Inverter Graphs, Hybrid Systems
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Automation of Logic
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{DammDischHungarJacobsPangPigorschSchollWaldmannWirtz2007,
AUTHOR = {Damm, Werner and Disch, Stefan and Hungar, Hardi and Jacobs, Swen and Pang, Jun and Pigorsch, Florian and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
EDITOR = {Namjoshi, Kedar S. and Yoneda, Tomohiro and Higashino, Teruo and Okamura, Yoshio},
TITLE = {Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space},
BOOKTITLE = {Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007},
PUBLISHER = {Springer},
YEAR = {2007},
VOLUME = {4762},
PAGES = {425--440},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Tokyo, Japan},
ISBN = {3-540-75595-1},
DOI = {10.1007/978-3-540-75596-8_30},
}


Entry last modified by Uwe Waldmann, 02/28/2008
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Waldmann
Created
12/07/2007 01:31:51 PM
Revision
0.



Editor
Uwe Waldmann



Edit Date
07.12.2007 13:31:51