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.
Recommendations
Cites work
- scientific article; zbMATH DE number 1865733 (Why is no real title available?)
- scientific article; zbMATH DE number 3056890 (Why is no real title available?)
- A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata
- Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
- Affine relationships among variables of a program
- Algorithm of polynomial complexity for factoring polynomials and finding the components of varieties in subexponential time
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Bounded Algol-Like Languages
- Decision problems for linear recurrence sequences
- Fast acceleration of ultimately periodic relations
- On the decidability of the existence of polyhedral invariants in transition systems
- Polynomial Invariants for Affine Programs
- Polynomial-time algorithm for the orbit problem
- Reachability in register machines with polynomial updates
- The general vector addition system reachability problem by Presburger inductive invariants
- Undecidability of infinite Post correspondence problem for instances of size 8
- Undecidability of infinite post correspondence problem for instances of Size 9
- Vector addition system reachability problem, a short self-contained proof
Cited in
(4)
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)
