Paper Info
Title
Template-Based unbounded time verification of affine hybrid automata
Abstract
Computing over-approximations of all possible time trajectories is an important task in the analysis of hybrid systems. Sankaranarayanan et al. [20] suggested to approximate the set of reachable states using template polyhedra. In the present paper, we use a max-strategy improvement algorithm for computing an abstract semantics for affine hybrid automata that is based on template polyhedra and safely over-approximates the concrete semantics. Based on our formulation, we show that the corresponding abstract reachability problem is in co-NP. Moreover, we obtain a polynomial-time algorithm for the time elapse operation over template polyhedra.
Year
DOI
Venue
2011
10.1007/978-3-642-25318-8_6
APLAS
Keywords
Field
DocType
hybrid system,template polyhedron,time elapse operation,concrete semantics,affine hybrid automaton,polynomial-time algorithm,max-strategy improvement algorithm,abstract semantics,possible time trajectory,template-based unbounded time verification,corresponding abstract reachability problem
Affine transformation,Computer science,Automaton,Polyhedron,Theoretical computer science,Reachability problem,Hybrid system,Semantics
Conference
Citations 
PageRank 
References 
7
0.47
20
Authors
2
Name
Order
Citations
PageRank
Thao Dang11722115.80
Thomas Martin Gawlitza2886.37