Undecidability of Inferring Linear Integer Invariants
classification
💻 cs.PL
keywords
integerlinearqfliaarithmeticdeterminingevenexistenceexpressed
pith:H5RIDTOQ Add to your LaTeX paper
What is a Pith Number?\usepackage{pith}
\pithnumber{H5RIDTOQ}
Prints a linked pith:H5RIDTOQ badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more
read the original abstract
We show that the problem of determining the existence of an inductive invariant in the language of quantifier free linear integer arithmetic (QFLIA) is undecidable, even for transition systems and safety properties expressed in QFLIA.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.