首页    期刊浏览 2024年11月26日 星期二
登录注册

文章基本信息

  • 标题:O-Minimal Invariants for Linear Loops
  • 作者:Shaull Almagor ; Dmitry Chistikov ; Jo{\"e}l Ouaknine
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2018
  • 卷号:107
  • 页码:114:1-114:14
  • DOI:10.4230/LIPIcs.ICALP.2018.114
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:The termination analysis of linear loops plays a key rôle in several areas of computer science, including program verification and abstract interpretation. Such deceptively simple questions also relate to a number of deep open problems, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of o-minimal invariants, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture in transcendental number theory.
  • 关键词:Invariants; linear loops; linear dynamical systems; non-termination; o-minimality
Loading...
联系我们|关于我们|网站声明
国家哲学社会科学文献中心版权所有