de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch
 
Hilfe Wegweiser Impressum Kontakt Einloggen
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization

MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44003

Althaus,  Ernst
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons98354

Beber,  Björn
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44562

Hagemann,  Willem
Automation of Logic, MPI for Informatics, Max Planck Society;
International Max Planck Research School, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45689

Waldmann,  Uwe
Automation of Logic, MPI for Informatics, Max Planck Society;

Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

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.


Zitierlink: http://hdl.handle.net/11858/00-001M-0000-002C-4540-0
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.