English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  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

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Althaus, Ernst1, Author           
Beber, Björn1, Author           
Damm, Werner2, Author
Disch, Stefan2, Author
Hagemann, Willem3, 4, Author           
Rakow, Astrid2, Author
Scholl, Christoph2, Author
Waldmann, Uwe3, Author                 
Wirtz, Boris2, Author
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              

Content

show
hide
Free keywords: -
 Abstract: 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

show
hide
Language(s): eng - English
 Dates: 20162016
 Publication Status: Issued
 Pages: 93 p.
 Publishing info: SFB/TR 14 AVACS
 Table of Contents: -
 Rev. Type: -
 Identifiers: Report Nr.: ATR103
BibTex Citekey: AlthausBeberDammEtAl2016ATR
 Degree: -

Event

show

Legal Case

show

Project information

show

Source 1

show
hide
Title: AVACS Technical Report
  Abbreviation : ATR
  Other : Reports of SFT/TR 14 AVACS
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 103 Sequence Number: - Start / End Page: - Identifier: ISSN: 1860-9821