Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4950737 | Information and Computation | 2016 | 24 Pages |
Abstract
One such abstraction is the aâ¼LU abstraction defined by Behrmann et al. Since this abstraction can potentially yield non-convex sets, it has not been used in implementations. Firstly, we prove that aâ¼LU abstraction is the coarsest abstraction with respect to LU-bounds that is sound and complete for reachability. Secondly, we provide an efficient technique to use the aâ¼LU abstraction to solve the reachability problem.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz,