Porous invariants for linear systems
We introduce the notion of <i>porous invariants</i> for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that...
| Main Authors: | , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Springer
2024
|
| _version_ | 1826317667239198720 |
|---|---|
| author | Lefaucheux, E Ouaknine, J Purser, D Worrell, J |
| author_facet | Lefaucheux, E Ouaknine, J Purser, D Worrell, J |
| author_sort | Lefaucheux, E |
| collection | OXFORD |
| description | We introduce the notion of <i>porous invariants</i> for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle reachability questions for various non-trivial classes of affine loops and target sets. For the class of
We introduce the notion of porous invariants for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle reachability questions for various non-trivial classes of affine loops and target sets. For the class of Z-linear invariants (those defined as conjunctions of linear equations with integer coefficients), we show that a strongest such invariant can be computed in polynomial time. For the more general class of N-semi-linear invariants (those defined as Boolean combinations of linear inequalities with integer coefficients), such a strongest invariant need not exist. Here we show that for point targets the existence of a separating invariant is undecidable in general. However we show that such separating invariants can be computed either by restricting the number of program variables or by restricting from multipath to single-path loops. Additionally, we consider porous targets, represented as Z-semi-linear sets (those defined as Boolean combinations of equations with integer coefficients). We show that an invariant can be computed providing the target spans the whole space. We present our tool POROUS, which computes porous invariants. |
| first_indexed | 2024-03-07T08:29:54Z |
| format | Journal article |
| id | oxford-uuid:eb033b24-fe37-4bf4-84bb-a501710f9e4d |
| institution | University of Oxford |
| language | English |
| last_indexed | 2025-03-11T16:57:32Z |
| publishDate | 2024 |
| publisher | Springer |
| record_format | dspace |
| spelling | oxford-uuid:eb033b24-fe37-4bf4-84bb-a501710f9e4d2025-02-27T12:20:10ZPorous invariants for linear systemsJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:eb033b24-fe37-4bf4-84bb-a501710f9e4dEnglishSymplectic ElementsSpringer2024Lefaucheux, EOuaknine, JPurser, DWorrell, JWe introduce the notion of <i>porous invariants</i> for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle reachability questions for various non-trivial classes of affine loops and target sets. For the class of We introduce the notion of porous invariants for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and connectedness. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle reachability questions for various non-trivial classes of affine loops and target sets. For the class of Z-linear invariants (those defined as conjunctions of linear equations with integer coefficients), we show that a strongest such invariant can be computed in polynomial time. For the more general class of N-semi-linear invariants (those defined as Boolean combinations of linear inequalities with integer coefficients), such a strongest invariant need not exist. Here we show that for point targets the existence of a separating invariant is undecidable in general. However we show that such separating invariants can be computed either by restricting the number of program variables or by restricting from multipath to single-path loops. Additionally, we consider porous targets, represented as Z-semi-linear sets (those defined as Boolean combinations of equations with integer coefficients). We show that an invariant can be computed providing the target spans the whole space. We present our tool POROUS, which computes porous invariants. |
| spellingShingle | Lefaucheux, E Ouaknine, J Purser, D Worrell, J Porous invariants for linear systems |
| title | Porous invariants for linear systems |
| title_full | Porous invariants for linear systems |
| title_fullStr | Porous invariants for linear systems |
| title_full_unstemmed | Porous invariants for linear systems |
| title_short | Porous invariants for linear systems |
| title_sort | porous invariants for linear systems |
| work_keys_str_mv | AT lefaucheuxe porousinvariantsforlinearsystems AT ouakninej porousinvariantsforlinearsystems AT purserd porousinvariantsforlinearsystems AT worrellj porousinvariantsforlinearsystems |