The existence of polyhedral invariants is undecidable for linear systems
En palabras de los autores
The existence of polyhedral inductive invariants suitable for proving that a given control location is unreachable is undecidable for programs using only linear arithmetic over Z or Q, by reduction from 2-counter machines.
Resultado principalEl resumen no menciona limitaciones.
Apareció: lunes, 28 de septiembre. arXiv. Preprint, todavía sin revisión por pares.