Porous invariants for linear systems

Lefaucheux, Engel, Ouaknine, Joël ORCID: 0000-0003-0031-9356, Purser, David ORCID: 0000-0003-0394-1634 and Worrell, James (2024) Porous invariants for linear systems. Formal Methods in System Design. pp. 1-37.

Text porous_journal.pdf - Author Accepted Manuscript Available under License Creative Commons Attribution. Download (643kB) | Preview

Abstract

<jats:title>Abstract</jats:title><jats:p>We introduce the notion of <jats:italic>porous invariants</jats:italic> 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 <jats:inline-formula><jats:alternatives><jats:tex-math>$$\mathbb {Z}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>Z</mml:mi> </mml:math></jats:alternatives></jats:inline-formula>-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 <jats:inline-formula><jats:alternatives><jats:tex-math>$$\mathbb {N}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>N</mml:mi> </mml:math></jats:alternatives></jats:inline-formula>-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 <jats:inline-formula><jats:alternatives><jats:tex-math>$$\mathbb {Z}$$</jats:tex-math><mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>Z</mml:mi> </mml:math></jats:alternatives></jats:inline-formula>-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 <jats:sc>porous</jats:sc>, which computes porous invariants.</jats:p>

Item Type:	Article
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	10 Jan 2024 12:09
Last Modified:	02 Apr 2024 15:52
DOI:	10.1007/s10703-024-00444-3
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3177792