Porous invariants

We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; that is, invariants defined using Presburger arithmetic/semi-linear sets and subclasses. These invariants are not necessarily convex, and can in fact contain infinitely many ‘holes’. Nevertheless, we show that in many cases such invariants can be automatically synthesised, and moreover can be used to settle (non-)reachability questions for various interesting classes of affine loops and target sets. Joint work with Engel Lefaucheux, Joël Ouaknine, and James Worrell

Authors

• David Purser

Keywords

No keywords are indexed for this paper.