Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

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

Action:

login to update

Options:




Library Locked Library locked




Author, Editor(s)

Author(s):

Damm, Werner
Dierks, Henning
Disch, Stefan
Hagemann, Willem
Pigorsch, Florian
Scholl, Christoph
Waldmann, Uwe
Wirtz, Boris

dblp
dblp
dblp
dblp
dblp
dblp
dblp
dblp

Not MPG Author(s):

Damm, Werner
Dierks, Henning
Disch, Stefan
Pigorsch, Florian
Scholl, Christoph
Wirtz, Boris

BibTeX cite key*:

DammDierksDischEtAl2012

Title

Title*:

Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces

Journal

Journal Title*:

Science of Computer Programming

Journal's URL:

http://www.journals.elsevier.com/science-of-computer-programming/

Download URL
for the article:

http://www.sciencedirect.com/science/article/pii/S0167642311001523

Language:

English

Publisher

Publisher's
Name:

Elsevier

Publisher's URL:


Publisher's
Address:

Amsterdam

ISSN:

0167-6423

Vol, No, pp, Date

Volume*:

77

Number:

10-11

Publishing Date:

September 2012

Pages*:

1122-1150

Number of
VG Pages:

72

Page Start:

1122

Page End:

1150

Sequence Number:


DOI:

10.1016/j.scico.2011.07.006

Note, Abstract, ©

Note:


(LaTeX) Abstract:

We propose an improved symbolic algorithm for the
verification of linear hybrid automata with large
discrete state spaces (where an explicit
representation of discrete states is difficult).
Here both the discrete part and the continuous
part of the hybrid state space are represented by
one symbolic representation called LinAIGs.
LinAIGs represent (possibly non-convex) polyhedra
extended by Boolean variables. Key components of
our method for state space traversal are
redundancy elimination and constraint
minimization: redundancy elimination eliminates
so-called redundant linear constraints from LinAIG
representations by a suitable exploitation of the
capabilities of SMT (Satisfiability Modulo
Theories) solvers. Constraint minimization
optimizes polyhedra by exploiting the fact that
states already reached in previous steps can be
interpreted as "don't cares" in the current step.
Experimental results (including comparisons to the
state-of-the-art model checkers PHAVer and RED)
demonstrate the advantages of our approach.

URL for the Abstract:


Categories,
Keywords:

Verification, Model Checking, Hybrid Systems

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Internal

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, VG Wort


BibTeX Entry:

@ARTICLE{DammDierksDischEtAl2012,
AUTHOR = {Damm, Werner and Dierks, Henning and Disch, Stefan and Hagemann, Willem and Pigorsch, Florian and Scholl, Christoph and Waldmann, Uwe and Wirtz, Boris},
TITLE = {Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces},
JOURNAL = {Science of Computer Programming},
PUBLISHER = {Elsevier},
YEAR = {2012},
NUMBER = {10-11},
VOLUME = {77},
PAGES = {1122--1150},
ADDRESS = {Amsterdam},
MONTH = {September},
ISBN = {0167-6423},
DOI = {10.1016/j.scico.2011.07.006},
}


Entry last modified by Anja Becker, 03/07/2013
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)
[Library]
Created
12/10/2012 06:04:54 PM
Revision
1.
0.


Editor
Anja Becker
Uwe Waldmann


Edit Date
07.03.2013 13:29:04
10.12.2012 18:04:54