Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration
Linear Time Invariant (LTI) systems are ubiquitous in software systems and control applications. Unbounded-time reachability analysis that can cope with industrial-scale models with thousands of variables is needed. To tackle this general problem, we use abstract acceleration, a method for unbounded...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
Springer
2015
|
| _version_ | 1797087610381795328 |
|---|---|
| author | Cattaruzza, D Abate, A Schrammel, P Kroening, D |
| author2 | Blazy, S |
| author_facet | Blazy, S Cattaruzza, D Abate, A Schrammel, P Kroening, D |
| author_sort | Cattaruzza, D |
| collection | OXFORD |
| description | Linear Time Invariant (LTI) systems are ubiquitous in software systems and control applications. Unbounded-time reachability analysis that can cope with industrial-scale models with thousands of variables is needed. To tackle this general problem, we use abstract acceleration, a method for unbounded-time polyhedral reachability analysis for linear systems. Existing variants of the method are restricted to closed systems, i.e., dynamical models without inputs or non-determinism. In this paper, we present an extension of abstract acceleration to linear loops with inputs, which correspond to discrete-time LTI control systems, and further study the interaction with guard conditions. The new method relies on a relaxation of the solution of the linear dynamical equation that leads to a precise over-approximation of the set of reachable states, which are evaluated using support functions. In order to increase scalability, we use floating-point computations and ensure soundness by interval arithmetic. Our experiments show that performance increases by several orders of magnitude over alternative approaches in the literature. In turn, this tremendous speedup allows us to improve on precision by computing more expensive abstractions. We outperform state-of-the-art tools for unbounded-time analysis of LTI system with inputs in speed as well as in precision. |
| first_indexed | 2024-03-07T02:38:06Z |
| format | Conference item |
| id | oxford-uuid:a97af922-4921-4b77-8c7b-b229fee3b00a |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:38:06Z |
| publishDate | 2015 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:a97af922-4921-4b77-8c7b-b229fee3b00a2022-03-27T03:08:46ZUnbounded-time analysis of guarded LTI systems with inputs by abstract accelerationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:a97af922-4921-4b77-8c7b-b229fee3b00aSymplectic Elements at OxfordSpringer2015Cattaruzza, DAbate, ASchrammel, PKroening, DBlazy, SJensen, TLinear Time Invariant (LTI) systems are ubiquitous in software systems and control applications. Unbounded-time reachability analysis that can cope with industrial-scale models with thousands of variables is needed. To tackle this general problem, we use abstract acceleration, a method for unbounded-time polyhedral reachability analysis for linear systems. Existing variants of the method are restricted to closed systems, i.e., dynamical models without inputs or non-determinism. In this paper, we present an extension of abstract acceleration to linear loops with inputs, which correspond to discrete-time LTI control systems, and further study the interaction with guard conditions. The new method relies on a relaxation of the solution of the linear dynamical equation that leads to a precise over-approximation of the set of reachable states, which are evaluated using support functions. In order to increase scalability, we use floating-point computations and ensure soundness by interval arithmetic. Our experiments show that performance increases by several orders of magnitude over alternative approaches in the literature. In turn, this tremendous speedup allows us to improve on precision by computing more expensive abstractions. We outperform state-of-the-art tools for unbounded-time analysis of LTI system with inputs in speed as well as in precision. |
| spellingShingle | Cattaruzza, D Abate, A Schrammel, P Kroening, D Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration |
| title | Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration |
| title_full | Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration |
| title_fullStr | Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration |
| title_full_unstemmed | Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration |
| title_short | Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration |
| title_sort | unbounded time analysis of guarded lti systems with inputs by abstract acceleration |
| work_keys_str_mv | AT cattaruzzad unboundedtimeanalysisofguardedltisystemswithinputsbyabstractacceleration AT abatea unboundedtimeanalysisofguardedltisystemswithinputsbyabstractacceleration AT schrammelp unboundedtimeanalysisofguardedltisystemswithinputsbyabstractacceleration AT kroeningd unboundedtimeanalysisofguardedltisystemswithinputsbyabstractacceleration |