Journal article icon

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:
Publisher copy:
10.1007/s00224-019-09913-3

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
St John's College
Role:
Author
More by this author
Institution:
University of Oxford
Department:
Computer Science
Role:
Author
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
Source identifiers:
971194
Keywords:
Pubs id:
pubs:971194
UUID:
uuid:393485f8-00c2-4b89-8175-12a90c8b494f
Local pid:
pubs:971194
Deposit date:
2019-02-12

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP