Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-hor...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Springer Verlag
2020
|
| _version_ | 1797069598888034304 |
|---|---|
| author | Cattaruzza, D Abate, A Schrammel, P Kroening, D |
| author_facet | Cattaruzza, D Abate, A Schrammel, P Kroening, D |
| author_sort | Cattaruzza, D |
| collection | OXFORD |
| description | Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-horizon) linear time-invariant (LTI) models with inputs using reachability analysis. We achieve this using counterexample-guided Abstract Acceleration: this approach over-approximates the reachability tube of the LTI model over an unbounded time horizon by using abstraction, possibly finding concrete counterexamples for refinement based on the given safety specification. The technique is applied to a number of LTI models and the results show robust performance when compared to state-of-the-art tools.
|
| first_indexed | 2024-03-06T22:26:50Z |
| format | Journal article |
| id | oxford-uuid:56f288de-9f80-4829-a52d-6a646ee77145 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T22:26:50Z |
| publishDate | 2020 |
| publisher | Springer Verlag |
| record_format | dspace |
| spelling | oxford-uuid:56f288de-9f80-4829-a52d-6a646ee771452022-03-26T16:53:34ZUnbounded-time safety verification of guarded LTI models with inputs by abstract accelerationJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:56f288de-9f80-4829-a52d-6a646ee77145EnglishSymplectic ElementsSpringer Verlag2020Cattaruzza, DAbate, ASchrammel, PKroening, DReachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-horizon) linear time-invariant (LTI) models with inputs using reachability analysis. We achieve this using counterexample-guided Abstract Acceleration: this approach over-approximates the reachability tube of the LTI model over an unbounded time horizon by using abstraction, possibly finding concrete counterexamples for refinement based on the given safety specification. The technique is applied to a number of LTI models and the results show robust performance when compared to state-of-the-art tools. |
| spellingShingle | Cattaruzza, D Abate, A Schrammel, P Kroening, D Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration |
| title | Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration |
| title_full | Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration |
| title_fullStr | Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration |
| title_full_unstemmed | Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration |
| title_short | Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration |
| title_sort | unbounded time safety verification of guarded lti models with inputs by abstract acceleration |
| work_keys_str_mv | AT cattaruzzad unboundedtimesafetyverificationofguardedltimodelswithinputsbyabstractacceleration AT abatea unboundedtimesafetyverificationofguardedltimodelswithinputsbyabstractacceleration AT schrammelp unboundedtimesafetyverificationofguardedltimodelswithinputsbyabstractacceleration AT kroeningd unboundedtimesafetyverificationofguardedltimodelswithinputsbyabstractacceleration |