Porous invariants

DOI10.1007/978-3-030-81688-9_8zbMATH Open1493.68117arXiv2106.00662OpenAlexW4252292105MaRDI QIDQ832262FDOQ832262

Authors: Engel Lefaucheux, Joël Ouaknine, David Purser, James Worrell 

Publication date: 25 March 2022

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.

Full work available at URL: https://arxiv.org/abs/2106.00662

Recommendations

• Polynomial Invariants for Affine Programs
• Deciding properties of affine loops
• Synthesizing invariants by solving solvable loops
• Invariant generation for multi-path loops with polynomial assignments
• Polynomial invariants by linear algebra

zbMATH Keywords

invariantsreachabilityPresburger arithmeticlinear dynamical systemslinear loops

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Bounded Algol-Like Languages
• Affine relationships among variables of a program
• Title not available (Why is that?)
• Vector addition system reachability problem, a short self-contained proof
• Polynomial-time algorithm for the orbit problem
• Fast acceleration of ultimately periodic relations
• A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata
• Algorithm of polynomial complexity for factoring polynomials and finding the components of varieties in subexponential time
• On the decidability of the existence of polyhedral invariants in transition systems
• The general vector addition system reachability problem by Presburger inductive invariants
• Reachability in register machines with polynomial updates
• Undecidability of infinite Post correspondence problem for instances of size 8
• Undecidability of infinite post correspondence problem for instances of Size 9
• Decision problems for linear recurrence sequences
• Polynomial Invariants for Affine Programs
• Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
• Title not available (Why is that?)

Cited In (4)

• Preface of the special issue on the conference on computer-aided verification 2020 and 2021
• Porous invariants for linear systems
• On topologies generated by lower porosity
• Termination of linear loops under commutative updates

Uses Software

• FLATA
• ALGOL 60

This page was built for publication: Porous invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832262)