Porous Invariants
Logic in Computer Science
2021-06-02 v1
Abstract
We introduce the notion of porous invariants for multipath (or branching/nondeterministic) affine loops over the integers; 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.
Cite
@article{arxiv.2106.00662,
title = {Porous Invariants},
author = {Engel Lefaucheux and Joël Ouaknine and David Purser and James Worrell},
journal= {arXiv preprint arXiv:2106.00662},
year = {2021}
}
Comments
Full version of paper to appear at CAV 2021