MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Damm, Werner
Disch, Stefan
Hungar, Hardi
Pang, Jun
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris		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):
Graf, Susanne
Zhang, Wenhui		dblp
dblp
Not MPII Editor(s):
Graf, Susanne
Zhang, Wenhui
BibTeX cite key*:
DammDischHungarPangPigorschSchollWaldmannWirtz2006
Title, Booktitle
Title*:
Automatic Verification of Hybrid Systems with Large Discrete State Space
Booktitle*:
Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006
Event, URLs
Conference URL::
http://lcs.ios.ac.cn/~atva06/
Downloading URL:
Event Address*:
Beijing, China
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
23 October 2006
Event End Date:
26 October 2006
Publisher
Name*:
Springer
URL:
http://www.springer.com/
Address*:
Berlin
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
4218
Number:
Month:
Pages:
276-291
Year*:
2006
VG Wort Pages:
31
ISBN/ISSN:
3-540-47237-1
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We address the problem of model checking hybrid systems which
exhibit nontrivial discrete behavior and thus cannot be
treated by considering the discrete states one by one, as most
currently available verification tools do. Our procedure
relies on a deep integration of several techniques and tools.
An extension of AND-Inverter-Graphs (AIGs) with first-order
constraints serves as a compact representation format for sets
of configurations which are composed of continuous regions and
discrete states. Boolean reasoning on the AIGs is complemented
by firstorder reasoning in various forms and on various
levels. These include implication checks for simple
constraints, test vector generation for fast inequality checks
of boolean combinations of constraints, and an exact
subsumption check for representations of two
configurations.\par
These techniques are integrated within a model checker for
universal CTL. Technically, it deals with discrete-time hybrid
systems with linear differentials. The paper presents the
approach, its prototype implementation, and first experimental
data.
Keywords:
model checking, discrete-time hybrid systems, FO-AIG
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, CCL bibliography



BibTeX Entry:
@INPROCEEDINGS{DammDischHungarPangPigorschSchollWaldmannWirtz2006,
AUTHOR = {Damm, Werner and Disch, Stefan and Hungar, Hardi and Pang, Jun and Pigorsch, Florian and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
 EDITOR = {Graf, Susanne and Zhang, Wenhui},
 TITLE = {Automatic Verification of Hybrid Systems with Large Discrete State Space},
 BOOKTITLE = {Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006},
 PUBLISHER = {Springer},
 YEAR = {2006},
 VOLUME = {4218},
 PAGES = {276--291},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Beijing, China},
 ISBN = {3-540-47237-1},
}

Entry last modified by Uwe Waldmann, 10/26/2006
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
10/26/2006 09:53:14 PM
Revision
0.



Editor
Uwe Waldmann



Edit Date
26.10.2006 21:53:14