Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem
Complete Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem
复制标题
Kannan-Lipton 轨道问题的完整半代数不变综合
DOI：
--
复制
发表时间：
2019
影响因子：
0.5
通讯作者：
J. Worrell
中科院分区：
文献类型：
--
作者：
Nathanaël Fijalkow;Pierre Ohlmann;Joël Ouaknine;Amaury Pouly;J. Worrell
The Orbit Problem consists of determining, given a matrix A on ℚddocumentclass[12pt]{minimal} usepackage{amsmath} usepackage{wasysym} usepackage{amsfonts} usepackage{amssymb} usepackage{amsbsy} usepackage{mathrsfs} usepackage{upgreek} setlength{oddsidemargin}{-69pt} egin{document}$mathbb {Q}^{d}$end{document}, 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 invariantsP⊆ℝddocumentclass[12pt]{minimal} usepackage{amsmath} usepackage{wasysym} usepackage{amsfonts} usepackage{amssymb} usepackage{amsbsy} usepackage{mathrsfs} usepackage{upgreek} setlength{oddsidemargin}{-69pt} egin{document}$mathcal {P} subseteq mathbb {R}^{d}$end{document}, 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 whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable succinct invariants of polynomial size. Our results imply that the class of closed semialgebraic invariants is closure-complete: there exists a closed semialgebraic invariant if and only if y is not in the topological closure of the orbit of x under A.
The Orbit Problem consists of determining, given a matrix A on ℚddocumentclass[12pt]{minimal} usepackage{amsmath} usepackage{wasysym} usepackage{amsfonts} usepackage{amssymb} usepackage{amsbsy} usepackage{mathrsfs} usepackage{upgreek} setlength{oddsidemargin}{-69pt} egin{document}$mathbb {Q}^{d}$end{document}, 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 invariantsP⊆ℝddocumentclass[12pt]{minimal} usepackage{amsmath} usepackage{wasysym} usepackage{amsfonts} usepackage{amssymb} usepackage{amsbsy} usepackage{mathrsfs} usepackage{upgreek} setlength{oddsidemargin}{-69pt} egin{document}$mathcal {P} subseteq mathbb {R}^{d}$end{document}, 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 whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable succinct invariants of polynomial size. Our results imply that the class of closed semialgebraic invariants is closure-complete: there exists a closed semialgebraic invariant if and only if y is not in the topological closure of the orbit of x under A.