Paper Info
Title
Discretizing affine hybrid automata with uncertainty
Abstract
Over-approximating the set of all reachable states of a given system is an important task for the verification of safety properties. Such an unbounded time verification is in particular challenging for hybrid systems. We recently developed an algorithm that over-approximates the set of all reachable states of a given affine hybrid automata by performing linear template-based abstract interpretation [4]. In this article we extend the previous results by adding uncertainty to the model of affine hybrid automata. Uncertainty can be used for abstracting the behavior of non-linear hybrid systems.We adapt our techniques to this model and show that, w.r.t. given linear templates, the abstract reachability problem is still in coNP by reducing abstract reachability for affine hybrid automata with uncertainty to abstract reachability for affine programs (affine hybrid automata where only discrete transitions are allowed). We thus provide a new connection between a continuous time model and a purely discrete model.
Year
DOI
Venue
2011
10.1007/978-3-642-24372-1_36
ATVA
Keywords
Field
DocType
continuous time model,non-linear hybrid system,hybrid system,linear template-based abstract interpretation,discrete model,abstract reachability,reachable state,abstract reachability problem,affine hybrid automaton,affine program
Affine transformation,Discrete mathematics,Discretization,Abstract interpretation,Computer science,Automaton,Algorithm,Theoretical computer science,Reachability,Reachability problem,Template,Hybrid system
Conference
Volume
ISSN
Citations 
6996
0302-9743
5
PageRank 
References 
Authors
0.42
10
2
Name
Order
Citations
PageRank
Thao Dang11722115.80
Thomas Martin Gawlitza2886.37