Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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

URL of the conference:

http://lcs.ios.ac.cn/~atva06/

URL for downloading the paper:

http://www.springerlink.com/content/9026r9668h3kr772/fulltext.pdf

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, Germany

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; 978-3-540-47237-7

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.

URL for the Abstract:

http://www.springerlink.com/content/9026r9668h3kr772/

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

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort



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},
; ISBN = {978-3-540-47237-7},
}


Entry last modified by Christine Kiesel, 03/06/2007
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
11/07/2006 11:46:09 AM
Revisions
2.
1.
0.

Editor(s)
Christine Kiesel
Christine Kiesel
Uwe Waldmann

Edit Dates
06.03.2007 14:16:50
06.03.2007 14:13:26
26.10.2006 21:53:14

Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section