Journal article
Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
- Abstract:
-
The Orbit Problem consists of determining, given a matrix A on Qd, together with vectors x and y, whether the orbit of x under repeated applications of A can ever reach y. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable invariants P⊆Rd , i.e., sets that are stable under A and contain x but not y, thereby providing compact and versatile certificates of non-reachability. We show that wh...
Expand abstract
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Accepted manuscript, pdf, 353.1KB)
-
- Publisher copy:
- 10.1007/s00224-019-09913-3
Authors
Bibliographic Details
- Publisher:
- Springer Nature Publisher's website
- Journal:
- Theory of Computing Systems Journal website
- Volume:
- 63
- Issue:
- 5
- Pages:
- 1027-1048
- Publication date:
- 2019-02-26
- Acceptance date:
- 2019-02-10
- DOI:
- EISSN:
-
1433-0490
- ISSN:
-
1432-4350
Item Description
- Keywords:
- Pubs id:
-
pubs:971194
- UUID:
-
uuid:393485f8-00c2-4b89-8175-12a90c8b494f
- Local pid:
- pubs:971194
- Source identifiers:
-
971194
- Deposit date:
- 2019-02-12
Terms of use
- Copyright holder:
- Springer Science+Business Media, LLC
- Copyright date:
- 2019
- Rights statement:
- © Springer Science+Business Media, LLC, part of Springer Nature 2019.
- Notes:
- This is the accepted manuscript version of the article. The final version is available online from Springer at: https://doi.org/10.1007/s00224-019-09913-3
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record