Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 DetailsÜbersicht
  Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization

Althaus, E., Beber, B., Damm, W., Disch, S., Hagemann, W., Rakow, A., et al.(2016). Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization (ATR103). SFB/TR 14 AVACS.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-002C-4540-0 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-002D-59E4-9
Genre: Bericht

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
http://www.avacs.org/fileadmin/Publikationen/Open/avacs_technical_report_103.pdf} (beliebiger Volltext)
Beschreibung:
-
OA-Status:

Urheber

einblenden:
ausblenden:
 Urheber:
Althaus, Ernst1, Autor           
Beber, Björn1, Autor           
Damm, Werner2, Autor
Disch, Stefan2, Autor
Hagemann, Willem3, 4, Autor           
Rakow, Astrid2, Autor
Scholl, Christoph2, Autor
Waldmann, Uwe3, Autor           
Wirtz, Boris2, Autor
Affiliations:
1Algorithms and Complexity, MPI for Informatics, Max Planck Society, ou_24019              
2External Organizations, ou_persistent22              
3Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
4International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: This paper provides a suite of optimization techniques for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can -- in contrast to purely functional controller models -- not analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The optimization techniques shown yield consistently a speedup of about 20 against previously published results for a similar benchmark suite, and complement these with new results on counterexample guided abstraction refinement. In combination with the methods guaranteeing preciseness of abstractions, this allows to significantly extend the class of models for which safety can be established, covering in particular models with 23 continuous variables and 2 to the 71 discrete states, 20 continuous variables and 2 to the 199 discrete states, and 9 continuous variables and 2 to the 271 discrete states.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 20162016
 Publikationsstatus: Erschienen
 Seiten: 93 p.
 Ort, Verlag, Ausgabe: SFB/TR 14 AVACS
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: Reportnr.: ATR103
BibTex Citekey: AlthausBeberDammEtAl2016ATR
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: AVACS Technical Report
  Kurztitel : ATR
  Andere : Reports of SFT/TR 14 AVACS
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 103 Artikelnummer: - Start- / Endseite: - Identifikator: ISSN: 1860-9821