Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse
  1. Datensatz Übersicht / 
  2. Datensatz ansehen

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 DetailsÜbersicht
  Automatic Verification of Hybrid Systems with Large Discrete State Space

Damm, W., Disch, S., Hungar, H., Pang, J., Pigorsch, F., Scholl, C., et al. (2006). Automatic Verification of Hybrid Systems with Large Discrete State Space. In S. Graf, & W. Zhang (Eds.), Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006 (pp. 276-291). Berlin, Germany: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-24BC-6 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-24BE-2
Genre: Konferenzbeitrag

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Damm, Werner, Autor
Disch, Stefan, Autor
Hungar, Hardi, Autor
Pang, Jun, Autor
Pigorsch, Florian, Autor
Scholl, Christoph, Autor
Waldmann, Uwe1, 2, Autor           
Wirtz, Boris, Autor
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2007-03-062006
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 521689
URI: http://www.springerlink.com/content/9026r9668h3kr772/fulltext.pdf
Anderer: Local-ID: C125716C0050FB51-2725E3E72B06EB08C125721F003B2848-DammDischHungarPangPigorschSchollWaldmannWirtz2006
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Beijing, China
Start-/Enddatum: 2006-10-23 - 2006-10-26

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006
Genre der Quelle: Konferenzband
 Urheber:
Graf, Susanne, Herausgeber
Zhang, Wenhui, Herausgeber
Affiliations:
-
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 276 - 291 Identifikator: ISBN: 3-540-47237-1

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Computer Science
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 4218 Artikelnummer: - Start- / Endseite: - Identifikator: -