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

URL of the conference:


URL for downloading the paper:


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
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
12/07/2007 01:31:51 PM
Revision
0.



Editor
Uwe Waldmann



Edit Date
07.12.2007 13:31:51



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